From 435ffd3d9ff211d7e5a7e1792229b0435389980d Mon Sep 17 00:00:00 2001 From: Alasdair Date: Mon, 13 Nov 2023 11:45:13 +0000 Subject: [PATCH] Remove Global constructor from Jib names --- language/jib.ott | 1 - src/lib/jib_compile.ml | 17 ++++++----------- src/lib/jib_compile.mli | 2 -- src/lib/jib_optimize.ml | 1 - src/lib/jib_util.ml | 9 +-------- src/lib/jib_util.mli | 1 - src/sail_c_backend/c_backend.ml | 8 +++----- src/sail_smt_backend/jib_ir.ml | 2 +- src/sail_smt_backend/jib_smt.ml | 18 +++++++++--------- src/sail_smt_backend/jib_ssa.ml | 1 - src/sail_sv_backend/jib_sv.ml | 1 - 11 files changed, 20 insertions(+), 41 deletions(-) diff --git a/language/jib.ott b/language/jib.ott index 7ff5905ef..52fe1101e 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -62,7 +62,6 @@ grammar name :: '' ::= | id nat :: :: name - | global id nat :: :: global | have_exception nat :: :: have_exception | current_exception nat :: :: current_exception | throw_location nat :: :: throw_location diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index a61492373..de4537dbd 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -247,9 +247,6 @@ module type CONFIG = sig val track_throw : bool end -let name_or_global ctx id = - if Env.is_register id ctx.local_env || IdSet.mem id (Env.get_toplevel_lets ctx.local_env) then global id else name id - module IdGraph = Graph.Make (Id) module IdGraphNS = Set.Make (Id) @@ -354,7 +351,7 @@ module Make (C : CONFIG) = struct | AV_id (id, typ) -> begin match Bindings.find_opt id ctx.locals with | Some (_, ctyp) -> ([], V_id (name id, ctyp), []) - | None -> ([], V_id (name_or_global ctx id, ctyp_of_typ ctx (lvar_typ typ)), []) + | None -> ([], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), []) end | 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), []) @@ -621,7 +618,7 @@ module Make (C : CONFIG) = struct match apat_aux with | AP_global (pid, typ) -> let global_ctyp = ctyp_of_typ ctx typ in - ([], [icopy l (CL_id (global pid, global_ctyp)) cval], [], ctx) + ([], [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx) | AP_id (pid, _) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with | Unbound _ -> ([], [idecl l ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx) @@ -717,10 +714,10 @@ module Make (C : CONFIG) = struct match alexp with | AL_id (id, typ) -> let ctyp = match Bindings.find_opt id ctx.locals with Some (_, ctyp) -> ctyp | None -> ctyp_of_typ ctx typ in - CL_id (name_or_global ctx id, ctyp) + CL_id (name id, ctyp) | AL_addr (id, typ) -> let ctyp = match Bindings.find_opt id ctx.locals with Some (_, ctyp) -> ctyp | None -> ctyp_of_typ ctx typ in - CL_addr (CL_id (name_or_global ctx id, ctyp)) + CL_addr (CL_id (name id, ctyp)) | AL_field (alexp, field_id) -> CL_field (compile_alexp ctx alexp, field_id) let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @@ -931,9 +928,7 @@ module Make (C : CONFIG) = struct when Id.compare id rid = 0 -> let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in - field_setup - @ [icopy l (CL_field (CL_id (name_or_global ctx id, ctyp_of_typ ctx typ), field_id)) cval] - @ field_cleanup + field_setup @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), field_id)) cval] @ field_cleanup in (List.concat (List.map compile_fields (Bindings.bindings fields)), (fun clexp -> icopy l clexp unit_cval), []) | AE_assign (alexp, aexp) -> @@ -1480,7 +1475,7 @@ module Make (C : CONFIG) = struct | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), _)) -> let aexp = C.optimize_anf ctx (no_shadow ctx.letbind_ids (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id (global id, ctyp_of_typ ctx typ))] @ cleanup in + let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in let instrs = unique_names instrs in ([CDEF_register (id, ctyp_of_typ ctx typ, instrs)], ctx) | DEF_val (VS_aux (VS_val_spec (_, id, ext), _)) -> diff --git a/src/lib/jib_compile.mli b/src/lib/jib_compile.mli index 258b4ce21..110402545 100644 --- a/src/lib/jib_compile.mli +++ b/src/lib/jib_compile.mli @@ -179,5 +179,3 @@ end convert several Sail language features, these are sail_assert, sail_exit, and sail_cons. *) val add_special_functions : Env.t -> Effects.side_effect_info -> Env.t * Effects.side_effect_info - -val name_or_global : ctx -> id -> name diff --git a/src/lib/jib_optimize.ml b/src/lib/jib_optimize.ml index 3781b6737..e6754694f 100644 --- a/src/lib/jib_optimize.ml +++ b/src/lib/jib_optimize.ml @@ -263,7 +263,6 @@ let rec find_function fid = function let ssa_name i = function | Name (id, _) -> Name (id, i) - | Global (id, _) -> Global (id, i) | Have_exception _ -> Have_exception i | Current_exception _ -> Current_exception i | Throw_location _ -> Throw_location i diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index 3aba10062..bd0be61cb 100644 --- a/src/lib/jib_util.ml +++ b/src/lib/jib_util.ml @@ -141,16 +141,11 @@ module Name = struct | Name (x, n), Name (y, m) -> let c1 = Id.compare x y in if c1 = 0 then compare n m else c1 - | Global (x, n), Global (y, m) -> - let c1 = Id.compare x y in - if c1 = 0 then compare n m else c1 | Have_exception n, Have_exception m -> compare n m | Current_exception n, Current_exception m -> compare n m | Return n, Return m -> compare n m | Name _, _ -> 1 | _, Name _ -> -1 - | Global _, _ -> 1 - | _, Global _ -> -1 | Have_exception _, _ -> 1 | _, Have_exception _ -> -1 | Current_exception _, _ -> 1 @@ -168,7 +163,6 @@ let throw_location = Throw_location (-1) let return = Return (-1) let name id = Name (id, -1) -let global id = Global (id, -1) class rename_visitor from_name to_name : jib_visitor = object @@ -206,8 +200,7 @@ let instrs_rename from_name to_name = visit_instrs (new rename_visitor from_name let string_of_name ?deref_current_exception:(dce = false) ?(zencode = true) = let ssa_num n = if n = -1 then "" else "/" ^ string_of_int n in function - | Name (id, n) | Global (id, n) -> - (if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n + | Name (id, n) -> (if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n | Have_exception n -> "have_exception" ^ ssa_num n | Return n -> "return" ^ ssa_num n | Current_exception n when dce -> "(*current_exception)" ^ ssa_num n diff --git a/src/lib/jib_util.mli b/src/lib/jib_util.mli index c4bae46f5..977f9d3bd 100644 --- a/src/lib/jib_util.mli +++ b/src/lib/jib_util.mli @@ -122,7 +122,6 @@ val throw_location : name val return : name val name : id -> name -val global : id -> name val cval_rename : name -> name -> cval -> cval val clexp_rename : name -> name -> clexp -> clexp diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index d75bc81ed..3344fc645 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -332,19 +332,19 @@ end) : CONFIG = struct try (* We need to check that id's type hasn't changed due to flow typing *) let _, ctyp' = Bindings.find id ctx.locals in - if ctyp_equal ctyp ctyp' then AV_cval (V_id (name_or_global ctx id, ctyp), typ) + if ctyp_equal ctyp ctyp' then AV_cval (V_id (name id, ctyp), typ) else (* id's type changed due to flow typing, so it's really still heap allocated! *) v with (* Hack: Assuming global letbindings don't change from flow typing... *) | Not_found -> - AV_cval (V_id (name_or_global ctx id, ctyp), typ) + AV_cval (V_id (name id, ctyp), typ) end else v | Register typ -> let ctyp = convert_typ ctx typ in - if is_stack_ctyp ctyp && not (never_optimize ctyp) then AV_cval (V_id (global id, ctyp), typ) else v + if is_stack_ctyp ctyp && not (never_optimize ctyp) then AV_cval (V_id (name id, ctyp), typ) else v | _ -> v end | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 -> @@ -1054,7 +1054,6 @@ let rec sgen_clexp l = function | CL_id (Throw_location _, _) -> "throw_location" | CL_id (Return _, _) -> Reporting.unreachable l __POS__ "CL_return should have been removed" | CL_id (Name (id, _), _) -> "&" ^ sgen_id id - | CL_id (Global (id, _), _) -> "&" ^ sgen_id id | CL_field (clexp, field) -> "&((" ^ sgen_clexp l clexp ^ ")->" ^ zencode_id field ^ ")" | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp l clexp ^ ")->ztup" ^ string_of_int n ^ ")" | CL_addr clexp -> "(*(" ^ sgen_clexp l clexp ^ "))" @@ -1067,7 +1066,6 @@ let rec sgen_clexp_pure l = function | CL_id (Throw_location _, _) -> "throw_location" | CL_id (Return _, _) -> Reporting.unreachable l __POS__ "CL_return should have been removed" | CL_id (Name (id, _), _) -> sgen_id id - | CL_id (Global (id, _), _) -> sgen_id id | CL_field (clexp, field) -> sgen_clexp_pure l clexp ^ "." ^ zencode_id field | CL_tuple (clexp, n) -> sgen_clexp_pure l clexp ^ ".ztup" ^ string_of_int n | CL_addr clexp -> "(*(" ^ sgen_clexp_pure l clexp ^ "))" diff --git a/src/sail_smt_backend/jib_ir.ml b/src/sail_smt_backend/jib_ir.ml index 51cd7a990..b743cc298 100644 --- a/src/sail_smt_backend/jib_ir.ml +++ b/src/sail_smt_backend/jib_ir.ml @@ -81,7 +81,7 @@ module StringMap = Map.Make (String) let string_of_name = let ssa_num n = if n = -1 then "" else "/" ^ string_of_int n in function - | Name (id, n) | Global (id, n) -> zencode_id id ^ ssa_num n + | Name (id, n) -> zencode_id id ^ ssa_num n | Have_exception n -> "have_exception" ^ ssa_num n | Return n -> "return" ^ ssa_num n | Current_exception n -> "current_exception" ^ ssa_num n diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 8ab062de8..d49af4972 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -358,7 +358,7 @@ let rec smt_cval ctx cval = | _ -> ( match cval with | V_lit (vl, ctyp) -> smt_value ctx vl ctyp - | V_id (((Name (id, _) | Global (id, _)) as ssa_id), _) -> begin + | V_id ((Name (id, _) as ssa_id), _) -> begin match Type_check.Env.lookup_id id ctx.tc_env with | Enum _ -> Enum (zencode_id id) | _ when Bindings.mem id ctx.shared -> Shared (zencode_id id) @@ -1355,8 +1355,8 @@ let rec generate_ctype_defs ctx = function | [] -> [] let rec generate_reg_decs ctx inits = function - | CDEF_register (id, ctyp, _) :: cdefs when not (NameMap.mem (Global (id, 0)) inits) -> - Declare_const (zencode_name (Global (id, 0)), smt_ctyp ctx ctyp) :: generate_reg_decs ctx inits cdefs + | CDEF_register (id, ctyp, _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits) -> + Declare_const (zencode_name (Name (id, 0)), smt_ctyp ctx ctyp) :: generate_reg_decs ctx inits cdefs | _ :: cdefs -> generate_reg_decs ctx inits cdefs | [] -> [] @@ -1848,7 +1848,7 @@ let smt_instr ctx = Reporting.unreachable l __POS__ "Register reference write should be re-written by now" | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) -> begin match (id, cval) with - | (Name (id, _) | Global (id, _)), _ when IdSet.mem id ctx.preserved -> + | Name (id, _), _ when IdSet.mem id ctx.preserved -> [preserve_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] | _, V_lit (VL_undefined, _) -> (* Declare undefined variables as arbitrary but fixed *) @@ -1896,7 +1896,7 @@ let smt_cfnode all_cdefs ctx ssa_elems = let rec find_function lets id = function | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 -> (lets, Some (heap_return, args, body)) | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (global id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (name id)) vars in find_function (lets @ vars @ setup) id cdefs | _ :: cdefs -> find_function lets id cdefs | [] -> (lets, None) @@ -2104,7 +2104,7 @@ let expand_reg_deref env register_map = function let next_label = label "next_reg_write_" in [ ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - ifuncall l (CL_id (global r, reg_ctyp)) function_id args; + ifuncall l (CL_id (name r, reg_ctyp)) function_id args; igoto end_label; ilabel next_label; ] @@ -2132,7 +2132,7 @@ let expand_reg_deref env register_map = function let next_label = label "next_reg_deref_" in [ ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label; - icopy l clexp (V_id (global r, reg_ctyp)); + icopy l clexp (V_id (name r, reg_ctyp)); igoto end_label; ilabel next_label; ] @@ -2155,7 +2155,7 @@ let expand_reg_deref env register_map = function let next_label = label "next_reg_write_" in [ ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - icopy l (CL_id (global r, reg_ctyp)) cval; + icopy l (CL_id (name r, reg_ctyp)) cval; igoto end_label; ilabel next_label; ] @@ -2297,7 +2297,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function let rec smt_cdefs props lets name_file ctx ast = function | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (global id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (name id)) vars in smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs | cdef :: cdefs -> smt_cdef props lets name_file ctx ast cdef; diff --git a/src/sail_smt_backend/jib_ssa.ml b/src/sail_smt_backend/jib_ssa.ml index 569efb484..5fb86ced3 100644 --- a/src/sail_smt_backend/jib_ssa.ml +++ b/src/sail_smt_backend/jib_ssa.ml @@ -488,7 +488,6 @@ let rename_variables graph root children = let ssa_name i = function | Name (id, _) -> Name (id, i) - | Global (id, _) -> Global (id, i) | Have_exception _ -> Have_exception i | Current_exception _ -> Current_exception i | Throw_location _ -> Throw_location i diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index 383db2d46..ba68b79ae 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -242,7 +242,6 @@ module Make (Config : CONFIG) = struct let sv_name = function | Name (id, _) -> sv_id id - | Global (id, _) -> sv_id id | Have_exception _ -> string "sail_have_exception" | Current_exception _ -> string "sail_current_exception" | Throw_location _ -> string "sail_throw_location"