Update the trace

2 files changed, 26 insertions, 76 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index e11adcbf..b105c97b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -10,6 +10,7 @@ module L = Logging
 open TypesUtils
 open ValuesUtils
 module Inv = Invariants
+open InterpreterUtils
 
 (* TODO: check that the value types are correct when evaluating *)
 (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
@@ -26,81 +27,6 @@ module Inv = Invariants
 
 (* TODO: remove the config parameters when they are useless *)
 
-(** Some utilities *)
-
-let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
-
-let ety_to_string = Print.EvalCtxCfimAst.ety_to_string
-
-let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string
-
-let place_to_string = Print.EvalCtxCfimAst.place_to_string
-
-let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
-
-let statement_to_string ctx =
-  Print.EvalCtxCfimAst.statement_to_string ctx "" "  "
-
-let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
-  sv0.V.sv_id = sv1.V.sv_id
-
-(* TODO: move *)
-let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
-    =
-  { A.index; name; var_ty }
-
-(** Small helper *)
-let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
-  { var_id; projection = [] }
-
-(** Deconstruct a type of the form `Box<T>` to retrieve the `T` inside *)
-let ty_get_box (box_ty : T.ety) : T.ety =
-  match box_ty with
-  | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> boxed_ty
-  | _ -> failwith "Not a boxed type"
-
-(** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and
-    the borrow kind, etc.)
- *)
-let ty_get_ref (ty : T.ety) : T.erased_region * T.ety * T.ref_kind =
-  match ty with
-  | T.Ref (r, ty, ref_kind) -> (r, ty, ref_kind)
-  | _ -> failwith "Not a ref type"
-
-(** Box a value *)
-let mk_box_value (v : V.typed_value) : V.typed_value =
-  let box_ty = T.Adt (T.Assumed T.Box, [], [ v.V.ty ]) in
-  let box_v = V.Adt { variant_id = None; field_values = [ v ] } in
-  mk_typed_value box_ty box_v
-
-(** Create a fresh symbolic proj comp *)
-let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty)
-    (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp =
-  let ctx, sv_id = C.fresh_symbolic_value_id ctx in
-  let svalue = { V.sv_id; V.sv_ty = ty } in
-  let sv = { V.svalue; rset_ended = ended_regions } in
-  (ctx, sv)
-
-(** Create a fresh symbolic value (as a complementary projector) *)
-let mk_fresh_symbolic_proj_comp_value (ended_regions : T.RegionId.set_t)
-    (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
-  let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ty ctx in
-  let value : V.value = V.Symbolic sv in
-  let ty : T.ety = Subst.erase_regions ty in
-  let sv : V.typed_value = { V.value; ty } in
-  (ctx, sv)
-
-let mk_typed_value_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_value =
-  let ty = Subst.erase_regions sv.V.svalue.V.sv_ty in
-  let value = V.Symbolic sv in
-  { V.value; ty }
-
-let mk_aproj_loans_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_avalue =
-  let ty = sv.V.svalue.V.sv_ty in
-  let proj = V.AProjLoans sv.V.svalue in
-  let value = V.ASymbolic proj in
-  { V.value; ty }
-
 (** TODO: change the name *)
 type eval_error = Panic
 
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 5caafa79..a36cae03 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -12,12 +12,21 @@ module A = CfimAst
 module L = Logging
 open TypesUtils
 open ValuesUtils
+open InterpreterUtils
+
+let debug_invariants : bool ref = ref false
 
 type borrow_info = {
   loan_kind : T.ref_kind;
   loan_ids : V.BorrowId.set_t;
   borrow_ids : V.BorrowId.set_t;
 }
+[@@deriving show]
+
+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
+  String.concat "\n" bindings
 
 type borrow_kind = Mut | Shared | Inactivated
 
@@ -198,10 +207,25 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
   (* Visit *)
   borrows_visitor#visit_eval_ctx () ctx;
 
+  (* Debugging *)
+  if !debug_invariants then (
+    L.log#ldebug
+      (lazy
+        ("\nAbout to check context invariant:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+    L.log#ldebug
+      (lazy
+        ("\Borrows information:\n"
+        ^ borrows_infos_to_string !borrows_infos
+        ^ "\n")));
+
   (* Finally, check that everything is consistant *)
   V.BorrowId.Map.iter
     (fun _ info ->
-      assert (info.loan_ids = info.borrow_ids);
+      (* Note that we can't directly compare the sets - I guess they are
+       * different depending on the order in which we add the elements... *)
+      assert (
+        V.BorrowId.Set.elements info.loan_ids
+        = V.BorrowId.Set.elements info.borrow_ids);
       match info.loan_kind with
       | T.Mut -> assert (V.BorrowId.Set.cardinal info.loan_ids = 1)
       | T.Shared -> ())