diff options
| -rw-r--r-- | src/CfimAst.ml | 6 | ||||
| -rw-r--r-- | src/Interpreter.ml | 36 |
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) |