summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-05 09:05:34 +0100
committerSon Ho2022-01-05 09:05:34 +0100
commitcc3e866f4a354c6e305bd9737dd46b0648e172af (patch)
treebdf8d5228d46f34352007b9bac5bb9e7570a2db8
parent882f7840d9a110cfc138fe376447783d63118223 (diff)
Make minor modifications
-rw-r--r--src/Interpreter.ml23
1 files changed, 13 insertions, 10 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 3c24f38a..a123f046 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2936,14 +2936,13 @@ let rec type_is_primitively_copyable (ty : T.ety) : bool =
Note that copying values might update the context. For instance, when
copying shared borrows, we need to insert new shared borrows in the context.
- Also, this function is actually more general than it should be: it allows
- to copy ADTs, while ADT copy should be done through the Copy trait (i.e.,
- by calling a dedicated function).
- TODO: maybe we should disallow the copy of ADTs, or control it through
- a boolean...
+ Also, this function is actually more general than it should be: it can be used
+ to copy concrete ADT values, while ADT copy should be done through the Copy
+ trait (i.e., by calling a dedicated function). This is why we added a parameter
+ to control this copy.
*)
-let rec copy_value (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 : C.config)
+ (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =
(* Remark: at some point we rewrote this function to use iterators, but then
* 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
@@ -2951,13 +2950,16 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
match v.V.value with
| V.Concrete _ -> (ctx, v)
| V.Adt av ->
+ assert allow_adt_copy;
(* Sanity check *)
(match v.V.ty with
| T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value"
| T.Adt ((T.AdtId _ | T.Tuple), _, _) -> () (* Ok *)
| _ -> failwith "Unreachable");
let ctx, fields =
- List.fold_left_map (copy_value config) ctx av.field_values
+ List.fold_left_map
+ (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 -> failwith "Can't copy ⊥"
@@ -2979,7 +2981,7 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
| V.MutLoan _ -> failwith "Can't copy a mutable loan"
| V.SharedLoan (_, sv) ->
(* We don't copy the shared loan: only the shared value inside *)
- copy_value config ctx sv)
+ copy_value allow_adt_copy config ctx sv)
| V.Symbolic sp ->
(* We can copy only if the type is "primitively" copyable.
* Note that in the general case, copy is a trait: copying values
@@ -3065,7 +3067,8 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
(* Copy the value *)
L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v));
assert (not (bottom_in_value v));
- copy_value config ctx 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