From 32eadcca12c4061bd09e36a65447123da6a4826c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 18 Jan 2022 18:00:09 +0100 Subject: Update the types and deserialization following charon's updates --- src/CfimAst.ml | 25 ------------ src/CfimOfJson.ml | 93 ++++++++++++++++++++++++++++--------------- src/Contexts.ml | 2 +- src/InterpreterBorrows.ml | 7 +++- src/InterpreterBorrowsCore.ml | 55 +++---------------------- src/InterpreterStatements.ml | 31 +++++++++------ src/Modules.ml | 46 ++++++++++----------- src/Substitute.ml | 12 +++--- src/Types.ml | 27 +++++++++++++ 9 files changed, 146 insertions(+), 152 deletions(-) (limited to 'src') diff --git a/src/CfimAst.ml b/src/CfimAst.ml index ac66d1a4..6d8c03e4 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -5,8 +5,6 @@ open Expressions module FunDefId = IdGen () -module RegionGroupId = IdGen () - type var = { index : VarId.id; (** Unique variable identifier *) name : string option; @@ -26,28 +24,6 @@ type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id type assertion = { cond : operand; expected : bool } [@@deriving show] -type ('id, 'r) g_region_group = { - id : 'id; - regions : 'r list; - parents : 'id list; -} -[@@deriving show] -(** A group of regions. - - Results from a lifetime analysis: we group the regions with the same - lifetime together, and compute the hierarchy between the regions. - This is necessary to introduce the proper abstraction with the - proper constraints, when evaluating a function call in symbolic mode. -*) - -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] @@ -182,7 +158,6 @@ type fun_def = { def_id : FunDefId.id; name : name; signature : fun_sig; - divergent : bool; arg_count : int; locals : var list; body : statement; diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index a1dd0ad1..dddfbd58 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -159,6 +159,21 @@ let type_def_kind_of_json (js : json) : (T.type_def_kind, string) result = Ok (T.Enum variants) | _ -> Error "") +let region_var_group_of_json (js : json) : (T.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 = T.RegionGroupId.id_of_json id in + let* regions = list_of_json T.RegionVarId.id_of_json regions in + let* parents = list_of_json T.RegionGroupId.id_of_json parents in + Ok { T.id; regions; parents } + | _ -> Error "") + +let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result + = + combine_error_msgs js "region_var_group_of_json" + (list_of_json region_var_group_of_json js) + let type_def_of_json (js : json) : (T.type_def, string) result = combine_error_msgs js "type_def_of_json" (match js with @@ -169,13 +184,23 @@ let type_def_of_json (js : json) : (T.type_def, string) result = ("region_params", region_params); ("type_params", type_params); ("kind", kind); + ("regions_hierarchy", regions_hierarchy); ] -> let* def_id = T.TypeDefId.id_of_json def_id in let* name = name_of_json name in let* region_params = list_of_json region_var_of_json region_params in let* type_params = list_of_json type_var_of_json type_params in let* kind = type_def_kind_of_json kind in - Ok { T.def_id; name; region_params; type_params; kind } + let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in + Ok + { + T.def_id; + name; + region_params; + type_params; + kind; + regions_hierarchy; + } | _ -> Error "") let var_of_json (js : json) : (A.var, string) result = @@ -436,21 +461,6 @@ let assertion_of_json (js : json) : (A.assertion, string) result = Ok { A.cond; expected } | _ -> Error "") -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 - let* regions = list_of_json T.RegionVarId.id_of_json regions in - let* parents = list_of_json A.RegionGroupId.id_of_json parents in - Ok { A.id; regions; parents } - | _ -> Error "") - -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" (match js with @@ -570,7 +580,6 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result = ("def_id", def_id); ("name", name); ("signature", signature); - ("divergent", divergent); ("arg_count", arg_count); ("locals", locals); ("body", body); @@ -578,28 +587,44 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result = let* def_id = A.FunDefId.id_of_json def_id in let* name = name_of_json name in let* signature = fun_sig_of_json signature in - let* divergent = bool_of_json divergent in let* arg_count = int_of_json arg_count in let* locals = list_of_json var_of_json locals in let* body = statement_of_json body in - Ok { A.def_id; name; signature; divergent; arg_count; locals; body } + Ok { A.def_id; name; signature; arg_count; locals; body } | _ -> Error "") -let declaration_of_json (js : json) : (M.declaration, string) result = +let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) + (js : json) : ('id M.g_declaration_group, string) result = + combine_error_msgs js "g_declaration_group_of_json" + (match js with + | `Assoc [ ("NonRec", `List [ id ]) ] -> + let* id = id_of_json id in + Ok (M.NonRec id) + | `Assoc [ ("Rec", `List [ ids ]) ] -> + let* ids = list_of_json id_of_json ids in + Ok (M.Rec ids) + | _ -> Error "") + +let type_declaration_group_of_json (js : json) : + (M.type_declaration_group, string) result = + combine_error_msgs js "type_declaration_group_of_json" + (g_declaration_group_of_json T.TypeDefId.id_of_json js) + +let fun_declaration_group_of_json (js : json) : + (M.fun_declaration_group, string) result = + combine_error_msgs js "fun_declaration_group_of_json" + (g_declaration_group_of_json A.FunDefId.id_of_json js) + +let declaration_group_of_json (js : json) : (M.declaration_group, string) result + = combine_error_msgs js "declaration_of_json" (match js with - | `Assoc [ ("Type", id) ] -> - let* id = T.TypeDefId.id_of_json id in - Ok (M.Type id) - | `Assoc [ ("Fun", id) ] -> - let* id = A.FunDefId.id_of_json id in - Ok (M.Fun id) - | `Assoc [ ("RecTypes", ids) ] -> - let* ids = list_of_json T.TypeDefId.id_of_json ids in - Ok (M.RecTypes ids) - | `Assoc [ ("RecFuns", ids) ] -> - let* ids = list_of_json A.FunDefId.id_of_json ids in - Ok (M.RecFuns ids) + | `Assoc [ ("Type", `List [ decl ]) ] -> + let* decl = type_declaration_group_of_json decl in + Ok (M.Type decl) + | `Assoc [ ("Fun", `List [ decl ]) ] -> + let* decl = fun_declaration_group_of_json decl in + Ok (M.Fun decl) | _ -> Error "") let cfim_module_of_json (js : json) : (M.cfim_module, string) result = @@ -611,7 +636,9 @@ let cfim_module_of_json (js : json) : (M.cfim_module, string) result = ("types", types); ("functions", functions); ] -> - let* declarations = list_of_json declaration_of_json declarations in + let* declarations = + list_of_json declaration_group_of_json declarations + in let* types = list_of_json type_def_of_json types in let* functions = list_of_json fun_def_of_json functions in Ok { M.declarations; types; functions } diff --git a/src/Contexts.ml b/src/Contexts.ml index 1a9dcfc8..f7a24d27 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -137,7 +137,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) : } type type_context = { - type_defs_groups : M.types_decl_group TypeDefId.Map.t; + type_defs_groups : M.type_declaration_group TypeDefId.Map.t; type_defs : type_def list; } [@@deriving show] diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 9d332543..9331d9f3 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -432,11 +432,14 @@ 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 local_regions local_ty = + 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 child_proj = if sv.sv_id = nsv.sv_id then None else - Some (mk_aproj_borrows_from_symbolic_value local_regions nsv local_ty) + Some (mk_aproj_borrows_from_symbolic_value abs.regions nsv abs_proj_ty) in V.AEndedProjLoans child_proj in diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 455d62c3..8f6827b3 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -831,19 +831,18 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) Note that the new value [nv] with which to replace the proj_loans could be untyped: we request a typed value for sanity checking. - [subst]: takes as parameters the projection regions and the projection type + [subst]: takes as parameters the abstraction and the projection type where we perform the substitution. *) let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value) - (subst : T.RegionId.Set.t -> T.rty -> V.aproj) (ctx : C.eval_ctx) : - C.eval_ctx = + (subst : V.abs -> T.rty -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = (* Small helpers for sanity checks *) let updated = ref false in - let update local_regions local_proj_ty : V.aproj = + let update abs local_proj_ty : V.aproj = assert (not !updated); updated := true; - subst local_regions local_proj_ty + subst abs local_proj_ty in (* The visitor *) let obj = @@ -864,7 +863,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) if projections_intersect proj_ty proj_regions sv'.V.sv_ty abs.regions - then update abs.regions sv'.V.sv_ty + then update abs sv'.V.sv_ty else super#visit_aproj (Some abs) sproj) else super#visit_aproj (Some abs) sproj end @@ -875,47 +874,3 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) assert !updated; (* Return *) ctx - -(* -let proj_loans_intersect (proj_loans : T.RegionId.Set.t * V.symbolic_value) - (proj_loans' : T.RegionId.Set.t * V.symbolic_value) : bool = - let regions, sv = proj_loans in - let regions', sv' = proj_loans' in - if same_symbolic_id sv sv' then - projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions' - else false - -*) -(*(** Substitute the proj_loans based an a symbolic id *) - let substitute_aproj_loans_with_id (sv : V.symbolic_value) - (subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = - (* Small helpers for sanity checks *) - let updated = ref false in - let update regions : V.aproj = - updated := true; - subst regions - in - (* The visitor *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_abs _ abs = super#visit_abs (Some abs) abs - - method! visit_aproj abs sproj = - match sproj with - | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows - | AIgnoredProjBorrows -> - super#visit_aproj abs sproj - | AProjLoans sv' -> - let abs = Option.get abs in - if same_symbolic_id sv sv' then update abs.regions - else super#visit_aproj (Some abs) sproj - end - in - (* Apply *) - let ctx = obj#visit_eval_ctx None ctx in - (* Check that we updated the context at least once *) - assert !updated; - (* Return *) - ctx*) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index aaf7a707..85c3acb4 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -406,7 +406,7 @@ let eval_box_deref_mut_or_shared_inst_sig (region_params : T.erased_region list) let output = mk_ref_ty r ty_param ref_kind in - let regions = { A.id = abs_id; regions = [ rid ]; parents = [] } in + let regions = { T.id = abs_id; regions = [ rid ]; parents = [] } in let inst_sg = { A.regions_hierarchy = [ regions ]; inputs = [ input ]; output } @@ -509,16 +509,16 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) List.fold_left_map (fun ctx rg -> let abs_id = C.fresh_abstraction_id () in - (ctx, (rg.A.id, abs_id))) + (ctx, (rg.T.id, abs_id))) ctx sg.regions_hierarchy in - let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t = + let asubst_map : V.AbstractionId.id T.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 + (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp) + T.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 + let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id = + T.RegionGroupId.Map.find rg_id asubst_map in (* Generate fresh regions and their substitutions *) let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in @@ -559,23 +559,23 @@ let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind) in (* Auxiliary function to create one abstraction *) let create_abs (rg : A.abs_region_group) : V.abs = - let abs_id = rg.A.id in + let abs_id = rg.T.id in let parents = List.fold_left (fun s pid -> V.AbstractionId.Set.add pid s) - V.AbstractionId.Set.empty rg.A.parents + V.AbstractionId.Set.empty rg.parents in let regions = List.fold_left (fun s rid -> T.RegionId.Set.add rid s) - T.RegionId.Set.empty rg.A.regions + T.RegionId.Set.empty rg.regions in let ancestors_regions = List.fold_left (fun acc parent_id -> T.RegionId.Set.union acc (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) - T.RegionId.Set.empty rg.A.parents + T.RegionId.Set.empty rg.parents in let ancestors_regions_union_current_regions = T.RegionId.Set.union ancestors_regions regions @@ -800,9 +800,10 @@ and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) : (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) - (fid : A.FunDefId.id) (_region_params : T.erased_region list) + (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 = + assert (region_params = []); (* Retrieve the (correctly instantiated) body *) let def = C.ctx_lookup_fun_def ctx fid in let tsubst = @@ -883,6 +884,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (ctx : C.eval_ctx) (fid : A.fun_id) (inst_sg : A.inst_fun_sig) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : C.eval_ctx = + assert (region_params = []); (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in @@ -899,6 +901,11 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (fun ((arg, rty) : V.typed_value * T.rty) -> arg.V.ty = Subst.erase_regions rty) args_with_rtypes); + (* Check that the input arguments don't contain symbolic values that can't + * 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; (* 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/Modules.ml b/src/Modules.ml index e4cb06c1..e437ad0a 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -1,55 +1,55 @@ open Types open CfimAst +type 'id g_declaration_group = NonRec of 'id | Rec of 'id list +[@@deriving show] + +type type_declaration_group = TypeDefId.id g_declaration_group [@@deriving show] + +type fun_declaration_group = FunDefId.id g_declaration_group [@@deriving show] + (** Module declaration *) -type declaration = - | Type of TypeDefId.id - | Fun of FunDefId.id - | RecTypes of TypeDefId.id list - | RecFuns of FunDefId.id list +type declaration_group = + | Type of type_declaration_group + | Fun of fun_declaration_group +[@@deriving show] type cfim_module = { - declarations : declaration list; + declarations : declaration_group list; types : type_def list; functions : fun_def list; } (** CFIM module *) -type 'id decl_group = NonRec of 'id | Rec of 'id list [@@deriving show] - -type types_decl_group = TypeDefId.id decl_group [@@deriving show] - -type funs_decl_group = FunDefId.id decl_group [@@deriving show] - (** Split a module's declarations between types and functions *) -let split_declarations (decls : declaration list) : - types_decl_group list * funs_decl_group list = +let split_declarations (decls : declaration_group list) : + type_declaration_group list * fun_declaration_group list = let rec split decls = match decls with | [] -> ([], []) | d :: decls' -> ( let types, funs = split decls' in match d with - | Type id -> (NonRec id :: types, funs) - | Fun id -> (types, NonRec id :: funs) - | RecTypes ids -> (Rec ids :: types, funs) - | RecFuns ids -> (types, Rec ids :: funs)) + | Type decl -> (decl :: types, funs) + | Fun decl -> (types, decl :: funs)) in split decls (** Split a module's declarations into two maps from type/fun ids to declaration groups. *) -let split_declarations_to_group_maps (decls : declaration list) : - types_decl_group TypeDefId.Map.t * funs_decl_group FunDefId.Map.t = +let split_declarations_to_group_maps (decls : declaration_group list) : + type_declaration_group TypeDefId.Map.t + * fun_declaration_group FunDefId.Map.t = let module G (M : Map.S) = struct - let add_group (map : M.key decl_group M.t) (group : M.key decl_group) : - M.key decl_group M.t = + let add_group (map : M.key g_declaration_group M.t) + (group : M.key g_declaration_group) : M.key g_declaration_group M.t = match group with | NonRec id -> M.add id group map | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids - let create_map (groups : M.key decl_group list) : M.key decl_group M.t = + let create_map (groups : M.key g_declaration_group list) : + M.key g_declaration_group M.t = List.fold_left add_group M.empty groups end in let types, funs = split_declarations decls in diff --git a/src/Substitute.ml b/src/Substitute.ml index 62a737ad..9db58812 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -323,7 +323,7 @@ let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety) (locals, body) (** Substitute a function signature *) -let substitute_signature (asubst : A.RegionGroupId.id -> V.AbstractionId.id) +let substitute_signature (asubst : T.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 = @@ -331,11 +331,11 @@ let substitute_signature (asubst : A.RegionGroupId.id -> V.AbstractionId.id) 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 } + let subst_region_group (rg : T.region_var_group) : A.abs_region_group = + let id = asubst rg.id in + let regions = List.map rsubst rg.regions in + let parents = List.map asubst rg.parents in + { 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/Types.ml b/src/Types.ml index b410c5a6..44855eb2 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -14,6 +14,8 @@ module RegionVarId = IdGen () module RegionId = IdGen () (** Region ids. Used for symbolic executions. *) +module RegionGroupId = IdGen () + type ('id, 'name) indexed_var = { index : 'id; (** Unique index identifying the variable *) name : 'name; (** Variable name *) @@ -46,6 +48,28 @@ type 'rid region = *) type erased_region = Erased [@@deriving show] +type ('id, 'r) g_region_group = { + id : 'id; + regions : 'r list; + parents : 'id list; +} +[@@deriving show] +(** A group of regions. + + Results from a lifetime analysis: we group the regions with the same + lifetime together, and compute the hierarchy between the regions. + This is necessary to introduce the proper abstraction with the + proper constraints, when evaluating a function call in symbolic mode. +*) + +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 integer_type = | Isize | I8 @@ -174,5 +198,8 @@ type type_def = { region_params : region_var list; type_params : type_var list; kind : type_def_kind; + regions_hierarchy : region_var_groups; + (** Stored the hierarchy between the regions (which regions have the same lifetime, + what is the hierarchy between the lifetimes) *) } [@@deriving show] -- cgit v1.2.3