From 54f2e83909f9e7b831d12c10caf0c1ed7ec2aa08 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 21 Feb 2020 17:48:50 +0000
Subject: Distinguish type identifiers in topological sorting

Fixes #61
---
 src/spec_analysis.ml | 44 +++++++++++++++++++++++---------------------
 1 file changed, 23 insertions(+), 21 deletions(-)

(limited to 'src/spec_analysis.ml')

diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 41426654..4814554b 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -72,7 +72,7 @@ let conditional_add typ_or_exp bound used id =
     if typ_or_exp (*true for typ*)
     then ["bit";"vector";"unit";"string";"int";"bool"]
     else ["=="; "!="; "|";"~";"&";"add_int"] in
-  let i = (string_of_id id) in
+  let i = (string_of_id (if typ_or_exp then prepend_id "typ:" id else id)) in
   if Nameset.mem i bound || List.mem i known_list
   then used
   else Nameset.add i used
@@ -106,12 +106,6 @@ and free_type_names_t_args consider_var targs =
   nameset_bigunion (List.map (free_type_names_t_arg consider_var) targs)
 
 
-let rec free_type_names_tannot consider_var tannot =
-  match Type_check.destruct_tannot tannot with
-  | None -> mt
-  | Some (_, t, _) -> free_type_names_t consider_var t
-
-
 let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
   match t with
   | Typ_var (Kid_aux (Var v,l)) ->
@@ -131,6 +125,11 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
        used t'
   | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
 
+and fv_of_tannot consider_var bound used tannot =
+  match Type_check.destruct_tannot tannot with
+  | None -> mt
+  | Some (_, t, _) -> fv_of_typ consider_var bound used t
+
 and fv_of_targ consider_var bound used (Ast.A_aux(targ,_)) : Nameset.t = match targ with
   | A_typ t -> fv_of_typ consider_var bound used t
   | A_nexp n -> fv_of_nexp consider_var bound used n
@@ -167,13 +166,13 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
   | P_as(p,id) -> let b,ns = pat_bindings consider_var bound used p in
     Nameset.add (string_of_id id) b,ns
   | P_typ(t,p) ->
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      let ns = fv_of_typ consider_var bound used t in pat_bindings consider_var bound ns p
   | P_id id ->
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      Nameset.add (string_of_id id) bound,used
   | P_app(id,pats) ->
-    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
     list_fv bound (Nameset.add (string_of_id id) used) pats
   | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
   | _ -> bound,used
@@ -185,7 +184,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
     list_fv bound used set es
   | E_id id | E_ref id ->
      let used = conditional_add_exp bound used id in
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      bound,used,set
   | E_cast (t,e) ->
     let u = fv_of_typ consider_var (if consider_var then bound else mt) used t in
@@ -211,7 +210,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
   | E_vector_update_subrange(v,i1,i2,e) -> list_fv bound used set [v;i1;i2;e]
   | E_vector_append(e1,e2) | E_cons(e1,e2) -> list_fv bound used set [e1;e2]
   | E_record fexps ->
-     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+     let used = fv_of_tannot consider_var bound used tannot in
      List.fold_right
        (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (bound,used,set)
   | E_record_update(e, fexps) ->
@@ -260,7 +259,7 @@ and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with
 and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
   match lexp with
   | LEXP_id id ->
-    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+    let used = fv_of_tannot consider_var bound used tannot in
     let i = string_of_id id in
     if Nameset.mem i bound
     then bound, used, Nameset.add i set
@@ -268,7 +267,7 @@ and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
   | LEXP_deref exp ->
     fv_of_exp consider_var bound used set exp
   | LEXP_cast(typ,id) ->
-    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
+    let used = fv_of_tannot consider_var bound used tannot in
     let i = string_of_id id in
     let used_t = fv_of_typ consider_var bound used typ in
     if Nameset.mem i bound
@@ -311,18 +310,18 @@ let fv_of_abbrev consider_var bound used typq typ_arg =
 
 let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
   | TD_abbrev(id,typq,typ_arg) ->
-     init_env (string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg)
+     init_env ("typ:" ^ string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg)
   | TD_record(id,typq,tids,_) ->
-    let binds = init_env (string_of_id id) in
+    let binds = init_env ("typ:" ^ string_of_id id) in
     let bounds = if consider_var then typq_bindings typq else mt in
     binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt
   | TD_variant(id,typq,tunions,_) ->
-    let bindings = Nameset.add (string_of_id id) (if consider_var then typq_bindings typq else mt) in
+    let bindings = Nameset.add ("typ:" ^ string_of_id id) (if consider_var then typq_bindings typq else mt) in
     typ_variants consider_var bindings tunions
   | TD_enum(id,ids,_) ->
-    Nameset.of_list (List.map string_of_id (id::ids)),mt
+    Nameset.of_list (("typ:" ^ string_of_id id) :: List.map string_of_id ids),mt
   | TD_bitfield(id,typ,_) ->
-    init_env (string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *)
+    init_env ("typ:" ^ string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *)
 
 let fv_of_tannot_opt consider_var (Typ_annot_opt_aux (t,_)) =
   match t with
@@ -534,11 +533,14 @@ let add_def_to_map id d defset =
 let add_def_to_graph (prelude, original_order, defset, graph) d =
   let bound, used = fv_of_def false true [] d in
   let used = match d with
-    | DEF_reg_dec _ ->
+    | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, _), annot))
+    | DEF_reg_dec (DEC_aux (DEC_config (_, typ, _), annot)) ->
        (* For a register, we need to ensure that any undefined_type
           functions for types used by the register are placed before
           the register declaration. *)
-       let undefineds = Nameset.map (fun name -> "undefined_" ^ name) used in
+       let env = Type_check.env_of_annot annot in
+       let typ' = Type_check.Env.expand_synonyms env typ in
+       let undefineds = Nameset.map (fun name -> "undefined_" ^ name) (free_type_names_t false typ') in
        Nameset.union undefineds used
     | _ -> used
   in
-- 
cgit v1.2.3