summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/FunsAnalysis.ml2
-rw-r--r--compiler/InterpreterExpressions.ml5
-rw-r--r--compiler/InterpreterStatements.ml73
-rw-r--r--compiler/InterpreterUtils.ml2
-rw-r--r--compiler/Substitute.ml4
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 01:20:58 +0000