summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-01-06 01:10:51 +0100
committerSon HO2023-02-03 11:21:46 +0100
commita2e52dd8e4f53600c74744026aeae15d99d104b0 (patch)
treead5c81fd1e9763955d1c8250d3dc730f39f678d5 /compiler
parent852ee63cb876d419d4830eb5192604d58b07b495 (diff)
Fix an issue with the translation of loops::clear
Diffstat (limited to '')
-rw-r--r--compiler/Interpreter.ml5
-rw-r--r--compiler/InterpreterLoops.ml93
-rw-r--r--compiler/ValuesUtils.ml2
3 files changed, 72 insertions, 28 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**.