diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CfimOfJson.ml | 7 | ||||
| -rw-r--r-- | src/Expressions.ml | 3 | ||||
| -rw-r--r-- | src/Interpreter.ml | 97 |
3 files changed, 90 insertions, 17 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 681bc009..dfa7527e 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -367,12 +367,15 @@ let aggregate_kind_of_json (js : json) : (aggregate_kind, string) result = combine_error_msgs js "operand_kind_of_json" (match js with | `String "AggregatedTuple" -> Ok AggregatedTuple - | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id ]) ] -> + | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ] + -> let* id = TypeDefId.id_of_json id in let* opt_variant_id = option_of_json VariantId.id_of_json opt_variant_id in - Ok (AggregatedAdt (id, opt_variant_id)) + let* regions = list_of_json erased_region_of_json regions in + let* tys = list_of_json ety_of_json tys in + Ok (AggregatedAdt (id, opt_variant_id, regions, tys)) | _ -> Error "") let rvalue_of_json (js : json) : (rvalue, string) result = diff --git a/src/Expressions.ml b/src/Expressions.ml index 0246530b..d5219678 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -69,7 +69,8 @@ type operand = type aggregate_kind = | AggregatedTuple - | AggregatedAdt of TypeDefId.id * VariantId.id option + | AggregatedAdt of + TypeDefId.id * VariantId.id option * erased_region list * ety list type rvalue = | Use of operand diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 5c5a9617..9af0f936 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1479,7 +1479,32 @@ let prepare_rplace (config : config) (access : access_kind) (p : place) let ctx2 = { ctx with env = env2 } in (ctx2, v) -let eval_operand (config : config) (ctx : eval_ctx) (op : operand) : +(** When we need to evaluate several operands (for a function call for instance), + we need to prepare *all* the values by ending borrows, etc. *then* update them + (by moving them, borrowing them, etc.). + + The reason is that borrows in some of the values we access may reference + some of the other values: we may not be able to update the borrows if those + values have, say, been moved (and are not present in the environment anymore). + + For this reason, we split [eval_operand] into two functions: + - [eval_operand_prepare] + - [eval_operand_apply] + which are then used in [eval_operand] and [eval_operands]. + *) +let eval_operand_prepare (config : config) (ctx : eval_ctx) (op : operand) : + eval_ctx = + match op with + | Expressions.Constant (ty, cv) -> ctx (* nothing to do *) + | Expressions.Copy p -> + let access = Read in + fst (prepare_rplace config access p ctx) + | Expressions.Move p -> + let access = Move in + fst (prepare_rplace config access p ctx) + +(** See [eval_operand_prepare] (which should have been called before) *) +let eval_operand_apply (config : config) (ctx : eval_ctx) (op : operand) : eval_ctx * typed_value = match op with | Expressions.Constant (ty, cv) -> @@ -1488,22 +1513,52 @@ let eval_operand (config : config) (ctx : eval_ctx) (op : operand) : | Expressions.Copy p -> (* Access the value *) let access = Read in - let ctx2, v = prepare_rplace config access p ctx in + let v = read_place_unwrap config access p ctx.env in (* Copy the value *) assert (not (bottom_in_value v)); - copy_value config ctx2 v + copy_value config ctx v | Expressions.Move p -> ( (* Access the value *) let access = Move in - let ctx2, v = prepare_rplace config access p ctx in + let v = read_place_unwrap config access p ctx.env in (* Move the value *) assert (not (bottom_in_value v)); let bottom = { value = Bottom; ty = v.ty } in - match write_place config access p bottom ctx2.env with + match write_place config access p bottom ctx.env with | Error _ -> failwith "Unreachable" - | Ok env3 -> - let ctx3 = { ctx2 with env = env3 } in - (ctx3, v)) + | Ok env1 -> + let ctx1 = { ctx with env = env1 } in + (ctx1, v)) + +(** Evaluate an operand. + + WARNING: it is ok to use this function only if we have exactly one + operand to evaluate. If there are several, use [eval_operands]. + Otherwise, we may break invariants (if some values refer to other + values via borrows). + *) +let eval_operand (config : config) (ctx : eval_ctx) (op : operand) : + eval_ctx * typed_value = + let ctx1 = eval_operand_prepare config ctx op in + eval_operand_apply config ctx1 op + +(** Evaluate several operands. + + *) +let eval_operands (config : config) (ctx : eval_ctx) (ops : operand list) : + eval_ctx * typed_value list = + (* First prepare the values to end/activate the borrows *) + let ctx1 = + List.fold_left (fun ctx op -> eval_operand_prepare config ctx op) ctx ops + in + (* Then actually apply the operands to move, borrow, copy... *) + List.fold_left_map (fun ctx op -> eval_operand_apply config ctx op) ctx ops + +let eval_two_operands (config : config) (ctx : eval_ctx) (op1 : operand) + (op2 : operand) : eval_ctx * typed_value * typed_value = + match eval_operands config ctx [ op1; op2 ] with + | ctx', [ v1; v2 ] -> (ctx', v1, v2) + | _ -> failwith "Unreachable" let eval_unary_op (config : config) (ctx : eval_ctx) (unop : unop) (op : operand) : (eval_ctx * typed_value) eval_result = @@ -1526,11 +1581,12 @@ let eval_binary_op (config : config) (ctx : eval_ctx) (binop : binop) (op1 : operand) (op2 : operand) : (eval_ctx * typed_value) eval_result = (* Evaluate the operands *) let access = Read in - let ctx1, v1 = eval_operand config ctx op1 in - let ctx2, v2 = eval_operand config ctx1 op2 in - (* Binary operations only apply on integer values, but when we check for - * equality *) - if binop = Eq || binop = Ne then ( + let ctx2, v1, v2 = eval_two_operands config ctx op1 op2 in + if + (* Binary operations only apply on integer values, but when we check for + * equality *) + binop = Eq || binop = Ne + then ( (* Equality/inequality check is primitive only on primitive types *) assert (v1.ty = v2.ty); let b = v1 = v2 in @@ -1661,4 +1717,17 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : Ok (ctx1, { value = Concrete (Scalar sv); ty = Integer Isize }) )) | _ -> failwith "Invalid input for `discriminant`") - | Aggregate (aggregate_kind, ops) -> raise Unimplemented + | Aggregate (aggregate_kind, ops) -> + (* Evaluate the operands *) + let ctx1, values = eval_operands config ctx ops in + raise Unimplemented +(* (* Match on the aggregate kind *) + match aggregate_kind with + | AggregatedTuple -> + let tys = List.map (fun v -> v.ty) values in + let values = FieldId.vector_of_list values in + Ok (ctx1, { value = Tuple values; ty = Types.Tuple tys }) + | AggregatedAdt (def_id, opt_variant_id) -> raise Unimplemented + begin match + let expected_types = ctx_get_adt_field_types def_id opt_variant_id + let fields = ctx_get_adt_fields def_id opt_variant_id in*) |