summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/CfimAst.ml33
-rw-r--r--src/CfimOfJson.ml13
-rw-r--r--src/Contexts.ml10
-rw-r--r--src/Interpreter.ml73
-rw-r--r--src/Substitute.ml50
-rw-r--r--src/Synthesis.ml2
-rw-r--r--src/Types.ml7
-rw-r--r--src/TypesUtils.ml22
-rw-r--r--src/Values.ml2
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 *)
}