From ba61ed50e7b2fdc78690de92d734a3747029f903 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Wed, 8 Jun 2022 12:32:14 +0200 Subject: read globals from LLBC JSON into functions --- src/Modules.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Modules.ml') diff --git a/src/Modules.ml b/src/Modules.ml index f52983c6..6d0cf70c 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -1,5 +1,6 @@ open Types open LlbcAst +open FunIdentifier type 'id g_declaration_group = NonRec of 'id | Rec of 'id list [@@deriving show] -- cgit v1.2.3 From 7703c4ca86a390303d0a120f8811c8fd704c5168 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Tue, 21 Jun 2022 11:41:09 +0200 Subject: concrete & symbolic evaluation work with new LLBC format --- src/Modules.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Modules.ml') diff --git a/src/Modules.ml b/src/Modules.ml index 6d0cf70c..b0e8878d 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -1,6 +1,5 @@ open Types open LlbcAst -open FunIdentifier type 'id g_declaration_group = NonRec of 'id | Rec of 'id list [@@deriving show] @@ -21,6 +20,7 @@ type llbc_module = { declarations : declaration_group list; types : type_decl list; functions : fun_decl list; + gid_conv : global_id_converter; } (** LLBC module - TODO: rename to crate *) -- cgit v1.2.3 From 47691de8fe3dc32a29663d4d8343eb415ce1d81e Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 30 Jun 2022 12:22:14 +0200 Subject: Traduct globals body separately (WIP) --- src/Modules.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Modules.ml') diff --git a/src/Modules.ml b/src/Modules.ml index b0e8878d..149de020 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -7,7 +7,8 @@ type 'id g_declaration_group = NonRec of 'id | Rec of 'id list type type_declaration_group = TypeDeclId.id g_declaration_group [@@deriving show] -type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] +type fun_declaration_group = FunDeclId.id g_declaration_group +[@@deriving show] (** Module declaration *) type declaration_group = -- cgit v1.2.3 From f9b324be57708e9496ca6e9ac0b7e68ffd9e7108 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Mon, 18 Jul 2022 16:27:00 +0200 Subject: Address much stuff of the PR, throw exceptions at remaining places --- src/Modules.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'src/Modules.ml') diff --git a/src/Modules.ml b/src/Modules.ml index 149de020..2f640636 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -21,12 +21,12 @@ type llbc_module = { declarations : declaration_group list; types : type_decl list; functions : fun_decl list; - gid_conv : global_id_converter; + globals : global_decl list; } (** LLBC module - TODO: rename to crate *) let compute_defs_maps (m : llbc_module) : - type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t = + type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t = let types_map = List.fold_left (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) @@ -37,7 +37,12 @@ let compute_defs_maps (m : llbc_module) : (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m) FunDeclId.Map.empty m.functions in - (types_map, funs_map) + let globals_map = + List.fold_left + (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m) + GlobalDeclId.Map.empty m.globals + in + (types_map, funs_map, globals_map) (** Split a module's declarations between types and functions *) let split_declarations (decls : declaration_group list) : -- cgit v1.2.3 From f9015d1e956ace6c875eb6a631caeac49cfb8148 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Fri, 29 Jul 2022 16:04:49 +0200 Subject: Create global declaration group, address PR changes but introduce bugs --- src/Modules.ml | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) (limited to 'src/Modules.ml') diff --git a/src/Modules.ml b/src/Modules.ml index 2f640636..009e1ba6 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -10,10 +10,11 @@ type type_declaration_group = TypeDeclId.id g_declaration_group type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] -(** Module declaration *) +(** Module declaration. Globals cannot be mutually dependent. *) type declaration_group = | Type of type_declaration_group | Fun of fun_declaration_group + | Global of GlobalDeclId.id [@@deriving show] type llbc_module = { @@ -44,26 +45,29 @@ let compute_defs_maps (m : llbc_module) : in (types_map, funs_map, globals_map) -(** Split a module's declarations between types and functions *) +(** Split a module's declarations between types, globals and functions *) let split_declarations (decls : declaration_group list) : - type_declaration_group list * fun_declaration_group list = + type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list = let rec split decls = match decls with - | [] -> ([], []) + | [] -> ([], [], []) | d :: decls' -> ( - let types, funs = split decls' in + let types, funs, globals = split decls' in match d with - | Type decl -> (decl :: types, funs) - | Fun decl -> (types, decl :: funs)) + | Type decl -> (decl :: types, funs, globals) + | Fun decl -> (types, decl :: funs, globals) + | Global decl -> (types, funs, decl :: globals) + ) in split decls -(** Split a module's declarations into two maps from type/fun ids to +(** Split a module's declarations into three maps from type/fun/global ids to declaration groups. *) let split_declarations_to_group_maps (decls : declaration_group list) : type_declaration_group TypeDeclId.Map.t - * fun_declaration_group FunDeclId.Map.t = + * fun_declaration_group FunDeclId.Map.t + * GlobalDeclId.Set.t = let module G (M : Map.S) = struct let add_group (map : M.key g_declaration_group M.t) (group : M.key g_declaration_group) : M.key g_declaration_group M.t = @@ -75,9 +79,10 @@ let split_declarations_to_group_maps (decls : declaration_group list) : M.key g_declaration_group M.t = List.fold_left add_group M.empty groups end in - let types, funs = split_declarations decls in + let types, funs, globals = split_declarations decls in let module TG = G (TypeDeclId.Map) in let types = TG.create_map types in let module FG = G (FunDeclId.Map) in let funs = FG.create_map funs in - (types, funs) + let globals = GlobalDeclId.Set.of_list globals in + (types, funs, globals) -- cgit v1.2.3 From f106fd4ad0a221611c840bf0af0b1c2ff23f3d0f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 17:44:04 +0200 Subject: Make minor modifications --- src/Modules.ml | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'src/Modules.ml') diff --git a/src/Modules.ml b/src/Modules.ml index 009e1ba6..7f372d09 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -7,10 +7,9 @@ type 'id g_declaration_group = NonRec of 'id | Rec of 'id list type type_declaration_group = TypeDeclId.id g_declaration_group [@@deriving show] -type fun_declaration_group = FunDeclId.id g_declaration_group -[@@deriving show] +type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] -(** Module declaration. Globals cannot be mutually dependent. *) +(** Module declaration. Globals cannot be mutually recursive. *) type declaration_group = | Type of type_declaration_group | Fun of fun_declaration_group @@ -27,7 +26,9 @@ type llbc_module = { (** LLBC module - TODO: rename to crate *) let compute_defs_maps (m : llbc_module) : - type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t = + type_decl TypeDeclId.Map.t + * fun_decl FunDeclId.Map.t + * global_decl GlobalDeclId.Map.t = let types_map = List.fold_left (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) @@ -45,9 +46,11 @@ let compute_defs_maps (m : llbc_module) : in (types_map, funs_map, globals_map) -(** Split a module's declarations between types, globals and functions *) +(** Split a module's declarations between types, functions and globals *) let split_declarations (decls : declaration_group list) : - type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list = + type_declaration_group list + * fun_declaration_group list + * GlobalDeclId.id list = let rec split decls = match decls with | [] -> ([], [], []) @@ -56,8 +59,7 @@ let split_declarations (decls : declaration_group list) : match d with | Type decl -> (decl :: types, funs, globals) | Fun decl -> (types, decl :: funs, globals) - | Global decl -> (types, funs, decl :: globals) - ) + | Global decl -> (types, funs, decl :: globals)) in split decls @@ -66,7 +68,7 @@ let split_declarations (decls : declaration_group list) : *) let split_declarations_to_group_maps (decls : declaration_group list) : type_declaration_group TypeDeclId.Map.t - * fun_declaration_group FunDeclId.Map.t + * fun_declaration_group FunDeclId.Map.t * GlobalDeclId.Set.t = let module G (M : Map.S) = struct let add_group (map : M.key g_declaration_group M.t) -- cgit v1.2.3