summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Assumed.ml7
-rw-r--r--src/CfimAstUtils.ml10
-rw-r--r--src/ExtractAst.ml2
-rw-r--r--src/Pure.ml31
-rw-r--r--src/PureToExtract.ml290
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
+*)