diff options
author | Son Ho | 2022-01-06 18:54:57 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 18:54:57 +0100 |
commit | a310c6036568d8f62e09804c67064686d106afd4 (patch) | |
tree | 13de8974489bc2d4a3aacb89d7550cd96be93a4e | |
parent | ff32d9e3f5133d469b92f17364c67fbc5b7dd13f (diff) |
Add debugging info
-rw-r--r-- | src/Invariants.ml | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index 86fa3d46..e214e820 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -35,6 +35,17 @@ let set_outer_mut (info : outer_borrow_info) : outer_borrow_info = let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info = { outer_borrow = true; outer_shared = true } +(* TODO: we need to factorize print functions for strings *) +let ids_reprs_to_string (reprs : V.BorrowId.id V.BorrowId.Map.t) : string = + let bindings = V.BorrowId.Map.bindings reprs in + let bindings = + List.map + (fun (id, repr_id) -> + V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id) + bindings + in + String.concat "\n" bindings + let borrows_infos_to_string (infos : borrow_info V.BorrowId.Map.t) : string = let bindings = V.BorrowId.Map.bindings infos in let bindings = List.map (fun (_, info) -> show_borrow_info info) bindings in @@ -160,10 +171,23 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (* Some utilities to register the borrows *) let find_info (bid : V.BorrowId.id) : borrow_info = (* Find the representant *) - let repr_bid = V.BorrowId.Map.find bid !ids_reprs in - (* Lookup the info *) - V.BorrowId.Map.find repr_bid !borrows_infos + match V.BorrowId.Map.find_opt bid !ids_reprs with + | Some repr_bid -> + (* Lookup the info *) + V.BorrowId.Map.find repr_bid !borrows_infos + | None -> + let err = + "find_info: could not find the representant of borrow " + ^ V.BorrowId.to_string bid ^ "\n" ^ "\n- Context:\n" + ^ eval_ctx_to_string ctx ^ "\n- representants:\n" + ^ ids_reprs_to_string !ids_reprs + ^ "\n- info:\n" + ^ borrows_infos_to_string !borrows_infos + in + L.log#serror err; + failwith err in + let update_info (bid : V.BorrowId.id) (info : borrow_info) : unit = (* Find the representant *) let repr_bid = V.BorrowId.Map.find bid !ids_reprs in |