Move global signal declaration from toplevel to the sail_toplevel module

First, a rewrite pass in the AST distinguishes global from local signals
by splitting E_id nodes into E_id or E_gid for local or global references.

Then the SV generation changes as follows :
- All signal declaration at toplevel (i.e. no parent module) are removed
- These signals are all added as 'sail_toplevel' internal signals instead
- All references to globals are prepended with the SAIL_GLOBALS macro

This prevents unresolved signal paths in EDA tools,
since now all existing signals are declared in a module.

language/jib.ott

@@ -129,6 +129,7 @@ uid :: 'UId_' ::=
 
 cval :: 'V_' ::=
   | name : ctyp                                     :: :: id
+  | name : ctyp                                     :: :: gid
   | id : ctyp                                       :: :: member
   | value : ctyp                                    :: :: lit
   | ( cval0 , ... , cvaln ) ctyp                    :: :: tuple

language/sail.ott

@@ -472,6 +472,8 @@ exp :: 'E_' ::=
     {{ com sequential block }}
   | id                                                  :: :: id
     {{ com identifier }}
+  | id                                                  :: :: gid
+    {{ com global identifier }}
   | lit                                                 :: :: lit
     {{ com literal constant }}
   | ( typ ) exp                                         :: :: typ

src/lib/anf.ml

@@ -98,6 +98,7 @@ and 'a apat_aux =
 and 'a aval =
   | AV_lit of lit * 'a
   | AV_id of id * 'a lvar
+  | AV_gid of id * 'a lvar
   | AV_abstract of id * 'a
   | AV_ref of id * 'a lvar
   | AV_tuple of 'a aval list
@@ -169,6 +170,7 @@ let rec apat_rename from_id to_id (AP_aux (apat_aux, annot)) =
 let rec aval_typ = function
   | AV_lit (_, typ) -> typ
   | AV_id (_, lvar) -> lvar_typ lvar
+  | AV_gid (_, lvar) -> lvar_typ lvar
   | AV_abstract (id, typ) -> typ
   | AV_ref (_, lvar) -> lvar_typ lvar
   | AV_tuple avals -> tuple_typ (List.map aval_typ avals)
@@ -201,6 +203,8 @@ let rec aval_rename from_id to_id = function
   | AV_lit (lit, typ) -> AV_lit (lit, typ)
   | AV_id (id, lvar) when Id.compare id from_id = 0 -> AV_id (to_id, lvar)
   | AV_id (id, lvar) -> AV_id (id, lvar)
+  | AV_gid (id, lvar) when Id.compare id from_id = 0 -> AV_gid (to_id, lvar)
+  | AV_gid (id, lvar) -> AV_gid (id, lvar)
   | AV_ref (id, lvar) when Id.compare id from_id = 0 -> AV_ref (to_id, lvar)
   | AV_ref (id, lvar) -> AV_ref (id, lvar)
   | AV_abstract (id, typ) ->
@@ -456,6 +460,8 @@ let pp_order = function Ord_aux (Ord_inc, _) -> string "inc" | Ord_aux (Ord_dec,
 
 let pp_id id = string (string_of_id id)
 
+let pp_gid id = pp_id id
+
 let rec pp_alexp = function
   | AL_id (id, typ) -> pp_annot typ (pp_id id)
   | AL_addr (id, typ) -> string "*" ^^ parens (pp_annot typ (pp_id id))
@@ -563,6 +569,7 @@ and pp_block = function
 and pp_aval = function
   | AV_lit (lit, typ) -> pp_annot typ (string (string_of_lit lit))
   | AV_id (id, lvar) -> pp_lvar lvar (pp_id id)
+  | AV_gid (id, lvar) -> pp_lvar lvar (pp_gid id)
   | AV_abstract (id, typ) -> string "sizeof" ^^ parens (pp_annot typ (pp_id id))
   | AV_tuple avals -> parens (separate_map (comma ^^ space) pp_aval avals)
   | AV_ref (id, lvar) -> string "ref" ^^ space ^^ pp_lvar lvar (pp_id id)
@@ -770,6 +777,11 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
       begin
         match lvar with _ -> mk_aexp (AE_val (AV_id (id, lvar)))
       end
+  | E_gid id ->
+      let lvar = Env.lookup_id id (env_of exp) in
+      begin
+        match lvar with _ -> mk_aexp (AE_val (AV_gid (id, lvar)))
+      end
   | E_ref id ->
       let lvar = Env.lookup_id id (env_of exp) in
       mk_aexp (AE_val (AV_ref (id, lvar)))

src/lib/anf.mli

@@ -129,6 +129,7 @@ and 'a apat_aux =
 and 'a aval =
   | AV_lit of lit * 'a
   | AV_id of id * 'a lvar
+  | AV_gid of id * 'a lvar
   | AV_abstract of id * 'a
   | AV_ref of id * 'a lvar
   | AV_tuple of 'a aval list

src/lib/ast_util.ml

@@ -842,6 +842,7 @@ let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
   | E_id id -> E_id id
+  | E_gid id -> E_gid id
   | E_ref id -> E_ref id
   | E_lit lit -> E_lit lit
   | E_typ (typ, exp) -> E_typ (typ, map_exp_annot f exp)
@@ -1242,7 +1243,7 @@ let string_of_order (Ord_aux (aux, _)) = match aux with Ord_inc -> "inc" | Ord_d
 let rec string_of_exp (E_aux (exp, _)) =
   match exp with
   | E_block exps -> "{ " ^ string_of_list "; " string_of_exp exps ^ " }"
-  | E_id v -> string_of_id v
+  | E_id v | E_gid v -> string_of_id v
   | E_ref id -> "ref " ^ string_of_id id
   | E_sizeof nexp -> "sizeof " ^ string_of_nexp nexp
   | E_constraint nc -> "constraint(" ^ string_of_n_constraint nc ^ ")"
@@ -1749,6 +1750,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     match e_aux with
     | E_block exps -> E_block (List.map (subst id value) exps)
     | E_id id' -> if Id.compare id id' = 0 then unaux_exp value else E_id id'
+    | E_gid id' -> if Id.compare id id' = 0 then unaux_exp value else E_gid id'
     | E_lit lit -> E_lit lit
     | E_typ (typ, exp) -> E_typ (typ, subst id value exp)
     | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps)
@@ -1987,6 +1989,7 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp =
     match e_aux with
     | E_block exps -> E_block (List.map (locate f) exps)
     | E_id id -> E_id (locate_id f id)
+    | E_gid id -> E_gid (locate_id f id)
     | E_lit lit -> E_lit (locate_lit f lit)
     | E_typ (typ, exp) -> E_typ (locate_typ f typ, locate f exp)
     | E_app (id, exps) -> E_app (locate_id f id, List.map (locate f) exps)

src/lib/constant_propagation.ml

@@ -345,7 +345,7 @@ let const_props target ast =
       | E_block es ->
           let es', assigns = threaded_map (const_prop_exp substs) assigns es in
           re (E_block es') assigns
-      | E_id id ->
+      | E_id id | E_gid id ->
           let env = Type_check.env_of_annot (l, annot) in
           ( ( try
                 match Env.lookup_id id env with

src/lib/jib_compile.ml

@@ -352,12 +352,17 @@ module Make (C : CONFIG) = struct
           ([iinit l ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs])
         )
         else ([], cval, [])
-    | AV_id (id, Enum typ) -> ([], V_member (id, ctyp_of_typ ctx typ), [])
+    | AV_gid (id, Enum typ) | AV_id (id, Enum typ) -> ([], V_member (id, ctyp_of_typ ctx typ), [])
     | AV_id (id, typ) -> begin
         match Bindings.find_opt id ctx.locals with
         | Some (_, ctyp) -> ([], V_id (name id, ctyp), [])
         | None -> ([], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), [])
       end
+    | AV_gid (id, typ) -> begin
+        match Bindings.find_opt id ctx.locals with
+        | Some (_, ctyp) -> ([], V_gid (name id, ctyp), [])
+        | None -> ([], V_gid (name id, ctyp_of_typ ctx (lvar_typ typ)), [])
+      end
     | AV_abstract (id, typ) -> ([], V_call (Get_abstract, [V_id (name id, ctyp_of_typ ctx typ)]), [])
     | AV_ref (id, typ) -> ([], V_lit (VL_ref (string_of_id id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [])
     | AV_lit (L_aux (L_string str, _), typ) -> ([], V_lit (VL_string (String.escaped str), ctyp_of_typ ctx typ), [])

src/lib/jib_optimize.ml

@@ -141,7 +141,7 @@ let unique_per_function_ids cdefs =
   List.mapi unique_cdef cdefs
 
 let rec cval_subst id subst = function
-  | V_id (id', ctyp) -> if Name.compare id id' = 0 then subst else V_id (id', ctyp)
+  | (V_gid (id', ctyp) as v) | (V_id (id', ctyp) as v) -> if Name.compare id id' = 0 then subst else v
   | V_member (id, ctyp) -> V_member (id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (op, cvals) -> V_call (op, List.map (cval_subst id subst) cvals)
@@ -154,6 +154,7 @@ let rec cval_subst id subst = function
 
 let rec cval_map_id f = function
   | V_id (id, ctyp) -> V_id (f id, ctyp)
+  | V_gid (id, ctyp) -> V_gid (f id, ctyp)
   | V_member (id, ctyp) -> V_member (id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (call, cvals) -> V_call (call, List.map (cval_map_id f) cvals)
@@ -498,6 +499,7 @@ let remove_tuples cdefs ctx =
         ctyp
   and fix_cval = function
     | V_id (id, ctyp) -> V_id (id, ctyp)
+    | V_gid (id, ctyp) -> V_gid (id, ctyp)
     | V_member (id, ctyp) -> V_member (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_ctor_kind (cval, ctor, ctyp) -> V_ctor_kind (fix_cval cval, ctor, ctyp)

src/lib/jib_ssa.ml

@@ -539,6 +539,12 @@ let rename_variables globals graph root children =
           let i = top_stack id in
           V_id (ssa_name i id, ctyp)
         )
+    | V_gid (id, ctyp) ->
+        if NameSet.mem id globals then V_gid (id, ctyp)
+        else (
+          let i = top_stack id in
+          V_gid (ssa_name i id, ctyp)
+        )
     | V_member (id, ctyp) -> V_member (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_call (id, fs) -> V_call (id, List.map fold_cval fs)

src/lib/jib_util.ml

@@ -309,6 +309,7 @@ let string_of_value = function
 
 let rec string_of_cval = function
   | V_id (id, _) -> string_of_name id
+  | V_gid (id, _) -> string_of_name id
   | V_member (id, _) -> Util.zencode_string (string_of_id id)
   | V_lit (VL_undefined, ctyp) -> string_of_value VL_undefined ^ " : " ^ string_of_ctyp ctyp
   | V_lit (vl, ctyp) -> string_of_value vl
@@ -646,6 +647,7 @@ let rec is_polymorphic = function
 
 let rec cval_deps = function
   | V_id (id, _) -> NameSet.singleton id
+  | V_gid (id, _) -> NameSet.singleton id
   | V_lit _ | V_member _ -> NameSet.empty
   | V_field (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval
   | V_call (_, cvals) | V_tuple (cvals, _) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals)
@@ -735,6 +737,7 @@ let rec map_clexp_ctyp f = function
 
 let rec map_cval_ctyp f = function
   | V_id (id, ctyp) -> V_id (id, f ctyp)
+  | V_gid (id, ctyp) -> V_gid (id, f ctyp)
   | V_member (id, ctyp) -> V_member (id, f ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, f ctyp)
   | V_ctor_kind (cval, (id, unifiers), ctyp) -> V_ctor_kind (map_cval_ctyp f cval, (id, List.map f unifiers), f ctyp)
@@ -999,6 +1002,7 @@ let rec infer_call op vs =
 
 and cval_ctyp = function
   | V_id (_, ctyp) -> ctyp
+  | V_gid (_, ctyp) -> ctyp
   | V_member (_, ctyp) -> ctyp
   | V_lit (_, ctyp) -> ctyp
   | V_ctor_kind _ -> CT_bool

src/lib/jib_visitor.ml

@@ -126,6 +126,10 @@ let rec visit_cval vis outer_cval =
         let name' = visit_name vis name in
         let ctyp' = visit_ctyp vis ctyp in
         if name == name' && ctyp == ctyp' then no_change else V_id (name', ctyp')
+    | V_gid (name, ctyp) ->
+        let name' = visit_name vis name in
+        let ctyp' = visit_ctyp vis ctyp in
+        if name == name' && ctyp == ctyp' then no_change else V_gid (name', ctyp')
     | V_member (id, ctyp) ->
         let ctyp' = visit_ctyp vis ctyp in
         if ctyp == ctyp' then no_change else V_member (id, ctyp')

src/lib/monomorphise.ml

@@ -1048,7 +1048,7 @@ let split_defs target all_errors (splits : split_req list) env ast =
         let re e = E_aux (e, annot) in
         match e with
         | E_block es -> re (E_block (List.map map_exp es))
-        | E_id _ | E_lit _ | E_sizeof _ | E_constraint _ | E_ref _ | E_internal_value _ -> ea
+        | E_id _ | E_gid _ | E_lit _ | E_sizeof _ | E_constraint _ | E_ref _ | E_internal_value _ -> ea
         | E_typ (t, e') -> re (E_typ (t, map_exp e'))
         | E_app (id, es) ->
             let es' = List.map map_exp es in
@@ -2233,7 +2233,7 @@ module Analysis = struct
                 (d, assigns, merge r r')
           in
           aux env assigns es
-      | E_id id -> begin
+      | E_id id | E_gid id -> begin
           match Bindings.find id env.var_deps with
           | args -> (args, assigns, empty)
           | exception Not_found -> (

src/lib/pretty_print_sail.ml

@@ -533,6 +533,7 @@ module Printer (Config : PRINT_CONFIG) = struct
     | E_typ (typ, exp) -> separate space [doc_atomic_exp exp; colon; doc_typ typ]
     | E_lit lit -> doc_lit lit
     | E_id id -> doc_id id
+    | E_gid id -> doc_id id
     | E_ref id -> string "ref" ^^ space ^^ doc_id id
     | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id
     | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid

src/lib/rewriter.ml

@@ -177,7 +177,7 @@ let rewrite_exp rewriters (E_aux (exp, (l, annot))) =
   let rewrite = rewriters.rewrite_exp rewriters in
   match exp with
   | E_block exps -> rewrap (E_block (List.map rewrite exps))
-  | E_id _ | E_lit _ -> rewrap exp
+  | E_id _ | E_gid _ | E_lit _ -> rewrap exp
   | E_typ (typ, exp) -> rewrap (E_typ (typ, rewrite exp))
   | E_app (id, exps) -> rewrap (E_app (id, List.map rewrite exps))
   | E_app_infix (el, id, er) -> rewrap (E_app_infix (rewrite el, id, rewrite er))
@@ -476,6 +476,7 @@ type ( 'a,
      exp_alg = {
   e_block : 'exp list -> 'exp_aux;
   e_id : id -> 'exp_aux;
+  e_gid : id -> 'exp_aux;
   e_ref : id -> 'exp_aux;
   e_lit : lit -> 'exp_aux;
   e_typ : Ast.typ * 'exp -> 'exp_aux;
@@ -538,6 +539,7 @@ type ( 'a,
 let rec fold_exp_aux alg = function
   | E_block es -> alg.e_block (List.map (fold_exp alg) es)
   | E_id id -> alg.e_id id
+  | E_gid id -> alg.e_gid id
   | E_ref id -> alg.e_ref id
   | E_lit lit -> alg.e_lit lit
   | E_typ (typ, e) -> alg.e_typ (typ, fold_exp alg e)
@@ -620,6 +622,7 @@ let id_exp_alg =
   {
     e_block = (fun es -> E_block es);
     e_id = (fun id -> E_id id);
+    e_gid = (fun id -> E_gid id);
     e_ref = (fun id -> E_ref id);
     e_lit = (fun lit -> E_lit lit);
     e_typ = (fun (typ, e) -> E_typ (typ, e));
@@ -729,6 +732,7 @@ let compute_exp_alg bot join =
   {
     e_block = split_join (fun es -> E_block es);
     e_id = (fun id -> (bot, E_id id));
+    e_gid = (fun id -> (bot, E_gid id));
     e_ref = (fun id -> (bot, E_ref id));
     e_lit = (fun lit -> (bot, E_lit lit));
     e_typ = (fun (typ, (v, e)) -> (v, E_typ (typ, e)));
@@ -850,6 +854,7 @@ let pure_exp_alg bot join =
   {
     e_block = join_list;
     e_id = (fun id -> bot);
+    e_gid = (fun id -> bot);
     e_ref = (fun id -> bot);
     e_lit = (fun lit -> bot);
     e_typ = (fun (typ, v) -> v);
@@ -997,7 +1002,7 @@ let default_fold_exp f x (E_aux (e, ann) as exp) =
           (x, []) es
       in
       (x, re (E_block (List.rev es)))
-  | E_id _ | E_ref _ | E_lit _ -> (x, exp)
+  | E_id _ | E_gid _ | E_ref _ | E_lit _ -> (x, exp)
   | E_typ (typ, e) ->
       let x, e = f x e in
       (x, re (E_typ (typ, e)))

src/lib/rewriter.mli

@@ -131,6 +131,7 @@ type ( 'a,
      exp_alg = {
   e_block : 'exp list -> 'exp_aux;
   e_id : id -> 'exp_aux;
+  e_gid : id -> 'exp_aux;
   e_ref : id -> 'exp_aux;
   e_lit : lit -> 'exp_aux;
   e_typ : Ast.typ * 'exp -> 'exp_aux;

src/lib/rewrites.ml

@@ -2315,7 +2315,7 @@ let rewrite_ast_letbind_effects effect_info env =
     let pure_rewrap e = purify (rewrap e) in
     match exp_aux with
     | E_block es -> failwith "E_block should have been removed till now"
-    | E_id id -> k exp
+    | E_id id | E_gid id -> k exp
     | E_ref id -> k exp
     | E_lit _ -> k exp
     | E_typ (typ, exp') -> n_exp_name exp' (fun exp' -> k (pure_rewrap (E_typ (typ, exp'))))
@@ -4320,6 +4320,14 @@ let rewrite_unroll_constant_loops _type_env defs =
     { rewriters_base with rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux }) }
     defs
 
+(** Distinguish between local and global references by splitting 'E_id' nodes into
+    either 'E_id' for local ones or 'E_gid' for global ones. *)
+let rewrite_remove_global_vars (type_env : Type_check.Env.t) defs =
+  let toplevel_lets = Type_check.Env.get_toplevel_lets type_env in
+  let e_id id = if IdSet.mem id toplevel_lets then E_gid id else E_id id in
+  let rewrite_exp _rewriters = fold_exp { id_exp_alg with e_id } in
+  rewrite_ast_base { rewriters_base with rewrite_exp } defs
+
 (** Remove bitfield records and turn them into plain bitvectors
     This can improve performance for Isabelle, because processing record types is slow there
     (and we don't gain much by having record types with just a `bits` field).
@@ -4554,6 +4562,7 @@ let all_rewriters =
     ("mapping_patterns", basic_rewriter (fun _ -> Mappings.rewrite_ast));
     ("truncate_hex_literals", basic_rewriter rewrite_truncate_hex_literals);
     ("unroll_constant_loops", basic_rewriter rewrite_unroll_constant_loops);
+    ("remove_global_vars", basic_rewriter rewrite_remove_global_vars);
     ("mono_rewrites", basic_rewriter mono_rewrites);
     ("complete_record_params", basic_rewriter rewrite_complete_record_params);
     ("toplevel_nexps", basic_rewriter rewrite_toplevel_nexps);