diff options
| -rw-r--r-- | src/Assumed.ml | 7 | ||||
| -rw-r--r-- | src/CfimAstUtils.ml | 10 | ||||
| -rw-r--r-- | src/ExtractAst.ml | 2 | ||||
| -rw-r--r-- | src/Pure.ml | 31 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 290 |
5 files changed, 245 insertions, 95 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml index 0e05e5b9..9664fbc4 100644 --- a/src/Assumed.ml +++ b/src/Assumed.ml @@ -89,3 +89,10 @@ let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list = (BoxDeref, box_deref_shared_sig); (BoxDerefMut, box_deref_mut_sig); ] + +let assumed_names : (A.assumed_fun_id * Identifiers.name) list = + [ + (BoxNew, [ "alloc"; "boxed"; "Box"; "new" ]); + (BoxDeref, [ "core"; "ops"; "deref"; "Deref"; "deref" ]); + (BoxDerefMut, [ "core"; "ops"; "deref"; "DerefMut"; "deref_mut" ]); + ] diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml index ae6665d4..902156f2 100644 --- a/src/CfimAstUtils.ml +++ b/src/CfimAstUtils.ml @@ -29,6 +29,16 @@ let lookup_fun_sig (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) : in sg +let lookup_fun_name (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) : + Identifiers.name = + match fun_id with + | Local id -> (FunDefId.Map.find id fun_defs).name + | Assumed aid -> + let _, sg = + List.find (fun (aid', _) -> aid = aid') Assumed.assumed_names + in + sg + (** Small utility: list the transitive parents of a region var group. We don't do that in an efficient manner, but it doesn't matter. diff --git a/src/ExtractAst.ml b/src/ExtractAst.ml index a80d3d08..da88dc04 100644 --- a/src/ExtractAst.ml +++ b/src/ExtractAst.ml @@ -2,6 +2,8 @@ This AST is voluntarily as simple as possible, so that the extraction can focus on pretty-printing and on the syntax specific to the different provers. + + TODO: we don't use this... *) type constant_value = Pure.constant_value diff --git a/src/Pure.ml b/src/Pure.ml index 8c416ed1..139b4c58 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -5,7 +5,7 @@ module E = Expressions module A = CfimAst module TypeDefId = T.TypeDefId module TypeVarId = T.TypeVarId -module RegionId = T.RegionId +module RegionGroupId = T.RegionGroupId module VariantId = T.VariantId module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId @@ -18,6 +18,8 @@ module SynthPhaseId = IdGen () module VarId = IdGen () (** Pay attention to the fact that we also define a [VarId] module in Values *) +type integer_type = T.integer_type [@@deriving show, ord] + type assumed_ty = | Result (** The assumed types for the pure AST. @@ -45,7 +47,7 @@ class ['self] iter_ty_base = method visit_type_id : 'env -> type_id -> unit = fun _ _ -> () - method visit_integer_type : 'env -> T.integer_type -> unit = fun _ _ -> () + method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> () end (** Ancestor for map visitor for [ty] *) @@ -57,7 +59,7 @@ class ['self] map_ty_base = method visit_type_id : 'env -> type_id -> type_id = fun _ id -> id - method visit_integer_type : 'env -> T.integer_type -> T.integer_type = + method visit_integer_type : 'env -> integer_type -> integer_type = fun _ ity -> ity end @@ -73,10 +75,10 @@ type ty = | TypeVar of TypeVarId.id | Bool | Char - | Integer of T.integer_type + | Integer of integer_type | Str - | Array of ty (* TODO: there should be a constant with the array *) - | Slice of ty + | Array of ty (* TODO: this should be an assumed type?... *) + | Slice of ty (* TODO: this should be an assumed type?... *) [@@deriving show, visitors @@ -346,14 +348,16 @@ and typed_rvalue = { value : rvalue; ty : ty } polymorphic = false; }] -type unop = Not | Neg of T.integer_type [@@deriving show] +type unop = Not | Neg of integer_type [@@deriving show] + +(* TODO: redefine assumed_fun_id (we need to get rid of box! *) type fun_id = | Regular of A.fun_id * T.RegionGroupId.id option (** Backward id: `Some` if the function is a backward function, `None` if it is a forward function *) | Unop of unop - | Binop of E.binop * T.integer_type + | Binop of E.binop * integer_type [@@deriving show] (** Meta-information stored in the AST *) @@ -366,7 +370,7 @@ class ['self] iter_expression_base = method visit_meta : 'env -> meta -> unit = fun _ _ -> () - method visit_integer_type : 'env -> T.integer_type -> unit = fun _ _ -> () + method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> () method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> () @@ -382,7 +386,7 @@ class ['self] map_expression_base = method visit_meta : 'env -> meta -> meta = fun _ x -> x - method visit_integer_type : 'env -> T.integer_type -> T.integer_type = + method visit_integer_type : 'env -> integer_type -> integer_type = fun _ x -> x method visit_scalar_value : 'env -> scalar_value -> scalar_value = @@ -400,7 +404,7 @@ class virtual ['self] reduce_expression_base = method visit_meta : 'env -> meta -> 'a = fun _ _ -> self#zero - method visit_integer_type : 'env -> T.integer_type -> 'a = + method visit_integer_type : 'env -> integer_type -> 'a = fun _ _ -> self#zero method visit_scalar_value : 'env -> scalar_value -> 'a = @@ -418,7 +422,7 @@ class virtual ['self] mapreduce_expression_base = method visit_meta : 'env -> meta -> meta * 'a = fun _ x -> (x, self#zero) - method visit_integer_type : 'env -> T.integer_type -> T.integer_type * 'a = + method visit_integer_type : 'env -> integer_type -> integer_type * 'a = fun _ x -> (x, self#zero) method visit_scalar_value : 'env -> scalar_value -> scalar_value * 'a = @@ -496,8 +500,7 @@ and call = { and switch_body = | If of texpression * texpression - | SwitchInt of - T.integer_type * (scalar_value * texpression) list * texpression + | SwitchInt of integer_type * (scalar_value * texpression) list * texpression | Match of match_branch list (* TODO: we could (should?) merge SwitchInt and Match *) diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 4b7b5ad8..b9f5a9a1 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -1,103 +1,231 @@ -(** This module is used to transform the pure ASTs to ASTs ready for extraction *) +(** This module is used to extract the pure ASTs to various theorem provers. + It defines utilities and helpers to make the work as easy as possible: + we try to factorize as much as possible the different extractions to the + backends we target. + *) open Errors open Pure -open CfimAstUtils -module Id = Identifiers -module T = Types -module V = Values -module E = Expressions -module A = CfimAst -module M = Modules -module S = SymbolicAst -module TA = TypesAnalysis -module L = Logging -module PP = PrintPure +open TranslateCore +module C = Contexts +module RegionVarId = T.RegionVarId (** The local logger *) let log = L.pure_to_extract_log -type name = - | FunName of A.FunDefId.id * T.RegionVarId.id option - | TypeName of T.TypeDefId.id -[@@deriving show, ord] - -let name_to_string (n : name) : string = show_name n +type extraction_ctx = { + type_context : C.type_context; + fun_context : C.fun_context; +} +(** Extraction context. -module NameOrderedType = struct - type t = name - - let compare = compare_name + Note that the extraction context contains information coming from the + CFIM AST (not only the pure AST). This is useful for naming, for instance: + we use the region information to generate the names of the backward + functions, etc. + *) - let to_string = name_to_string +(** We use identifiers to look for name clashes *) +type id = + | FunId of FunDefId.id * RegionGroupId.id option + | TypeId of TypeDefId.id + | VarId of VarId.id + | UnknownId + (** Used for stored various strings like keywords, definitions which + should always be in context, etc. and which can't be linked to one + of the above. + *) +[@@deriving show, ord] - let pp_t = pp_name +type region_group_info = { + id : RegionGroupId.id; + (** The id of the region group. + Note that a simple way of generating unique names for backward + functions is to use the region group ids. + *) + region_names : string option list; + (** The names of the region variables included in this group. + Note that names are not always available... + *) +} - let show_t = show_name -end +type name = Identifiers.name -module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType) -(** Notice that we use the *injective* map to map identifiers to names. +type name_formatter = { + bool_name : string; + char_name : string; + int_name : integer_type -> string; + str_name : string; + type_name : name -> string; (** Provided a basename, compute a type name. *) + fun_name : A.fun_id -> name -> int -> region_group_info option -> string; + (** Inputs: + - function id: this is especially useful to identify whether the + function is an assumed function or a local function + - function basename + - number of region groups + - region group information in case of a backward function + (`None` if forward function) + *) + var_basename : name -> string; + (** Generates a variable basename. - Of course, even if those names (which are string lists) don't collide, - when converting them to strings we can still introduce collisions: we - check that later. + Note that once the formatter generated a basename, we add an index + if necessary to prevent name clashes. + *) +} +(** A name formatter's role is to come up with name suggestions. + For instance, provided some information about a function (its basename, + information about the region group, etc.) it should come up with an + appropriate name for the forward/backward function. - Note that we use injective maps for sanity: though we write the name - generation with collision in mind, it is always good to have such checks. + It can of course apply many transformations, like changing to camel case/ + snake case, adding prefixes/suffixes, etc. *) -let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) : - Id.name = - let sg = fdef.signature in - (* General function to generate a suffix for a region group - * (i.e., an abstraction)*) - let rg_to_string (rg : T.region_var_group) : string = - (* We are just a little bit smart: - - if there is exactly one region id in the region group and this region - has a name, we use this name - - otherwise, we use the region number (note that region names shouldn't - start with numbers) - *) - match rg.T.regions with - | [ rid ] -> ( - let rvar = T.RegionVarId.nth sg.region_params rid in - match rvar.name with - | None -> T.RegionGroupId.to_string rg.T.id - | Some name -> name) - | _ -> T.RegionGroupId.to_string rg.T.id - in +let compute_type_def_name (fmt : name_formatter) (def : type_def) : string = + fmt.type_name def.name + +(** A helper function: generates a function suffix from a region group + information. + TODO: move all those helpers. +*) +let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) + : string = (* There are several cases: - - this is a forward function: we add "_fwd" - - this is a backward function: - - this function has one backward function: we add "_back" + - [rg] is `Some`: this is a forward function: + - if there are no region groups (i.e., no backward functions) we don't + add any suffix + - if there are region gruops, we add "_fwd" + - [rg] is `None`: this is a backward function: + - this function has one region group: we add "_back" - this function has several backward function: we add "_back" and an additional suffix to identify the precise backward function *) - let suffix = - match bid with - | None -> "_fwd" - | Some bid -> ( - match sg.regions_hierarchy with - | [] -> - failwith "Unreachable" - (* we can't get there if we ask for a back function *) - | [ _ ] -> - (* Exactly one backward function *) - "_back" - | _ -> - (* Several backward functions *) - let rg = T.RegionGroupId.nth sg.regions_hierarchy bid in - "_back" ^ rg_to_string rg) - in - (* Final name *) - let rec add_to_last (n : Id.name) : Id.name = - match n with - | [] -> failwith "Unreachable" - | [ x ] -> [ x ^ suffix ] - | x :: n -> x :: add_to_last n + match rg with + | None -> if num_region_groups = 0 then "" else "_fwd" + | Some rg -> + assert (num_region_groups > 0); + if num_region_groups = 1 then (* Exactly one backward function *) + "_back" + else if + (* Several region groups/backward functions: + - if all the regions in the group have names, we use those names + - otherwise we use an index + *) + List.for_all Option.is_some rg.region_names + then + (* Concatenate the region names *) + "_back" ^ String.concat "" (List.map Option.get rg.region_names) + else (* Use the region index *) + "_back" ^ RegionGroupId.to_string rg.id + +(** Extract information from a function, and give this information to a + [name_formatter] to generate a function's name. + + Note that we need region information coming from CFIM (when generating + the name for a backward function, we try to use the names of the regions + to + *) +let compute_fun_def_name (ctx : extraction_ctx) (fmt : name_formatter) + (fun_id : A.fun_id) (rg_id : RegionGroupId.id option) : string = + (* Lookup the function CFIM signature (we need the region information) *) + let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in + let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in + (* Compute the regions information *) + let num_region_groups = List.length sg.regions_hierarchy in + let rg_info = + match rg_id with + | None -> None + | Some rg_id -> + let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in + let regions = + List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions + in + let region_names = + List.map (fun (r : T.region_var) -> r.name) regions + in + Some { id = rg.id; region_names } in - add_to_last fdef.name + fmt.fun_name fun_id basename num_region_groups rg_info + +(* + let name_to_string (n : name) : string = show_name n + + module NameOrderedType = struct + type t = name + + let compare = compare_name + + let to_string = name_to_string + + let pp_t = pp_name + + let show_t = show_name + end + + module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType) + (** Notice that we use the *injective* map to map identifiers to names. + + Of course, even if those names (which are string lists) don't collide, + when converting them to strings we can still introduce collisions: we + check that later. + + Note that we use injective maps for sanity: though we write the name + generation with collision in mind, it is always good to have such checks. + *)*) + +(*let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) : + Id.name = + let sg = fdef.signature in + (* General function to generate a suffix for a region group + * (i.e., an abstraction)*) + let rg_to_string (rg : T.region_var_group) : string = + (* We are just a little bit smart: + - if there is exactly one region id in the region group and this region + has a name, we use this name + - otherwise, we use the region number (note that region names shouldn't + start with numbers) + *) + match rg.T.regions with + | [ rid ] -> ( + let rvar = T.RegionVarId.nth sg.region_params rid in + match rvar.name with + | None -> T.RegionGroupId.to_string rg.T.id + | Some name -> name) + | _ -> T.RegionGroupId.to_string rg.T.id + in + (* There are several cases: + - this is a forward function: we add "_fwd" + - this is a backward function: + - this function has one backward function: we add "_back" + - this function has several backward function: we add "_back" and an + additional suffix to identify the precise backward function + *) + let suffix = + match bid with + | None -> "_fwd" + | Some bid -> ( + match sg.regions_hierarchy with + | [] -> + failwith "Unreachable" + (* we can't get there if we ask for a back function *) + | [ _ ] -> + (* Exactly one backward function *) + "_back" + | _ -> + (* Several backward functions *) + let rg = T.RegionGroupId.nth sg.regions_hierarchy bid in + "_back" ^ rg_to_string rg) + in + (* Final name *) + let rec add_to_last (n : Id.name) : Id.name = + match n with + | [] -> failwith "Unreachable" + | [ x ] -> [ x ^ suffix ] + | x :: n -> x :: add_to_last n + in + add_to_last fdef.name -(** Generates a name for a type (simply reuses the name in the definition) *) -let translate_type_name (def : T.type_def) : Id.name = def.T.name + (** Generates a name for a type (simply reuses the name in the definition) *) + let translate_type_name (def : T.type_def) : Id.name = def.T.name +*) |