Move the AssignGlobal case from statement to rvalue

5 files changed, 46 insertions, 40 deletions

diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 59373985..9413bd6a 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -62,7 +62,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
 
           method! visit_rvalue _env rv =
             match rv with
-            | Use _ | Ref _ | Discriminant _ | Aggregate _ -> ()
+            | Use _ | Ref _ | Global _ | Discriminant _ | Aggregate _ -> ()
             | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail
             | BinaryOp (bop, _, _) ->
                 can_fail := EU.binop_can_fail bop || !can_fail
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 5a6947b0..fbe36b6a 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -697,11 +697,11 @@ let eval_rvalue_aggregate (config : C.config)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-(** Evaluate an rvalue.
+(** Evaluate an rvalue which is not a global.
 
     Transmits the computed rvalue to the received continuation.
  *)
-let eval_rvalue (config : C.config) (rvalue : E.rvalue)
+let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
     (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue");
@@ -720,3 +720,4 @@ let eval_rvalue (config : C.config) (rvalue : E.rvalue)
   | E.Aggregate (aggregate_kind, ops) ->
       comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
   | E.Discriminant p -> comp_wrap (eval_rvalue_discriminant config p) ctx
+  | E.Global _ -> raise (Failure "Unreachable")
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index fc3b0975..debf3004 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -486,7 +486,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
       in
       let borrow_kind = if is_mut then E.Mut else E.Shared in
       let rv = E.Ref (p, borrow_kind) in
-      let cf_borrow = eval_rvalue config rv in
+      let cf_borrow = eval_rvalue_not_global config rv in
 
       (* Move the borrow to its destination *)
       let cf_move cf res : m_fun =
@@ -812,39 +812,46 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
   let cf_eval_st cf : m_fun =
    fun ctx ->
     match st.content with
-    | A.Assign (p, rvalue) ->
-        (* Evaluate the rvalue *)
-        let cf_eval_rvalue = eval_rvalue config rvalue in
-        (* Assign *)
-        let cf_assign cf (res : (V.typed_value, eval_error) result) ctx =
-          log#ldebug
-            (lazy
-              ("about to assign to place: " ^ place_to_string ctx p
-             ^ "\n- Context:\n" ^ eval_ctx_to_string ctx));
-          match res with
-          | Error EPanic -> cf Panic ctx
-          | Ok rv -> (
-              let expr = assign_to_place config rv p (cf Unit) ctx in
-              (* Update the synthesized AST - here we store meta-information.
-               * We do it only in specific cases (it is not always useful, and
-               * also it can lead to issues - for instance, if we borrow an
-               * inactivated borrow, we later can't translate it to pure values...) *)
-              match rvalue with
-              | E.Use _
-              | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut))
-              | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ ->
-                  let rp = rvalue_get_place rvalue in
-                  let rp =
-                    match rp with
-                    | Some rp -> Some (S.mk_mplace rp ctx)
-                    | None -> None
-                  in
-                  S.synthesize_assignment (S.mk_mplace p ctx) rv rp expr)
-        in
+    | A.Assign (p, rvalue) -> (
+        (* We handle global assignments separately *)
+        match rvalue with
+        | E.Global gid ->
+            (* Evaluate the global *)
+            eval_global config p gid cf ctx
+        | _ ->
+            (* Evaluate the rvalue *)
+            let cf_eval_rvalue = eval_rvalue_not_global config rvalue in
+            (* Assign *)
+            let cf_assign cf (res : (V.typed_value, eval_error) result) ctx =
+              log#ldebug
+                (lazy
+                  ("about to assign to place: " ^ place_to_string ctx p
+                 ^ "\n- Context:\n" ^ eval_ctx_to_string ctx));
+              match res with
+              | Error EPanic -> cf Panic ctx
+              | Ok rv -> (
+                  let expr = assign_to_place config rv p (cf Unit) ctx in
+                  (* Update the synthesized AST - here we store meta-information.
+                   * We do it only in specific cases (it is not always useful, and
+                   * also it can lead to issues - for instance, if we borrow an
+                   * inactivated borrow, we later can't translate it to pure values...) *)
+                  match rvalue with
+                  | E.Global _ -> raise (Failure "Unreachable")
+                  | E.Use _
+                  | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut))
+                  | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _
+                  | E.Aggregate _ ->
+                      let rp = rvalue_get_place rvalue in
+                      let rp =
+                        match rp with
+                        | Some rp -> Some (S.mk_mplace rp ctx)
+                        | None -> None
+                      in
+                      S.synthesize_assignment (S.mk_mplace p ctx) rv rp expr)
+            in
 
-        (* Compose and apply *)
-        comp cf_eval_rvalue cf_assign cf ctx
-    | A.AssignGlobal { dst; global } -> eval_global config dst global cf ctx
+            (* Compose and apply *)
+            comp cf_eval_rvalue cf_assign cf ctx)
     | A.FakeRead p ->
         let expand_prim_copy = false in
         let cf_prepare cf =
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 578ee5ef..31f25f45 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -242,4 +242,4 @@ let rvalue_get_place (rv : E.rvalue) : E.place option =
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
   | Ref (p, _) -> Some p
-  | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> None
+  | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 5e5858de..bc5febdc 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -233,6 +233,7 @@ let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) :
   | E.BinaryOp (binop, op1, op2) ->
       E.BinaryOp (binop, op_subst op1, op_subst op2)
   | E.Discriminant p -> E.Discriminant (p_subst p)
+  | E.Global _ -> (* Globals don't have type parameters *) rv
   | E.Aggregate (kind, ops) ->
       let ops = List.map op_subst ops in
       let kind =
@@ -285,9 +286,6 @@ and raw_statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
       let p = place_substitute tsubst p in
       let rvalue = rvalue_substitute tsubst rvalue in
       A.Assign (p, rvalue)
-  | A.AssignGlobal g ->
-      (* Globals don't have type parameters *)
-      A.AssignGlobal g
   | A.FakeRead p ->
       let p = place_substitute tsubst p in
       A.FakeRead p