Implement the sanity checks for consumption of symbolic values by

abstractions (as input or given back values)

1 files changed, 22 insertions, 0 deletions

diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index ca437593..be899c08 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -224,3 +224,25 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
     obj#visit_typed_value () v;
     false
   with Found -> true
+
+let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
+    (v : V.typed_value) : bool =
+  let obj =
+    object
+      inherit [_] V.iter_typed_value
+
+      method! visit_symbolic_value _ s =
+        match s.sv_kind with
+        | V.FunCallRet ->
+            if ty_has_borrow_below_mut ctx.type_context.type_infos s.sv_ty then
+              raise Found
+            else ()
+        | V.SynthInput -> ()
+        | V.FunCallGivenBack | V.SynthGivenBack -> failwith "Unreachable"
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true