diff options
| -rw-r--r-- | TODO.md | 2 | ||||
| -rw-r--r-- | src/Collections.ml | 14 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 1 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 20 |
4 files changed, 32 insertions, 5 deletions
@@ -78,7 +78,7 @@ 6. add `mvalue` (meta values) stored in abstractions when ending loans -8. The following doesn't work: +8. The following doesn't work (if we don't expand the symbolic values): ``` fn f1<'c, T>(p : (&'c mut T, &'c mut T)) -> (&'c mut T, &'c mut T) diff --git a/src/Collections.ml b/src/Collections.ml index 2cb298a7..351b6523 100644 --- a/src/Collections.ml +++ b/src/Collections.ml @@ -184,6 +184,7 @@ module type Set = sig val pp : Format.formatter -> t -> unit val show : t -> string + val pairwise_distinct : elt list -> bool end module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct @@ -218,6 +219,19 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct pp_string "}" let show s = to_string None s + + let pairwise_distinct ls = + let s = ref empty in + let rec check ls = + match ls with + | [] -> true + | x :: ls' -> + if mem x !s then false + else ( + s := add x !s; + check ls') + in + check ls end (** A map where the bindings are injective (i.e., if two keys are distinct, diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index edd27138..16ab9aad 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -771,6 +771,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) [end_borrows]: if false, we only end the outer loans we find. If true, we end all the loans and the borrows we find. + TODO: end_borrows is not necessary anymore. *) let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 34310ea1..ae9e59fe 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -20,20 +20,32 @@ open InterpreterExpressions (** The local logger *) let log = L.statements_log -(** Drop a value at a given place *) +(** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) let drop_value (config : C.config) (p : E.place) : cm_fun = fun cf ctx -> - log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); - (* Prepare the place (by ending the outer loans and the borrows). + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" + ^ eval_ctx_to_string ctx)); + (* Prepare the place (by ending the outer loans). * Note that [prepare_lplace] will use the `Write` access kind: * it is ok, because when updating the value with [Bottom] below, * we will use the `Move` access *) - let end_borrows = true in + let end_borrows = false in let prepare = prepare_lplace config end_borrows p in (* Replace the value with [Bottom] *) let replace cf (v : V.typed_value) ctx = + (* Move the value at destination (that we will overwrite) to a dummy variable + * to preserve the borrows *) + let mv = read_place_unwrap config Write p ctx in + let ctx = C.ctx_push_dummy_var ctx mv in + (* Update the destination to ⊥ *) let nv = { v with value = V.Bottom } in let ctx = write_place_unwrap config Move p nv ctx in + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ctx)); cf ctx in (* Compose and apply *) |