From de18990a44e2059aefe92485f1790645a412cd0a Mon Sep 17 00:00:00 2001 From: Nicolas Phan Date: Thu, 23 Jan 2025 16:35:58 +0100 Subject: [PATCH] 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 | 1 + language/sail.ott | 2 ++ src/lib/anf.ml | 12 ++++++++ src/lib/anf.mli | 1 + src/lib/ast_util.ml | 5 ++- src/lib/constant_propagation.ml | 2 +- src/lib/jib_compile.ml | 7 ++++- src/lib/jib_optimize.ml | 4 ++- src/lib/jib_ssa.ml | 6 ++++ src/lib/jib_util.ml | 4 +++ src/lib/jib_visitor.ml | 4 +++ src/lib/monomorphise.ml | 4 +-- src/lib/pretty_print_sail.ml | 1 + src/lib/rewriter.ml | 9 ++++-- src/lib/rewriter.mli | 1 + src/lib/rewrites.ml | 11 ++++++- src/lib/smt_exp.ml | 16 ++++++---- src/lib/smt_gen.ml | 1 + src/lib/spec_analysis.ml | 2 +- src/sail_c_backend/c_backend.ml | 2 +- src/sail_coq_backend/pretty_print_coq.ml | 5 +-- src/sail_lean_backend/pretty_print_lean.ml | 1 + src/sail_lem_backend/pretty_print_lem.ml | 2 +- src/sail_smt_backend/jib_smt.ml | 2 +- src/sail_sv_backend/jib_sv.ml | 36 +++++++++++++++------- src/sail_sv_backend/jib_sv.mli | 6 ++-- src/sail_sv_backend/sail_plugin_sv.ml | 7 +++++ src/sail_sv_backend/sv_ir.ml | 3 ++ src/sail_sv_backend/sv_optimize.ml | 6 ++-- 29 files changed, 126 insertions(+), 37 deletions(-) diff --git a/language/jib.ott b/language/jib.ott index bda70256e..b45bbbc8e 100644 --- a/language/jib.ott +++ b/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 diff --git a/language/sail.ott b/language/sail.ott index 3eec12f7c..0712e5186 100644 --- a/language/sail.ott +++ b/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 diff --git a/src/lib/anf.ml b/src/lib/anf.ml index b57602ca3..2dae73afd 100644 --- a/src/lib/anf.ml +++ b/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))) diff --git a/src/lib/anf.mli b/src/lib/anf.mli index 29228c3c5..36aa9857d 100644 --- a/src/lib/anf.mli +++ b/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 diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 955a27981..6b41d4fd1 100644 --- a/src/lib/ast_util.ml +++ b/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) diff --git a/src/lib/constant_propagation.ml b/src/lib/constant_propagation.ml index 99be000de..99daa9550 100644 --- a/src/lib/constant_propagation.ml +++ b/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 diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index fb2707088..51d9a15e8 100644 --- a/src/lib/jib_compile.ml +++ b/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), []) diff --git a/src/lib/jib_optimize.ml b/src/lib/jib_optimize.ml index de4a064b6..8dca45025 100644 --- a/src/lib/jib_optimize.ml +++ b/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) diff --git a/src/lib/jib_ssa.ml b/src/lib/jib_ssa.ml index 4ab64f03c..65b93f1ab 100644 --- a/src/lib/jib_ssa.ml +++ b/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) diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index 7d00fa411..d5d1b0193 100644 --- a/src/lib/jib_util.ml +++ b/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 diff --git a/src/lib/jib_visitor.ml b/src/lib/jib_visitor.ml index 9aa68bd58..d8464d9a5 100644 --- a/src/lib/jib_visitor.ml +++ b/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') diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 44dc43965..4e1b383e2 100644 --- a/src/lib/monomorphise.ml +++ b/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 -> ( diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index 83fabe14d..f6697854a 100644 --- a/src/lib/pretty_print_sail.ml +++ b/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 diff --git a/src/lib/rewriter.ml b/src/lib/rewriter.ml index f4e22a9b6..0ca00ef9f 100644 --- a/src/lib/rewriter.ml +++ b/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))) diff --git a/src/lib/rewriter.mli b/src/lib/rewriter.mli index 6b9146135..6d509af81 100644 --- a/src/lib/rewriter.mli +++ b/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; diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index b91f48014..c9917df91 100644 --- a/src/lib/rewrites.ml +++ b/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); diff --git a/src/lib/smt_exp.ml b/src/lib/smt_exp.ml index 7300d0c2e..195eabe7d 100644 --- a/src/lib/smt_exp.ml +++ b/src/lib/smt_exp.ml @@ -75,6 +75,7 @@ type smt_exp = | Real_lit of string | String_lit of string | Var of Jib.name + | Global_var of Jib.name | Unit | Member of Ast.id | Fn of string * smt_exp list @@ -98,7 +99,7 @@ let rec pp_smt_exp = | Real_lit str -> string str | String_lit str -> string ("\"" ^ str ^ "\"") | Bitvec_lit bv -> string (Sail2_values.show_bitlist_prefix '#' bv) - | Var id -> string (zencode_name id) + | Global_var id | Var id -> string (zencode_name id) | Member id -> string (zencode_id id) | Unit -> string "unit" | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps) @@ -134,7 +135,9 @@ let rec fold_smt_exp f = function | Tl (tl_op, xs) -> f (Tl (tl_op, fold_smt_exp f xs)) | Struct (struct_id, fields) -> f (Struct (struct_id, List.map (fun (field_id, exp) -> (field_id, fold_smt_exp f exp)) fields)) - | (Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Var _ | Unit | Member _ | Empty_list) as exp -> f exp + | (Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Global_var _ | Var _ | Unit | Member _ | Empty_list) as exp + -> + f exp let rec iter_smt_exp f exp = f exp; @@ -158,7 +161,7 @@ let rec iter_smt_exp f exp = iter_smt_exp f index; iter_smt_exp f exp | Struct (_, fields) -> List.iter (fun (_, field) -> iter_smt_exp f field) fields - | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Var _ | Unit | Member _ | Empty_list -> () + | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Global_var _ | Var _ | Unit | Member _ | Empty_list -> () let rec smt_exp_size = function | Fn (_, args) -> 1 + List.fold_left (fun n arg -> n + smt_exp_size arg) 0 args @@ -174,7 +177,7 @@ let rec smt_exp_size = function 1 + smt_exp_size exp | Store (_, _, arr, index, exp) -> 1 + smt_exp_size arr + smt_exp_size index + smt_exp_size exp | Struct (_, fields) -> 1 + List.fold_left (fun n (_, field) -> n + smt_exp_size field) 0 fields - | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Var _ | Unit | Member _ | Empty_list -> 1 + | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Global_var _ | Var _ | Unit | Member _ | Empty_list -> 1 let extract ~from i j x = Extract (i, j, from, x) @@ -887,7 +890,8 @@ module Simplifier = struct | Struct (struct_id, fields) -> let fields' = map_no_copy (fun (field_id, exp) -> (field_id, go simpset exp)) fields in if fields == fields' then no_change else Struct (struct_id, fields') - | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Var _ | Unit | Member _ | Empty_list -> no_change + | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Global_var _ | Var _ | Unit | Member _ | Empty_list -> + no_change in let exp = go simpset exp in (!changes, exp) @@ -929,7 +933,7 @@ let simp simpset exp = Repeat rule_or_assume; ] ) - | Var _ -> run_strategy simpset exp rule_var + | Global_var _ | Var _ -> run_strategy simpset exp rule_var | Fn ("=", _) -> run_strategy simpset exp (Then [rule_inequality; rule_simp_eq; rule_concat_literal_eq]) | Fn ("not", _) -> run_strategy simpset exp diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml index 1b2ec9a5c..0d58bb78e 100644 --- a/src/lib/smt_gen.ml +++ b/src/lib/smt_gen.ml @@ -370,6 +370,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct match cval with | V_lit (vl, ctyp) -> literal vl ctyp | V_id (id, _) -> return (Var id) + | V_gid (id, _) -> return (Global_var id) | V_member (id, _) -> return (Member id) | V_call (List_hd, [arg]) -> let* l = current_location in diff --git a/src/lib/spec_analysis.ml b/src/lib/spec_analysis.ml index 0f0cbc851..a70f3d56d 100644 --- a/src/lib/spec_analysis.ml +++ b/src/lib/spec_analysis.ml @@ -182,7 +182,7 @@ let nexp_subst_fns substs = let re e = E_aux (e, (l, s_tannot annot)) in match e with | E_block es -> re (E_block (List.map s_exp es)) - | E_id _ | E_ref _ | E_lit _ | E_internal_value _ -> re e + | E_id _ | E_gid _ | E_ref _ | E_lit _ | E_internal_value _ -> re e | E_sizeof ne -> begin let ne' = subst_kids_nexp substs ne in match ne' with Nexp_aux (Nexp_constant i, l) -> re (E_lit (L_aux (L_num i, l))) | _ -> re (E_sizeof ne') diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index 2db3bbc7e..fc645c219 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -952,7 +952,7 @@ let sgen_value = function | VL_undefined -> Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal" let rec sgen_cval = function - | V_id (id, _) -> sgen_name id + | V_gid (id, _) | V_id (id, _) -> sgen_name id | V_member (id, _) -> sgen_id id | V_lit (vl, _) -> sgen_value vl | V_call (op, cvals) -> sgen_call op cvals diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml index 7a5a72b88..86b425636 100644 --- a/src/sail_coq_backend/pretty_print_coq.ml +++ b/src/sail_coq_backend/pretty_print_coq.ml @@ -1479,7 +1479,7 @@ let doc_exp, doc_let = let env = env_of full_exp in let doc_loop_var (E_aux (e, (l, _)) as exp) = match e with - | E_id id -> + | E_id id | E_gid id -> let id_pp = doc_id ctxt id in let typ = general_typ_of exp in (id_pp, id_pp) @@ -1917,7 +1917,7 @@ let doc_exp, doc_let = ) | E_block [] -> string "tt" | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.") - | E_id id | E_ref id -> + | E_id id | E_gid id | E_ref id -> let env = env_of full_exp in let typ = typ_of full_exp in let eff = effect_of full_exp in @@ -2016,6 +2016,7 @@ let doc_exp, doc_let = let var, let_pp = match e with | E_aux (E_id id, _) -> (id, empty) + | E_aux (E_gid id, _) -> (id, empty) | _ -> let v = mk_id "_record" in (* TODO: collision avoid *) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index bd49c7009..f05bc7bb2 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -181,6 +181,7 @@ let string_of_exp_con (E_aux (e, _)) = | E_internal_assume _ -> "E_internal_assume" | E_internal_value _ -> "E_internal_value" | E_id _ -> "E_id" + | E_gid _ -> "E_gid" | E_lit _ -> "E_lit" | E_typ _ -> "E_typ" | E_app _ -> "E_app" diff --git a/src/sail_lem_backend/pretty_print_lem.ml b/src/sail_lem_backend/pretty_print_lem.ml index 403c3094f..9eccf3769 100644 --- a/src/sail_lem_backend/pretty_print_lem.ml +++ b/src/sail_lem_backend/pretty_print_lem.ml @@ -1000,7 +1000,7 @@ let doc_exp_lem, doc_let_lem = ) | E_block [] -> string "()" | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.") - | E_id id | E_ref id -> + | E_id id | E_gid id | E_ref id -> let env = env_of full_exp in let typ = typ_of full_exp in let base_typ = Env.base_typ_of env typ in diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 6f7f04aa4..12d4f6ce9 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -100,7 +100,7 @@ module Make_optimizer (S : Sequence) = struct let uses = NameHashtbl.create (Stack.length stack) in let rec uses_in_exp = function - | Var var -> begin + | Global_var var | Var var -> begin match NameHashtbl.find_opt uses var with | Some n -> NameHashtbl.replace uses var (n + 1) | None -> NameHashtbl.add uses var 1 diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index c7fab8e5b..6297cc434 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -363,7 +363,7 @@ type spec_info = { (* A list of constructor functions *) constructors : IdSet.t; (* Global letbindings *) - global_lets : NameSet.t; + global_lets : ctyp NameMap.t; (* Global let numbers *) global_let_numbers : Ast.id list IntMap.t; (* Function footprint information *) @@ -407,12 +407,12 @@ let collect_spec_info ctx cdefs = (fun (names, nums) cdef -> match cdef with | CDEF_aux (CDEF_let (n, bindings, _), _) -> - ( List.fold_left (fun acc (id, _) -> NameSet.add (name id) acc) names bindings, + ( List.fold_left (fun acc (id, ctyp) -> NameMap.add (name id) ctyp acc) names bindings, IntMap.add n (List.map fst bindings) nums ) | _ -> (names, nums) ) - (NameSet.empty, IntMap.empty) cdefs + (NameMap.empty, IntMap.empty) cdefs in let footprints = List.fold_left @@ -552,6 +552,7 @@ module type CONFIG = sig val max_unknown_bitvector_width : int val line_directives : bool val no_strings : bool + val no_toplevel_globals : bool val no_packed : bool val no_assertions : bool val never_pack_unions : bool @@ -592,17 +593,17 @@ module Make (Config : CONFIG) = struct in Str.string_match regexp s 0 - let pp_id_string id = + let pp_id_string ?(is_global = false) id = let s = string_of_id id in if valid_sv_identifier s && (not (has_bad_prefix s)) && (not (StringSet.mem s Keywords.sv_reserved_words)) && not (StringSet.mem s Keywords.sv_used_words) - then s + then if Config.no_toplevel_globals && is_global then "`SAIL_GLOBALS." ^ s else s else Util.zencode_string s - let pp_id id = string (pp_id_string id) + let pp_id ?(is_global = false) id = string (pp_id_string ~is_global id) let pp_sv_name_string = function SVN_id id -> pp_id_string id | SVN_string s -> s @@ -719,10 +720,10 @@ module Make (Config : CONFIG) = struct let mapM = Smt_gen.mapM let fmap = Smt_gen.fmap - let pp_name = + let pp_name ?(is_global = false) = let ssa_num n = if n = -1 then empty else string ("_" ^ string_of_int n) in function - | Name (id, n) -> pp_id id ^^ ssa_num n + | Name (id, n) -> pp_id ~is_global id ^^ ssa_num n | Have_exception n -> string "sail_have_exception" ^^ ssa_num n | Current_exception n -> string "sail_current_exception" ^^ ssa_num n | Throw_location n -> string "sail_throw_location" ^^ ssa_num n @@ -1069,6 +1070,7 @@ module Make (Config : CONFIG) = struct else if n = m then braces (pp_smt x) ^^ lbracket ^^ string (string_of_int n) ^^ rbracket else braces (pp_smt x) ^^ lbracket ^^ string (string_of_int n) ^^ colon ^^ string (string_of_int m) ^^ rbracket | Var v -> pp_name v + | Global_var v -> pp_name ~is_global:true v | Tester (ctor, v) -> opt_parens (separate space @@ -1855,9 +1857,10 @@ module Make (Config : CONFIG) = struct in let open Jib_ssa in + let global_names = NameSet.of_list @@ List.map fst @@ NameMap.bindings spec_info.global_lets in let _, end_node, cfg = ssa - ~globals:(NameSet.diff spec_info.global_lets (NameSet.of_list (List.map Jib_util.name params))) + ~globals:(NameSet.diff global_names (NameSet.of_list (List.map Jib_util.name params))) ?debug_prefix:(Option.map (fun _ -> string_of_sv_name name) debug_attr) (visit_instrs (new thread_registers ctx spec_info) body) in @@ -2160,6 +2163,12 @@ module Make (Config : CONFIG) = struct let prefix = Attr.get_string ~default:"SAIL START\\n" "prefix" attr in let suffix = Attr.get_string ~default:"SAIL END\\n" "suffix" attr in + let global_defs = + if Config.no_toplevel_globals then + NameMap.fold (fun name ctyp acc -> SVD_var (name, ctyp) :: acc) spec_info.global_lets [] + else [] + in + let register_resets, register_inputs, register_outputs = Bindings.fold (fun reg ctyp (resets, ins, outs) -> @@ -2323,7 +2332,7 @@ module Make (Config : CONFIG) = struct | _ -> ([], [mk_port Jib_util.return ret_ctyp]) in let defs = - register_inputs @ register_outputs @ throws_outputs @ channel_outputs @ memory_writes @ return_def + global_defs @ register_inputs @ register_outputs @ throws_outputs @ channel_outputs @ memory_writes @ return_def @ initialize_letbindings @ initialize_registers @ [instantiate_main; always_block] in { @@ -2399,7 +2408,12 @@ module Make (Config : CONFIG) = struct and pp_def in_module (SVD_aux (aux, _)) = match aux with | SVD_null -> empty - | SVD_var (id, ctyp) -> wrap_type ctyp (pp_name id) ^^ semi + | SVD_var (id, ctyp) -> + if + (* If globals are moved to the sail_toplevel module, don't print them at toplevel *) + Config.no_toplevel_globals && Option.is_none in_module + then empty + else wrap_type ctyp (pp_name id) ^^ semi | SVD_initial statement -> string "initial" ^^ space ^^ pp_statement ~terminator:semi statement | SVD_always_ff statement -> let posedge_clk = char '@' ^^ parens (string "posedge" ^^ space ^^ string "clk") in diff --git a/src/sail_sv_backend/jib_sv.mli b/src/sail_sv_backend/jib_sv.mli index 0145d0c11..191943027 100644 --- a/src/sail_sv_backend/jib_sv.mli +++ b/src/sail_sv_backend/jib_sv.mli @@ -74,6 +74,8 @@ module type CONFIG = sig SystemVerilog. *) val no_strings : bool + val no_toplevel_globals : bool + val no_packed : bool (** If true, then all assertions are treated as no-ops *) @@ -150,9 +152,9 @@ module Make (Config : CONFIG) : sig val wrap_type : Jib.ctyp -> PPrint.document -> PPrint.document - val pp_id_string : Ast.id -> string + val pp_id_string : ?is_global:bool -> Ast.id -> string - val pp_id : Ast.id -> PPrint.document + val pp_id : ?is_global:bool -> Ast.id -> PPrint.document val main_args : Jib.cdef option -> diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index bdda41ed3..44a0c3b00 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -91,6 +91,7 @@ let opt_max_unknown_integer_width = ref 128 let opt_max_unknown_bitvector_width = ref 128 let opt_no_strings = ref false +let opt_no_toplevel_globals = ref false let opt_no_packed = ref false let opt_no_assertions = ref false let opt_never_pack_unions = ref false @@ -170,6 +171,10 @@ let verilog_options = "set the maximum width for bitvectors with unknown width" ); (Flag.create ~prefix:["sv"] "no_strings", Arg.Set opt_no_strings, "don't emit any strings, instead emit units"); + ( Flag.create ~prefix:["sv"] "no_toplevel_globals", + Arg.Set opt_no_toplevel_globals, + "declare global signals in 'sail_toplevel' module instead of toplevel." + ); (Flag.create ~prefix:["sv"] "no_packed", Arg.Set opt_no_packed, "don't emit packed datastructures"); (Flag.create ~prefix:["sv"] "no_assertions", Arg.Set opt_no_assertions, "ignore all Sail asserts"); (Flag.create ~prefix:["sv"] "never_pack_unions", Arg.Set opt_never_pack_unions, "never emit a packed union"); @@ -227,6 +232,7 @@ let verilog_rewrites = ("merge_function_clauses", []); ("recheck_defs", []); ("constant_fold", [String_arg "systemverilog"]); + ("remove_global_vars", []); ("unroll_constant_loops", [If_flag opt_unroll_loops]); ] @@ -446,6 +452,7 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = let max_unknown_bitvector_width = !opt_max_unknown_bitvector_width let line_directives = !opt_line_directives let no_strings = !opt_no_strings + let no_toplevel_globals = !opt_no_toplevel_globals let no_packed = !opt_no_packed let no_assertions = !opt_no_assertions let never_pack_unions = !opt_never_pack_unions diff --git a/src/sail_sv_backend/sv_ir.ml b/src/sail_sv_backend/sv_ir.ml index a8c953fa4..1e540f621 100644 --- a/src/sail_sv_backend/sv_ir.ml +++ b/src/sail_sv_backend/sv_ir.ml @@ -173,6 +173,9 @@ let rec visit_smt_exp (vis : svir_visitor) outer_smt_exp = | Var name -> let name' = visit_name (vis :> common_visitor) name in if name == name' then no_change else Var name' + | Global_var name -> + let name' = visit_name (vis :> common_visitor) name in + if name == name' then no_change else Global_var name' | ZeroExtend (n, m, exp) -> let exp' = visit_smt_exp vis exp in if exp == exp' then no_change else ZeroExtend (n, m, exp') diff --git a/src/sail_sv_backend/sv_optimize.ml b/src/sail_sv_backend/sv_optimize.ml index e19ffb38b..a4de14046 100644 --- a/src/sail_sv_backend/sv_optimize.ml +++ b/src/sail_sv_backend/sv_optimize.ml @@ -316,7 +316,7 @@ module RemoveUnusedVariables = struct else Forbid | Field (_, _, x) -> can_propagate stack name x | Unwrap (_, _, x) -> can_propagate stack name x - | Var v -> + | Global_var v | Var v -> let rec walk found = function | Block (_, vars) :: tail -> let found = found || NameMap.mem name vars in @@ -365,7 +365,7 @@ module RemoveUnusedVariables = struct method! vsmt_exp = function - | Var name -> begin + | Global_var name | Var name -> begin match self#get_vnum name with | Some (_, vnum, ctyp) -> let usage = Option.value ~default:no_usage (Hashtbl.find_opt uses vnum) in @@ -524,7 +524,7 @@ module RemoveUnusedVariables = struct | None -> () let rec smt_uses ?(propagated = false) stack uses = function - | Var name -> add_use ~read:true ~propagated name stack uses + | Global_var name | Var name -> add_use ~read:true ~propagated name stack uses | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Unit | Member _ | Empty_list -> () | SignExtend (_, _, exp) | ZeroExtend (_, _, exp)