diff options
| -rw-r--r-- | src/Interpreter.ml | 438 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 476 |
2 files changed, 477 insertions, 437 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 4ca7d58f..73967f61 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -17,6 +17,7 @@ open InterpreterProjectors open InterpreterBorrows open InterpreterExpansion open InterpreterPaths +open InterpreterExpressions (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -33,443 +34,6 @@ open InterpreterPaths (* TODO: remove the config parameters when they are useless *) -(** TODO: change the name *) -type eval_error = Panic - -type 'a eval_result = ('a, eval_error) result - -(** Convert a constant operand value to a typed value *) -let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) - (cv : E.operand_constant_value) : V.typed_value = - (* Check the type while converting *) - match (ty, cv) with - (* Unit *) - | T.Adt (T.Tuple, [], []), Unit -> mk_unit_value - (* Adt with one variant and no fields *) - | T.Adt (T.AdtId def_id, [], []), ConstantAdt def_id' -> - assert (def_id = def_id'); - (* Check that the adt definition only has one variant with no fields, - compute the variant id at the same time. *) - let def = C.ctx_lookup_type_def ctx def_id in - assert (List.length def.region_params = 0); - assert (List.length def.type_params = 0); - let variant_id = - match def.kind with - | Struct fields -> - assert (List.length fields = 0); - None - | Enum variants -> - assert (List.length variants = 1); - let variant_id = T.VariantId.zero in - let variant = T.VariantId.nth variants variant_id in - assert (List.length variant.fields = 0); - Some variant_id - in - let value = V.Adt { variant_id; field_values = [] } in - { value; ty } - (* Scalar, boolean... *) - | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty } - | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty } - | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty } - | T.Integer int_ty, ConstantValue (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) - listing as much as we can on purpose - (allows to catch errors at compilation if the definitions change) *) - | _, Unit | _, ConstantAdt _ | _, ConstantValue _ -> - failwith "Improperly typed constant value" - -(** Small utility *) -let prepare_rplace (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - let ctx = update_ctx_along_read_place config access p ctx in - let ctx = end_loans_at_place config access p ctx in - let v = read_place_unwrap config access p ctx in - (ctx, v) - -(** Prepare the evaluation of an operand. *) -let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand) - : C.eval_ctx * V.typed_value = - let ctx, v = - match op with - | Expressions.Constant (ty, cv) -> - let v = constant_value_to_typed_value ctx ty cv in - (ctx, v) - | Expressions.Copy p -> - (* Access the value *) - let access = Read in - prepare_rplace config access p ctx - | Expressions.Move p -> - (* Access the value *) - let access = Move in - prepare_rplace config access p ctx - in - assert (not (bottom_in_value v)); - (ctx, v) - -(** Evaluate an operand. *) -let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : - C.eval_ctx * V.typed_value = - (* Debug *) - L.log#ldebug - (lazy - ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n" - ^ operand_to_string ctx op ^ "\n")); - (* Evaluate *) - match op with - | Expressions.Constant (ty, cv) -> - let v = constant_value_to_typed_value ctx ty cv in - (ctx, v) - | Expressions.Copy p -> - (* Access the value *) - let access = Read in - let ctx, v = prepare_rplace config access p ctx in - (* Copy the value *) - L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v)); - assert (not (bottom_in_value v)); - let allow_adt_copy = false in - copy_value allow_adt_copy config ctx v - | Expressions.Move p -> ( - (* Access the value *) - let access = Move in - let ctx, v = prepare_rplace config access p ctx in - (* Move the value *) - L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v)); - assert (not (bottom_in_value 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 -> (ctx, v)) - -(** Evaluate several operands. *) -let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list) - : C.eval_ctx * V.typed_value list = - List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops - -let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand) - (op2 : E.operand) : C.eval_ctx * V.typed_value * V.typed_value = - match eval_operands config ctx [ op1; op2 ] with - | ctx, [ v1; v2 ] -> (ctx, v1, v2) - | _ -> failwith "Unreachable" - -let eval_unary_op_concrete (config : C.config) (ctx : C.eval_ctx) - (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result - = - (* Evaluate the operand *) - let ctx, v = eval_operand config ctx op in - (* Apply the unop *) - match (unop, v.V.value) with - | E.Not, V.Concrete (Bool b) -> - Ok (ctx, { 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 _ -> Error Panic - | Ok sv -> Ok (ctx, { v with V.value = V.Concrete (V.Scalar sv) })) - | _ -> failwith "Invalid input for unop" - -let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx) - (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result - = - (* Evaluate the operand *) - let ctx, v = eval_operand config ctx op in - (* Generate a fresh symbolic value to store the result *) - let ctx, res_sv_id = C.fresh_symbolic_value_id ctx 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 - | _ -> failwith "Invalid input for unop" - in - let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in - (* Synthesize *) - S.synthesize_unary_op unop v res_sv; - (* Return *) - Ok (ctx, mk_typed_value_from_symbolic_value res_sv) - -let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : E.unop) - (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result = - match config.mode with - | C.ConcreteMode -> eval_unary_op_concrete config ctx unop op - | C.SymbolicMode -> eval_unary_op_symbolic config ctx unop op - -let eval_binary_op_concrete (config : C.config) (ctx : C.eval_ctx) - (binop : E.binop) (op1 : E.operand) (op2 : E.operand) : - (C.eval_ctx * V.typed_value) eval_result = - (* Evaluate the operands *) - let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in - (* 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 (type_is_primitively_copyable v1.ty); - let b = v1 = v2 in - Ok (ctx, { 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) -> ( - let res = - (* 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 -> - failwith "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 -> - failwith "Unreachable" - in - match res with - | Error err -> Error err - | 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 -> failwith "Unreachable" - in - match res with Error _ -> Error Panic | Ok v -> Ok (ctx, v)) - | _ -> failwith "Invalid inputs for binop" - -let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx) - (binop : E.binop) (op1 : E.operand) (op2 : E.operand) : - (C.eval_ctx * V.typed_value) eval_result = - (* Evaluate the operands *) - let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in - (* Generate a fresh symbolic value to store the result *) - let ctx, res_sv_id = C.fresh_symbolic_value_id ctx 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 (type_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 -> failwith "Unreachable") - | _ -> failwith "Invalid inputs for binop" - in - let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in - (* Synthesize *) - S.synthesize_binary_op binop v1 v2 res_sv; - (* Return *) - Ok (ctx, mk_typed_value_from_symbolic_value res_sv) - -let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop) - (op1 : E.operand) (op2 : E.operand) : - (C.eval_ctx * V.typed_value) eval_result = - match config.mode with - | C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2 - | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2 - -(** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *) -let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - (* Note that discriminant values have type `isize` *) - (* Access the value *) - let access = Read in - let ctx, v = prepare_rplace config access p ctx in - match v.V.value with - | Adt av -> ( - match av.variant_id with - | None -> - failwith "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 _ -> - failwith "Disciminant id out of range" - (* Should really never happen *) - | Ok sv -> - (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize })) - ) - | _ -> failwith "Invalid input for `discriminant`" - -let eval_rvalue_discriminant (config : C.config) (p : E.place) - (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list = - S.synthesize_eval_rvalue_discriminant p; - (* Note that discriminant values have type `isize` *) - (* Access the value *) - let access = Read in - let ctx, v = prepare_rplace config access p ctx in - match v.V.value with - | Adt _ -> [ eval_rvalue_discriminant_concrete config p ctx ] - | Symbolic sv -> - (* Expand the symbolic value - may lead to branching *) - let ctxl = expand_symbolic_enum_value config sv ctx in - (* This time the value is concrete: reevaluate *) - List.map (eval_rvalue_discriminant_concrete config p) ctxl - | _ -> failwith "Invalid input for `discriminant`" - -let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place) - (bkind : E.borrow_kind) : C.eval_ctx * V.typed_value = - S.synthesize_eval_rvalue_ref p bkind; - match bkind with - | E.Shared | E.TwoPhaseMut -> - (* Access the value *) - let access = if bkind = E.Shared then Read else Write in - let ctx, v = prepare_rplace config access p ctx in - (* Compute the rvalue - simply a shared borrow with a fresh id *) - let ctx, bid = C.fresh_borrow_id ctx in - (* 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 bid - else V.InactivatedMutBorrow bid - in - let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in - (* Compute the value with which to replace the value at place p *) - let nv = - 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)) } - | _ -> - (* 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' } - in - (* Update the value in the context *) - let ctx = write_place_unwrap config access p nv ctx in - (* Return *) - (ctx, rv) - | E.Mut -> - (* Access the value *) - let access = Write in - let ctx, v = prepare_rplace config access p ctx in - (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) - let ctx, bid = C.fresh_borrow_id ctx 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 - (* Return *) - (ctx, rv) - -let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx) - (aggregate_kind : E.aggregate_kind) (ops : E.operand list) : - C.eval_ctx * V.typed_value = - S.synthesize_eval_rvalue_aggregate aggregate_kind ops; - (* Evaluate the operands *) - let ctx, values = eval_operands config ctx ops in - (* 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 - (ctx, { V.value = v; ty }) - | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> - (* Sanity checks *) - let type_def = C.ctx_lookup_type_def ctx def_id in - assert (List.length type_def.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 - (ctx, { V.value = Adt av; ty = aty }) - -(** Evaluate an rvalue which is not a discriminant. - - We define a function for this specific case, because evaluating - a discriminant might lead to branching (if we evaluate the discriminant - of a symbolic enumeration value), while it is not the case for the - other rvalues. - *) -let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx) - (rvalue : E.rvalue) : (C.eval_ctx * V.typed_value) eval_result = - match rvalue with - | E.Use op -> Ok (eval_operand config ctx op) - | E.Ref (p, bkind) -> Ok (eval_rvalue_ref config ctx p bkind) - | E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op - | E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2 - | E.Aggregate (aggregate_kind, ops) -> - Ok (eval_rvalue_aggregate config ctx aggregate_kind ops) - | E.Discriminant _ -> failwith "Unreachable" - -(** Evaluate an rvalue in a given context: return the updated context and - the computed value. - - Returns a list of pairs (new context, computed rvalue) because - `discriminant` might lead to a branching in case it is applied - on a symbolic enumeration value. -*) -let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : - (C.eval_ctx * V.typed_value) list eval_result = - match rvalue with - | E.Discriminant p -> Ok (eval_rvalue_discriminant config p ctx) - | _ -> ( - match eval_rvalue_non_discriminant config ctx rvalue with - | Error e -> Error e - | Ok res -> Ok [ res ]) - (** Result of evaluating a statement *) type statement_eval_res = Unit | Break of int | Continue of int | Return diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml new file mode 100644 index 00000000..41eda802 --- /dev/null +++ b/src/InterpreterExpressions.ml @@ -0,0 +1,476 @@ +module T = Types +module V = Values +open Scalars +module E = Expressions +open Errors +module C = Contexts +module Subst = Substitute +module A = CfimAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = Synthesis +open Utils +open InterpreterUtils +open InterpreterProjectors +open InterpreterBorrows +open InterpreterExpansion +open InterpreterPaths + +(** TODO: change the name *) +type eval_error = Panic + +type 'a eval_result = ('a, eval_error) result + +(** Convert a constant operand value to a typed value *) +let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) + (cv : E.operand_constant_value) : V.typed_value = + (* Check the type while converting *) + match (ty, cv) with + (* Unit *) + | T.Adt (T.Tuple, [], []), Unit -> mk_unit_value + (* Adt with one variant and no fields *) + | T.Adt (T.AdtId def_id, [], []), ConstantAdt def_id' -> + assert (def_id = def_id'); + (* Check that the adt definition only has one variant with no fields, + compute the variant id at the same time. *) + let def = C.ctx_lookup_type_def ctx def_id in + assert (List.length def.region_params = 0); + assert (List.length def.type_params = 0); + let variant_id = + match def.kind with + | Struct fields -> + assert (List.length fields = 0); + None + | Enum variants -> + assert (List.length variants = 1); + let variant_id = T.VariantId.zero in + let variant = T.VariantId.nth variants variant_id in + assert (List.length variant.fields = 0); + Some variant_id + in + let value = V.Adt { variant_id; field_values = [] } in + { value; ty } + (* Scalar, boolean... *) + | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty } + | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty } + | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty } + | T.Integer int_ty, ConstantValue (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) - listing as much as we can on purpose + (allows to catch errors at compilation if the definitions change) *) + | _, Unit | _, ConstantAdt _ | _, ConstantValue _ -> + failwith "Improperly typed constant value" + +(** Small utility *) +let prepare_rplace (config : C.config) (access : access_kind) (p : E.place) + (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + let ctx = update_ctx_along_read_place config access p ctx in + let ctx = end_loans_at_place config access p ctx in + let v = read_place_unwrap config access p ctx in + (ctx, v) + +(** Prepare the evaluation of an operand. *) +let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand) + : C.eval_ctx * V.typed_value = + let ctx, v = + match op with + | Expressions.Constant (ty, cv) -> + let v = constant_value_to_typed_value ctx ty cv in + (ctx, v) + | Expressions.Copy p -> + (* Access the value *) + let access = Read in + prepare_rplace config access p ctx + | Expressions.Move p -> + (* Access the value *) + let access = Move in + prepare_rplace config access p ctx + in + assert (not (bottom_in_value v)); + (ctx, v) + +(** Evaluate an operand. *) +let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : + C.eval_ctx * V.typed_value = + (* Debug *) + L.log#ldebug + (lazy + ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n" + ^ operand_to_string ctx op ^ "\n")); + (* Evaluate *) + match op with + | Expressions.Constant (ty, cv) -> + let v = constant_value_to_typed_value ctx ty cv in + (ctx, v) + | Expressions.Copy p -> + (* Access the value *) + let access = Read in + let ctx, v = prepare_rplace config access p ctx in + (* Copy the value *) + L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v)); + assert (not (bottom_in_value v)); + let allow_adt_copy = false in + copy_value allow_adt_copy config ctx v + | Expressions.Move p -> ( + (* Access the value *) + let access = Move in + let ctx, v = prepare_rplace config access p ctx in + (* Move the value *) + L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v)); + assert (not (bottom_in_value 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 -> (ctx, v)) + +(** Evaluate several operands. *) +let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list) + : C.eval_ctx * V.typed_value list = + List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops + +let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand) + (op2 : E.operand) : C.eval_ctx * V.typed_value * V.typed_value = + match eval_operands config ctx [ op1; op2 ] with + | ctx, [ v1; v2 ] -> (ctx, v1, v2) + | _ -> failwith "Unreachable" + +let eval_unary_op_concrete (config : C.config) (ctx : C.eval_ctx) + (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result + = + (* Evaluate the operand *) + let ctx, v = eval_operand config ctx op in + (* Apply the unop *) + match (unop, v.V.value) with + | E.Not, V.Concrete (Bool b) -> + Ok (ctx, { 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 _ -> Error Panic + | Ok sv -> Ok (ctx, { v with V.value = V.Concrete (V.Scalar sv) })) + | _ -> failwith "Invalid input for unop" + +let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx) + (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result + = + (* Evaluate the operand *) + let ctx, v = eval_operand config ctx op in + (* Generate a fresh symbolic value to store the result *) + let ctx, res_sv_id = C.fresh_symbolic_value_id ctx 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 + | _ -> failwith "Invalid input for unop" + in + let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in + (* Synthesize *) + S.synthesize_unary_op unop v res_sv; + (* Return *) + Ok (ctx, mk_typed_value_from_symbolic_value res_sv) + +let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : E.unop) + (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result = + match config.mode with + | C.ConcreteMode -> eval_unary_op_concrete config ctx unop op + | C.SymbolicMode -> eval_unary_op_symbolic config ctx unop op + +let eval_binary_op_concrete (config : C.config) (ctx : C.eval_ctx) + (binop : E.binop) (op1 : E.operand) (op2 : E.operand) : + (C.eval_ctx * V.typed_value) eval_result = + (* Evaluate the operands *) + let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in + (* 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 (type_is_primitively_copyable v1.ty); + let b = v1 = v2 in + Ok (ctx, { 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) -> ( + let res = + (* 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 -> + failwith "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 -> + failwith "Unreachable" + in + match res with + | Error err -> Error err + | 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 -> failwith "Unreachable" + in + match res with Error _ -> Error Panic | Ok v -> Ok (ctx, v)) + | _ -> failwith "Invalid inputs for binop" + +let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx) + (binop : E.binop) (op1 : E.operand) (op2 : E.operand) : + (C.eval_ctx * V.typed_value) eval_result = + (* Evaluate the operands *) + let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in + (* Generate a fresh symbolic value to store the result *) + let ctx, res_sv_id = C.fresh_symbolic_value_id ctx 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 (type_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 -> failwith "Unreachable") + | _ -> failwith "Invalid inputs for binop" + in + let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in + (* Synthesize *) + S.synthesize_binary_op binop v1 v2 res_sv; + (* Return *) + Ok (ctx, mk_typed_value_from_symbolic_value res_sv) + +let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop) + (op1 : E.operand) (op2 : E.operand) : + (C.eval_ctx * V.typed_value) eval_result = + match config.mode with + | C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2 + | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2 + +(** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *) +let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place) + (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (* Note that discriminant values have type `isize` *) + (* Access the value *) + let access = Read in + let ctx, v = prepare_rplace config access p ctx in + match v.V.value with + | Adt av -> ( + match av.variant_id with + | None -> + failwith "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 _ -> + failwith "Disciminant id out of range" + (* Should really never happen *) + | Ok sv -> + (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize })) + ) + | _ -> failwith "Invalid input for `discriminant`" + +let eval_rvalue_discriminant (config : C.config) (p : E.place) + (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list = + S.synthesize_eval_rvalue_discriminant p; + (* Note that discriminant values have type `isize` *) + (* Access the value *) + let access = Read in + let ctx, v = prepare_rplace config access p ctx in + match v.V.value with + | Adt _ -> [ eval_rvalue_discriminant_concrete config p ctx ] + | Symbolic sv -> + (* Expand the symbolic value - may lead to branching *) + let ctxl = expand_symbolic_enum_value config sv ctx in + (* This time the value is concrete: reevaluate *) + List.map (eval_rvalue_discriminant_concrete config p) ctxl + | _ -> failwith "Invalid input for `discriminant`" + +let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place) + (bkind : E.borrow_kind) : C.eval_ctx * V.typed_value = + S.synthesize_eval_rvalue_ref p bkind; + match bkind with + | E.Shared | E.TwoPhaseMut -> + (* Access the value *) + let access = if bkind = E.Shared then Read else Write in + let ctx, v = prepare_rplace config access p ctx in + (* Compute the rvalue - simply a shared borrow with a fresh id *) + let ctx, bid = C.fresh_borrow_id ctx in + (* 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 bid + else V.InactivatedMutBorrow bid + in + let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in + (* Compute the value with which to replace the value at place p *) + let nv = + 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)) } + | _ -> + (* 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' } + in + (* Update the value in the context *) + let ctx = write_place_unwrap config access p nv ctx in + (* Return *) + (ctx, rv) + | E.Mut -> + (* Access the value *) + let access = Write in + let ctx, v = prepare_rplace config access p ctx in + (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) + let ctx, bid = C.fresh_borrow_id ctx 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 + (* Return *) + (ctx, rv) + +let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx) + (aggregate_kind : E.aggregate_kind) (ops : E.operand list) : + C.eval_ctx * V.typed_value = + S.synthesize_eval_rvalue_aggregate aggregate_kind ops; + (* Evaluate the operands *) + let ctx, values = eval_operands config ctx ops in + (* 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 + (ctx, { V.value = v; ty }) + | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> + (* Sanity checks *) + let type_def = C.ctx_lookup_type_def ctx def_id in + assert (List.length type_def.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 + (ctx, { V.value = Adt av; ty = aty }) + +(** Evaluate an rvalue which is not a discriminant. + + We define a function for this specific case, because evaluating + a discriminant might lead to branching (if we evaluate the discriminant + of a symbolic enumeration value), while it is not the case for the + other rvalues. + *) +let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx) + (rvalue : E.rvalue) : (C.eval_ctx * V.typed_value) eval_result = + match rvalue with + | E.Use op -> Ok (eval_operand config ctx op) + | E.Ref (p, bkind) -> Ok (eval_rvalue_ref config ctx p bkind) + | E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op + | E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2 + | E.Aggregate (aggregate_kind, ops) -> + Ok (eval_rvalue_aggregate config ctx aggregate_kind ops) + | E.Discriminant _ -> failwith "Unreachable" + +(** Evaluate an rvalue in a given context: return the updated context and + the computed value. + + Returns a list of pairs (new context, computed rvalue) because + `discriminant` might lead to a branching in case it is applied + on a symbolic enumeration value. +*) +let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : + (C.eval_ctx * V.typed_value) list eval_result = + match rvalue with + | E.Discriminant p -> Ok (eval_rvalue_discriminant config p ctx) + | _ -> ( + match eval_rvalue_non_discriminant config ctx rvalue with + | Error e -> Error e + | Ok res -> Ok [ res ]) + +(** Drop a value at a given place *) +let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx + = + L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); + (* Prepare the place (by ending the loans, then the borrows) *) + let ctx, v = prepare_lplace config p ctx in + (* Replace the value with [Bottom] *) + let nv = { v with value = V.Bottom } in + let ctx = write_place_unwrap config Write p nv ctx in + ctx + +(** Assign a value to a given place *) +let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) + (p : E.place) : C.eval_ctx = + (* Prepare the destination *) + let ctx, _ = prepare_lplace config p ctx in + (* Update the destination *) + let ctx = write_place_unwrap config Write p v ctx in + ctx |