From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 31 Aug 2023 12:47:43 +0200 Subject: Start adding support for traits --- compiler/FunsAnalysis.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index b72fa078..f4406653 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -70,14 +70,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with - | Use _ | Ref _ | Global _ | Discriminant _ | Aggregate _ -> () + | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> () | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := EU.binop_can_fail bop || !can_fail method! visit_Call env call = (match call.func with - | Regular id -> + | FunId (Regular id) -> if FunDeclId.Set.mem id fun_ids then ( can_diverge := true; is_rec := true) @@ -86,9 +86,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) self#may_fail info.can_fail; stateful := !stateful || info.stateful; can_diverge := !can_diverge || info.can_diverge - | Assumed id -> + | FunId (Assumed id) -> (* None of the assumed functions can diverge nor are considered stateful *) - can_fail := !can_fail || Assumed.assumed_can_fail id); + can_fail := !can_fail || Assumed.assumed_can_fail id + | TraitMethod _ -> + (* We consider trait functions can fail, diverge, and are not stateful *) + can_fail := true; + can_diverge := true); super#visit_Call env call method! visit_Panic env = @@ -141,7 +145,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let rec analyze_decl_groups (decls : declaration_group list) : unit = match decls with | [] -> () - | Type _ :: decls' -> analyze_decl_groups decls' + | (Type _ | TraitDecl _ | TraitImpl _) :: decls' -> + analyze_decl_groups decls' | Fun decl :: decls' -> analyze_fun_decl_group decl; analyze_decl_groups decls' -- cgit v1.2.3 From f11d5186b467df318f7c09eedf8b5629c165b453 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 20 Oct 2023 15:05:00 +0200 Subject: Start updating to handle function pointers --- 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 f4406653..a09a6d05 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -76,7 +76,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) can_fail := EU.binop_can_fail bop || !can_fail method! visit_Call env call = - (match call.func with + (match call.func.func with | FunId (Regular id) -> if FunDeclId.Set.mem id fun_ids then ( can_diverge := true; -- cgit v1.2.3 From c27c3052ec3f9a093b06a41f56b3a361cb65e950 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Sun, 22 Oct 2023 16:34:46 -0700 Subject: Add more support for numeric operations, xor, rotate --- compiler/FunsAnalysis.ml | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f4406653..f8aa06dc 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -58,6 +58,24 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let can_diverge = ref false in let is_rec = ref false in + (* We have some specialized knowledge of some library functions; we don't + have any more custom treatment than this, and these functions can be modeled + suitably in Primitives.fst, rather than special-casing for them all the + way. *) + let module M = struct type opaque_info = { fallible: bool; stateful: bool } end in + let open M in + let opaque_info (f: fun_decl) = + match f.name with + | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "wrapping_add" ] + | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "rotate_left" ] -> + { fallible = false; stateful = false } + | _ -> + (* Opaque function: we consider they fail by default *) + { fallible = true; stateful = true } + in + + (* JP: Why not use a reduce visitor here with a tuple of the values to be + computed? *) let visit_fun (f : fun_decl) : unit = let obj = object (self) @@ -108,9 +126,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) assert ((not f.is_global_decl_body) || not !stateful); match f.body with | None -> - (* Opaque function: we consider they fail by default *) - obj#may_fail true; - stateful := (not f.is_global_decl_body) && use_state + let info = opaque_info f in + obj#may_fail info.fallible; + stateful := (not f.is_global_decl_body) && use_state && info.stateful | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; -- 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/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 a09a6d05..5e849ba7 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -88,7 +88,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) can_diverge := !can_diverge || info.can_diverge | FunId (Assumed id) -> (* None of the assumed functions can diverge nor are considered stateful *) - can_fail := !can_fail || Assumed.assumed_can_fail id + can_fail := !can_fail || Assumed.assumed_fun_can_fail id | TraitMethod _ -> (* We consider trait functions can fail, diverge, and are not stateful *) can_fail := true; -- cgit v1.2.3 From 9c230dddebb171ee1b3e0176838441163836b875 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 24 Oct 2023 18:16:53 +0200 Subject: Handle properly the builtin, non fallible functions --- compiler/FunsAnalysis.ml | 34 +++++++++++++++++++--------------- 1 file changed, 19 insertions(+), 15 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 1273f57d..3ba5d35d 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -57,21 +57,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let stateful = ref false in let can_diverge = ref false in let is_rec = ref false in + let is_builtin_non_fallible_group = ref false in (* We have some specialized knowledge of some library functions; we don't have any more custom treatment than this, and these functions can be modeled suitably in Primitives.fst, rather than special-casing for them all the way. *) - let module M = struct type opaque_info = { fallible: bool; stateful: bool } end in - let open M in - let opaque_info (f: fun_decl) = - match f.name with - | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "wrapping_add" ] - | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "rotate_left" ] -> - { fallible = false; stateful = false } - | _ -> - (* Opaque function: we consider they fail by default *) - { fallible = true; stateful = true } + let is_builtin_non_fallible (f : fun_decl) : bool = + let open ExtractBuiltin in + let name = name_to_simple_name f.name in + SimpleNameSet.mem name builtin_non_fallible_funs_set in (* JP: Why not use a reduce visitor here with a tuple of the values to be @@ -124,11 +119,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) in (* Sanity check: global bodies don't contain stateful calls *) assert ((not f.is_global_decl_body) || not !stateful); + let is_builtin_non_fallible = is_builtin_non_fallible f in + is_builtin_non_fallible_group := + !is_builtin_non_fallible_group || is_builtin_non_fallible; match f.body with | None -> - let info = opaque_info f in - obj#may_fail info.fallible; - stateful := (not f.is_global_decl_body) && use_state && info.stateful + obj#may_fail (not is_builtin_non_fallible); + stateful := + (not f.is_global_decl_body) + && use_state + && not is_builtin_non_fallible | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; @@ -136,12 +136,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * 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 !is_builtin_non_fallible_group) || List.length d = 1); (* 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. - * However, we do keep the result of the analysis for global bodies. + * However, we do keep the result of the analysis for global bodies and for + * builtin functions which are marked as non-fallible. * *) - can_fail := (not is_global_decl_body) || !can_fail; + can_fail := + ((not is_global_decl_body) && not !is_builtin_non_fallible_group) + || !can_fail; { can_fail = !can_fail; stateful = !stateful; -- cgit v1.2.3 From 005ad3cc03745bc9211defa481d5e45738a6d832 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 26 Oct 2023 14:37:34 +0200 Subject: Improve the handling of saved function effects in ExtractBuiltin.ml --- compiler/FunsAnalysis.ml | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 3ba5d35d..9eac3e6f 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -57,16 +57,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let stateful = ref false in let can_diverge = ref false in let is_rec = ref false in - let is_builtin_non_fallible_group = ref false in + let group_has_builtin_info = ref false in (* We have some specialized knowledge of some library functions; we don't have any more custom treatment than this, and these functions can be modeled suitably in Primitives.fst, rather than special-casing for them all the way. *) - let is_builtin_non_fallible (f : fun_decl) : bool = + let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option = let open ExtractBuiltin in let name = name_to_simple_name f.name in - SimpleNameSet.mem name builtin_non_fallible_funs_set + SimpleNameMap.find_opt name builtin_fun_effects_map in (* JP: Why not use a reduce visitor here with a tuple of the values to be @@ -119,16 +119,21 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) in (* Sanity check: global bodies don't contain stateful calls *) assert ((not f.is_global_decl_body) || not !stateful); - let is_builtin_non_fallible = is_builtin_non_fallible f in - is_builtin_non_fallible_group := - !is_builtin_non_fallible_group || is_builtin_non_fallible; + 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; match f.body with | None -> - obj#may_fail (not is_builtin_non_fallible); + let info_can_fail, info_stateful = + match builtin_info with + | None -> (true, false) + | Some { can_fail; stateful } -> (can_fail, stateful) + in + obj#may_fail info_can_fail; stateful := (not f.is_global_decl_body) && use_state - && not is_builtin_non_fallible + && not (has_builtin_info && not info_stateful) | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; @@ -136,7 +141,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * 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 !is_builtin_non_fallible_group) || List.length d = 1); + assert ((not !group_has_builtin_info) || List.length d = 1); (* 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. @@ -144,8 +149,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * builtin functions which are marked as non-fallible. * *) can_fail := - ((not is_global_decl_body) && not !is_builtin_non_fallible_group) - || !can_fail; + if is_global_decl_body then !can_fail + else if !group_has_builtin_info then !can_fail + else true; { can_fail = !can_fail; stateful = !stateful; -- cgit v1.2.3 From 7ffcb8e9c5c03f198362fd27bd42f30064541509 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 26 Oct 2023 15:06:36 +0200 Subject: Fix some issues and regenerate the HashmapMain example for Lean --- compiler/FunsAnalysis.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 9eac3e6f..69c0df71 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -76,6 +76,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) object (self) inherit [_] iter_statement as super method may_fail b = can_fail := !can_fail || b + method maybe_stateful b = stateful := !stateful || b method! visit_Assert env a = self#may_fail true; @@ -126,14 +127,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) | None -> let info_can_fail, info_stateful = match builtin_info with - | None -> (true, false) + | None -> (true, use_state) | Some { can_fail; stateful } -> (can_fail, stateful) in obj#may_fail info_can_fail; - stateful := - (not f.is_global_decl_body) - && use_state - && not (has_builtin_info && not info_stateful) + obj#maybe_stateful + (if f.is_global_decl_body then false + else if not use_state then false + else info_stateful) | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; -- cgit v1.2.3 From 3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 16:22:09 +0100 Subject: Make the traits work for Coq --- compiler/FunsAnalysis.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 69c0df71..e17ea16f 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -104,9 +104,10 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* None of the assumed functions can diverge nor are considered stateful *) can_fail := !can_fail || Assumed.assumed_fun_can_fail id | TraitMethod _ -> - (* We consider trait functions can fail, diverge, and are not stateful *) - can_fail := true; - can_diverge := true); + (* We consider trait functions can fail, but can not diverge and are not stateful. + TODO: this may cause issues if we use use a fuel parameter. + *) + can_fail := true); super#visit_Call env call method! visit_Panic env = -- cgit v1.2.3