From e2d7496f86c4e7fd6ecdf63a6409a8a2b29eca1d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 13 Nov 2023 13:23:48 +0100 Subject: [PATCH] Remove regions_hierarchy.rs --- charon-ml/src/Collections.ml | 6 + charon-ml/src/GAst.ml | 5 +- charon-ml/src/GAstOfJson.ml | 31 +- charon-ml/src/GAstUtils.ml | 14 +- charon-ml/src/LlbcOfJson.ml | 1 - charon-ml/src/PrintTypes.ml | 2 +- charon-ml/src/Types.ml | 112 ++- charon-ml/src/TypesUtils.ml | 13 + charon/src/driver.rs | 5 - charon/src/lib.rs | 1 - charon/src/regions_hierarchy.rs | 866 --------------------- charon/src/translate_functions_to_ullbc.rs | 2 - charon/src/translate_types.rs | 3 - charon/src/types.rs | 13 - charon/src/types_utils.rs | 1 - 15 files changed, 124 insertions(+), 951 deletions(-) delete mode 100644 charon/src/regions_hierarchy.rs diff --git a/charon-ml/src/Collections.ml b/charon-ml/src/Collections.ml index 89133a54..2c0cdb13 100644 --- a/charon-ml/src/Collections.ml +++ b/charon-ml/src/Collections.ml @@ -112,6 +112,10 @@ module List = struct f (); iter_times (n - 1) f) else () + + let filter_mapi (f : int -> 'a -> 'b option) (l : 'a list) : 'b list = + let l = mapi f l in + filter_map (fun x -> x) l end module type OrderedType = sig @@ -149,6 +153,7 @@ module type Map = sig val add_list : (key * 'a) list -> 'a t -> 'a t val of_list : (key * 'a) list -> 'a t + val keys : 'a t -> key list val values : 'a t -> 'a list (** "Simple" pretty printing function. @@ -192,6 +197,7 @@ module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct let add_list bl m = List.fold_left (fun s (key, e) -> add key e s) m bl let of_list bl = add_list bl empty + let keys m = List.map fst (bindings m) let values m = List.map snd (bindings m) let to_string indent_opt a_to_string m = diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml index 7ee1ecad..0116e598 100644 --- a/charon-ml/src/GAst.ml +++ b/charon-ml/src/GAst.ml @@ -32,14 +32,14 @@ type var = { class ['self] iter_ast_base = object (_self : 'self) inherit [_] iter_rvalue - method visit_meta : 'env -> meta -> unit = fun _ _ -> () + inherit! [_] iter_predicates end (** Ancestor the AST map visitors *) class ['self] map_ast_base = object (_self : 'self) inherit [_] map_rvalue - method visit_meta : 'env -> meta -> meta = fun _ x -> x + inherit! [_] map_predicates end (* Below: the types need not be mutually recursive, but it makes it easier @@ -97,7 +97,6 @@ type fun_sig = { parent_params_info : params_info option; inputs : ty list; output : ty; - regions_hierarchy : region_groups; } [@@deriving show] diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 325ae0e8..1fdc32bc 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -495,8 +495,8 @@ let trait_clause_of_json (id_to_file : id_to_file_map) (js : json) : let* clause_id = T.TraitClauseId.id_of_json clause_id in let* meta = option_of_json (meta_of_json id_to_file) meta in let* trait_id = T.TraitDeclId.id_of_json trait_id in - let* generics = generic_args_of_json generics in - Ok ({ clause_id; meta; trait_id; generics } : T.trait_clause) + let* clause_generics = generic_args_of_json generics in + Ok ({ clause_id; meta; trait_id; clause_generics } : T.trait_clause) | _ -> Error "") let generic_params_of_json (id_to_file : id_to_file_map) (js : json) : @@ -589,7 +589,6 @@ let type_decl_of_json (id_to_file : id_to_file_map) (js : json) : ("generics", generics); ("preds", preds); ("kind", kind); - ("regions_hierarchy", regions_hierarchy); ] -> let* def_id = T.TypeDeclId.id_of_json def_id in let* meta = meta_of_json id_to_file meta in @@ -598,18 +597,7 @@ let type_decl_of_json (id_to_file : id_to_file_map) (js : json) : let* generics = generic_params_of_json id_to_file generics in let* preds = predicates_of_json preds in let* kind = type_decl_kind_of_json id_to_file kind in - let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in - Ok - { - T.def_id; - meta; - is_local; - name; - generics; - preds; - kind; - regions_hierarchy; - } + Ok { T.def_id; meta; is_local; name; generics; preds; kind } | _ -> Error "") let var_of_json (js : json) : (A.var, string) result = @@ -912,7 +900,6 @@ let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : ("parent_params_info", parent_params_info); ("inputs", inputs); ("output", output); - ("regions_hierarchy", regions_hierarchy); ] -> let* is_unsafe = bool_of_json is_unsafe in let* generics = generic_params_of_json id_to_file generics in @@ -922,17 +909,7 @@ let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) : in let* inputs = list_of_json ty_of_json inputs in let* output = ty_of_json output in - let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in - Ok - { - A.is_unsafe; - generics; - preds; - parent_params_info; - inputs; - output; - regions_hierarchy; - } + Ok { A.is_unsafe; generics; preds; parent_params_info; inputs; output } | _ -> Error "") let call_of_json (js : json) : (A.call, string) result = diff --git a/charon-ml/src/GAstUtils.ml b/charon-ml/src/GAstUtils.ml index 8ae1c880..44dca35a 100644 --- a/charon-ml/src/GAstUtils.ml +++ b/charon-ml/src/GAstUtils.ml @@ -6,14 +6,14 @@ module T = Types This list *doesn't* include the current region. *) -let rec list_ancestor_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) : - T.RegionGroupId.Set.t = - let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in +let rec list_ancestor_region_groups (regions_hierarchy : T.region_groups) + (gid : T.RegionGroupId.id) : T.RegionGroupId.Set.t = + let rg = T.RegionGroupId.nth regions_hierarchy gid in let parents = List.fold_left (fun s gid -> (* Compute the parents *) - let parents = list_ancestor_region_groups sg gid in + let parents = list_ancestor_region_groups regions_hierarchy gid in (* Parents U current region *) let parents = T.RegionGroupId.Set.add gid parents in (* Make the union with the accumulator *) @@ -23,13 +23,13 @@ let rec list_ancestor_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) : parents (** Small utility: same as {!list_ancestor_region_groups}, but returns an ordered list. *) -let list_ordered_ancestor_region_groups (sg : fun_sig) +let list_ordered_ancestor_region_groups (regions_hierarchy : T.region_groups) (gid : T.RegionGroupId.id) : T.RegionGroupId.id list = - let pset = list_ancestor_region_groups sg gid in + let pset = list_ancestor_region_groups regions_hierarchy gid in let parents = List.filter (fun (rg : T.region_group) -> T.RegionGroupId.Set.mem rg.id pset) - sg.regions_hierarchy + regions_hierarchy in let parents = List.map (fun (rg : T.region_group) -> rg.id) parents in parents diff --git a/charon-ml/src/LlbcOfJson.ml b/charon-ml/src/LlbcOfJson.ml index b096c0b1..2d2f2ce2 100644 --- a/charon-ml/src/LlbcOfJson.ml +++ b/charon-ml/src/LlbcOfJson.ml @@ -142,7 +142,6 @@ let global_decl_of_json (id_to_file : id_to_file_map) (js : json) generics = TypesUtils.mk_empty_generic_params; preds = TypesUtils.mk_empty_predicates; parent_params_info = None; - regions_hierarchy = []; inputs = []; output = ty; } diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 2f605924..3e491cf1 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -171,7 +171,7 @@ let trait_clause_to_string (fmt : type_formatter) (clause : T.trait_clause) : string = let clause_id = fmt.trait_clause_id_to_string clause.clause_id in let trait_id = fmt.trait_decl_id_to_string clause.trait_id in - let generics = generic_args_to_string fmt clause.generics in + let generics = generic_args_to_string fmt clause.clause_generics in "[" ^ clause_id ^ "]: " ^ trait_id ^ generics let generic_params_to_strings (fmt : type_formatter) diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index cc2b2e23..f38bf519 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -237,7 +237,6 @@ type assumed_ty = TBox | TArray | TSlice | TStr *) and type_id = TAdtId of type_decl_id | TTuple | TAssumed of assumed_ty -(* TODO: we should prefix the type variants with "T", this would avoid collisions *) and ty = | TAdt of type_id * generic_args (** {!Types.ty.TAdt} encodes ADTs, tuples and assumed types *) @@ -330,24 +329,76 @@ and region = polymorphic = false; }] +(** Ancestor for iter visitor for {!type: Types.predicates} *) +class ['self] iter_predicates_base = + object (self : 'self) + inherit [_] iter_ty + method visit_meta : 'env -> meta -> unit = fun _ _ -> () + + method visit_type_var : 'env -> type_var -> unit = + fun env x -> + let { index; name } : type_var = x in + self#visit_type_var_id env index; + self#visit_string env name + + method visit_region_var : 'env -> region_var -> unit = + fun env x -> + let { index; name } : region_var = x in + self#visit_region_id env index; + self#visit_option self#visit_string env name + + method visit_const_generic_var : 'env -> const_generic_var -> unit = + fun env x -> + let { index; name; ty } : const_generic_var = x in + self#visit_const_generic_var_id env index; + self#visit_string env name; + self#visit_literal_type env ty + end + +(** Ancestor for map visitor for {!type: Types.ty} *) +class virtual ['self] map_predicates_base = + object (self : 'self) + inherit [_] map_ty + method visit_meta : 'env -> meta -> meta = fun _ x -> x + + method visit_region_var : 'env -> region_var -> region_var = + fun env x -> + let { index; name } : region_var = x in + let index = self#visit_region_id env index in + let name = self#visit_option self#visit_string env name in + { index; name } + + method visit_type_var : 'env -> type_var -> type_var = + fun env x -> + let { index; name } : type_var = x in + let index = self#visit_type_var_id env index in + let name = self#visit_string env name in + { index; name } + + method visit_const_generic_var + : 'env -> const_generic_var -> const_generic_var = + fun env x -> + let { index; name; ty } : const_generic_var = x in + let index = self#visit_const_generic_var_id env index in + let name = self#visit_string env name in + let ty = self#visit_literal_type env ty in + { index; name; ty } + end + (** Type with erased regions (this only has an informative purpose) *) -type ety = ty [@@deriving show, ord] +type ety = ty (** Type with non-erased regions (this only has an informative purpose) *) -type rty = ty [@@deriving show, ord] - -type field = { meta : meta; field_name : string option; field_ty : ty } -[@@deriving show] +and rty = ty -type trait_clause = { +and trait_clause = { clause_id : trait_clause_id; meta : meta option; trait_id : trait_decl_id; - generics : generic_args; + clause_generics : generic_args; } -[@@deriving show] -type generic_params = { +and generic_params = { regions : region_var list; types : type_var list; (** The type parameters can be indexed with {!Types.TypeVarId.id}. @@ -361,25 +412,45 @@ type generic_params = { *) trait_clauses : trait_clause list; } -[@@deriving show] -type region_outlives = region * region [@@deriving show] -type type_outlives = ty * region [@@deriving show] +(** ('long, 'short) means that 'long outlives 'short *) +and region_outlives = region * region + +(** (T, 'a) means that T outlives 'a *) +and type_outlives = ty * region -type trait_type_constraint = { +and trait_type_constraint = { trait_ref : trait_ref; generics : generic_args; type_name : trait_item_name; ty : ty; } -[@@deriving show] -type predicates = { +and predicates = { regions_outlive : region_outlives list; types_outlive : type_outlives list; trait_type_constraints : trait_type_constraint list; } -[@@deriving show] +[@@deriving + show, + visitors + { + name = "iter_predicates"; + variety = "iter"; + ancestors = [ "iter_predicates_base" ]; + nude = true (* Don't inherit {!VisitorsRuntime.iter} *); + concrete = true; + polymorphic = false; + }, + visitors + { + name = "map_predicates"; + variety = "map"; + ancestors = [ "map_predicates_base" ]; + nude = true (* Don't inherit {!VisitorsRuntime.map} *); + concrete = false; + polymorphic = false; + }] (** A group of regions. @@ -398,6 +469,9 @@ type 'id g_region_group = { type region_group = RegionGroupId.id g_region_group [@@deriving show] type region_groups = region_group list [@@deriving show] +type field = { meta : meta; field_name : string option; field_ty : ty } +[@@deriving show] + type variant = { meta : meta; variant_name : string; @@ -432,9 +506,5 @@ type type_decl = { generics : generic_params; preds : predicates; kind : type_decl_kind; - regions_hierarchy : region_groups; - (** Stores the hierarchy between the regions (which regions have the - same lifetime, which lifetime should end before which other lifetime, - etc.) *) } [@@deriving show] diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml index c0781305..7fbddfec 100644 --- a/charon-ml/src/TypesUtils.ml +++ b/charon-ml/src/TypesUtils.ml @@ -1,6 +1,19 @@ +open Collections open Types open Utils +module RegionOrderedType : OrderedType with type t = region = struct + type t = region + + let compare = compare_region + let to_string = show_region + let pp_t = pp_region + let show_t = show_region +end + +module RegionMap = Collections.MakeMap (RegionOrderedType) +module RegionSet = Collections.MakeSet (RegionOrderedType) + let type_decl_is_opaque (d : type_decl) : bool = match d.kind with Struct _ | Enum _ -> false | Opaque -> true diff --git a/charon/src/driver.rs b/charon/src/driver.rs index c190675a..0cfa02a0 100644 --- a/charon/src/driver.rs +++ b/charon/src/driver.rs @@ -7,7 +7,6 @@ use crate::index_to_function_calls; use crate::insert_assign_return_unit; use crate::ops_to_function_calls; use crate::reconstruct_asserts; -use crate::regions_hierarchy; use crate::remove_drop_never; use crate::remove_dynamic_checks; use crate::remove_read_discriminant; @@ -169,10 +168,6 @@ pub fn translate(sess: &Session, tcx: TyCtxt, internal: &CharonCallbacks) -> Res // - group the mutually recursive definitions let ordered_decls = reorder_decls::reorder_declarations(&ctx)?; - // # Compute the regions hierarchies for the types and the function signatures - // TODO: move to Aeneas - regions_hierarchy::compute(&mut ctx, &ordered_decls); - // // ================= // **Micro-passes**: diff --git a/charon/src/lib.rs b/charon/src/lib.rs index 8cfba600..500433c7 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -69,7 +69,6 @@ pub mod names; pub mod names_utils; pub mod ops_to_function_calls; pub mod reconstruct_asserts; -pub mod regions_hierarchy; pub mod remove_drop_never; pub mod remove_dynamic_checks; pub mod remove_read_discriminant; diff --git a/charon/src/regions_hierarchy.rs b/charon/src/regions_hierarchy.rs deleted file mode 100644 index 50472486..00000000 --- a/charon/src/regions_hierarchy.rs +++ /dev/null @@ -1,866 +0,0 @@ -//! Analysis of type defintions and function signatures to compute the -//! hierarchy between regions. -#![allow(dead_code)] - -use crate::common::*; -use crate::formatter::Formatter; -use crate::graphs::*; -use crate::llbc_ast::FunDecls; -use crate::reorder_decls as rd; -use crate::reorder_decls::{DeclarationGroup, DeclarationsGroups}; -use crate::translate_ctx::TransCtx; -use crate::types as ty; -use crate::types::*; -use crate::ullbc_ast::FunDeclId; -use hashlink::linked_hash_map::LinkedHashMap; -use macros::generate_index_type; -use petgraph::algo::tarjan_scc; -use petgraph::graphmap::DiGraphMap; -use petgraph::Direction; -use serde::Serialize; -use std::collections::{HashMap, HashSet}; -use std::iter::FromIterator; - -generate_index_type!(RegionGroupId); - -pub type TypeDeclarationGroup = rd::GDeclarationGroup; - -pub fn region_group_id_to_pretty_string(rid: RegionGroupId::Id) -> String { - format!("rg@{rid}") -} - -#[derive(Clone)] -pub struct LifetimeConstraint { - region: Region, - parent: Region, -} - -/// An edge from r1 to r2 means: -/// r1 : r2 (i.e.: r1 lasts longer than r2) -type LifetimeConstraints = DiGraphMap; - -/// A group of regions. -/// -/// Is used to group regions with the same lifetime together, and express -/// the lifetime hierarchy between different groups of regions. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] -pub struct RegionGroup { - /// The region group identifier - pub id: RegionGroupId::Id, - /// The regions included in this group - pub regions: Vec, - /// The parent region groups - pub parents: Vec, -} - -pub type RegionGroups = RegionGroupId::Vector; - -/// Compute the region strongly connected components from a constraints graph. -fn compute_sccs_from_lifetime_constraints( - constraints_graph: &LifetimeConstraints, - region_params: &RegionId::Vector, -) -> SCCs { - // Apply Tarjan's algorithms to group the regions and the borrows which have - // the same lifetime. We then reorder those group of regions to be as close - // as possible to the original order. - let region_sccs = tarjan_scc(&constraints_graph); - - // Reorder the SCCs - let get_region_parents = &|r: Region| { - constraints_graph - .neighbors_directed(r, Direction::Outgoing) - .collect() - }; - - // Option::iter is a trick to easily append a single region to the var regions - // Maybe there is a better way. - let all_var_regions = region_params.iter_indices().map(Region::Var); - let all_rids: Vec = all_var_regions - .chain(Some(Region::Static).into_iter()) - .collect(); - trace!("all_rids: {:?}\nregion_sccs: {:?}", all_rids, region_sccs); - let sccs = reorder_sccs(get_region_parents, &all_rids, ®ion_sccs); - - // Debugging - trace!( - "{}", - vec_to_string( - &|scc: &Vec| { - let ids: Vec = scc.iter().map(|r| r.to_string()).collect(); - format!("[{}]", ids.join(", ")) - }, - &sccs.sccs - ) - ); - - sccs -} - -/// The computation of a regions hierarchy is done in two steps: -/// - first we visit the type definition/function signature to register the -/// constraints between the different regions -/// - then we compute the hierarchy from those accumulated constraints -/// This function performs the second step. -fn compute_regions_hierarchy_from_constraints(mut constraints: SCCs) -> RegionGroups { - // The last SCC **MUST** contain the static region. - // For now, we don't handle cases where regions different from 'static - // can live as long as 'static, so we check that the last scc is the - // {static} singleton. - // TODO: general support for 'static - assert!(!constraints.sccs.is_empty()); - assert!(constraints.sccs.last().unwrap() == &vec![Region::Static]); - - // Pop the last SCC (which is {'static}). - let _ = constraints.sccs.pop(); - let _ = constraints.scc_deps.pop(); - - // Compute the hierarchy - let mut groups = RegionGroups::new(); - for (i, scc) in constraints.sccs.into_iter().enumerate() { - // Compute the id - let id = RegionGroupId::Id::new(i); - - // Retrieve the set of regions in the group - let regions: Vec = scc.into_iter().map(|r| *r.as_var()).collect(); - - // Compute the set of parent region groups - let parents: Vec = constraints - .scc_deps - .get(i) - .unwrap() - .iter() - .map(|j| RegionGroupId::Id::new(*j)) - .collect(); - - // Push the group - groups.push_back(RegionGroup { - id, - regions, - parents, - }); - } - - // Return - groups -} - -/// See [TypesConstraintsMap] -pub type RegionVarsConstraintsMap = LinkedHashMap>; - -/// See [TypesConstraintsMap] -pub type TypeVarsConstraintsMap = LinkedHashMap>; - -/// See [TypesConstraintsMap] -#[derive(Debug, Clone)] -pub struct TypeDeclConstraintsMap { - region_vars_constraints: RegionVarsConstraintsMap, - type_vars_constraints: TypeVarsConstraintsMap, -} - -impl TypeDeclConstraintsMap { - fn new() -> Self { - TypeDeclConstraintsMap { - region_vars_constraints: RegionVarsConstraintsMap::new(), - type_vars_constraints: TypeVarsConstraintsMap::new(), - } - } -} - -/// This map gives, for every definition: -/// - for every region parameter: the set of regions which outlive this region -/// parameter. -/// - for every type parameter: the set of regions under which the type parameter -/// appears. This means that every region appearing in this type parameter's -/// instantiation must outlive the regions in this set. -/// -/// For instance, for the following type definition: -/// ```text -/// struct S<'a, 'b, T1, T2> { -/// x : T1, -/// y : &'a mut &'b mut T2, -/// } -/// ``` -/// -/// We would have: -/// ```text -/// 'a -> {} -/// 'b -> {'a} -/// -/// T1 -> {} -/// T2 -> {'a, 'b} -/// ``` -/// -/// Note: we use linked hash maps to preserve the order for printing. -pub type TypesConstraintsMap = LinkedHashMap; - -fn add_region_constraints( - updated: &mut bool, - acc_constraints: &mut LifetimeConstraints, - type_def_constraints: &mut Option, - region: Region, - parent_regions: &im::HashSet, -) { - // Check that the region is indeed in the nodes - if !acc_constraints.contains_node(region) { - *updated = true; - acc_constraints.add_node(region); - } - - for parent in parent_regions.iter() { - let parent = *parent; - if !acc_constraints.contains_node(parent) { - *updated = true; - acc_constraints.add_node(parent); - } - if !acc_constraints.contains_edge(region, parent) { - *updated = true; - acc_constraints.add_edge(region, parent, ()); - } - } - - match (®ion, type_def_constraints) { - (_, None) | (Region::Static, _) => (), - (Region::Erased, _) => unreachable!(), - (Region::Var(rid), Some(type_def_constraints)) => { - let current_parents = type_def_constraints - .region_vars_constraints - .get_mut(rid) - .unwrap(); - for parent in parent_regions.iter() { - if !current_parents.contains(parent) { - *updated = true; - current_parents.insert(*parent); - } - } - } - (Region::Unknown, _) => { - // Ignoring this case, which stems from errors - } - } - - // Also constrain with regards to static: - if !acc_constraints.contains_edge(Region::Static, region) { - *updated = true; - acc_constraints.add_edge(Region::Static, region, ()); - } -} - -/// TODO: detailed explanations -fn compute_full_regions_constraints_for_ty( - updated: &mut bool, - constraints_map: &TypesConstraintsMap, - acc_constraints: &mut LifetimeConstraints, - type_def_constraints: &mut Option, // TODO: rename - parent_regions: im::HashSet, - ty: &Ty, -) { - match ty { - Ty::Adt(type_id, generics) => { - // Introduce constraints for all the regions given as parameters - for r in &generics.regions { - add_region_constraints( - updated, - acc_constraints, - type_def_constraints, - *r, - &parent_regions, - ); - } - - // Compute the map from region param id to region instantation, for - // this ADT instantiation - let region_inst: RegionId::Vector = - RegionId::Vector::from_iter(generics.regions.iter().copied()); - - // Lookup the constraints for this type definition - match type_id { - TypeId::Adt(type_def_id) => { - // Lookup the (non-instantiated) type parameter constraints for this ADT - let adt_constraints = constraints_map.get(type_def_id).unwrap(); - - // Add the region constraints - for (region_param_id, region) in region_inst.iter_indexed_values() { - let additional_parents = adt_constraints - .region_vars_constraints - .get(®ion_param_id) - .unwrap(); - - // We need to instantiate the additional parents - let additional_parents = - im::HashSet::from_iter(additional_parents.iter().map(|r| match r { - Region::Unknown => Region::Unknown, - Region::Static => Region::Static, - Region::Erased => Region::Erased, - Region::Var(rid) => *region_inst.get(*rid).unwrap(), - })); - - // Add the constraints - add_region_constraints( - updated, - acc_constraints, - type_def_constraints, - *region, - &additional_parents, - ); - } - - // Explore the types given as parameters - let types: TypeVarId::Vector<&Ty> = - TypeVarId::Vector::from_iter(generics.types.iter()); - for (type_param_id, fty) in types.iter_indexed_values() { - // Retrieve the (non-instantiated) parent regions for this type param - let type_param_constraints = adt_constraints - .type_vars_constraints - .get(&type_param_id) - .unwrap(); - - // Instantiate the parent regions constraints - let mut parent_regions = parent_regions.clone(); - for r in type_param_constraints { - let region = match r { - Region::Unknown => Region::Unknown, - Region::Static => Region::Static, - Region::Erased => Region::Erased, - Region::Var(rid) => *region_inst.get(*rid).unwrap(), - }; - parent_regions.insert(region); - } - - // Explore the type parameter - compute_full_regions_constraints_for_ty( - updated, - constraints_map, - acc_constraints, - type_def_constraints, - parent_regions.clone(), - fty, - ); - } - } - TypeId::Tuple - | TypeId::Assumed( - AssumedTy::Box - | AssumedTy::PtrUnique - | AssumedTy::Str - | AssumedTy::PtrNonNull - | AssumedTy::Array - | AssumedTy::Slice, - ) => { - // Explore the types given as parameters - for fty in &generics.types { - compute_full_regions_constraints_for_ty( - updated, - constraints_map, - acc_constraints, - type_def_constraints, - parent_regions.clone(), - fty, - ); - } - } - } - } - Ty::Literal(_) | Ty::Never => { - // Nothing to do - } - Ty::Ref(region, ref_ty, _mutability) => { - // Add the constraint for the region in the reference - add_region_constraints( - updated, - acc_constraints, - type_def_constraints, - *region, - &parent_regions, - ); - - // Update the parent regions, then continue exploring - let mut parent_regions = parent_regions.clone(); - parent_regions.insert(*region); - compute_full_regions_constraints_for_ty( - updated, - constraints_map, - acc_constraints, - type_def_constraints, - parent_regions, - ref_ty, - ); - } - Ty::RawPtr(ptr_ty, _) => { - // Dive in - compute_full_regions_constraints_for_ty( - updated, - constraints_map, - acc_constraints, - type_def_constraints, - parent_regions, - ptr_ty, - ); - } - Ty::TypeVar(var_id) => { - // Add the parent regions in the set of parent regions for the type variable - match type_def_constraints { - None => (), - Some(type_def_constraints) => { - let parents_set = type_def_constraints - .type_vars_constraints - .get_mut(var_id) - .unwrap(); - for parent in parent_regions { - if !parents_set.contains(&parent) { - *updated = true; - parents_set.insert(parent); - } - } - } - } - } - Ty::TraitType(_trait_ref, generics, _name) => { - // TODO: A bit unclear what we should do here - - // Introduce constraints for all the regions given as parameters - for r in &generics.regions { - add_region_constraints( - updated, - acc_constraints, - type_def_constraints, - *r, - &parent_regions, - ); - } - } - Ty::Arrow(inputs, box output) => { - for ty in inputs.iter().chain(std::iter::once(output)) { - compute_full_regions_constraints_for_ty( - updated, - constraints_map, - acc_constraints, - type_def_constraints, - parent_regions.clone(), - ty, - ); - } - } - } -} - -/// Auxiliary function. -/// -/// Compute the region constraints for a type declaration group. -/// -/// Note that recursive types in rust are very general. For instance, they allow -/// non-uniform polymorphism: -/// ```text -/// enum E { -/// V1, -/// V2(Box>) -/// } -/// ``` -/// -/// Following this, we compute the constraints by computing a fixed -/// point: for every variant of every type appearing in the type declaration -/// group, we compute a properly initialized set of constraints. -/// We then explore all those types: as long as exploring one of those types -/// leads to a new constraint, we reexplore them all. -fn compute_regions_constraints_for_type_decl_group( - constraints_map: &mut TypesConstraintsMap, - types: &TypeDecls, - decl: &TypeDeclarationGroup, -) -> Vec> { - // List the type ids in the type declaration group - let type_ids: HashSet = match decl { - TypeDeclarationGroup::NonRec(id) => { - let mut ids = HashSet::new(); - ids.insert(*id); - ids - } - TypeDeclarationGroup::Rec(ids) => HashSet::from_iter(ids.iter().copied()), - }; - - // TODO: take into account the where clauses - - // Initialize the constraints map - TODO: this will be different once we - // support constraints over the generics in the definitions - for id in type_ids.iter() { - let type_def = types.get(*id).unwrap(); - let region_vars_constraints = RegionVarsConstraintsMap::from_iter( - type_def - .generics - .regions - .iter() - .map(|var| (var.index, HashSet::new())), - ); - let type_vars_constraints = TypeVarsConstraintsMap::from_iter( - type_def - .generics - .types - .iter() - .map(|var| (var.index, HashSet::new())), - ); - let type_def_constraints = TypeDeclConstraintsMap { - region_vars_constraints, - type_vars_constraints, - }; - constraints_map.insert(*id, type_def_constraints); - } - - let mut updated = true; - let mut acc_constraints_map: HashMap = - HashMap::from_iter(type_ids.iter().map(|id| { - (*id, { - let mut graph = LifetimeConstraints::new(); - graph.add_node(Region::Static); - let d = types.get(*id).unwrap(); - d.generics.regions.iter().for_each(|id| { - let _ = graph.add_node(Region::Var(id.index)); - }); - graph - }) - })); - - while updated { - updated = false; - - // Accumulate constraints for every variant of every type - for id in type_ids.iter() { - let type_def = types.get(*id).unwrap(); - - // If the type is transparent, we explore the ADT variants. - // If the type is opaque, there is nothing to do. - // TODO: will be slightly different once we support constraints - // over the generics in the type declarations - - // Instantiate the type definition variants - let region_params = Vec::from_iter( - type_def - .generics - .regions - .iter() - .map(|rvar| Region::Var(rvar.index)), - ); - let type_params = Vec::from_iter( - type_def - .generics - .types - .iter() - .map(|tvar| Ty::TypeVar(tvar.index)), - ); - let variants_fields_tys = - type_def.get_instantiated_variants(®ion_params, &type_params); - - match variants_fields_tys { - Option::None => { - // Opaque type: nothing to do - } - Option::Some(variants_fields_tys) => { - // Transparent type - - // Retreive the accumulated constraints for this type def - let acc_constraints = acc_constraints_map.get_mut(id).unwrap(); - - // Clone the type vars constraints map - we can't accumulate in the - // original map, so we have to clone - // TODO: this is not efficient - but the sets should be super small - let mut updt_type_vars_constraints = - Some(constraints_map.get(id).unwrap().clone()); - - // Explore the field types of all the variants - for field_tys in variants_fields_tys.iter() { - for ty in field_tys.iter() { - compute_full_regions_constraints_for_ty( - &mut updated, - constraints_map, - acc_constraints, - &mut updt_type_vars_constraints, - im::HashSet::new(), - ty, - ); - } - } - - // Update the type vars constraints map - let updt_type_vars_constraints = updt_type_vars_constraints.unwrap(); - let type_def_constraints = constraints_map.get_mut(id).unwrap(); - let region_vars_constraints = &mut type_def_constraints.region_vars_constraints; - let type_vars_constraints = &mut type_def_constraints.type_vars_constraints; - - // The constraints over region parameters - for (r_id, updt_set) in - updt_type_vars_constraints.region_vars_constraints.iter() - { - let set = region_vars_constraints.get_mut(r_id).unwrap(); - for r in updt_set.iter() { - set.insert(*r); - } - } - - // The constraints over type parameters - for (var_id, updt_set) in - updt_type_vars_constraints.type_vars_constraints.iter() - { - let set = type_vars_constraints.get_mut(var_id).unwrap(); - for r in updt_set.iter() { - set.insert(*r); - } - } - } - } - } - } - - // Compute the SCCs - let mut sccs_vec: Vec> = Vec::new(); - for id in type_ids.iter() { - let type_def = types.get(*id).unwrap(); - let sccs = compute_sccs_from_lifetime_constraints( - acc_constraints_map.get(id).unwrap(), - &type_def.generics.regions, - ); - sccs_vec.push(sccs); - } - - // Return - sccs_vec -} - -/// Compute the region hierarchy (the order between the region's lifetimes) -/// for a (group of mutually recursive) type definitions. -/// Note that [TypeDecl] already contains a regions hierarchy: when translating -/// function signatures, we first translate the signature without this hierarchy, -/// then compute this hierarchy and add it to the type definition: this is -/// why this function performs in-place modifications instead of returning -/// a [RegionGroups]. -pub fn compute_regions_hierarchy_for_type_decl_group( - constraints_map: &mut TypesConstraintsMap, - types: &mut TypeDecls, - decl: &TypeDeclarationGroup, -) { - // TODO: for now we don't properly handle mutually recursive groups of definitions - // which use lifetimes. - { - let ids = decl.get_ids(); - assert!( - ids.len() == 1 - || ids.iter().all(|id| { - let d = types.get(*id).unwrap(); - d.generics.regions.is_empty() - }) - ); - } - - // Compute the constraints for every definition in the declaration group - let constraints = compute_regions_constraints_for_type_decl_group(constraints_map, types, decl); - - // Compute the regions hierarchies from every set of constraints, and - // update the type definitions - let type_ids: Vec = match decl { - TypeDeclarationGroup::NonRec(id) => vec![*id], - TypeDeclarationGroup::Rec(ids) => ids.clone(), - }; - for (id, sccs) in type_ids.into_iter().zip(constraints.into_iter()) { - let regions_group = compute_regions_hierarchy_from_constraints(sccs); - - let type_def = types.get_mut(id).unwrap(); - type_def.regions_hierarchy = regions_group; - } -} - -/// Compute the constraints between the different regions of a type (which -/// region lasts longer than which other region, etc.). -/// Note that the region hierarchies should already have been computed for all -/// the types: this function should be used when computing constraints for -/// **function signatures** only. -fn compute_regions_constraints_for_ty( - constraints_map: &TypesConstraintsMap, - acc_constraints: &mut LifetimeConstraints, - ty: &Ty, -) { - // We need to provide some values to [compute_full_regions_constraints_for_ty], - // but we don't use them in the present case (they are use by this function - // to communicate us information). - let mut updated = false; - let type_def_constraints = &mut None; - compute_full_regions_constraints_for_ty( - &mut updated, - constraints_map, - acc_constraints, - type_def_constraints, - im::HashSet::new(), - ty, - ) -} - -/// Compute the constraints between the different regions of a function -/// signature (which region lasts longer than which other region, etc.). -/// This is used to compute the order (in given by the region lifetime's) -/// between the regions. -/// TODO: rename. compute_ordered_regions_constraints...? -fn compute_regions_constraints_for_sig( - types_constraints: &TypesConstraintsMap, - sig: &FunSig, -) -> SCCs { - trace!("sig: {sig:?}"); - - let mut constraints_graph = LifetimeConstraints::new(); - // Add a node for every region - constraints_graph.add_node(Region::Static); - for r in &sig.generics.regions { - constraints_graph.add_node(Region::Var(r.index)); - } - - for input_ty in &sig.inputs { - compute_regions_constraints_for_ty(types_constraints, &mut constraints_graph, input_ty); - } - compute_regions_constraints_for_ty(types_constraints, &mut constraints_graph, &sig.output); - - // Compute the SCCs from the region constraints - compute_sccs_from_lifetime_constraints(&constraints_graph, &sig.generics.regions) -} - -/// Compute the region hierarchy (the order between the region's lifetimes) -/// for a function signature. -/// Note that [FunSig] already contains a regions hierarchy: when translating -/// function signatures, we first translate the signature without this hierarchy, -/// then compute this hierarchy and add it to the signature information. -pub fn compute_regions_hierarchy_for_sig( - types_constraints: &TypesConstraintsMap, - sig: &FunSig, -) -> RegionGroups { - // Compute the constraints between the regions and group them accordingly - let sccs = compute_regions_constraints_for_sig(types_constraints, sig); - - // Compute the regions hierarchy - compute_regions_hierarchy_from_constraints(sccs) -} - -/// Compute the region hierarchy (the order between the region's lifetimes) for -/// a set of function definitions. -pub fn compute_regions_hierarchies_for_functions( - types_constraints: &TypesConstraintsMap, - defs: &FunDecls, -) -> FunDeclId::Vector { - FunDeclId::Vector::from_iter( - defs.iter() - .map(|def| compute_regions_hierarchy_for_sig(types_constraints, &def.signature)), - ) -} - -impl RegionGroup { - pub fn fmt_with_ctx(&self, ctx: &T) -> String - where - T: Formatter, - { - // The parent region groups - let parents: Vec = self.parents.iter().map(|gid| gid.to_string()).collect(); - let parents = format!("{{{}}}", parents.join(",")); - - // The regions included in the group - let regions: Vec = self - .regions - .iter() - .map(|rid| ctx.format_object(*rid)) - .collect(); - let regions = format!("{{{}}}", regions.join(",")); - - // Put everything together - format!( - "{}{{parents={}}}={}", - region_group_id_to_pretty_string(self.id), - parents, - regions - ) - } -} - -fn types_def_constraints_map_fmt_with_ctx<'a, 'b, 'c, T>( - cs: &'a TypeDeclConstraintsMap, - ctx: &'b T, - indent: &'c str, -) -> String -where - T: Formatter + Formatter + Formatter<&'a Region>, -{ - let region_constraints = cs.region_vars_constraints.iter().map(|(rid, regions)| { - format!( - "{}{} -> {{{}}}", - indent, - ctx.format_object(*rid), - regions - .iter() - .map(|r| ctx.format_object(r)) - .collect::>() - .join(",") - ) - }); - let type_constraints = cs.type_vars_constraints.iter().map(|(vid, regions)| { - format!( - "{}{} -> {{{}}}", - indent, - ctx.format_object(*vid), - regions - .iter() - .map(|r| ctx.format_object(r)) - .collect::>() - .join(",") - ) - }); - let all_constraints: Vec = region_constraints.chain(type_constraints).collect(); - all_constraints.join(",\n") -} - -pub fn types_constraints_map_fmt_with_ctx( - cs: &TypesConstraintsMap, - types: &ty::TypeDecls, -) -> String { - // We iterate over the type definitions, not the types constraints map, - // in order to make sure we preserve the type definitions order - let types_constraints: Vec = types - .iter() - .map(|type_def| { - let cmap = cs.get(&type_def.def_id).unwrap(); - if type_def.generics.regions.len() + type_def.generics.types.len() == 0 { - format!("{} -> []", types.format_object(type_def.def_id)) - } else { - let ctx = type_def; - format!( - "{} -> [\n{}\n]", - types.format_object(type_def.def_id), - types_def_constraints_map_fmt_with_ctx(cmap, ctx, " ") - ) - } - }) - .collect(); - types_constraints.join("\n") -} - -pub fn compute(ctx: &mut TransCtx, ordered_decls: &DeclarationsGroups) { - // First, compute the regions hierarchy for the types, and compute the types - // constraints map while doing so. We compute by working on a whole type - // declaration group at a time. - let mut types_constraints = TypesConstraintsMap::new(); - for dgroup in ordered_decls { - trace!("{}", dgroup.fmt_with_ctx(ctx)); - match dgroup { - DeclarationGroup::Type(decl) => { - compute_regions_hierarchy_for_type_decl_group( - &mut types_constraints, - &mut ctx.type_defs, - decl, - ); - } - DeclarationGroup::Fun(_) - | DeclarationGroup::Global(_) - | DeclarationGroup::TraitDecl(_) - | DeclarationGroup::TraitImpl(_) => { - // Ignore the functions, constants and traits - } - } - } - - // Use the types constraints map to compute the regions hierarchies for the - // function signatures - for decl in &mut ctx.fun_defs.iter_mut() { - trace!("decl: {:?}", &decl.name); - decl.signature.regions_hierarchy = - compute_regions_hierarchy_for_sig(&types_constraints, &decl.signature); - } -} diff --git a/charon/src/translate_functions_to_ullbc.rs b/charon/src/translate_functions_to_ullbc.rs index 3738b4e2..da27ed6f 100644 --- a/charon/src/translate_functions_to_ullbc.rs +++ b/charon/src/translate_functions_to_ullbc.rs @@ -11,7 +11,6 @@ use crate::formatter::Formatter; use crate::get_mir::{boxes_are_desugared, get_mir_for_def_id_and_level}; use crate::id_vector; use crate::names_utils::{def_id_to_name, extended_def_id_to_name}; -use crate::regions_hierarchy::RegionGroups; use crate::translate_ctx::*; use crate::translate_types; use crate::types::*; @@ -1574,7 +1573,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { generics: self.get_generics(), preds: self.get_predicates(), is_unsafe, - regions_hierarchy: RegionGroups::new(), // Hierarchy not yet computed parent_params_info, inputs, output, diff --git a/charon/src/translate_types.rs b/charon/src/translate_types.rs index ccea6c43..5149833c 100644 --- a/charon/src/translate_types.rs +++ b/charon/src/translate_types.rs @@ -2,7 +2,6 @@ use crate::assumed; use crate::common::*; use crate::gast::*; use crate::names_utils::{def_id_to_name, extended_def_id_to_name}; -use crate::regions_hierarchy::RegionGroups; use crate::translate_ctx::*; use crate::types::*; use core::convert::*; @@ -610,8 +609,6 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> { generics, preds: bt_ctx.get_predicates(), kind, - // Dummy value for now: we compute this later - regions_hierarchy: RegionGroups::new(), }; trace!("translate_type: preds: {:?}", &type_def.preds); diff --git a/charon/src/types.rs b/charon/src/types.rs index be9c451a..91eed3a8 100644 --- a/charon/src/types.rs +++ b/charon/src/types.rs @@ -3,7 +3,6 @@ pub use crate::gast::TraitItemName; use crate::meta::Meta; use crate::names::TypeName; -use crate::regions_hierarchy::RegionGroups; pub use crate::types_utils::*; use crate::values::Literal; use derivative::Derivative; @@ -320,12 +319,6 @@ pub struct TypeDecl { pub preds: Predicates, /// The type kind: enum, struct, or opaque. pub kind: TypeDeclKind, - /// The lifetime's hierarchy between the different regions. - /// We initialize it to a dummy value, then compute it once the whole crate - /// has been translated. - /// - /// TODO: move to Aeneas - pub regions_hierarchy: RegionGroups, } #[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize)] @@ -615,10 +608,4 @@ pub struct FunSig { pub parent_params_info: Option, pub inputs: Vec, pub output: Ty, - /// The lifetime's hierarchy between the different regions. - /// We initialize it to a dummy value, and compute it once the whole - /// crate has been translated from MIR. - /// - /// TODO: move to Aeneas. - pub regions_hierarchy: RegionGroups, } diff --git a/charon/src/types_utils.rs b/charon/src/types_utils.rs index fa121607..248287b9 100644 --- a/charon/src/types_utils.rs +++ b/charon/src/types_utils.rs @@ -1836,7 +1836,6 @@ pub trait TypeVisitor { parent_params_info: _, inputs, output, - regions_hierarchy: _, } = sig; self.visit_generic_params(generics);