summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Interpreter.ml5
-rw-r--r--compiler/InterpreterLoops.ml93
-rw-r--r--compiler/ValuesUtils.ml2
-rw-r--r--tests/coq/misc/Loops.v8
-rw-r--r--tests/fstar/misc/Loops.Funs.fst14
5 files changed, 78 insertions, 44 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index ea61e2b2..c87aa6f2 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -261,9 +261,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return
}
]}
*)
- match C.ctx_find_abs ctx pred with
- | Some abs -> (abs.abs_id, false)
- | None -> (fun_abs_id, true)
+ let abs = Option.get (C.ctx_find_abs ctx pred) in
+ (abs.abs_id, false)
in
log#ldebug
(lazy
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 76085b55..2b7241ba 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -243,9 +243,9 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
(** Refresh the ids of the fresh abstractions.
We do this because {!prepare_ashared_loans} introduces some non-fixed
- abstractions in contexts which are later joined: we have to make sure
- two contexts we join don't have non-fixed abstractions with the same ids.
- *)
+ abstractions in contexts which are later joined: we have to make sure two
+ contexts we join don't have non-fixed abstractions with the same ids.
+ *)
let refresh_abs (old_abs : V.AbstractionId.Set.t) (ctx : C.eval_ctx) :
C.eval_ctx =
let ids, _ = compute_context_ids ctx in
@@ -1230,7 +1230,65 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
let match_mut_borrows (ty : T.ety) (bid0 : V.borrow_id) (bv0 : V.typed_value)
(bid1 : V.borrow_id) (bv1 : V.typed_value) (bv : V.typed_value) :
V.borrow_id * V.typed_value =
- if bid0 = bid1 then (bid0, bv)
+ if bid0 = bid1 then (
+ (* If the merged value is not the same as the original value, we introduce
+ an abstraction:
+
+ {[
+ { MB bid0, ML nbid } // where nbid fresh
+ ]}
+
+ and we use bid' for the borrow id that we return.
+
+ We do this because we want to make sure that, whenever a mutably
+ borrowed value is modified in a loop iteration, then there is
+ a fresh abstraction between this borrowed value and the fixed
+ abstractions.
+ *)
+ assert (not (value_has_borrows S.ctx bv.V.value));
+
+ if bv0 = bv1 then (
+ assert (bv0 = bv);
+ (bid0, bv))
+ else
+ let rid = C.fresh_region_id () in
+ let nbid = C.fresh_borrow_id () in
+
+ let kind = T.Mut in
+ let bv_ty = ety_no_regions_to_rty bv.V.ty in
+ let borrow_ty = mk_ref_ty (T.Var rid) bv_ty kind in
+
+ let borrow_av =
+ let ty = borrow_ty in
+ let value = V.ABorrow (V.AMutBorrow (bid0, mk_aignored bv_ty)) in
+ mk_typed_avalue ty value
+ in
+
+ let loan_av =
+ let ty = borrow_ty in
+ let value = V.ALoan (V.AMutLoan (nbid, mk_aignored bv_ty)) in
+ mk_typed_avalue ty value
+ in
+
+ let avalues = [ borrow_av; loan_av ] in
+
+ (* Generate the abstraction *)
+ let abs =
+ {
+ V.abs_id = C.fresh_abstraction_id ();
+ kind = V.Loop (S.loop_id, None, LoopSynthInput);
+ can_end = true;
+ parents = V.AbstractionId.Set.empty;
+ original_parents = [];
+ regions = T.RegionId.Set.singleton rid;
+ ancestors_regions = T.RegionId.Set.empty;
+ avalues;
+ }
+ in
+ push_abs abs;
+
+ (* Return the new borrow *)
+ (nbid, bv))
else
(* We replace bid0 and bid1 with a fresh borrow id, and introduce
an abstraction which links all of them:
@@ -2459,11 +2517,9 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
We do this because it makes it easier to compute joins and fixed points.
- We return the new context and the set of fresh abs ids.
-
**REMARK**:
- As a side note, only reborrow the loan ids whose corresponding borrows appear in
- values (i.e., not in abstractions).
+ As a side note, we only reborrow the loan ids whose corresponding borrows
+ appear in values (i.e., not in abstractions).
For instance, if we have:
{[
@@ -3019,23 +3075,12 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
(* Retrieve the first id of the group *)
match ids with
| [] ->
- (* This happens for instance in the following case (there
- is no "magic wand" linking the values before and after
- the loop, in particular because we return nothing):
-
- Example:
- ========
- {[
- fn clear(v: &mut Vec<u32>) {
- let mut i = 0;
- while i < v.len() {
- v[i] = 0;
- i += 1;
- }
- }
- ]}
+ (* We shouldn't get there: we actually introduce reborrows with
+ {!prepare_ashared_loans} and in the [match_mut_borrows] function
+ of {!MakeJoinMatcher} to introduce some fresh abstractions for
+ this purpose.
*)
- ()
+ raise (Failure "Unexpected")
| id0 :: ids ->
let id0 = ref id0 in
(* Add the proper region group into the abstraction *)
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 4612b019..abbfad31 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -159,7 +159,7 @@ let rec value_strip_shared_loans (v : typed_value) : typed_value =
(** Check if a symbolic value has borrows *)
let symbolic_value_has_borrows (infos : TA.type_infos) (sv : symbolic_value) :
bool =
- ty_has_borrow_under_mut infos sv.sv_ty
+ ty_has_borrows infos sv.sv_ty
(** Check if a value has borrows in **a general sense**.
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ec8fa39c..29f312bf 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -63,7 +63,7 @@ Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
.
(** [loops::clear] *)
-Definition clear_loop_fwd_back
+Fixpoint clear_loop_fwd_back
(n : nat) (v : vec u32) (i : usize) : result (vec u32) :=
match n with
| O => Fail_ OutOfFuel
@@ -73,16 +73,14 @@ Definition clear_loop_fwd_back
then (
i1 <- usize_add i 1%usize;
v0 <- vec_index_mut_back u32 v i (0%u32);
- v1 <- clear_loop_fwd n0 v0 i1;
- let _ := v1 in
- Return v0)
+ clear_loop_fwd_back n0 v0 i1)
else Return v
end
.
(** [loops::clear] *)
Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) :=
- v0 <- clear_loop_fwd n v (0%usize); let _ := v0 in Return v
+ clear_loop_fwd_back n v (0%usize)
.
(** [loops::List] *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index d19e9328..c0aca975 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -70,7 +70,7 @@ let sum_with_shared_borrows_fwd (max : u32) : result u32 =
sum_with_shared_borrows_loop_fwd max 0 0
(** [loops::clear] *)
-let clear_loop_fwd_back
+let rec clear_loop_fwd_back
(v : vec u32) (i : usize) :
Tot (result (vec u32)) (decreases (clear_decreases v i))
=
@@ -82,21 +82,13 @@ let clear_loop_fwd_back
| Return i1 ->
begin match vec_index_mut_back u32 v i 0 with
| Fail e -> Fail e
- | Return v0 ->
- begin match clear_loop_fwd v0 i1 with
- | Fail e -> Fail e
- | Return _ -> Return v0
- end
+ | Return v0 -> clear_loop_fwd_back v0 i1
end
end
else Return v
(** [loops::clear] *)
-let clear_fwd_back (v : vec u32) : result (vec u32) =
- begin match clear_loop_fwd v 0 with
- | Fail e -> Fail e
- | Return _ -> Return v
- end
+let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0
(** [loops::list_mem] *)
let rec list_mem_loop_fwd
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 07:27:35 +0000