summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-05 09:03:21 +0100
committerSon Ho2022-01-05 09:03:21 +0100
commit882f7840d9a110cfc138fe376447783d63118223 (patch)
treee2b9e2355949826c1ae5019bd192d0cc774c52bb /src
parentd7ac73c207461559f55623e8ff61d2bb7e5cf982 (diff)
Implement the symbolic case of copy_value
Diffstat (limited to 'src')
-rw-r--r--src/CfimAst.ml6
-rw-r--r--src/Interpreter.ml36
2 files changed, 36 insertions, 6 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 6c9b596e..250cd223 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -86,9 +86,9 @@ type fun_def = {
body : statement;
}
[@@deriving show]
-(** TODO: the type and function definitions contain information like `divergent`
- * or `copyable`. I wonder if this information should be stored directly inside
- * the definitions or inside separate maps/sets.
+(** TODO: function definitions (and maybe type definitions in the future)
+ * contain information like `divergent`. I wonder if this information should
+ * be stored directly inside the definitions or inside separate maps/sets.
* Of course, if everything is stored in separate maps/sets, nothing
* prevents us from computing this info in Charon (and thus exporting directly
* it with the type/function defs), in which case we just have to implement special
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index a335a0d5..3c24f38a 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2917,10 +2917,30 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
ctx
with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx)
+(** Return true if a type is "primitively copyable".
+ *
+ * "primitively copyable" means that copying instances of this type doesn't
+ * require calling dedicated functions defined through the Copy trait. It
+ * is the case for types like integers, shared borrows, etc.
+ *)
+let rec type_is_primitively_copyable (ty : T.ety) : bool =
+ match ty with
+ | T.Adt (_, _, _) | T.TypeVar _ | T.Never | T.Str | T.Array _ | T.Slice _ ->
+ false
+ | T.Bool | T.Char | T.Integer _ -> true
+ | T.Ref (_, _, T.Mut) -> false
+ | T.Ref (_, _, T.Shared) -> true
+
(** Copy a value, and return the resulting value.
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...
*)
let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
C.eval_ctx * V.typed_value =
@@ -2960,9 +2980,19 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
| V.SharedLoan (_, sv) ->
(* We don't copy the shared loan: only the shared value inside *)
copy_value config ctx sv)
- | V.Symbolic _sp ->
- (* TODO: check that the value is copyable *)
- raise Unimplemented
+ | 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
+ * thus requires calling the proper function. Here, we copy values
+ * for very simple types such as integers, shared borrows, etc. *)
+ assert (
+ type_is_primitively_copyable (Subst.erase_regions sp.V.svalue.V.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
+ * borrows: when doing so, every occurrence of the same symbolic value
+ * must use a fresh borrow id. *)
+ (ctx, v)
(** Convert a constant operand value to a typed value *)
let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)