summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-24 23:11:09 +0100
committerSon Ho2021-11-24 23:11:09 +0100
commit8fb482d937b7514344cf5afa1fd20ee2c58fc395 (patch)
tree0df65144fdd84a51ad087a142f3116c13b983039
parent6ee26448d36ee5ff49eeb4a1246f164e3a33ff50 (diff)
Make progress on eval_rvalue and update aggregate_kind
-rw-r--r--src/CfimOfJson.ml7
-rw-r--r--src/Expressions.ml3
-rw-r--r--src/Interpreter.ml97
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*)