diff options
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 579 |
1 files changed, 301 insertions, 278 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 469bebec..ac6c9ede 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -1,24 +1,20 @@ -module T = Types -module PV = PrimitiveValues -module V = Values -module LA = LlbcAst +open Types +open Values +open LlbcAst open Scalars -module E = Expressions +open Expressions open Utils -module C = Contexts -module Subst = Substitute -module L = Logging +open Contexts open TypesUtils open ValuesUtils -module Inv = Invariants -module S = SynthesizeSymbolic +open SynthesizeSymbolic open Cps open InterpreterUtils open InterpreterExpansion open InterpreterPaths (** The local logger *) -let log = L.expressions_log +let log = Logging.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. @@ -28,8 +24,8 @@ let log = L.expressions_log 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 = +let expand_primitively_copyable_at_place (config : config) + (access : access_kind) (p : place) : cm_fun = fun cf ctx -> (* Small helper *) let rec expand : cm_fun = @@ -42,8 +38,7 @@ let expand_primitively_copyable_at_place (config : C.config) | None -> cf ctx | Some sv -> let cc = - expand_symbolic_value_no_branching config sv - (Some (S.mk_mplace p ctx)) + expand_symbolic_value_no_branching config sv (Some (mk_mplace p ctx)) in comp cc expand cf ctx in @@ -55,8 +50,8 @@ let expand_primitively_copyable_at_place (config : C.config) We also check that the value *doesn't contain bottoms or reserved borrows*. *) -let read_place (access : access_kind) (p : E.place) - (cf : V.typed_value -> m_fun) : m_fun = +let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) : + m_fun = fun ctx -> let v = read_place access p ctx in (* Check that there are no bottoms in the value *) @@ -66,9 +61,9 @@ let read_place (access : access_kind) (p : E.place) (* Call the continuation *) cf v ctx -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 = +let access_rplace_reorganize_and_read (config : config) + (expand_prim_copy : bool) (access : access_kind) (p : place) + (cf : 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 @@ -86,31 +81,30 @@ let access_rplace_reorganize_and_read (config : C.config) (* 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 = +let access_rplace_reorganize (config : config) (expand_prim_copy : bool) + (access : access_kind) (p : 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 literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) : - V.typed_value = +let literal_to_typed_value (ty : literal_type) (cv : literal) : typed_value = (* Check the type while converting - we actually need some information * contained in the type *) log#ldebug (lazy ("literal_to_typed_value:" ^ "\n- cv: " - ^ Print.PrimitiveValues.literal_to_string cv)); + ^ Print.Values.literal_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) - | PV.Bool, Bool v -> { V.value = V.Literal (Bool v); ty = T.Literal ty } - | Char, Char v -> { V.value = V.Literal (Char v); ty = T.Literal ty } - | Integer int_ty, PV.Scalar v -> + | TBool, VBool v -> { value = VLiteral (VBool v); ty = TLiteral ty } + | TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty } + | TInteger int_ty, VScalar v -> (* Check the type and the ranges *) assert (int_ty = v.int_ty); assert (check_scalar_value_in_range v); - { V.value = V.Literal (PV.Scalar v); ty = T.Literal ty } + { value = VLiteral (VScalar v); ty = TLiteral ty } (* Remaining cases (invalid) *) | _, _ -> raise (Failure "Improperly typed constant value") @@ -125,8 +119,8 @@ let literal_to_typed_value (ty : PV.literal_type) (cv : V.literal) : parameter to control this copy ([allow_adt_copy]). Note that here by ADT we mean the user-defined ADTs (not tuples or assumed types). *) -let rec copy_value (allow_adt_copy : bool) (config : C.config) - (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value = +let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx) + (v : typed_value) : eval_ctx * typed_value = log#ldebug (lazy ("copy_value: " @@ -136,16 +130,24 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) * we reverted the changes: the result was less clear actually. In particular, * the fact that we have exhaustive matches below makes very obvious the cases * in which we need to fail *) - match v.V.value with - | V.Literal _ -> (ctx, v) - | V.Adt av -> + match v.value with + | VLiteral _ -> (ctx, v) + | VAdt av -> (* Sanity check *) - (match v.V.ty with - | T.Adt (T.Assumed (T.Box | Vec), _, _, _) -> + (match v.ty with + | TAdt (TAssumed TBox, _) -> raise (Failure "Can't copy an assumed value other than Option") - | T.Adt (T.AdtId _, _, _, _) -> assert allow_adt_copy - | T.Adt ((T.Assumed Option | T.Tuple), _, _, _) -> () (* Ok *) - | T.Adt (T.Assumed (Slice | T.Array), [], [ ty ], []) -> + | TAdt (TAdtId _, _) as ty -> + assert (allow_adt_copy || ty_is_primitively_copyable ty) + | TAdt (TTuple, _) -> () (* Ok *) + | TAdt + ( TAssumed (TSlice | TArray), + { + regions = []; + types = [ ty ]; + const_generics = []; + trait_refs = []; + } ) -> assert (ty_is_primitively_copyable ty) | _ -> raise (Failure "Unreachable")); let ctx, fields = @@ -153,33 +155,33 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) (copy_value allow_adt_copy config) ctx av.field_values in - (ctx, { v with V.value = V.Adt { av with field_values = fields } }) - | V.Bottom -> raise (Failure "Can't copy ⊥") - | V.Borrow bc -> ( + (ctx, { v with value = VAdt { av with field_values = fields } }) + | VBottom -> raise (Failure "Can't copy ⊥") + | VBorrow bc -> ( (* We can only copy shared borrows *) match bc with - | SharedBorrow bid -> + | VSharedBorrow bid -> (* We need to create a new borrow id for the copied borrow, and * update the context accordingly *) - let bid' = C.fresh_borrow_id () in + let bid' = fresh_borrow_id () in let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in - (ctx, { v with V.value = V.Borrow (SharedBorrow bid') }) - | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") - | V.ReservedMutBorrow _ -> + (ctx, { v with value = VBorrow (VSharedBorrow bid') }) + | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") + | VReservedMutBorrow _ -> raise (Failure "Can't copy a reserved mut borrow")) - | V.Loan lc -> ( + | VLoan lc -> ( (* We can only copy shared loans *) match lc with - | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan") - | V.SharedLoan (_, sv) -> + | VMutLoan _ -> raise (Failure "Can't copy a mutable loan") + | VSharedLoan (_, sv) -> (* We don't copy the shared loan: only the shared value inside *) copy_value allow_adt_copy config ctx sv) - | V.Symbolic sp -> + | VSymbolic sp -> (* We can copy only if the type is "primitively" copyable. * Note that in the general case, copy is a trait: copying values * thus requires calling the proper function. Here, we copy values * for very simple types such as integers, shared borrows, etc. *) - assert (ty_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty)); + assert (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)); (* If the type is copyable, we simply return the current value. Side * remark: what is important to look at when copying symbolic values * is symbolic expansion. The important subcase is the expansion of shared @@ -224,23 +226,21 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) what we do in the formalization (because we don't enforce the same constraints as MIR in the formalization). *) -let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : - cm_fun = +let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun = fun cf ctx -> let prepare : cm_fun = fun cf ctx -> match op with - | Expressions.Constant (ty, cv) -> + | Constant _ -> (* No need to reorganize the context *) - literal_to_typed_value (TypesUtils.ty_as_literal ty) cv |> ignore; cf ctx - | Expressions.Copy p -> + | 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 -> + | Move p -> (* Access the value *) let access = Move in let expand_prim_copy = false in @@ -250,8 +250,8 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : 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 = +let eval_operand_no_reorganize (config : config) (op : operand) + (cf : typed_value -> m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug @@ -260,9 +260,70 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with - | Expressions.Constant (ty, cv) -> - cf (literal_to_typed_value (TypesUtils.ty_as_literal ty) cv) ctx - | Expressions.Copy p -> + | Constant cv -> ( + match cv.value with + | CLiteral lit -> + cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx + | CTraitConst (trait_ref, generics, const_name) -> ( + assert (generics = empty_generic_args); + match trait_ref.trait_id with + | TraitImpl _ -> + (* This shouldn't happen: if we refer to a concrete implementation, we + should directly refer to the top-level constant *) + raise (Failure "Unreachable") + | _ -> ( + (* We refer to a constant defined in a local clause: simply + introduce a fresh symbolic value *) + let ctx0 = ctx in + (* Lookup the trait declaration to retrieve the type of the symbolic value *) + let trait_decl = + ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id + in + let _, (ty, _) = + List.find (fun (name, _) -> name = const_name) trait_decl.consts + in + (* Introduce a fresh symbolic value *) + let v = mk_fresh_symbolic_typed_value TraitConst ty in + (* Continue the evaluation *) + let e = cf v ctx in + (* We have to wrap the generated expression *) + match e with + | None -> None + | Some e -> + Some + (SymbolicAst.IntroSymbolic + ( ctx0, + None, + value_as_symbolic v.value, + SymbolicAst.VaTraitConstValue + (trait_ref, generics, const_name), + e )))) + | CVar vid -> ( + let ctx0 = ctx in + (* Lookup the const generic value *) + let cv = ctx_lookup_const_generic_value ctx vid in + (* Copy the value *) + let allow_adt_copy = false in + let ctx, v = copy_value allow_adt_copy config ctx cv in + (* Continue *) + let e = cf v ctx in + (* We have to wrap the generated expression *) + match e with + | None -> None + | Some e -> + (* If we are synthesizing a symbolic AST, it means that we are in symbolic + mode: the value of the const generic is necessarily symbolic. *) + assert (is_symbolic cv.value); + (* *) + Some + (SymbolicAst.IntroSymbolic + ( ctx0, + None, + value_as_symbolic v.value, + SymbolicAst.VaCgValue vid, + e ))) + | CFnPtr _ -> raise (Failure "TODO")) + | Copy p -> (* Access the value *) let access = Read in let cc = read_place access p in @@ -283,7 +344,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) in (* Compose and apply *) comp cc copy cf ctx - | Expressions.Move p -> + | Move p -> (* Access the value *) let access = Move in let cc = read_place access p in @@ -292,15 +353,15 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) 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 + let bottom : typed_value = { value = VBottom; ty = v.ty } in let ctx = write_place access p bottom ctx in cf v ctx in (* Compose and apply *) comp cc move cf ctx -let eval_operand (config : C.config) (op : E.operand) - (cf : V.typed_value -> m_fun) : m_fun = +let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) : + m_fun = fun ctx -> (* Debug *) log#ldebug @@ -317,13 +378,13 @@ let eval_operand (config : C.config) (op : E.operand) See [prepare_eval_operand_reorganize]. *) -let prepare_eval_operands_reorganize (config : C.config) (ops : E.operand list) - : cm_fun = +let prepare_eval_operands_reorganize (config : config) (ops : 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 = +let eval_operands (config : config) (ops : operand list) + (cf : typed_value list -> m_fun) : m_fun = fun ctx -> (* Prepare the operands *) let prepare = prepare_eval_operands_reorganize config ops in @@ -334,8 +395,8 @@ let eval_operands (config : C.config) (ops : E.operand list) (* 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_two_operands (config : config) (op1 : operand) (op2 : operand) + (cf : typed_value * typed_value -> m_fun) : m_fun = let eval_op = eval_operands config [ op1; op2 ] in let use_res cf res = match res with @@ -344,73 +405,73 @@ let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand) 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 = +let eval_unary_op_concrete (config : config) (unop : unop) (op : operand) + (cf : (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.Literal (Bool b) -> - cf (Ok { v with V.value = V.Literal (Bool (not b)) }) - | E.Neg, V.Literal (PV.Scalar sv) -> ( - let i = Z.neg sv.PV.value in + let apply cf (v : typed_value) : m_fun = + match (unop, v.value) with + | Not, VLiteral (VBool b) -> + cf (Ok { v with value = VLiteral (VBool (not b)) }) + | Neg, VLiteral (VScalar sv) -> ( + let i = Z.neg sv.value in match mk_scalar sv.int_ty i with | Error _ -> cf (Error EPanic) - | Ok sv -> cf (Ok { v with V.value = V.Literal (PV.Scalar sv) })) - | E.Cast (src_ty, tgt_ty), V.Literal (PV.Scalar sv) -> ( + | Ok sv -> cf (Ok { v with value = VLiteral (VScalar sv) })) + | Cast (CastInteger (src_ty, tgt_ty)), VLiteral (VScalar sv) -> ( assert (src_ty = sv.int_ty); - let i = sv.PV.value in + let i = sv.value in match mk_scalar tgt_ty i with | Error _ -> cf (Error EPanic) | Ok sv -> - let ty = T.Literal (Integer tgt_ty) in - let value = V.Literal (PV.Scalar sv) in - cf (Ok { V.ty; value })) + let ty = TLiteral (TInteger tgt_ty) in + let value = VLiteral (VScalar sv) in + cf (Ok { 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 = +let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand) + (cf : (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 = + let apply cf (v : typed_value) : m_fun = fun ctx -> - let res_sv_id = C.fresh_symbolic_value_id () in + let res_sv_id = fresh_symbolic_value_id () in let res_sv_ty = - match (unop, v.V.ty) with - | E.Not, (T.Literal Bool as lty) -> lty - | E.Neg, (T.Literal (Integer _) as lty) -> lty - | E.Cast (_, tgt_ty), _ -> T.Literal (Integer tgt_ty) + match (unop, v.ty) with + | Not, (TLiteral TBool as lty) -> lty + | Neg, (TLiteral (TInteger _) as lty) -> lty + | Cast (CastInteger (_, tgt_ty)), _ -> TLiteral (TInteger 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 } + { sv_kind = FunCallRet; 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 ctx unop v - (S.mk_opt_place_from_op op ctx) + synthesize_unary_op ctx unop v + (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 = +let eval_unary_op (config : config) (unop : unop) (op : operand) + (cf : (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 + | ConcreteMode -> eval_unary_op_concrete config unop op cf + | 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 = +let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value) + (v2 : typed_value) : (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 ( @@ -419,53 +480,52 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) (* 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.Literal (Bool b); ty = T.Literal Bool }) + Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) else (* For the non-equality operations, the input values are necessarily scalars *) - match (v1.V.value, v2.V.value) with - | V.Literal (PV.Scalar sv1), V.Literal (PV.Scalar sv2) -> ( + match (v1.value, v2.value) with + | VLiteral (VScalar sv1), VLiteral (VScalar 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 -> + | Lt | Le | Ge | 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.PV.value sv2.PV.value - | E.Le -> Z.leq sv1.PV.value sv2.PV.value - | E.Ge -> Z.geq sv1.PV.value sv2.PV.value - | E.Gt -> Z.gt sv1.PV.value sv2.PV.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 -> + | Lt -> Z.lt sv1.value sv2.value + | Le -> Z.leq sv1.value sv2.value + | Ge -> Z.geq sv1.value sv2.value + | Gt -> Z.gt sv1.value sv2.value + | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl + | Shr | Ne | Eq -> raise (Failure "Unreachable") in Ok - ({ V.value = V.Literal (Bool b); ty = T.Literal Bool } - : V.typed_value) - | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr - -> ( + ({ value = VLiteral (VBool b); ty = TLiteral TBool } + : typed_value) + | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | 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.PV.value = Z.zero then Error () - else mk_scalar sv1.int_ty (Z.div sv1.PV.value sv2.PV.value) - | E.Rem -> + | Div -> + if sv2.value = Z.zero then Error () + else mk_scalar sv1.int_ty (Z.div sv1.value sv2.value) + | Rem -> (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *) - if sv2.PV.value = Z.zero then Error () - else mk_scalar sv1.int_ty (Z.rem sv1.PV.value sv2.PV.value) - | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.PV.value sv2.PV.value) - | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.PV.value sv2.PV.value) - | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.PV.value sv2.PV.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 -> + if sv2.value = Z.zero then Error () + else mk_scalar sv1.int_ty (Z.rem sv1.value sv2.value) + | Add -> mk_scalar sv1.int_ty (Z.add sv1.value sv2.value) + | Sub -> mk_scalar sv1.int_ty (Z.sub sv1.value sv2.value) + | Mul -> mk_scalar sv1.int_ty (Z.mul sv1.value sv2.value) + | BitXor -> raise Unimplemented + | BitAnd -> raise Unimplemented + | BitOr -> raise Unimplemented + | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq -> raise (Failure "Unreachable") in match res with @@ -473,100 +533,96 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value) | Ok sv -> Ok { - V.value = V.Literal (PV.Scalar sv); - ty = T.Literal (Integer sv1.int_ty); + value = VLiteral (VScalar sv); + ty = TLiteral (TInteger sv1.int_ty); }) - | E.Shl | E.Shr -> raise Unimplemented - | E.Ne | E.Eq -> raise (Failure "Unreachable")) + | Shl | Shr -> raise Unimplemented + | Ne | 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 = +let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand) + (op2 : operand) (cf : (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 compute cf (res : typed_value * 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 = +let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand) + (op2 : operand) (cf : (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 = + let compute cf ((v1, v2) : typed_value * 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_id = 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.Literal Bool) + TLiteral TBool) else (* Other operations: input types are integers *) - match (v1.V.ty, v2.V.ty) with - | T.Literal (Integer int_ty1), T.Literal (Integer int_ty2) -> ( + match (v1.ty, v2.ty) with + | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> ( match binop with - | E.Lt | E.Le | E.Ge | E.Gt -> + | Lt | Le | Ge | Gt -> assert (int_ty1 = int_ty2); - T.Literal Bool - | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd - | E.BitOr -> + TLiteral TBool + | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> assert (int_ty1 = int_ty2); - T.Literal (Integer int_ty1) - | E.Shl | E.Shr -> + TLiteral (TInteger int_ty1) + | Shl | Shr -> (* The number of bits can be of a different integer type than the operand *) - T.Literal (Integer int_ty1) - | E.Ne | E.Eq -> raise (Failure "Unreachable")) + TLiteral (TInteger int_ty1) + | Ne | 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 } + { sv_kind = FunCallRet; 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 ctx binop v1 p1 v2 p2 res_sv None expr + let p1 = mk_opt_place_from_op op1 ctx in + let p2 = mk_opt_place_from_op op2 ctx in + synthesize_binary_op ctx 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 - = +let eval_binary_op (config : config) (binop : binop) (op1 : operand) + (op2 : operand) (cf : (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 + | ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf + | SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf -let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) - (cf : V.typed_value -> m_fun) : m_fun = +let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind) + (cf : typed_value -> m_fun) : m_fun = fun ctx -> match bkind with - | E.Shared | E.TwoPhaseMut | E.Shallow -> + | BShared | BTwoPhaseMut | BShallow -> (* **REMARK**: we initially treated shallow borrows like shared borrows. In practice this restricted the behaviour too much, so for now we forbid them. *) - assert (bkind <> E.Shallow); + assert (bkind <> BShallow); (* Access the value *) let access = match bkind with - | E.Shared | E.Shallow -> Read - | E.TwoPhaseMut -> Write + | BShared | BShallow -> Read + | BTwoPhaseMut -> Write | _ -> raise (Failure "Unreachable") in @@ -575,23 +631,21 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) 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 = + let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun = fun ctx -> (* Generate the fresh borrow id *) - let bid = C.fresh_borrow_id () in + let bid = fresh_borrow_id () in (* Compute the loan value, with which to replace the value at place p *) let nv = - match v.V.value with - | V.Loan (V.SharedLoan (bids, sv)) -> + match v.value with + | VLoan (VSharedLoan (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)) } + let bids1 = BorrowId.Set.add bid bids in + { v with value = VLoan (VSharedLoan (bids1, 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' } + let v' = VLoan (VSharedLoan (BorrowId.Set.singleton bid, v)) in + { v with value = v' } in (* Update the borrowed value in the context *) let ctx = write_place access p nv ctx in @@ -599,27 +653,27 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) * Note that the reference is *mutable* if we do a two-phase borrow *) let ref_kind = match bkind with - | E.Shared | E.Shallow -> T.Shared - | E.TwoPhaseMut -> T.Mut + | BShared | BShallow -> RShared + | BTwoPhaseMut -> RMut | _ -> raise (Failure "Unreachable") in - let rv_ty = T.Ref (T.Erased, v.ty, ref_kind) in + let rv_ty = TRef (RErased, v.ty, ref_kind) in let bc = match bkind with - | E.Shared | E.Shallow -> + | BShared | BShallow -> (* See the remark at the beginning of the match branch: we handle shallow borrows like shared borrows *) - V.SharedBorrow bid - | E.TwoPhaseMut -> V.ReservedMutBorrow bid + VSharedBorrow bid + | BTwoPhaseMut -> VReservedMutBorrow bid | _ -> raise (Failure "Unreachable") in - let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in + let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in (* Continue *) cf rv ctx in (* Compose and apply *) comp prepare eval cf ctx - | E.Mut -> + | BMut -> (* Access the value *) let access = Write in let expand_prim_copy = false in @@ -627,16 +681,16 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) 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 = + let eval (cf : typed_value -> m_fun) (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 } + let bid = fresh_borrow_id () in + let rv_ty = TRef (RErased, v.ty, RMut) in + let rv : typed_value = + { value = VBorrow (VMutBorrow (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 + let nv = { v with value = VLoan (VMutLoan bid) } in (* Update the value in the context *) let ctx = write_place access p nv ctx in (* Continue *) @@ -645,129 +699,98 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* 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 = +let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind) + (ops : operand list) (cf : 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 = + let compute (cf : typed_value -> m_fun) (values : 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, cgs) -> - (* 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 cgs - 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, cgs) in - let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in - (* Call the continuation *) - cf aggregated ctx - | E.AggregatedRange ety -> - (* There should be two fields exactly *) - let v0, v1 = - match values with - | [ v0; v1 ] -> (v0, v1) - | _ -> raise (Failure "Unreachable") - in - (* Ranges are parametric over the type of indices. For now we only - support scalars, which can be of any type *) - assert (literal_type_is_integer (ty_as_literal ety)); - assert (v0.ty = ety); - assert (v1.ty = ety); - (* Construct the value *) - let av : V.adt_value = - { V.variant_id = None; V.field_values = values } - in - let aty = T.Adt (T.Assumed T.Range, [], [ ety ], []) in - let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in - (* Call the continuation *) - cf aggregated ctx - | E.AggregatedArray (ety, cg) -> ( + | AggregatedAdt (type_id, opt_variant_id, generics) -> ( + match type_id with + | TTuple -> + let tys = List.map (fun (v : typed_value) -> v.ty) values in + let v = VAdt { variant_id = None; field_values = values } in + let generics = mk_generic_args [] tys [] [] in + let ty = TAdt (TTuple, generics) in + let aggregated : typed_value = { value = v; ty } in + (* Call the continuation *) + cf aggregated ctx + | TAdtId def_id -> + (* Sanity checks *) + let type_decl = ctx_lookup_type_decl ctx def_id in + assert ( + List.length type_decl.generics.regions + = List.length generics.regions); + let expected_field_types = + AssociatedTypes.ctx_adt_get_inst_norm_field_etypes ctx def_id + opt_variant_id generics + in + assert ( + expected_field_types + = List.map (fun (v : typed_value) -> v.ty) values); + (* Construct the value *) + let av : adt_value = + { variant_id = opt_variant_id; field_values = values } + in + let aty = TAdt (TAdtId def_id, generics) in + let aggregated : typed_value = { value = VAdt av; ty = aty } in + (* Call the continuation *) + cf aggregated ctx + | TAssumed _ -> raise (Failure "Unreachable")) + | AggregatedArray (ety, cg) -> ( (* Sanity check: all the values have the proper type *) - assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values); + assert (List.for_all (fun (v : typed_value) -> v.ty = ety) values); (* Sanity check: the number of values is consistent with the length *) let len = (literal_as_scalar (const_generic_as_literal cg)).value in assert (len = Z.of_int (List.length values)); - let ty = T.Adt (T.Assumed T.Array, [], [ ety ], [ cg ]) in + let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in + let ty = TAdt (TAssumed TArray, generics) in (* In order to generate a better AST, we introduce a symbolic value equal to the array. The reason is that otherwise, the array we introduce here might be duplicated in the generated code: by introducing a symbolic value we introduce a let-binding in the generated code. *) - let saggregated = - mk_fresh_symbolic_typed_value_from_ety V.Aggregate ty - in + let saggregated = mk_fresh_symbolic_typed_value Aggregate ty in (* Call the continuation *) match cf saggregated ctx with | None -> None | Some e -> (* Introduce the symbolic value in the AST *) let sv = ValuesUtils.value_as_symbolic saggregated.value in - Some (SymbolicAst.IntroSymbolic (ctx, None, sv, Array values, e))) + Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))) in (* Compose and apply *) comp eval_ops compute cf -let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue) - (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = +let eval_rvalue_not_global (config : config) (rvalue : rvalue) + (cf : (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 = + let wrap_in_result (cf : (typed_value, eval_error) result -> m_fun) + (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) -> + | Use op -> comp_wrap (eval_operand config op) ctx + | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx + | UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx + | BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx + | Aggregate (aggregate_kind, ops) -> comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx - | E.Discriminant _ -> + | Discriminant _ -> raise (Failure "Unreachable: discriminant reads should have been eliminated from \ the AST") - | E.Global _ -> raise (Failure "Unreachable") + | Global _ -> raise (Failure "Unreachable") -let eval_fake_read (config : C.config) (p : E.place) : cm_fun = +let eval_fake_read (config : config) (p : place) : cm_fun = fun cf ctx -> let expand_prim_copy = false in let cf_prepare cf = |