diff options
| -rw-r--r-- | src/CfimAst.ml | 33 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 13 | ||||
| -rw-r--r-- | src/Contexts.ml | 10 | ||||
| -rw-r--r-- | src/Interpreter.ml | 73 | ||||
| -rw-r--r-- | src/Substitute.ml | 50 | ||||
| -rw-r--r-- | src/Synthesis.ml | 2 | ||||
| -rw-r--r-- | src/Types.ml | 7 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 22 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
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 *) } |