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/InterpreterExpressions.ml | 146 +++++++++++++++++++++++++++--------------- 1 file changed, 95 insertions(+), 51 deletions(-) (limited to 'src/InterpreterExpressions.ml') 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 -> -- cgit v1.2.3