summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Collections.ml14
-rw-r--r--src/InterpreterPaths.ml1
-rw-r--r--src/InterpreterStatements.ml20
3 files changed, 31 insertions, 4 deletions
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 *)