diff options
Diffstat (limited to '')
| -rw-r--r-- | src/CfimAst.ml | 4 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 10 | ||||
| -rw-r--r-- | src/Interpreter.ml | 15 | ||||
| -rw-r--r-- | src/Print.ml | 72 | ||||
| -rw-r--r-- | src/Substitute.ml | 4 | ||||
| -rw-r--r-- | src/Types.ml | 16 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
7 files changed, 86 insertions, 37 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 64151a48..192638cf 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -28,8 +28,8 @@ type fun_sig = { region_params : region_var list; num_early_bound_regions : int; type_params : type_var list; - inputs : rty list; - output : rty; + inputs : sty list; + output : sty; } [@@deriving show] diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 0a7eeb78..3494f004 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -124,8 +124,8 @@ let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) : Ok (T.Ref (region, ty, ref_kind)) | _ -> Error "") -let rty_of_json (js : json) : (T.rty, string) result = - combine_error_msgs js "rty_of_json" (ty_of_json region_of_json js) +let sty_of_json (js : json) : (T.sty, string) result = + combine_error_msgs js "sty_of_json" (ty_of_json region_of_json js) let ety_of_json (js : json) : (T.ety, string) result = combine_error_msgs js "ety_of_json" (ty_of_json erased_region_of_json js) @@ -135,7 +135,7 @@ let field_of_json (js : json) : (T.field, string) result = (match js with | `Assoc [ ("name", name); ("ty", ty) ] -> let* name = string_of_json name in - let* ty = rty_of_json ty in + let* ty = sty_of_json ty in Ok { T.field_name = name; field_ty = ty } | _ -> Error "") @@ -450,8 +450,8 @@ 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* type_params = list_of_json type_var_of_json type_params in - let* inputs = list_of_json rty_of_json inputs in - let* output = rty_of_json output in + let* inputs = list_of_json sty_of_json inputs in + let* output = sty_of_json output in Ok { A.region_params; diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 8b929b0f..9555b0ca 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -584,8 +584,12 @@ exception FoundOuter of outer_borrows_or_abs Note that the two abstractions have different views (in terms of regions) of the symbolic value (hence the two region types). *) -let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty) - (rset2 : V.RegionId.set_t) : bool = +let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t) + (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool = + 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 + in match (ty1, ty2) with | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false | T.Integer int_ty1, T.Integer int_ty2 -> @@ -603,8 +607,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty) let regions = List.combine regions1 regions2 in let tys = List.combine tys1 tys2 in List.exists - (fun (r1, r2) -> - V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem r2 rset2) + (fun (r1, r2) -> region_in_set r1 rset1 && region_in_set r2 rset2) regions || List.exists (fun (ty1, ty2) -> projections_intersect ty1 rset1 ty2 rset2) @@ -616,7 +619,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty) assert (kind1 = kind2); (* The projections intersect if the borrows intersect or their contents * intersect *) - (V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem r2 rset2) + (region_in_set r1 rset1 && region_in_set r2 rset2) || projections_intersect ty1 rset1 ty2 rset2 | _ -> failwith "Unreachable" @@ -628,7 +631,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty) map borrows to regions - or to interpret the borrows as belonging to some regions...) *) -let apply_proj_borrows (regions : V.RegionId.set_t) (v : V.typed_value) +let apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : V.typed_avalue = (* Sanity check - TODO: move this elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) diff --git a/src/Print.ml b/src/Print.ml index e9ba4730..bf07e57e 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -16,6 +16,12 @@ module Types = struct | Some name -> name | None -> T.RegionVarId.to_string rv.index + let region_var_id_to_string (rid : T.RegionVarId.id) : string = + "rv@" ^ T.RegionVarId.to_string rid + + let region_id_to_string (rid : T.RegionId.id) : string = + "r@" ^ T.RegionId.to_string rid + let region_to_string (rid_to_string : 'rid -> string) (r : 'rid T.region) : string = match r with Static -> "'static" | Var rid -> rid_to_string rid @@ -33,9 +39,11 @@ module Types = struct type_def_id_to_string : T.TypeDefId.id -> string; } - type etype_formatter = T.erased_region type_formatter + type stype_formatter = T.RegionVarId.id T.region type_formatter - type rtype_formatter = T.RegionVarId.id T.region type_formatter + type rtype_formatter = T.RegionId.id T.region type_formatter + + type etype_formatter = T.erased_region type_formatter let integer_type_to_string = function | T.Isize -> "isize" @@ -87,9 +95,14 @@ module Types = struct else if List.length regions + List.length types > 0 then "<" ^ params ^ ">" else "" - let rty_to_string fmt (ty : T.rty) : string = ty_to_string fmt ty + let sty_to_string (fmt : stype_formatter) (ty : T.sty) : string = + ty_to_string fmt ty + + let rty_to_string (fmt : rtype_formatter) (ty : T.rty) : string = + ty_to_string fmt ty - let ety_to_string fmt (ty : T.ety) : string = ty_to_string fmt ty + let ety_to_string (fmt : etype_formatter) (ty : T.ety) : string = + ty_to_string fmt ty let field_to_string fmt (f : T.field) : string = f.field_name ^ " : " ^ ty_to_string fmt f.field_ty @@ -148,7 +161,8 @@ module PT = Types (* local module *) (** Pretty-printing for values *) module Values = struct type value_formatter = { - r_to_string : T.RegionVarId.id -> string; + rvar_to_string : T.RegionVarId.id -> string; + r_to_string : T.RegionId.id -> string; type_var_id_to_string : T.TypeVarId.id -> string; type_def_id_to_string : T.TypeDefId.id -> string; adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string; @@ -171,6 +185,13 @@ module Values = struct PT.type_def_id_to_string = fmt.type_def_id_to_string; } + let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter = + { + PT.r_to_string = PT.region_to_string fmt.rvar_to_string; + PT.type_var_id_to_string = fmt.type_var_id_to_string; + PT.type_def_id_to_string = fmt.type_def_id_to_string; + } + let var_id_to_string (id : V.VarId.id) : string = "var@" ^ V.VarId.to_string id @@ -191,14 +212,11 @@ module Values = struct let symbolic_value_to_string (fmt : PT.rtype_formatter) (sv : V.symbolic_value) : string = - symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.ty_to_string fmt sv.sv_ty - - let region_id_to_string (rid : V.RegionId.id) : string = - "r@" ^ V.RegionId.to_string rid + symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.rty_to_string fmt sv.sv_ty let symbolic_proj_comp_to_string (fmt : PT.rtype_formatter) (sp : V.symbolic_proj_comp) : string = - let regions = V.RegionId.set_to_string sp.rset_ended in + let regions = T.RegionId.set_to_string sp.rset_ended in "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")" let symbolic_value_proj_to_string (fmt : value_formatter) @@ -411,7 +429,7 @@ module Values = struct ^ "{parents=" ^ V.AbstractionId.set_to_string abs.parents ^ "}" ^ "{regions=" - ^ V.RegionId.set_to_string abs.regions + ^ T.RegionId.set_to_string abs.regions ^ "}" ^ " {\n" ^ avs ^ "\n}" end @@ -465,8 +483,10 @@ module Contexts = struct Some fields let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter = - (* We shouldn't use r_to_string *) - let r_to_string _ = failwith "Unexpected use of r_to_string" in + (* We shouldn't use rvar_to_string *) + let rvar_to_string r = failwith "Unexpected use of rvar_to_string" in + let r_to_string r = PT.region_id_to_string r in + let type_var_id_to_string vid = let v = C.lookup_type_var ctx vid in v.name @@ -484,6 +504,7 @@ module Contexts = struct in let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in { + rvar_to_string; r_to_string; type_var_id_to_string; type_def_id_to_string; @@ -527,7 +548,8 @@ module PC = Contexts (* local module *) (** Pretty-printing for contexts (generic functions) *) module CfimAst = struct type ast_formatter = { - r_to_string : T.RegionVarId.id -> string; + rvar_to_string : T.RegionVarId.id -> string; + r_to_string : T.RegionId.id -> string; type_var_id_to_string : T.TypeVarId.id -> string; type_def_id_to_string : T.TypeDefId.id -> string; adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string; @@ -541,6 +563,7 @@ module CfimAst = struct let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter = { + PV.rvar_to_string = fmt.rvar_to_string; PV.r_to_string = fmt.r_to_string; PV.type_var_id_to_string = fmt.type_var_id_to_string; PV.type_def_id_to_string = fmt.type_def_id_to_string; @@ -563,6 +586,13 @@ module CfimAst = struct PT.type_def_id_to_string = fmt.type_def_id_to_string; } + let ast_to_stype_formatter (fmt : ast_formatter) : PT.stype_formatter = + { + PT.r_to_string = PT.region_to_string fmt.rvar_to_string; + PT.type_var_id_to_string = fmt.type_var_id_to_string; + PT.type_def_id_to_string = fmt.type_def_id_to_string; + } + let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def list) : T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string = fun def_id opt_variant_id field_id -> @@ -581,6 +611,7 @@ module CfimAst = struct PT.name_to_string def.name in { + rvar_to_string = ctx_fmt.PV.rvar_to_string; r_to_string = ctx_fmt.PV.r_to_string; type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string; type_def_id_to_string = ctx_fmt.PV.type_def_id_to_string; @@ -790,6 +821,8 @@ module CfimAst = struct (indent_incr : string) (def : A.fun_def) : string = let rty_fmt = ast_to_rtype_formatter fmt in let rty_to_string = PT.rty_to_string rty_fmt in + let sty_fmt = ast_to_stype_formatter fmt in + let sty_to_string = PT.sty_to_string sty_fmt in let ety_fmt = ast_to_etype_formatter fmt in let ety_to_string = PT.ety_to_string ety_fmt in let sg = def.signature in @@ -814,7 +847,7 @@ module CfimAst = struct let args = List.combine inputs sg.inputs in let args = List.map - (fun (var, rty) -> var_to_string var ^ " : " ^ rty_to_string rty) + (fun (var, rty) -> var_to_string var ^ " : " ^ sty_to_string rty) args in let args = String.concat ", " args in @@ -822,7 +855,7 @@ module CfimAst = struct (* Return type *) let ret_ty = sg.output in let ret_ty = - if TU.ty_is_unit ret_ty then "" else " -> " ^ rty_to_string ret_ty + if TU.ty_is_unit ret_ty then "" else " -> " ^ sty_to_string ret_ty in (* All the locals (with erased regions) *) @@ -863,10 +896,14 @@ module Module = struct with the variables local to a function's definition *) let def_ctx_to_ast_formatter (type_context : T.type_def list) (fun_context : A.fun_def list) (def : A.fun_def) : PA.ast_formatter = - let r_to_string vid = + let rvar_to_string vid = let var = T.RegionVarId.nth def.signature.region_params vid in PT.region_var_to_string var in + let r_to_string vid = + (* TODO: we might want something more informative *) + PT.region_id_to_string vid + in let type_var_id_to_string vid = let var = T.TypeVarId.nth def.signature.type_params vid in PT.type_var_to_string var @@ -891,6 +928,7 @@ module Module = struct in let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_context in { + rvar_to_string; r_to_string; type_var_id_to_string; type_def_id_to_string; diff --git a/src/Substitute.ml b/src/Substitute.ml index 78109913..9adbf4a6 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -37,8 +37,8 @@ let erase_regions (ty : T.rty) : T.ety = (** Erase the regions in a type and substitute the type variables *) let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety) - (ty : T.rty) : T.ety = - let rsubst (_ : T.RegionVarId.id T.region) : T.erased_region = T.Erased in + (ty : 'r T.region T.ty) : T.ety = + let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in ty_substitute rsubst tsubst ty (** Create a type substitution from a list of type variable ids and a list of diff --git a/src/Types.ml b/src/Types.ml index 59a512eb..c9eeff7e 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -9,6 +9,10 @@ module VariantId = IdGen () module FieldId = IdGen () module RegionVarId = IdGen () +(** Region variable ids. Used in function signatures. *) + +module RegionId = IdGen () +(** Region ids. Used for symbolic executions. *) type ('id, 'name) indexed_var = { index : 'id; (** Unique index identifying the variable *) @@ -79,19 +83,25 @@ type 'r ty = [@@deriving show] (* TODO: group Bool, Char, etc. in Constant *) -type rty = RegionVarId.id region ty [@@deriving show] -(** Type with *R*egions. +type sty = RegionVarId.id region ty [@@deriving show] +(** *S*ignature types. Used in function signatures and type definitions. *) +type rty = RegionId.id region ty [@@deriving show] +(** Type with *R*egions. + + Used during symbolic execution. + *) + type ety = erased_region ty [@@deriving show] (** Type with *E*rased regions. Used in function bodies, "general" value types, etc. *) -type field = { field_name : string; field_ty : rty } [@@deriving show] +type field = { field_name : string; field_ty : sty } [@@deriving show] type variant = { variant_name : string; fields : field list } [@@deriving show] diff --git a/src/Values.ml b/src/Values.ml index 4b5b9b4e..96feb814 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -13,8 +13,6 @@ module SymbolicValueId = IdGen () module AbstractionId = IdGen () -module RegionId = IdGen () - (** A variable *) type big_int = Z.t |