Merge pull request #77 from julienfreche/fix_name_instead_of_global_c2

c2: primop: -O: make sure to pick global or name correctly

3 files changed, 11 insertions, 9 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 9dedb830..b2447125 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -320,21 +320,21 @@ module C_config(Opts : sig val branch_coverage : out_channel option end) : Confi
                   (* 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 id, ctyp), typ)
+                    AV_cval (V_id (name_or_global ctx 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 id, ctyp), typ)
+                  Not_found -> AV_cval (V_id (name_or_global ctx 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 (name id, ctyp), typ)
+              AV_cval (V_id (global id, ctyp), typ)
             else
               v
          | _ -> v
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 5e234eae..5bf53009 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -182,6 +182,12 @@ 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 Make(C: Config) = struct
 
 let ctyp_of_typ ctx typ = C.convert_typ ctx typ
@@ -191,12 +197,6 @@ let rec chunkify n xs =
   | xs, [] -> [xs]
   | xs, ys -> xs :: chunkify n ys
 
-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
-
 let coverage_branch_count = ref 0
 
 let coverage_loc_args l =
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 3756e58a..30f379d8 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -134,3 +134,5 @@ end
    convert several Sail language features, these are sail_assert,
    sail_exit, and sail_cons. *)
 val add_special_functions : Env.t -> Env.t
+
+val name_or_global : ctx -> id -> name