From 20279216a270c1f8f8c76cc060ca44ad23186430 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 14 Jan 2022 14:01:48 +0100
Subject: Implement loop detection when ending borrows/abstractions

---
 src/InterpreterBorrowsCore.ml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'src/InterpreterBorrowsCore.ml')

diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 00d2cbb3..3c39e76b 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -52,6 +52,31 @@ type loan_or_borrow_content =
   | BorrowContent of V.borrow_content
 [@@deriving show]
 
+type borrow_or_abs_id =
+  | BorrowId of V.BorrowId.id
+  | AbsId of V.AbstractionId.id
+
+type borrow_or_abs_ids = borrow_or_abs_id list
+
+let borrow_or_abs_id_to_string (id : borrow_or_abs_id) : string =
+  match id with
+  | AbsId id -> "abs@" ^ V.AbstractionId.to_string id
+  | BorrowId id -> "l@" ^ V.BorrowId.to_string id
+
+let borrow_or_abs_ids_chain_to_string (ids : borrow_or_abs_ids) : string =
+  let ids = List.rev ids in
+  let ids = List.map borrow_or_abs_id_to_string ids in
+  String.concat " -> " ids
+
+(** Add a borrow or abs id to a chain of ids, while checking that we don't loop *)
+let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id)
+    (ids : borrow_or_abs_ids) : borrow_or_abs_ids =
+  if List.mem id ids then
+    failwith
+      (msg ^ "detected a loop in the chain of ids: "
+      ^ borrow_or_abs_ids_chain_to_string (id :: ids))
+  else id :: ids
+
 (** Check if two different projections intersect. This is necessary when
     giving a symbolic value to an abstraction: we need to check that
     the regions which are already ended inside the abstraction don't
-- 
cgit v1.2.3