From 8b18c0da053e069b5a2d9fbf06f45eae2f05a029 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 7 Sep 2023 15:28:06 +0200 Subject: Map some globals like u32::MAX to standard definitions --- compiler/LlbcAstUtils.ml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 1111c297..8c8bbabe 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -12,3 +12,23 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_name aid + +(** Return the opaque declarations found in the crate. + + Remark: the list of functions also contains the list of opaque global bodies. + *) +let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list = + let open ExtractAssumed in + let is_opaque_fun (d : fun_decl) : bool = + let sname = name_to_simple_name d.name in + d.body = None && not (SimpleNameMap.mem sname assumed_globals_map) + in + let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in + (* Note that by checking the function bodies we also the globals *) + ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), + List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) + +(** Return true if the crate contains opaque declarations, ignoring the assumed + definitions. *) +let crate_has_opaque_decls (k : crate) : bool = + crate_get_opaque_decls k <> ([], []) -- cgit v1.2.3 From 952c4c964e33eeb6956d84efce3ef1b7575f311f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 17 Sep 2023 00:56:51 +0200 Subject: Fix more issues with the extraction --- compiler/LlbcAstUtils.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 8c8bbabe..a982af30 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -15,13 +15,22 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : (** Return the opaque declarations found in the crate. + [filter_assumed]: if [true], do not consider as opaque the external definitions + that we will map to definitions from the standard library. + Remark: the list of functions also contains the list of opaque global bodies. *) -let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list = +let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : + T.type_decl list * fun_decl list = let open ExtractAssumed in let is_opaque_fun (d : fun_decl) : bool = let sname = name_to_simple_name d.name in - d.body = None && not (SimpleNameMap.mem sname assumed_globals_map) + d.body = None + (* Something to pay attention to: we must ignore trait method *declarations* + (which don't have a body but must not be considered as opaque) *) + && (match d.kind with TraitMethodDecl _ -> false | _ -> true) + && ((not filter_assumed) + || not (SimpleNameMap.mem sname assumed_globals_map)) in let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in (* Note that by checking the function bodies we also the globals *) @@ -30,5 +39,5 @@ let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list = (** Return true if the crate contains opaque declarations, ignoring the assumed definitions. *) -let crate_has_opaque_decls (k : crate) : bool = - crate_get_opaque_decls k <> ([], []) +let crate_has_opaque_decls (k : crate) (filter_assumed : bool) : bool = + crate_get_opaque_decls k filter_assumed <> ([], []) -- cgit v1.2.3 From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 23 Oct 2023 13:47:39 +0200 Subject: Remove some assumed types and add more support for builtin definitions --- compiler/LlbcAstUtils.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index a982af30..2553127a 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -5,13 +5,13 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).signature - | Assumed aid -> Assumed.get_assumed_sig aid + | Assumed aid -> Assumed.get_assumed_fun_sig aid let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : Names.fun_name = match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).name - | Assumed aid -> Assumed.get_assumed_name aid + | Assumed aid -> Assumed.get_assumed_fun_name aid (** Return the opaque declarations found in the crate. @@ -22,7 +22,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : *) let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : T.type_decl list * fun_decl list = - let open ExtractAssumed in + let open ExtractBuiltin in let is_opaque_fun (d : fun_decl) : bool = let sname = name_to_simple_name d.name in d.body = None @@ -30,7 +30,7 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || not (SimpleNameMap.mem sname assumed_globals_map)) + || not (SimpleNameMap.mem sname builtin_globals_map)) in let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in (* Note that by checking the function bodies we also the globals *) -- cgit v1.2.3 From e3cb3646bbe3d50240aa0bf4763f8e816fb9a706 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 15:36:06 +0200 Subject: Fix some issues at extraction and add builtins --- compiler/LlbcAstUtils.ml | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 2553127a..0ab4ed94 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -13,14 +13,14 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : | Regular id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_fun_name aid -(** Return the opaque declarations found in the crate. +(** Return the opaque declarations found in the crate, which are also *not builtin*. [filter_assumed]: if [true], do not consider as opaque the external definitions that we will map to definitions from the standard library. Remark: the list of functions also contains the list of opaque global bodies. *) -let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : +let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : T.type_decl list * fun_decl list = let open ExtractBuiltin in let is_opaque_fun (d : fun_decl) : bool = @@ -30,14 +30,21 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || not (SimpleNameMap.mem sname builtin_globals_map)) + || (not (SimpleNameMap.mem sname builtin_globals_map)) + && not (SimpleNameMap.mem sname (builtin_funs_map ()))) + in + let is_opaque_type (d : T.type_decl) : bool = + let sname = name_to_simple_name d.name in + d.kind = T.Opaque + && ((not filter_assumed) + || not (SimpleNameMap.mem sname (builtin_types_map ()))) in - let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in (* Note that by checking the function bodies we also the globals *) ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) (** Return true if the crate contains opaque declarations, ignoring the assumed definitions. *) -let crate_has_opaque_decls (k : crate) (filter_assumed : bool) : bool = - crate_get_opaque_decls k filter_assumed <> ([], []) +let crate_has_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : + bool = + crate_get_opaque_non_builtin_decls k filter_assumed <> ([], []) -- cgit v1.2.3 From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/LlbcAstUtils.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 0ab4ed94..46b36851 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -4,14 +4,14 @@ include Charon.LlbcAstUtils let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = match fun_id with - | Regular id -> (FunDeclId.Map.find id fun_decls).signature - | Assumed aid -> Assumed.get_assumed_fun_sig aid + | FRegular id -> (FunDeclId.Map.find id fun_decls).signature + | FAssumed aid -> Assumed.get_assumed_fun_sig aid let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : Names.fun_name = match fun_id with - | Regular id -> (FunDeclId.Map.find id fun_decls).name - | Assumed aid -> Assumed.get_assumed_fun_name aid + | FRegular id -> (FunDeclId.Map.find id fun_decls).name + | FAssumed aid -> Assumed.get_assumed_fun_name aid (** Return the opaque declarations found in the crate, which are also *not builtin*. -- cgit v1.2.3 From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 13 Nov 2023 13:27:02 +0100 Subject: Add RegionsHierarchy.ml --- compiler/LlbcAstUtils.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 46b36851..de46320b 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -1,5 +1,18 @@ open LlbcAst include Charon.LlbcAstUtils +open Collections + +module FunIdOrderedType : OrderedType with type t = fun_id = struct + type t = fun_id + + let compare = compare_fun_id + let to_string = show_fun_id + let pp_t = pp_fun_id + let show_t = show_fun_id +end + +module FunIdMap = Collections.MakeMap (FunIdOrderedType) +module FunIdSet = Collections.MakeSet (FunIdOrderedType) let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/LlbcAstUtils.ml | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index de46320b..01216157 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -1,3 +1,4 @@ +open Types open LlbcAst include Charon.LlbcAstUtils open Collections @@ -20,12 +21,6 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : | FRegular id -> (FunDeclId.Map.find id fun_decls).signature | FAssumed aid -> Assumed.get_assumed_fun_sig aid -let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : - Names.fun_name = - match fun_id with - | FRegular id -> (FunDeclId.Map.find id fun_decls).name - | FAssumed aid -> Assumed.get_assumed_fun_name aid - (** Return the opaque declarations found in the crate, which are also *not builtin*. [filter_assumed]: if [true], do not consider as opaque the external definitions @@ -34,7 +29,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : Remark: the list of functions also contains the list of opaque global bodies. *) let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : - T.type_decl list * fun_decl list = + type_decl list * fun_decl list = let open ExtractBuiltin in let is_opaque_fun (d : fun_decl) : bool = let sname = name_to_simple_name d.name in @@ -46,15 +41,15 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : || (not (SimpleNameMap.mem sname builtin_globals_map)) && not (SimpleNameMap.mem sname (builtin_funs_map ()))) in - let is_opaque_type (d : T.type_decl) : bool = + let is_opaque_type (d : type_decl) : bool = let sname = name_to_simple_name d.name in - d.kind = T.Opaque + d.kind = Opaque && ((not filter_assumed) || not (SimpleNameMap.mem sname (builtin_types_map ()))) in (* Note that by checking the function bodies we also the globals *) - ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), - List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) + ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls), + List.filter is_opaque_fun (FunDeclId.Map.values k.fun_decls) ) (** Return true if the crate contains opaque declarations, ignoring the assumed definitions. *) -- cgit v1.2.3 From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 21:58:25 +0100 Subject: Use the name matcher implemented in Charon --- compiler/LlbcAstUtils.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 01216157..ffdce481 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -31,21 +31,26 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : type_decl list * fun_decl list = let open ExtractBuiltin in + let ctx : Charon.NameMatcher.ctx = + { + type_decls = k.type_decls; + global_decls = k.global_decls; + trait_decls = k.trait_decls; + } + in let is_opaque_fun (d : fun_decl) : bool = - let sname = name_to_simple_name d.name in d.body = None (* Something to pay attention to: we must ignore trait method *declarations* (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || (not (SimpleNameMap.mem sname builtin_globals_map)) - && not (SimpleNameMap.mem sname (builtin_funs_map ()))) + || (not (NameMatcherMap.mem ctx d.name builtin_globals_map)) + && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ()))) in let is_opaque_type (d : type_decl) : bool = - let sname = name_to_simple_name d.name in d.kind = Opaque && ((not filter_assumed) - || not (SimpleNameMap.mem sname (builtin_types_map ()))) + || not (NameMatcherMap.mem ctx d.name (builtin_types_map ()))) in (* Note that by checking the function bodies we also the globals *) ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls), -- cgit v1.2.3