Make progress on implementing the symbolic evaluation for the non-local

function calls

3 files changed, 134 insertions, 52 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index f753206c..0adff0dc 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -12,6 +12,7 @@ open ValuesUtils
 module Inv = Invariants
 open InterpreterUtils
 module S = Synthesis
+open Utils
 
 (* TODO: check that the value types are correct when evaluating *)
 (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
@@ -74,33 +75,6 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
     None
   with FoundLoanContent lc -> Some lc
 
-(** Check if a region is in a set of regions *)
-let region_in_set (r : T.RegionId.id T.region) (rset : T.RegionId.set_t) : bool
-    =
-  match r with T.Static -> false | T.Var id -> T.RegionId.Set.mem id rset
-
-(** Return the set of regions in an rty *)
-let rty_regions (ty : T.rty) : T.RegionId.set_t =
-  let s = ref T.RegionId.Set.empty in
-  let add_region (r : T.RegionId.id T.region) =
-    match r with T.Static -> () | T.Var rid -> s := T.RegionId.Set.add rid !s
-  in
-  let obj =
-    object
-      inherit [_] T.iter_ty
-
-      method! visit_'r _env r = add_region r
-    end
-  in
-  (* Explore the type *)
-  obj#visit_ty () ty;
-  (* Return the set of accumulated regions *)
-  !s
-
-let rty_regions_intersect (ty : T.rty) (regions : T.RegionId.set_t) : bool =
-  let ty_regions = rty_regions ty in
-  not (T.RegionId.Set.disjoint ty_regions regions)
-
 (** 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
@@ -3667,8 +3641,9 @@ let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value)
   ctx
 
 (** Auxiliary function - see [eval_non_local_function_call] *)
-let eval_box_new (config : C.config) (region_params : T.erased_region list)
-    (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result =
+let eval_box_new_concrete (config : C.config)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (ctx : C.eval_ctx) : C.eval_ctx eval_result =
   (* Check and retrieve the arguments *)
   match (region_params, type_params, ctx.env) with
   | ( [],
@@ -3700,7 +3675,7 @@ let eval_box_new (config : C.config) (region_params : T.erased_region list)
 
 (** Auxiliary function which factorizes code to evaluate `std::Deref::deref`
     and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *)
-let eval_box_deref_mut_or_shared (config : C.config)
+let eval_box_deref_mut_or_shared_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
     (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx eval_result =
   (* Check the arguments *)
@@ -3735,17 +3710,20 @@ let eval_box_deref_mut_or_shared (config : C.config)
   | _ -> failwith "Inconsistent state"
 
 (** Auxiliary function - see [eval_non_local_function_call] *)
-let eval_box_deref (config : C.config) (region_params : T.erased_region list)
-    (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result =
+let eval_box_deref_concrete (config : C.config)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (ctx : C.eval_ctx) : C.eval_ctx eval_result =
   let is_mut = false in
-  eval_box_deref_mut_or_shared config region_params type_params is_mut ctx
+  eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut
+    ctx
 
 (** Auxiliary function - see [eval_non_local_function_call] *)
-let eval_box_deref_mut (config : C.config)
+let eval_box_deref_mut_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
     (ctx : C.eval_ctx) : C.eval_ctx eval_result =
   let is_mut = true in
-  eval_box_deref_mut_or_shared config region_params type_params is_mut ctx
+  eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut
+    ctx
 
 (** Auxiliary function - see [eval_non_local_function_call].
 
@@ -3768,7 +3746,7 @@ let eval_box_deref_mut (config : C.config)
 *)
 let eval_box_free (config : C.config) (region_params : T.erased_region list)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place)
-    (ctx : C.eval_ctx) : C.eval_ctx eval_result =
+    (ctx : C.eval_ctx) : C.eval_ctx =
   match (region_params, type_params, args) with
   | [], [ boxed_ty ], [ E.Move input_box_place ] ->
       (* Required type checking *)
@@ -3783,9 +3761,38 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
       let ctx = assign_to_place config ctx mk_unit_value dest in
 
       (* Return *)
-      Ok ctx
+      ctx
   | _ -> failwith "Inconsistent state"
 
+(** Auxiliary function - see [eval_non_local_function_call] *)
+let eval_box_new_symbolic (config : C.config)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+  raise Unimplemented
+
+(** Auxiliary function which factorizes code to evaluate `std::Deref::deref`
+    and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *)
+let eval_box_deref_mut_or_shared_symbolic (config : C.config)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+  raise Unimplemented
+
+(** Auxiliary function - see [eval_non_local_function_call] *)
+let eval_box_deref_symbolic (config : C.config)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+  let is_mut = false in
+  eval_box_deref_mut_or_shared_symbolic config region_params type_params is_mut
+    ctx
+
+(** Auxiliary function - see [eval_non_local_function_call] *)
+let eval_box_deref_mut_symbolic (config : C.config)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+  let is_mut = true in
+  eval_box_deref_mut_or_shared_symbolic config region_params type_params is_mut
+    ctx
+
 (** Evaluate a non-local function call in concrete mode *)
 let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
     (fid : A.assumed_fun_id) (region_params : T.erased_region list)
@@ -3799,7 +3806,7 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
   match fid with
   | A.BoxFree ->
       (* Degenerate case: box_free *)
-      eval_box_free config region_params type_params args dest ctx
+      Ok (eval_box_free config region_params type_params args dest ctx)
   | _ -> (
       (* "Normal" case: not box_free *)
       (* Evaluate the operands *)
@@ -3830,10 +3837,11 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
          access to a body. *)
       let res =
         match fid with
-        | A.BoxNew -> eval_box_new config region_params type_params ctx
-        | A.BoxDeref -> eval_box_deref config region_params type_params ctx
+        | A.BoxNew -> eval_box_new_concrete config region_params type_params ctx
+        | A.BoxDeref ->
+            eval_box_deref_concrete config region_params type_params ctx
         | A.BoxDerefMut ->
-            eval_box_deref_mut config region_params type_params ctx
+            eval_box_deref_mut_concrete config region_params type_params ctx
         | A.BoxFree -> failwith "Unreachable"
         (* should have been treated above *)
       in
@@ -3855,11 +3863,45 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
 let eval_non_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
     (fid : A.assumed_fun_id) (region_params : T.erased_region list)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
-    C.eval_ctx eval_result =
+    C.eval_ctx =
   (* Synthesis *)
   S.synthesize_non_local_function_call fid region_params type_params args dest;
 
-  raise Unimplemented
+  (* Sanity check: make sure the type parameters don't contain regions -
+   * this is a current limitation of our synthesis *)
+  assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params);
+
+  (* There are two cases (and this is extremely annoying):
+     - the function is not box_free
+     - the function is box_free
+     See [eval_box_free]
+  *)
+  match fid with
+  | A.BoxFree ->
+      (* Degenerate case: box_free *)
+      eval_box_free config region_params type_params args dest ctx
+  | _ ->
+      (* "Normal" case: not box_free *)
+      (* Evaluate the operands *)
+      let ctx, args_vl = eval_operands config ctx args in
+
+      (* Evaluate the function call *)
+      let ctx, ret_value =
+        match fid with
+        | A.BoxNew -> eval_box_new_symbolic config region_params type_params ctx
+        | A.BoxDeref ->
+            eval_box_deref_symbolic config region_params type_params ctx
+        | A.BoxDerefMut ->
+            eval_box_deref_mut_symbolic config region_params type_params ctx
+        | A.BoxFree -> failwith "Unreachable"
+        (* should have been treated above *)
+      in
+
+      (* Move the return value to its destination *)
+      let ctx = assign_to_place config ctx ret_value dest in
+
+      (* Return *)
+      ctx
 
 (** Evaluate a non-local (i.e, assumed) function call such as `Box::deref`
     (auxiliary helper for [eval_statement]) *)
@@ -3888,8 +3930,9 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
       eval_non_local_function_call_concrete config ctx fid region_params
         type_params args dest
   | C.SymbolicMode ->
-      eval_non_local_function_call_symbolic config ctx fid region_params
-        type_params args dest
+      Ok
+        (eval_non_local_function_call_symbolic config ctx fid region_params
+           type_params args dest)
 
 (** Evaluate a statement *)
 let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 20d4c3af..66ca8998 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -9,6 +9,7 @@ module A = CfimAst
 module L = Logging
 open TypesUtils
 open ValuesUtils
+open Utils
 
 (** Some utilities *)
 
@@ -147,13 +148,6 @@ type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
 
 type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id
 
-exception Found
-(** Utility exception
-
-    When looking for something while exploring a term, it can be easier to
-    just throw an exception to signal we found what we were looking for.
- *)
-
 exception FoundBorrowContent of V.borrow_content
 (** Utility exception *)
 
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 4b3d8b0f..faf77eac 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -1,4 +1,5 @@
 open Types
+open Utils
 
 (** Retrieve the list of fields for the given variant of a [type_def].
 
@@ -22,6 +23,32 @@ let ty_is_unit (ty : 'r ty) : bool =
 (** The unit type *)
 let mk_unit_ty : ety = Adt (Tuple, [], [])
 
+(** Check if a region is in a set of regions *)
+let region_in_set (r : RegionId.id region) (rset : RegionId.set_t) : bool =
+  match r with Static -> false | Var id -> RegionId.Set.mem id rset
+
+(** Return the set of regions in an rty *)
+let rty_regions (ty : rty) : RegionId.set_t =
+  let s = ref RegionId.Set.empty in
+  let add_region (r : RegionId.id region) =
+    match r with Static -> () | Var rid -> s := RegionId.Set.add rid !s
+  in
+  let obj =
+    object
+      inherit [_] iter_ty
+
+      method! visit_'r _env r = add_region r
+    end
+  in
+  (* Explore the type *)
+  obj#visit_ty () ty;
+  (* Return the set of accumulated regions *)
+  !s
+
+let rty_regions_intersect (ty : rty) (regions : RegionId.set_t) : bool =
+  let ty_regions = rty_regions ty in
+  not (RegionId.Set.disjoint ty_regions regions)
+
 (** Convert an [ety], containing no region variables, to an [rty].
 
     In practice, it is the identity.
@@ -43,3 +70,21 @@ let rec ety_no_regions_to_rty (ty : ety) : rty =
       failwith
         "Can't convert a ref with erased regions to a ref with non-erased \
          regions"
+
+(** Check if a [ty] contains regions *)
+let rec ty_has_regions (ty : ety) : bool =
+  let obj =
+    object
+      inherit [_] iter_ty as super
+
+      method! visit_Adt env type_id regions tys =
+        if regions = [] then super#visit_Adt env type_id regions tys
+        else raise Found
+
+      method! visit_Ref _ _ _ _ = raise Found
+    end
+  in
+  try
+    obj#visit_ty () ty;
+    false
+  with Found -> true