From f24f1043e72cddad2b29b09b79649ffc5e1d7c42 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Jun 2022 06:19:11 +0200 Subject: Update eval_operand_prepare to not give a value to the continuation --- src/Cps.ml | 37 +++++++++-- src/InterpreterExpansion.ml | 31 +++++---- src/InterpreterExpressions.ml | 146 +++++++++++++++++++++++++++--------------- src/InterpreterStatements.ml | 76 ++++++++++------------ 4 files changed, 181 insertions(+), 109 deletions(-) diff --git a/src/Cps.ml b/src/Cps.ml index d7c50f26..2d7dd2be 100644 --- a/src/Cps.ml +++ b/src/Cps.ml @@ -77,7 +77,6 @@ let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun) comp f g let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx - let id_cm_fun : cm_fun = fun cf ctx -> cf ctx (** If we have a list of [inputs] of type `'a list` and a function [f] which @@ -92,7 +91,37 @@ let id_cm_fun : cm_fun = fun cf ctx -> cf ctx See the unit test below for an illustration. *) -let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) +let fold_left_apply_continuation (f : 'a -> ('c -> 'd) -> 'c -> 'd) + (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = + let rec eval_list (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = + fun ctx -> + match inputs with + | [] -> cf ctx + | x :: inputs -> comp (f x) (fun cf -> eval_list inputs cf) cf ctx + in + eval_list inputs cf + +(** Unit test/example for [fold_left_apply_continuation] *) +let _ = + fold_left_apply_continuation + (fun x cf (ctx : int) -> cf (ctx + x)) + [ 1; 20; 300; 4000 ] + (fun (ctx : int) -> assert (ctx = 4321)) + 0 + +(** If we have a list of [inputs] of type `'a list` and a function [f] which + evaluates one element of type `'a` to compute a result of type `'b` before + giving it to a continuation, the following function performs a fold operation: + it evaluates all the inputs one by one by accumulating the results in a list, + and gives the list to a continuation. + + Note that we make sure that the results are listed in the order in + which they were computed (the first element of the list is the result + of applying [f] to the first element of the inputs). + + See the unit test below for an illustration. + *) +let fold_left_list_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) (inputs : 'a list) (cf : 'b list -> 'c -> 'd) : 'c -> 'd = let rec eval_list (inputs : 'a list) (cf : 'b list -> 'c -> 'd) (outputs : 'b list) : 'c -> 'd = @@ -104,9 +133,9 @@ let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) in eval_list inputs cf [] -(** Unit test/example for [fold_left_apply_continuation] *) +(** Unit test/example for [fold_left_list_apply_continuation] *) let _ = - fold_left_apply_continuation + fold_left_list_apply_continuation (fun x cf (ctx : unit) -> cf (10 + x) ctx) [ 0; 1; 2; 3; 4 ] (fun values _ctx -> assert (values = [ 10; 11; 12; 13; 14 ])) diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 0b65a372..c34051a8 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -188,8 +188,6 @@ let replace_symbolic_values (at_most_once : bool) in (* Apply the substitution *) let ctx = obj#visit_eval_ctx None ctx in - (* Check that we substituted *) - assert !replaced; (* Return *) ctx @@ -469,8 +467,24 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) let seel = List.map fst see_cf_l in S.synthesize_symbolic_expansion sv sv_place seel subterms -(** Expand a symbolic value which is not an enumeration with several variants - (i.e., in a situation where it doesn't lead to branching). +(** Expand a symbolic boolean *) +let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value) + (sp_place : SA.mplace option) (cf_true : m_fun) (cf_false : m_fun) : m_fun = + fun ctx -> + (* Compute the expanded value *) + let original_sv = sp in + let original_sv_place = sp_place in + let rty = original_sv.V.sv_ty in + assert (rty = T.Bool); + (* Expand the symbolic value to true or false and continue execution *) + let see_true = V.SeConcrete (V.Bool true) in + let see_false = V.SeConcrete (V.Bool false) in + let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in + (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) + apply_branching_symbolic_expansions_non_borrow config original_sv + original_sv_place seel ctx + +(** Expand a symbolic value. [allow_branching]: if `true` we can branch (by expanding enumerations with stricly more than one variant), otherwise we can't. @@ -554,14 +568,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) (* Booleans *) | T.Bool -> assert allow_branching; - (* Expand the symbolic value to true or false and continue execution *) - let see_true = V.SeConcrete (V.Bool true) in - let see_false = V.SeConcrete (V.Bool false) in - let seel = [ see_true; see_false ] in - let seel = List.map (fun see -> (Some see, cf)) seel in - (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) - apply_branching_symbolic_expansions_non_borrow config original_sv - original_sv_place seel ctx + expand_symbolic_bool config sp sp_place cf cf ctx | _ -> raise (Failure ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty)) diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 4549365d..bdcadf3a 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -48,13 +48,24 @@ let expand_primitively_copyable_at_place (config : C.config) (* Apply *) expand cf ctx +(** Read a place (CPS-style function *) +let read_place (config : C.config) (access : access_kind) (p : E.place) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + let v = read_place_unwrap config access p ctx in + cf v ctx + (** Small utility. + Prepare the access to a place in a right-value (typically an operand) by + reorganizing the environment. + [expand_prim_copy]: if true, expand the symbolic values which are primitively copyable and contain borrows. *) -let prepare_rplace (config : C.config) (expand_prim_copy : bool) - (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = +let access_rplace_reorganize_and_read (config : C.config) + (expand_prim_copy : bool) (access : access_kind) (p : E.place) + (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> let cc = update_ctx_along_read_place config access p in let cc = comp cc (end_loans_at_place config access p) in @@ -63,13 +74,16 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool) comp cc (expand_primitively_copyable_at_place config access p) else cc in - let read_place cf : m_fun = - fun ctx -> - let v = read_place_unwrap config access p ctx in - cf v ctx - in + let read_place = read_place config access p in comp cc read_place cf ctx +let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) + (access : access_kind) (p : E.place) : cm_fun = + fun cf ctx -> + access_rplace_reorganize_and_read config expand_prim_copy access p + (fun _v -> cf) + ctx + (** Convert an operand constant operand value to a typed value *) let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) (cv : E.operand_constant_value) : V.typed_value = @@ -119,10 +133,10 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) | _, ConstantAdt _ | _, ConstantValue _ -> failwith "Improperly typed constant value" -(** Prepare the evaluation of an operand. +(** Reorganize the environment in preparation for the evaluation of an operand. - Evaluating an operand requires updating the context to get access to a - given place (by ending borrows, expanding symbolic values...) then + Evaluating an operand requires reorganizing the environment to get access + to a given place (by ending borrows, expanding symbolic values...) then applying the operand operation (move, copy, etc.). Sometimes, we want to decouple the two operations. @@ -136,7 +150,7 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) dest <- f(move x, move y); ... ``` - Because of the way end_borrow is implemented, when giving back the borrow + Because of the way `end_borrow` is implemented, when giving back the borrow `l0` upon evaluating `move y`, we won't notice that `shared_borrow l0` has disappeared from the environment (it has been moved and not assigned yet, and so is hanging in "thin air"). @@ -144,51 +158,49 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) By first "preparing" the operands evaluation, we make sure no such thing happens. To be more precise, we make sure all the updates to borrows triggered by access *and* move operations have already been applied. + + Rk.: in the formalization, we always have an explicit "reorganization" step + in the rule premises, before the actual operand evaluation. - As a side note: doing this is actually not completely necessary because when + Rk.: doing this is actually not completely necessary because when generating MIR, rustc introduces intermediate assignments for all the function parameters. Still, it is better for soundness purposes, and corresponds to - what we do in the formal semantics. + what we do in the formalization (because we don't enforce constraints + in the formalization). *) -let eval_operand_prepare (config : C.config) (op : E.operand) - (cf : V.typed_value -> m_fun) : m_fun = - fun ctx -> - let prepare (cf : V.typed_value -> m_fun) : m_fun = - fun ctx -> +let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : + cm_fun = + fun cf ctx -> + let prepare : cm_fun = + fun cf ctx -> match op with - | Expressions.Constant (ty, cv) -> - let v = operand_constant_value_to_typed_value ctx ty cv in - cf v ctx + | Expressions.Constant _ -> + (* No need to reorganize the context *) + cf ctx | Expressions.Copy p -> (* Access the value *) let access = Read in (* Expand the symbolic values, if necessary *) let expand_prim_copy = true in - prepare_rplace config expand_prim_copy access p cf ctx + access_rplace_reorganize config expand_prim_copy access p cf ctx | Expressions.Move p -> (* Access the value *) let access = Move in let expand_prim_copy = false in - prepare_rplace config expand_prim_copy access p cf ctx + access_rplace_reorganize config expand_prim_copy access p cf ctx in - (* Sanity check *) - let check cf v : m_fun = - fun ctx -> - assert (not (bottom_in_value ctx.ended_regions v)); - cf v ctx - in - (* Compose and apply *) - comp prepare check cf ctx + (* Apply *) + prepare cf ctx -(** Evaluate an operand. *) -let eval_operand (config : C.config) (op : E.operand) +(** Evaluate an operand, without reorganizing the context before *) +let eval_operand_no_reorganize (config : C.config) (op : E.operand) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug (lazy - ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n" - ^ eval_ctx_to_string ctx ^ "\n")); + ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op + ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with | Expressions.Constant (ty, cv) -> @@ -197,8 +209,7 @@ let eval_operand (config : C.config) (op : E.operand) | Expressions.Copy p -> (* Access the value *) let access = Read in - let expand_prim_copy = true in - let cc = prepare_rplace config expand_prim_copy access p in + let cc = read_place config access p in (* Copy the value *) let copy cf v : m_fun = fun ctx -> @@ -208,8 +219,8 @@ let eval_operand (config : C.config) (op : E.operand) Option.is_none (find_first_primitively_copyable_sv_with_borrows ctx.type_context.type_infos v)); - let allow_adt_copy = false in (* Actually perform the copy *) + let allow_adt_copy = false in let ctx, v = copy_value allow_adt_copy config ctx v in (* Continue *) cf v ctx @@ -219,11 +230,11 @@ let eval_operand (config : C.config) (op : E.operand) | Expressions.Move p -> (* Access the value *) let access = Move in - let expand_prim_copy = false in - let cc = prepare_rplace config expand_prim_copy access p in + let cc = read_place config access p in (* Move the value *) let move cf v : m_fun = fun ctx -> + (* Check that there are no bottoms in the value we are about to move *) assert (not (bottom_in_value ctx.ended_regions v)); let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in match write_place config access p bottom ctx with @@ -233,24 +244,49 @@ let eval_operand (config : C.config) (op : E.operand) (* Compose and apply *) comp cc move cf ctx +(** Evaluate an operand. + + Reorganize the context, then evaluate the operand. + + **Warning**: this function shouldn't be used to evaluate a list of + operands (for a function call, for instance): we must do *one* reorganization + of the environment, before evaluating all the operands at once. + Use [`eval_operands`] instead. + *) +let eval_operand (config : C.config) (op : E.operand) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + (* Debug *) + log#ldebug + (lazy + ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n" + ^ eval_ctx_to_string ctx ^ "\n")); + (* We reorganize the context, then evaluate the operand *) + comp + (prepare_eval_operand_reorganize config op) + (eval_operand_no_reorganize config op) + cf ctx + (** Small utility. - See [eval_operand_prepare]. + See [prepare_eval_operand_reorganize]. *) -let eval_operands_prepare (config : C.config) (ops : E.operand list) - (cf : V.typed_value list -> m_fun) : m_fun = - fold_left_apply_continuation (eval_operand_prepare config) ops cf +let prepare_eval_operands_reorganize (config : C.config) (ops : E.operand list) + : cm_fun = + fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops (** Evaluate several operands. *) let eval_operands (config : C.config) (ops : E.operand list) (cf : V.typed_value list -> m_fun) : m_fun = fun ctx -> (* Prepare the operands *) - let prepare = eval_operands_prepare config ops in + let prepare = prepare_eval_operands_reorganize config ops in (* Evaluate the operands *) - let eval = fold_left_apply_continuation (eval_operand config) ops in + let eval = + fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops + in (* Compose and apply *) - comp prepare (fun cf (_ : V.typed_value list) -> eval cf) cf ctx + comp prepare eval cf ctx let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand) (cf : V.typed_value * V.typed_value -> m_fun) : m_fun = @@ -469,7 +505,9 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place) (* Access the value *) let access = Read in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Read the value *) let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = (* The value may be shared: we need to ignore the shared loans *) @@ -507,7 +545,9 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place) (* Access the value *) let access = Read in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Read the value *) let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = fun ctx -> @@ -539,7 +579,9 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* Access the value *) let access = if bkind = E.Shared then Read else Write in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Evaluate the borrowing operation *) let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = fun ctx -> @@ -580,7 +622,9 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* Access the value *) let access = Write in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Evaluate the borrowing operation *) let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = fun ctx -> diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 1083d643..e2775a1d 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -150,13 +150,10 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) : *) let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = fun cf ctx -> - (* There may be a symbolic expansion, so don't fully evaluate the operand - * (if we moved the value, we can't expand it because it is hanging in - * thin air, outside of the environment...): simply update the environment - * to make sure we have access to the value we want to check. *) - let prepare = eval_operand_prepare config assertion.cond in + (* Evaluate the operand *) + let eval_op = eval_operand config assertion.cond in (* Evaluate the assertion *) - let eval cf (v : V.typed_value) : m_fun = + let eval_assert cf (v : V.typed_value) : m_fun = fun ctx -> assert (v.ty = T.Bool); (* We make a choice here: we could completely decouple the concrete and @@ -171,20 +168,22 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = | Symbolic sv -> assert (config.mode = C.SymbolicMode); assert (sv.V.sv_ty = T.Bool); - (* Expand the symbolic value, then call the evaluation function for the - * non-symbolic case *) - let allow_branching = true in + (* Expand the symbolic value and call the proper continuation functions + * for the true and false cases - TODO: call an "assert" function instead *) + let cf_true : m_fun = fun ctx -> cf Unit ctx in + let cf_false : m_fun = fun ctx -> cf Panic ctx in let expand = - expand_symbolic_value config allow_branching sv + expand_symbolic_bool config sv (S.mk_opt_place_from_op assertion.cond ctx) + cf_true cf_false in - comp expand (eval_assertion_concrete config assertion) cf ctx + expand ctx | _ -> raise (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) in (* Compose and apply *) - comp prepare eval cf ctx + comp eval_op eval_assert cf ctx (** Updates the discriminant of a value at a given place. @@ -823,8 +822,14 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = comp cf_eval_rvalue cf_assign cf ctx | A.FakeRead p -> let expand_prim_copy = false in - let cf_prepare = prepare_rplace config expand_prim_copy Read p in - let cf_continue cf _ = cf in + let cf_prepare cf = + access_rplace_reorganize_and_read config expand_prim_copy Read p cf + in + let cf_continue cf v : m_fun = + fun ctx -> + assert (not (bottom_in_value ctx.ended_regions v)); + cf ctx + in comp cf_prepare cf_continue (cf Unit) ctx | A.SetDiscriminant (p, variant_id) -> set_discriminant config p variant_id cf ctx @@ -905,7 +910,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : * (and would thus floating in thin air...)! * *) (* Prepare the operand *) - let cf_prepare_op cf : m_fun = eval_operand_prepare config op cf in + let cf_eval_op cf : m_fun = eval_operand config op cf in (* Match on the targets *) let cf_match (cf : st_m_fun) (op_v : V.typed_value) : m_fun = fun ctx -> @@ -913,39 +918,29 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : | A.If (st1, st2) -> ( match op_v.value with | V.Concrete (V.Bool b) -> - (* Evaluate the operand *) - let cf_eval_op cf : m_fun = eval_operand config op cf in (* Evaluate the if and the branch body *) - let cf_branch cf op_v' : m_fun = - assert (op_v' = op_v); + let cf_branch cf : m_fun = (* Branch *) if b then eval_statement config st1 cf else eval_statement config st2 cf in (* Compose the continuations *) - comp cf_eval_op cf_branch cf ctx + cf_branch cf ctx | V.Symbolic sv -> - (* Expand the symbolic value *) - let allows_branching = true in - let cf_expand cf = - expand_symbolic_value config allows_branching sv - (S.mk_opt_place_from_op op ctx) - cf - in - (* Retry *) - let cf_eval_if cf = eval_switch config op tgts cf in - (* Compose *) - comp cf_expand cf_eval_if cf ctx + (* Expand the symbolic boolean, and continue by evaluating + * the branches *) + let cf_true : m_fun = eval_statement config st1 cf in + let cf_false : m_fun = eval_statement config st2 cf in + expand_symbolic_bool config sv + (S.mk_opt_place_from_op op ctx) + cf_true cf_false ctx | _ -> raise (Failure "Inconsistent state")) | A.SwitchInt (int_ty, stgts, otherwise) -> ( match op_v.value with | V.Concrete (V.Scalar sv) -> - (* Evaluate the operand *) - let cf_eval_op cf = eval_operand config op cf in (* Evaluate the branch *) - let cf_eval_branch cf op_v' = + let cf_eval_branch cf = (* Sanity check *) - assert (op_v' = op_v); assert (sv.V.int_ty = int_ty); (* Find the branch *) match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with @@ -953,13 +948,10 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : | Some (_, tgt) -> eval_statement config tgt cf in (* Compose *) - comp cf_eval_op cf_eval_branch cf ctx + cf_eval_branch cf ctx | V.Symbolic sv -> - (* Expand the symbolic value - note that contrary to the boolean - * case, we can't expand then retry, because when switching over - * arbitrary integers we need to have an `otherwise` case, in - * which the scrutinee remains symbolic: if we expand the symbolic, - * reevaluate the switch, we loop... *) + (* Expand the symbolic value and continue by evaluating the + * proper branches *) let stgts = List.map (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st cf)) @@ -984,7 +976,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : | _ -> raise (Failure "Inconsistent state")) in (* Compose the continuations *) - comp cf_prepare_op cf_match cf ctx + comp cf_eval_op cf_match cf ctx (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = -- cgit v1.2.3