Make good progress on eval_local_function_call_symbolic

9 files changed, 191 insertions, 21 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 28f23758..23c8f1aa 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -26,10 +26,10 @@ type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
 
 type assertion = { cond : operand; expected : bool } [@@deriving show]
 
-type region_group = {
-  id : RegionGroupId.id;
-  regions : RegionVarId.id list;
-  parents : RegionGroupId.id list;
+type ('id, 'r) g_region_group = {
+  id : 'id;
+  regions : 'r list;
+  parents : 'id list;
 }
 [@@deriving show]
 (** A group of regions.
@@ -40,17 +40,38 @@ type region_group = {
     proper constraints, when evaluating a function call in symbolic mode.
 *)
 
-type region_groups = region_group list [@@deriving show]
+type ('r, 'id) g_region_groups = ('r, 'id) g_region_group list [@@deriving show]
+
+type region_var_group = (RegionGroupId.id, RegionVarId.id) g_region_group
+[@@deriving show]
+
+type region_var_groups = (RegionGroupId.id, RegionVarId.id) g_region_groups
+[@@deriving show]
+
+type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
+[@@deriving show]
+
+type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups
+[@@deriving show]
 
 type fun_sig = {
   region_params : region_var list;
   num_early_bound_regions : int;
-  regions_hierarchy : region_groups;
+  regions_hierarchy : region_var_groups;
   type_params : type_var list;
   inputs : sty list;
   output : sty;
 }
 [@@deriving show]
+(** A function signature, as used when declaring functions *)
+
+type inst_fun_sig = {
+  regions_hierarchy : abs_region_groups;
+  inputs : rty list;
+  output : rty;
+}
+[@@deriving show]
+(** A function signature, after instantiation *)
 
 type call = {
   func : fun_id;
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 4f39d7ff..a1dd0ad1 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -436,8 +436,8 @@ let assertion_of_json (js : json) : (A.assertion, string) result =
         Ok { A.cond; expected }
     | _ -> Error "")
 
-let region_group_of_json (js : json) : (A.region_group, string) result =
-  combine_error_msgs js "region_group_of_json"
+let region_var_group_of_json (js : json) : (A.region_var_group, string) result =
+  combine_error_msgs js "region_var_group_of_json"
     (match js with
     | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] ->
         let* id = A.RegionGroupId.id_of_json id in
@@ -446,9 +446,10 @@ let region_group_of_json (js : json) : (A.region_group, string) result =
         Ok { A.id; regions; parents }
     | _ -> Error "")
 
-let region_groups_of_json (js : json) : (A.region_groups, string) result =
-  combine_error_msgs js "region_group_of_json"
-    (list_of_json region_group_of_json js)
+let region_var_groups_of_json (js : json) : (A.region_var_groups, string) result
+    =
+  combine_error_msgs js "region_var_group_of_json"
+    (list_of_json region_var_group_of_json js)
 
 let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
   combine_error_msgs js "fun_sig_of_json"
@@ -464,7 +465,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
         ] ->
         let* region_params = list_of_json region_var_of_json region_params in
         let* num_early_bound_regions = int_of_json num_early_bound_regions in
-        let* regions_hierarchy = region_groups_of_json regions_hierarchy in
+        let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
         let* type_params = list_of_json type_var_of_json type_params in
         let* inputs = list_of_json sty_of_json inputs in
         let* output = sty_of_json output in
diff --git a/src/Contexts.ml b/src/Contexts.ml
index fec1e11b..89056680 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -71,6 +71,8 @@ type eval_ctx = {
   (* TODO: make this global? *)
   borrow_counter : BorrowId.generator;
   (* TODO: make this global? *)
+  region_counter : RegionId.generator;
+  (* TODO: make this global? *)
   abstraction_counter : AbstractionId.generator; (* TODO: make this global? *)
 }
 [@@deriving show]
@@ -84,6 +86,14 @@ let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id =
   let id, counter' = BorrowId.fresh ctx.borrow_counter in
   ({ ctx with borrow_counter = counter' }, id)
 
+let fresh_region_id (ctx : eval_ctx) : eval_ctx * RegionId.id =
+  let id, counter' = RegionId.fresh ctx.region_counter in
+  ({ ctx with region_counter = counter' }, id)
+
+let fresh_abstraction_id (ctx : eval_ctx) : eval_ctx * AbstractionId.id =
+  let id, counter' = AbstractionId.fresh ctx.abstraction_counter in
+  ({ ctx with abstraction_counter = counter' }, id)
+
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 00821668..ed5c52d3 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -4158,8 +4158,68 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
 and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
     (fid : A.FunDefId.id) (region_params : T.erased_region list)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
-    C.eval_ctx eval_result list =
-  raise Unimplemented
+    C.eval_ctx =
+  (* Retrieve the (correctly instantiated) signature *)
+  let def = C.ctx_lookup_fun_def ctx fid in
+  let sg = def.A.signature in
+  (* Generate fresh abstraction ids and create a substitution from region
+   * group ids to abstraction ids *)
+  let ctx, rg_abs_ids_bindings =
+    List.fold_left_map
+      (fun ctx rg ->
+        let ctx, abs_id = C.fresh_abstraction_id ctx in
+        (ctx, (rg.A.id, abs_id)))
+      ctx sg.regions_hierarchy
+  in
+  let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t =
+    List.fold_left
+      (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp)
+      A.RegionGroupId.Map.empty rg_abs_ids_bindings
+  in
+  let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id =
+    A.RegionGroupId.Map.find rg_id asubst_map
+  in
+  (* Generate fresh regions and their substitutions *)
+  let ctx, fresh_regions, rsubst, _ =
+    Subst.fresh_regions_with_substs sg.region_params ctx
+  in
+  (* Generate the type substitution
+   * Note that we need the substitution to map the type variables to
+   * [rty] types (not [ety]). In order to do that, we convert the
+   * type parameters to types with regions. This is possible only
+   * if those types don't contain any regions.
+   * This is a current limitation of the analysis: there is still some
+   * work to do to properly handle full type parametrization.
+   * *)
+  let rtype_params = List.map ety_no_regions_to_rty type_params in
+  let tsubst =
+    Subst.make_type_subst
+      (List.map (fun v -> v.T.index) sg.type_params)
+      rtype_params
+  in
+  (* Substitute the signature *)
+  let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in
+  (* Generate a fresh symbolic value for the result *)
+  let res_sv_ty = inst_sg.A.output in
+  let ctx, res_sv =
+    mk_fresh_symbolic_proj_comp T.RegionId.Set.empty res_sv_ty ctx
+  in
+  (* Generate the abstractions from the region groups *)
+  let generate_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) :
+      C.eval_ctx * V.abs =
+    raise Unimplemented
+  in
+  let ctx, abs =
+    List.fold_left_map generate_abs ctx inst_sg.A.regions_hierarchy
+  in
+  (* Add the abstractions to the context *)
+  let abs = List.rev (List.map (fun abs -> C.Abs abs) abs) in
+  let ctx = { ctx with C.env = List.append abs ctx.C.env } in
+  (* Synthesis *)
+  S.synthesize_local_function_call fid region_params type_params args dest
+    res_sv.V.svalue;
+  (* Return *)
+  ctx
 
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
@@ -4167,7 +4227,6 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
     (fid : A.FunDefId.id) (region_params : T.erased_region list)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
     C.eval_ctx eval_result list =
-  S.synthesize_local_function_call fid region_params type_params args dest;
   (* Retrieve the (correctly instantiated) body *)
   let def = C.ctx_lookup_fun_def ctx fid in
   match config.mode with
@@ -4175,8 +4234,11 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
       eval_local_function_call_concrete config ctx fid region_params type_params
         args dest
   | SymbolicMode ->
-      eval_local_function_call_symbolic config ctx fid region_params type_params
-        args dest
+      [
+        Ok
+          (eval_local_function_call_symbolic config ctx fid region_params
+             type_params args dest);
+      ]
 
 (** Evaluate a statement seen as a function body (auxiliary helper for
     [eval_statement]) *)
@@ -4222,6 +4284,7 @@ module Test = struct
         C.env = [];
         C.symbolic_counter = V.SymbolicValueId.generator_zero;
         C.borrow_counter = V.BorrowId.generator_zero;
+        C.region_counter = T.RegionId.generator_zero;
         C.abstraction_counter = V.AbstractionId.generator_zero;
       }
     in
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 81b0ec7e..dd89025b 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -35,6 +35,38 @@ let rec ty_substitute (rsubst : 'r1 -> 'r2)
 let erase_regions (ty : T.rty) : T.ety =
   ty_substitute (fun _ -> T.Erased) (fun vid -> T.TypeVar vid) ty
 
+(** Generate fresh regions for region variables.
+
+    Return the list of new regions and appropriate substitutions from the
+    original region variables to the fresh regions.
+  *)
+let fresh_regions_with_substs (region_vars : T.region_var list)
+    (ctx : C.eval_ctx) :
+    C.eval_ctx
+    * T.RegionId.id list
+    * (T.RegionVarId.id -> T.RegionId.id)
+    * (T.RegionVarId.id T.region -> T.RegionId.id T.region) =
+  (* Generate fresh regions *)
+  let ctx, fresh_region_ids =
+    List.fold_left_map (fun ctx _ -> C.fresh_region_id ctx) ctx region_vars
+  in
+  let fresh_regions = List.map (fun rid -> T.Var rid) fresh_region_ids in
+  (* Generate the map from region var ids to regions *)
+  let ls = List.combine region_vars fresh_region_ids in
+  let rid_map =
+    List.fold_left
+      (fun mp (k, v) -> T.RegionVarId.Map.add k.T.index v mp)
+      T.RegionVarId.Map.empty ls
+  in
+  (* Generate the substitution from region var id to region *)
+  let rid_subst id = T.RegionVarId.Map.find id rid_map in
+  (* Generate the substitution from region to region *)
+  let rsubst r =
+    match r with T.Static -> T.Static | T.Var id -> T.Var (rid_subst id)
+  in
+  (* Return *)
+  (ctx, fresh_region_ids, rid_subst, rsubst)
+
 (** Erase the regions in a type and substitute the type variables *)
 let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
     (ty : 'r T.region T.ty) : T.ety =
@@ -292,3 +324,21 @@ let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
   in
   let body = statement_substitute tsubst def.body in
   (locals, body)
+
+(** Substitute a function signature *)
+let substitute_signature (asubst : A.RegionGroupId.id -> V.AbstractionId.id)
+    (rsubst : T.RegionVarId.id -> T.RegionId.id)
+    (tsubst : T.TypeVarId.id -> T.rty) (sg : A.fun_sig) : A.inst_fun_sig =
+  let rsubst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
+    match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
+  in
+  let inputs = List.map (ty_substitute rsubst' tsubst) sg.A.inputs in
+  let output = ty_substitute rsubst' tsubst sg.A.output in
+  let subst_region_group (rg : A.region_var_group) : A.abs_region_group =
+    let id = asubst rg.A.id in
+    let regions = List.map rsubst rg.A.regions in
+    let parents = List.map asubst rg.A.parents in
+    { A.id; regions; parents }
+  in
+  let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
+  { A.regions_hierarchy; inputs; output }
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index dce40470..f317a5f9 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -70,5 +70,5 @@ let synthesize_non_local_function_call (fid : A.assumed_fun_id)
 
 let synthesize_local_function_call (fid : A.FunDefId.id)
     (region_params : T.erased_region list) (type_params : T.ety list)
-    (args : E.operand list) (dest : E.place) : unit =
+    (args : E.operand list) (dest : E.place) (res : V.symbolic_value) : unit =
   ()
diff --git a/src/Types.ml b/src/Types.ml
index 8b2b0bd9..b33df0ac 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -135,13 +135,16 @@ type 'r ty =
       }]
 (* TODO: group Bool, Char, etc. in Constant *)
 
-type sty = RegionVarId.id region ty [@@deriving show]
+type 'r gr_ty = 'r region ty [@@deriving show]
+(** Generic type with regions *)
+
+type sty = RegionVarId.id gr_ty [@@deriving show]
 (** *S*ignature types.
 
     Used in function signatures and type definitions.
  *)
 
-type rty = RegionId.id region ty [@@deriving show]
+type rty = RegionId.id gr_ty [@@deriving show]
 (** Type with *R*egions.
 
     Used during symbolic execution.
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 9741004c..4b3d8b0f 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -21,3 +21,25 @@ let ty_is_unit (ty : 'r ty) : bool =
 
 (** The unit type *)
 let mk_unit_ty : ety = Adt (Tuple, [], [])
+
+(** Convert an [ety], containing no region variables, to an [rty].
+
+    In practice, it is the identity.
+ *)
+let rec ety_no_regions_to_rty (ty : ety) : rty =
+  match ty with
+  | Adt (type_id, regions, tys) ->
+      assert (regions = []);
+      Adt (type_id, [], List.map ety_no_regions_to_rty tys)
+  | TypeVar v -> TypeVar v
+  | Bool -> Bool
+  | Char -> Char
+  | Never -> Never
+  | Integer int_ty -> Integer int_ty
+  | Str -> Str
+  | Array ty -> Array (ety_no_regions_to_rty ty)
+  | Slice ty -> Slice (ety_no_regions_to_rty ty)
+  | Ref (_, _, _) ->
+      failwith
+        "Can't convert a ref with erased regions to a ref with non-erased \
+         regions"
diff --git a/src/Values.ml b/src/Values.ml
index 0239da5e..001c0347 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -544,7 +544,7 @@ type abs = {
   parents : (AbstractionId.set_t[@opaque]);  (** The parent abstractions *)
   acc_regions : (RegionId.set_t[@opaque]);
       (** Union of the regions owned by the (transitive) parent abstractions and
-          by the current abstraction *)
+          by the current abstraction. TODO: why do we need those? *)
   regions : (RegionId.set_t[@opaque]);  (** Regions owned by this abstraction *)
   avalues : typed_avalue list;  (** The values in this abstraction *)
 }