1 files changed, 84 insertions, 0 deletions
diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml
new file mode 100644
index 00000000..7b93b019
--- /dev/null
+++ b/src/SymbolicAstUtils.ml
@@ -0,0 +1,84 @@
+open Errors
+module T = Types
+module V = Values
+module E = Expressions
+module A = CfimAst
+open SymbolicAst
+open ValuesUtils
+open InterpreterUtils
+
+type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's
+
+type ended_loan = (V.mvalue, V.mvalue list) ended
+
+type ended_borrow = (V.mvalue, V.mvalue) ended
+
+type ended_loan_or_borrow =
+  | EndedLoan of ended_loan
+  | EndedBorrow of ended_borrow
+
+(** Return the list of the meta-values given to the top owned ended mutable
+    loans/borrows of an abstraction
+    
+    We expect an abstraction where all the loans/borrows have ended.
+ *)
+let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list
+    =
+  (* The accumulator *)
+  let acc = ref [] in
+  let add x = acc := x :: !acc in
+  let add_loan x = add (EndedLoan x) in
+  let add_borrow x = add (EndedBorrow x) in
+  let add_sloan x = add_loan (EndedSymbolic x) in
+  let add_cloan x = add_loan (EndedConcrete x) in
+  let add_sborrow x = add_borrow (EndedSymbolic x) in
+  let add_cborrow x = add_borrow (EndedConcrete x) in
+
+  (* The visitor *)
+  let obj =
+    object
+      inherit [_] V.iter_abs as super
+
+      method! visit_aproj env aproj =
+        match aproj with
+        | AEndedProjLoans (msv, []) ->
+            (* The symbolic value was left unchanged *)
+            add_sloan [ mk_typed_value_from_symbolic_value msv ]
+        | AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl)
+        | AEndedProjBorrows mv -> add_sborrow mv
+        | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
+            failwith "Unreachable"
+
+      method! visit_aloan_content env lc =
+        match lc with
+        | AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable"
+        | AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
+            (* Add the meta-value and stop the exploration *)
+            add_cloan given_back_meta
+        | AEndedSharedLoan (_, _) -> raise Unimplemented
+        | AEndedIgnoredMutLoan _ ->
+            (* Dive in *)
+            super#visit_aloan_content env lc
+        | AIgnoredSharedLoan _ ->
+            (* Ignore *)
+            ()
+
+      method! visit_aborrow_content env bc =
+        match bc with
+        | AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
+            failwith "Unreachable"
+        | AEndedMutBorrow (mv, _) ->
+            (* Add the meta-value and stop the exploration *)
+            add_cborrow mv
+        | AEndedIgnoredMutBorrow _ ->
+            (* Dive in *)
+            super#visit_aborrow_content env bc
+        | AProjSharedBorrow _ ->
+            (* Ignore *)
+            ()
+    end
+  in
+  (* Apply *)
+  obj#visit_abs () abs;
+  (* Return the accumulated values *)
+  List.rev !acc