Remove Global constructor from Jib names

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

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), _)) ->

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

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

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

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

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 ^ "))"

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

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;

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

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"