Implement the sanity checks for consumption of symbolic values by

abstractions (as input or given back values)

5 files changed, 68 insertions, 9 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 9331d9f3..034d566a 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -432,14 +432,39 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
 let give_back_symbolic_value (_config : C.config)
     (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value)
     (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
-  let subst (abs : V.abs) abs_proj_ty =
-    (* TODO: check that we can consume this symbolic value - this is not
-     * a precondition, purely a sanity check *)
-    raise Errors.Unimplemented;
+  let subst (_abs : V.abs) _abs_proj_ty =
+    (* Compute the projection over the given back value *)
     let child_proj =
+      (* If it is the same symbolic value, it means it was left unchanged:
+       * we don't have to project it *)
       if sv.sv_id = nsv.sv_id then None
-      else
-        Some (mk_aproj_borrows_from_symbolic_value abs.regions nsv abs_proj_ty)
+      else (
+        (* Not the same symbolic value: it was updated (because given to a
+         * function or returned) *)
+        (* For now, we can only have the following case *)
+        assert (nsv.sv_kind = V.SynthGivenBack);
+        match nsv.sv_kind with
+        | V.SynthGivenBack ->
+            (* The given back value comes from the return value of the function
+             * we are currently synthesizing (as it is given back, it means
+             * we ended one of the regions appearing in the signature: we are
+             * currently synthesizing one of the backward functions *)
+            (* As we don't allow borrow overwrites on returned value, we can
+             * (and MUST) forget the borrows *)
+            None
+        | V.FunCallGivenBack ->
+            (* The value was fed as input to a function, and was given back *)
+            (* For now, we don't allow borrow overwrites on returned values,
+             * meaning the given back value can't have borrows below mutable
+             * borrows. *)
+            let has_borrow_below_mut =
+              ty_has_borrow_below_mut ctx.type_context.type_infos nsv.sv_ty
+            in
+            assert (not has_borrow_below_mut);
+            (* We don't allow overwrites: we must thus not project over the
+             * given back value *)
+            None
+        | _ -> failwith "Unreachable")
     in
     V.AEndedProjLoans child_proj
   in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 74886bf9..67a4bac5 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -905,7 +905,11 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
    * be fed to functions (i.e., symbolic values output from function return
    * values and which contain borrows of borrows can't be used as function
    * inputs *)
-  raise Errors.Unimplemented;
+  assert (
+    List.for_all
+      (fun arg ->
+        not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg))
+      args);
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let empty_absl =
     create_empty_abstractions_from_abs_region_groups V.FunCall
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
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index ef260830..e34add63 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -92,7 +92,7 @@ let rec ety_no_regions_to_rty (ty : ety) : rty =
         "Can't convert a ref with erased regions to a ref with non-erased \
          regions"
 
-(** Retuns true if a type contains borrows.
+(** Retuns true if the type contains borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
     we erase the lists of regions (by replacing them with `[]` when using `ety`,
@@ -102,7 +102,7 @@ let ty_has_borrows (infos : TA.type_infos) (ty : 'r ty) : bool =
   let info = TA.analyze_ty infos ty in
   info.TA.contains_borrow
 
-(** Retuns true if a type contains nested borrows.
+(** Retuns true if the type contains nested borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
     we erase the lists of regions (by replacing them with `[]` when using `ety`,
@@ -112,6 +112,10 @@ let ty_has_nested_borrows (infos : TA.type_infos) (ty : 'r ty) : bool =
   let info = TA.analyze_ty infos ty in
   info.TA.contains_nested_borrows
 
+(** Retuns true if the type contains a borrow below a mutable borrow *)
+let ty_has_borrow_below_mut (infos : TA.type_infos) (ty : 'r ty) : bool =
+  raise Errors.Unimplemented
+
 (** Check if a [ty] contains regions from a given set *)
 let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool =
   let obj =
diff --git a/src/Values.ml b/src/Values.ml
index a64d4467..6386f8db 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -232,6 +232,10 @@ type aproj =
       (** When ending a proj_loans over a symbolic value, we may need to insert
           (and keep track of) a proj_borrows over the given back value, if the
           symbolic value was consumed by an abstraction then updated.
+          
+          Rk.: for now this is useless, because we forbid borrow overwrites on
+          returned values. A consequence is that when a proj_loans over a symbolic
+          value ends, we don't project the given back value.
        *)
   | AEndedProjBorrows
   (* TODO: remove AEndedProjBorrows? We might need it for synthesis, to contain