summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--TODO.md7
-rw-r--r--src/InterpreterBorrows.ml1
-rw-r--r--src/Invariants.ml11
-rw-r--r--src/Print.ml4
-rw-r--r--src/main.ml4
5 files changed, 22 insertions, 5 deletions
diff --git a/TODO.md b/TODO.md
index 1632a3ca..b9ae7934 100644
--- a/TODO.md
+++ b/TODO.md
@@ -56,6 +56,13 @@
Then, once we collected all the borrows, we would convert it to:
`AEndedProjLoans of (mvalue * aproj) list`
If the list is empty, it means the value was not modified.
+
+9. The way we currently give back symbolic values to symbolic values (inside
+ abstractions) is wrong.
+ We get things like :
+ `AProjLoans (s0 <: &'a mut T) [AProjBorrows (s1 <: &'a mut T)]`
+ while in the case of `s1` we should ignore the outer borrow (we
+ gave back something because this borrow ended...).
* write a function to check that the code we are about to synthesize is in the proper
subset. In particular:
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index b231722d..d2964c90 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -454,6 +454,7 @@ let give_back_symbolic_value (_config : C.config)
V.AProjBorrows (nsv, sv.V.sv_ty)
| _ -> failwith "Unreachable"
in
+ (* TODO: this actually doesn't work, or at least there is something subtle... *)
V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
in
update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
diff --git a/src/Invariants.ml b/src/Invariants.ml
index ee58a1a3..2d26404d 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -595,13 +595,22 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| V.ASymbolic aproj, ty -> (
let ty1 = Subst.erase_regions ty in
match aproj with
- | V.AProjLoans (sv, _) | V.AProjBorrows (sv, _) ->
+ | V.AProjLoans (sv, _) ->
let ty2 = Subst.erase_regions sv.V.sv_ty in
assert (ty1 = ty2);
(* Also check that the symbolic values contain regions of interest -
* otherwise they should have been reduced to `_` *)
let abs = Option.get info in
+ log#ldebug (lazy (symbolic_value_to_string ctx sv));
assert (ty_has_regions_in_set abs.regions sv.V.sv_ty)
+ | V.AProjBorrows (sv, proj_ty) ->
+ let ty2 = Subst.erase_regions sv.V.sv_ty in
+ assert (ty1 = ty2);
+ (* Also check that the symbolic values contain regions of interest -
+ * otherwise they should have been reduced to `_` *)
+ let abs = Option.get info in
+ log#ldebug (lazy (symbolic_value_to_string ctx sv));
+ assert (ty_has_regions_in_set abs.regions proj_ty)
| V.AEndedProjLoans (_msv, given_back_ls) ->
List.iter
(fun (_, proj) ->
diff --git a/src/Print.ml b/src/Print.ml
index da6158b5..e1834ca6 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -317,9 +317,9 @@ module Values = struct
let given_back = List.map (aproj_to_string fmt) given_back in
" (" ^ String.concat "," given_back ^ ") "
in
- "["
+ "⌊"
^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv
- ^ given_back ^ "]"
+ ^ given_back ^ "⌋"
| AProjBorrows (sv, rty) ->
"(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
| AEndedProjLoans (_, given_back) ->
diff --git a/src/main.ml b/src/main.ml
index 2e1e552e..e803c49c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -55,7 +55,7 @@ let () =
expressions_log#set_level EL.Debug;
expansion_log#set_level EL.Debug;
borrows_log#set_level EL.Debug;
- invariants_log#set_level EL.Warning;
+ invariants_log#set_level EL.Debug;
(* Load the module *)
let json = Yojson.Basic.from_file !filename in
match cfim_module_of_json json with
@@ -68,7 +68,7 @@ let () =
let config =
{
C.check_invariants = true;
- greedy_expand_symbolics_with_borrows = false;
+ greedy_expand_symbolics_with_borrows = true;
}
in