From a261d407443faa4a95ee8f2b0fbf5e8e046d17ca Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 28 Oct 2022 12:39:24 +0200 Subject: Move the AssignGlobal case from statement to rvalue --- compiler/FunsAnalysis.ml | 2 +- compiler/InterpreterExpressions.ml | 5 +-- compiler/InterpreterStatements.ml | 73 +++++++++++++++++++++----------------- compiler/InterpreterUtils.ml | 2 +- compiler/Substitute.ml | 4 +-- 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 -- cgit v1.2.3