From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 21 Mar 2024 12:34:40 +0100 Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to do and we need to see how translate_crate can give meta to the functions it calls --- compiler/FunsAnalysis.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f6976f23..14185a3d 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -9,6 +9,7 @@ open LlbcAst open ExpressionsUtils +open Errors (** Various information about a function. @@ -36,7 +37,6 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) : modules_funs_info = let infos = ref FunDeclId.Map.empty in - let register_info (id : FunDeclId.id) (info : fun_info) : unit = assert (not (FunDeclId.Map.mem id !infos)); infos := FunDeclId.Map.add id info !infos @@ -119,7 +119,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_Call env call = (match call.func with | FnOpMove _ -> - (* Ignoring this: we lookup the called function upon creating + (* Ignoring this: we lookup t he called function upon creating the closure *) () | FnOpRegular func -> ( @@ -145,7 +145,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - assert ((not f.is_global_decl_body) || not !stateful); + cassert ((not f.is_global_decl_body) || not !stateful) f.meta "Global bodies should not contain stateful calls"; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; @@ -167,8 +167,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* We need to know if the declaration group contains a global - note that * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in - assert ((not is_global_decl_body) || List.length d = 1); - assert ((not !group_has_builtin_info) || List.length d = 1); + cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration"; (*TODO recheck how to get meta*) + cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration"; (* We ignore on purpose functions that cannot fail and consider they *can* * fail: the result of the analysis is not used yet to adjust the translation * so that the functions which syntactically can't fail don't use an error monad. -- cgit v1.2.3 From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 27 Mar 2024 10:22:06 +0100 Subject: Added sanity_check and sanity_check_opt_meta helpers and changed sanity checks related cassert to these helpers to have a proper error message --- compiler/FunsAnalysis.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 14185a3d..f3840a8c 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -145,7 +145,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - cassert ((not f.is_global_decl_body) || not !stateful) f.meta "Global bodies should not contain stateful calls"; + sanity_check ((not f.is_global_decl_body) || not !stateful) f.meta; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; -- cgit v1.2.3 From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 13:56:31 +0100 Subject: Should answer all comments, there are still some TODO: error message left --- compiler/FunsAnalysis.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f3840a8c..9ca35e79 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -167,8 +167,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* We need to know if the declaration group contains a global - note that * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in - cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration"; (*TODO recheck how to get meta*) - cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration"; + cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "This global definition is in a group of mutually recursive definitions"; + cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "This builtin function belongs to a group of mutually recursive definitions"; (* We ignore on purpose functions that cannot fail and consider they *can* * fail: the result of the analysis is not used yet to adjust the translation * so that the functions which syntactically can't fail don't use an error monad. -- cgit v1.2.3 From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 17:14:27 +0100 Subject: formatting --- compiler/FunsAnalysis.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 9ca35e79..f85f9d1e 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -167,8 +167,15 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* We need to know if the declaration group contains a global - note that * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in - cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "This global definition is in a group of mutually recursive definitions"; - cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "This builtin function belongs to a group of mutually recursive definitions"; + cassert + ((not is_global_decl_body) || List.length d = 1) + (List.hd d).meta + "This global definition is in a group of mutually recursive definitions"; + cassert + ((not !group_has_builtin_info) || List.length d = 1) + (List.hd d).meta + "This builtin function belongs to a group of mutually recursive \ + definitions"; (* We ignore on purpose functions that cannot fail and consider they *can* * fail: the result of the analysis is not used yet to adjust the translation * so that the functions which syntactically can't fail don't use an error monad. -- cgit v1.2.3 From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 13:21:08 +0100 Subject: added file and line arg to craise and cassert --- compiler/FunsAnalysis.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f85f9d1e..df2a010d 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -145,7 +145,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - sanity_check ((not f.is_global_decl_body) || not !stateful) f.meta; + sanity_check __FILE__ __LINE__ ((not f.is_global_decl_body) || not !stateful) f.meta; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; @@ -167,11 +167,11 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* We need to know if the declaration group contains a global - note that * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in - cassert + cassert __FILE__ __LINE__ ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "This global definition is in a group of mutually recursive definitions"; - cassert + cassert __FILE__ __LINE__ ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "This builtin function belongs to a group of mutually recursive \ -- cgit v1.2.3 From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 14:07:36 +0100 Subject: formatting and changed save_error condition for failing from b to not b --- compiler/FunsAnalysis.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index df2a010d..cad469f9 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -145,7 +145,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - sanity_check __FILE__ __LINE__ ((not f.is_global_decl_body) || not !stateful) f.meta; + sanity_check __FILE__ __LINE__ + ((not f.is_global_decl_body) || not !stateful) + f.meta; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; -- cgit v1.2.3 From 1a86cac476c1f5c0d64d5a12db267d3ac651561b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 29 Mar 2024 17:49:46 +0100 Subject: Cleanup and fix a mistake --- compiler/FunsAnalysis.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index cad469f9..f194d4e5 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -119,7 +119,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_Call env call = (match call.func with | FnOpMove _ -> - (* Ignoring this: we lookup t he called function upon creating + (* Ignoring this: we lookup the called function upon creating the closure *) () | FnOpRegular func -> ( @@ -145,9 +145,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - sanity_check __FILE__ __LINE__ + cassert __FILE__ __LINE__ ((not f.is_global_decl_body) || not !stateful) - f.meta; + f.meta "Global definition containing a stateful call in its body"; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; -- cgit v1.2.3