diff options
| -rw-r--r-- | TODO.md | 7 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 1 | ||||
| -rw-r--r-- | src/Invariants.ml | 11 | ||||
| -rw-r--r-- | src/Print.ml | 4 | ||||
| -rw-r--r-- | src/main.ml | 4 |
5 files changed, 22 insertions, 5 deletions
@@ -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 |