diff options
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 720 |
1 files changed, 720 insertions, 0 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml new file mode 100644 index 00000000..62d9b80b --- /dev/null +++ b/compiler/InterpreterExpressions.ml @@ -0,0 +1,720 @@ +module T = Types +module V = Values +module LA = LlbcAst +open Scalars +module E = Expressions +open Errors +module C = Contexts +module Subst = Substitute +module L = Logging +module PV = Print.Values +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = SynthesizeSymbolic +open Cps +open InterpreterUtils +open InterpreterExpansion +open InterpreterPaths + +(** The local logger *) +let log = L.expressions_log + +(** As long as there are symbolic values at a given place (potentially in subvalues) + which contain borrows and are primitively copyable, expand them. + + We use this function before copying values. + + Note that the place should have been prepared so that there are no remaining + loans. +*) +let expand_primitively_copyable_at_place (config : C.config) + (access : access_kind) (p : E.place) : cm_fun = + fun cf ctx -> + (* Small helper *) + let rec expand : cm_fun = + fun cf ctx -> + let v = read_place_unwrap config access p ctx in + match + find_first_primitively_copyable_sv_with_borrows + ctx.type_context.type_infos v + with + | None -> cf ctx + | Some sv -> + let cc = + expand_symbolic_value_no_branching config sv + (Some (S.mk_mplace p ctx)) + in + comp cc expand cf ctx + in + (* Apply *) + expand cf ctx + +(** Read a place (CPS-style function). + + We also check that the value *doesn't contain bottoms or inactivated + borrows. + *) +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 + (* Check that there are no bottoms in the value *) + assert (not (bottom_in_value ctx.ended_regions v)); + (* Check that there are no inactivated borrows in the value *) + assert (not (inactivated_in_value v)); + (* Call the continuation *) + cf v ctx + +(** Small utility. + + Prepare the access to a place in a right-value (typically an operand) by + reorganizing the environment. + + We reorganize the environment so that: + - we can access the place (we prepare *along* the path) + - the value at the place itself doesn't contain loans (the [access_kind] + controls whether we only end mutable loans, or also shared loans). + + We also check, after the reorganization, that the value at the place + *doesn't contain any bottom nor inactivated borrows*. + + [expand_prim_copy]: if true, expand the symbolic values which are primitively + copyable and contain borrows. + *) +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 -> + (* Make sure we can evaluate the path *) + let cc = update_ctx_along_read_place config access p in + (* End the proper loans at the place itself *) + let cc = comp cc (end_loans_at_place config access p) in + (* Expand the copyable values which contain borrows (which are necessarily shared + * borrows) *) + let cc = + if expand_prim_copy then + comp cc (expand_primitively_copyable_at_place config access p) + else cc + in + (* Read the place - note that this checks that the value doesn't contain bottoms *) + let read_place = read_place config access p in + (* Compose *) + 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 constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value + = + (* Check the type while converting - we actually need some information + * contained in the type *) + log#ldebug + (lazy + ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv)); + match (ty, cv) with + (* Scalar, boolean... *) + | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty } + | T.Char, Char v -> { V.value = V.Concrete (Char v); ty } + | T.Str, String v -> { V.value = V.Concrete (String v); ty } + | T.Integer int_ty, V.Scalar v -> + (* Check the type and the ranges *) + assert (int_ty = v.int_ty); + assert (check_scalar_value_in_range v); + { V.value = V.Concrete (V.Scalar v); ty } + (* Remaining cases (invalid) *) + | _, _ -> failwith "Improperly typed constant value" + +(** Reorganize the environment in preparation for the evaluation of an operand. + + 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. + Consider the following example: + {[ + context = { + x -> shared_borrow l0 + y -> shared_loan {l0} v + } + + dest <- f(move x, move y); + ... + ]} + 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"). + + 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. + + 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 formalization (because we don't enforce constraints + in the formalization). + *) +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) -> + (* No need to reorganize the context *) + constant_to_typed_value ty cv |> ignore; + cf ctx + | Expressions.Copy p -> + (* Access the value *) + let access = Read in + (* Expand the symbolic values, if necessary *) + let expand_prim_copy = true in + 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 + access_rplace_reorganize config expand_prim_copy access p cf ctx + in + (* Apply *) + prepare cf ctx + +(** 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_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) -> cf (constant_to_typed_value ty cv) ctx + | Expressions.Copy p -> + (* Access the value *) + let access = Read in + let cc = read_place config access p in + (* Copy the value *) + let copy cf v : m_fun = + fun ctx -> + (* Sanity checks *) + assert (not (bottom_in_value ctx.ended_regions v)); + assert ( + Option.is_none + (find_first_primitively_copyable_sv_with_borrows + ctx.type_context.type_infos v)); + (* 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 + in + (* Compose and apply *) + comp cc copy cf ctx + | Expressions.Move p -> + (* Access the value *) + let access = Move 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 + | Error _ -> failwith "Unreachable" + | Ok ctx -> cf v ctx + in + (* 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 [prepare_eval_operand_reorganize]. + *) +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 = prepare_eval_operands_reorganize config ops in + (* Evaluate the operands *) + let eval = + fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops + in + (* Compose and apply *) + 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 = + let eval_op = eval_operands config [ op1; op2 ] in + let use_res cf res = + match res with [ v1; v2 ] -> cf (v1, v2) | _ -> failwith "Unreachable" + in + comp eval_op use_res cf + +let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand) + (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + (* Evaluate the operand *) + let eval_op = eval_operand config op in + (* Apply the unop *) + let apply cf (v : V.typed_value) : m_fun = + match (unop, v.V.value) with + | E.Not, V.Concrete (Bool b) -> + cf (Ok { v with V.value = V.Concrete (Bool (not b)) }) + | E.Neg, V.Concrete (V.Scalar sv) -> ( + let i = Z.neg sv.V.value in + match mk_scalar sv.int_ty i with + | Error _ -> cf (Error EPanic) + | Ok sv -> cf (Ok { v with V.value = V.Concrete (V.Scalar sv) })) + | E.Cast (src_ty, tgt_ty), V.Concrete (V.Scalar sv) -> ( + assert (src_ty == sv.int_ty); + let i = sv.V.value in + match mk_scalar tgt_ty i with + | Error _ -> cf (Error EPanic) + | Ok sv -> + let ty = T.Integer tgt_ty in + let value = V.Concrete (V.Scalar sv) in + cf (Ok { V.ty; value })) + | _ -> raise (Failure "Invalid input for unop") + in + comp eval_op apply cf + +let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) + (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + fun ctx -> + (* Evaluate the operand *) + let eval_op = eval_operand config op in + (* Generate a fresh symbolic value to store the result *) + let apply cf (v : V.typed_value) : m_fun = + fun ctx -> + let res_sv_id = C.fresh_symbolic_value_id () in + let res_sv_ty = + match (unop, v.V.ty) with + | E.Not, T.Bool -> T.Bool + | E.Neg, T.Integer int_ty -> T.Integer int_ty + | E.Cast (_, tgt_ty), _ -> T.Integer tgt_ty + | _ -> raise (Failure "Invalid input for unop") + in + let res_sv = + { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty } + in + (* Call the continuation *) + let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in + (* Synthesize the symbolic AST *) + S.synthesize_unary_op unop v + (S.mk_opt_place_from_op op ctx) + res_sv None expr + in + (* Compose and apply *) + comp eval_op apply cf ctx + +let eval_unary_op (config : C.config) (unop : E.unop) (op : E.operand) + (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + match config.mode with + | C.ConcreteMode -> eval_unary_op_concrete config unop op cf + | C.SymbolicMode -> eval_unary_op_symbolic config unop op cf + +(** Small helper for [eval_binary_op_concrete]: computes the result of applying + the binop *after* the operands have been successfully evaluated + *) +let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) + (v2 : V.typed_value) : (V.typed_value, eval_error) result = + (* Equality check binops (Eq, Ne) accept values from a wide variety of types. + * The remaining binops only operate on scalars. *) + if binop = Eq || binop = Ne then ( + (* Equality operations *) + assert (v1.ty = v2.ty); + (* Equality/inequality check is primitive only for a subset of types *) + assert (ty_is_primitively_copyable v1.ty); + let b = v1 = v2 in + Ok { V.value = V.Concrete (Bool b); ty = T.Bool }) + else + (* For the non-equality operations, the input values are necessarily scalars *) + match (v1.V.value, v2.V.value) with + | V.Concrete (V.Scalar sv1), V.Concrete (V.Scalar sv2) -> ( + (* There are binops which require the two operands to have the same + type, and binops for which it is not the case. + There are also binops which return booleans, and binops which + return integers. + *) + match binop with + | E.Lt | E.Le | E.Ge | E.Gt -> + (* The two operands must have the same type and the result is a boolean *) + assert (sv1.int_ty = sv2.int_ty); + let b = + match binop with + | E.Lt -> Z.lt sv1.V.value sv2.V.value + | E.Le -> Z.leq sv1.V.value sv2.V.value + | E.Ge -> Z.geq sv1.V.value sv2.V.value + | E.Gt -> Z.gt sv1.V.value sv2.V.value + | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd + | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq -> + raise (Failure "Unreachable") + in + Ok ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value) + | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr + -> ( + (* The two operands must have the same type and the result is an integer *) + assert (sv1.int_ty = sv2.int_ty); + let res = + match binop with + | E.Div -> + if sv2.V.value = Z.zero then Error () + else mk_scalar sv1.int_ty (Z.div sv1.V.value sv2.V.value) + | E.Rem -> + (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *) + if sv2.V.value = Z.zero then Error () + else mk_scalar sv1.int_ty (Z.rem sv1.V.value sv2.V.value) + | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.V.value sv2.V.value) + | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.V.value sv2.V.value) + | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.V.value sv2.V.value) + | E.BitXor -> raise Unimplemented + | E.BitAnd -> raise Unimplemented + | E.BitOr -> raise Unimplemented + | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq -> + raise (Failure "Unreachable") + in + match res with + | Error _ -> Error EPanic + | Ok sv -> + Ok + { + V.value = V.Concrete (V.Scalar sv); + ty = Integer sv1.int_ty; + }) + | E.Shl | E.Shr -> raise Unimplemented + | E.Ne | E.Eq -> raise (Failure "Unreachable")) + | _ -> raise (Failure "Invalid inputs for binop") + +let eval_binary_op_concrete (config : C.config) (binop : E.binop) + (op1 : E.operand) (op2 : E.operand) + (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + (* Evaluate the operands *) + let eval_ops = eval_two_operands config op1 op2 in + (* Compute the result of the binop *) + let compute cf (res : V.typed_value * V.typed_value) = + let v1, v2 = res in + cf (eval_binary_op_concrete_compute binop v1 v2) + in + (* Compose and apply *) + comp eval_ops compute cf + +let eval_binary_op_symbolic (config : C.config) (binop : E.binop) + (op1 : E.operand) (op2 : E.operand) + (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + fun ctx -> + (* Evaluate the operands *) + let eval_ops = eval_two_operands config op1 op2 in + (* Compute the result of applying the binop *) + let compute cf ((v1, v2) : V.typed_value * V.typed_value) : m_fun = + fun ctx -> + (* Generate a fresh symbolic value to store the result *) + let res_sv_id = C.fresh_symbolic_value_id () in + let res_sv_ty = + if binop = Eq || binop = Ne then ( + (* Equality operations *) + assert (v1.ty = v2.ty); + (* Equality/inequality check is primitive only for a subset of types *) + assert (ty_is_primitively_copyable v1.ty); + T.Bool) + else + (* Other operations: input types are integers *) + match (v1.V.ty, v2.V.ty) with + | T.Integer int_ty1, T.Integer int_ty2 -> ( + match binop with + | E.Lt | E.Le | E.Ge | E.Gt -> + assert (int_ty1 = int_ty2); + T.Bool + | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd + | E.BitOr -> + assert (int_ty1 = int_ty2); + T.Integer int_ty1 + | E.Shl | E.Shr -> raise Unimplemented + | E.Ne | E.Eq -> raise (Failure "Unreachable")) + | _ -> raise (Failure "Invalid inputs for binop") + in + let res_sv = + { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty } + in + (* Call the continuattion *) + let v = mk_typed_value_from_symbolic_value res_sv in + let expr = cf (Ok v) ctx in + (* Synthesize the symbolic AST *) + let p1 = S.mk_opt_place_from_op op1 ctx in + let p2 = S.mk_opt_place_from_op op2 ctx in + S.synthesize_binary_op binop v1 p1 v2 p2 res_sv None expr + in + (* Compose and apply *) + comp eval_ops compute cf ctx + +let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand) + (op2 : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun + = + match config.mode with + | C.ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf + | C.SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf + +(** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *) +let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place) + (cf : V.typed_value -> m_fun) : m_fun = + (* Note that discriminant values have type [isize] *) + (* Access the value *) + let access = Read in + let expand_prim_copy = false 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 *) + let v = value_strip_shared_loans v in + match v.V.value with + | Adt av -> ( + match av.variant_id with + | None -> + raise + (Failure + "Invalid input for `discriminant`: structure instead of enum") + | Some variant_id -> ( + let id = Z.of_int (T.VariantId.to_int variant_id) in + match mk_scalar Isize id with + | Error _ -> raise (Failure "Disciminant id out of range") + (* Should really never happen *) + | Ok sv -> + cf { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize })) + | _ -> + raise + (Failure ("Invalid input for `discriminant`: " ^ V.show_typed_value v)) + in + (* Compose and apply *) + comp prepare read cf + +(** Evaluate the discriminant of an ADT value. + + Might lead to branching, if the value is symbolic. + *) +let eval_rvalue_discriminant (config : C.config) (p : E.place) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + log#ldebug (lazy "eval_rvalue_discriminant"); + (* Note that discriminant values have type [isize] *) + (* Access the value *) + let access = Read in + let expand_prim_copy = false 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 -> + (* The value may be shared: we need to ignore the shared loans *) + let v = value_strip_shared_loans v in + match v.V.value with + | Adt _ -> eval_rvalue_discriminant_concrete config p cf ctx + | Symbolic sv -> + (* Expand the symbolic value - may lead to branching *) + let allow_branching = true in + let cc = + expand_symbolic_value config allow_branching sv + (Some (S.mk_mplace p ctx)) + in + (* This time the value is concrete: reevaluate *) + comp cc (eval_rvalue_discriminant_concrete config p) cf ctx + | _ -> + raise + (Failure ("Invalid input for `discriminant`: " ^ V.show_typed_value v)) + in + (* Compose and apply *) + comp prepare read cf ctx + +let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + match bkind with + | E.Shared | E.TwoPhaseMut -> + (* Access the value *) + let access = if bkind = E.Shared then Read else Write in + let expand_prim_copy = false 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 -> + (* Generate the fresh borrow id *) + let bid = C.fresh_borrow_id () in + (* Compute the loan value, with which to replace the value at place p *) + let nv, shared_mvalue = + match v.V.value with + | V.Loan (V.SharedLoan (bids, sv)) -> + (* Shared loan: insert the new borrow id *) + let bids1 = V.BorrowId.Set.add bid bids in + ({ v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }, sv) + | _ -> + (* Not a shared loan: add a wrapper *) + let v' = + V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) + in + ({ v with V.value = v' }, v) + in + (* Update the borrowed value in the context *) + let ctx = write_place_unwrap config access p nv ctx in + (* Compute the rvalue - simply a shared borrow with a the fresh id. + * Note that the reference is *mutable* if we do a two-phase borrow *) + let rv_ty = + T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut) + in + let bc = + if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid) + else V.InactivatedMutBorrow (shared_mvalue, bid) + in + let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in + (* Continue *) + cf rv ctx + in + (* Compose and apply *) + comp prepare eval cf ctx + | E.Mut -> + (* Access the value *) + let access = Write in + let expand_prim_copy = false 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 -> + (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) + let bid = C.fresh_borrow_id () in + let rv_ty = T.Ref (T.Erased, v.ty, Mut) in + let rv : V.typed_value = + { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } + in + (* Compute the value with which to replace the value at place p *) + let nv = { v with V.value = V.Loan (V.MutLoan bid) } in + (* Update the value in the context *) + let ctx = write_place_unwrap config access p nv ctx in + (* Continue *) + cf rv ctx + in + (* Compose and apply *) + comp prepare eval cf ctx + +let eval_rvalue_aggregate (config : C.config) + (aggregate_kind : E.aggregate_kind) (ops : E.operand list) + (cf : V.typed_value -> m_fun) : m_fun = + (* Evaluate the operands *) + let eval_ops = eval_operands config ops in + (* Compute the value *) + let compute (cf : V.typed_value -> m_fun) (values : V.typed_value list) : + m_fun = + fun ctx -> + (* Match on the aggregate kind *) + match aggregate_kind with + | E.AggregatedTuple -> + let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in + let v = V.Adt { variant_id = None; field_values = values } in + let ty = T.Adt (T.Tuple, [], tys) in + let aggregated : V.typed_value = { V.value = v; ty } in + (* Call the continuation *) + cf aggregated ctx + | E.AggregatedOption (variant_id, ty) -> + (* Sanity check *) + if variant_id == T.option_none_id then assert (values == []) + else if variant_id == T.option_some_id then + assert (List.length values == 1) + else raise (Failure "Unreachable"); + (* Construt the value *) + let aty = T.Adt (T.Assumed T.Option, [], [ ty ]) in + let av : V.adt_value = + { V.variant_id = Some variant_id; V.field_values = values } + in + let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in + (* Call the continuation *) + cf aggregated ctx + | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> + (* Sanity checks *) + let type_decl = C.ctx_lookup_type_decl ctx def_id in + assert (List.length type_decl.region_params = List.length regions); + let expected_field_types = + Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id + types + in + assert ( + expected_field_types + = List.map (fun (v : V.typed_value) -> v.V.ty) values); + (* Construct the value *) + let av : V.adt_value = + { V.variant_id = opt_variant_id; V.field_values = values } + in + let aty = T.Adt (T.AdtId def_id, regions, types) in + let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in + (* Call the continuation *) + cf aggregated ctx + in + (* Compose and apply *) + comp eval_ops compute cf + +(** Evaluate an rvalue. + + Transmits the computed rvalue to the received continuation. + *) +let eval_rvalue (config : C.config) (rvalue : E.rvalue) + (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + fun ctx -> + log#ldebug (lazy "eval_rvalue"); + (* Small helpers *) + let wrap_in_result (cf : (V.typed_value, eval_error) result -> m_fun) + (v : V.typed_value) : m_fun = + cf (Ok v) + in + let comp_wrap f = comp f wrap_in_result cf in + (* Delegate to the proper auxiliary function *) + match rvalue with + | E.Use op -> comp_wrap (eval_operand config op) ctx + | E.Ref (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx + | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx + | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx + | 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 |