summaryrefslogtreecommitdiff
path: root/compiler/FunsAnalysis.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/FunsAnalysis.ml')
-rw-r--r--compiler/FunsAnalysis.ml112
1 files changed, 86 insertions, 26 deletions
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index b72fa078..f6976f23 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -8,7 +8,7 @@
*)
open LlbcAst
-module EU = ExpressionsUtils
+open ExpressionsUtils
(** Various information about a function.
@@ -57,12 +57,44 @@ 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 group_has_builtin_info = ref false in
+ let name_matcher_ctx : Charon.NameMatcher.ctx =
+ {
+ type_decls = m.type_decls;
+ global_decls = m.global_decls;
+ fun_decls = m.fun_decls;
+ trait_decls = m.trait_decls;
+ trait_impls = m.trait_impls;
+ }
+ 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 get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option =
+ let open ExtractBuiltin in
+ NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map
+ 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)
inherit [_] iter_statement as super
method may_fail b = can_fail := !can_fail || b
+ method maybe_stateful b = stateful := !stateful || b
+
+ method visit_fid id =
+ if FunDeclId.Set.mem id fun_ids then (
+ can_diverge := true;
+ is_rec := true)
+ else
+ let info = FunDeclId.Map.find id !infos in
+ self#may_fail info.can_fail;
+ stateful := !stateful || info.stateful;
+ can_diverge := !can_diverge || info.can_diverge
method! visit_Assert env a =
self#may_fail true;
@@ -70,25 +102,37 @@ 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 _ -> ()
- | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail
+ | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> ()
+ | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail
| BinaryOp (bop, _, _) ->
- can_fail := EU.binop_can_fail bop || !can_fail
+ can_fail := binop_can_fail bop || !can_fail
+
+ method! visit_Closure env id args =
+ (* Remark: `Closure` is a trait instance id - TODO: rename this variant *)
+ self#visit_fid id;
+ super#visit_Closure env id args
+
+ method! visit_AggregatedClosure env id args =
+ self#visit_fid id;
+ super#visit_AggregatedClosure env id args
method! visit_Call env call =
(match call.func with
- | Regular id ->
- if FunDeclId.Set.mem id fun_ids then (
- can_diverge := true;
- is_rec := true)
- else
- let info = FunDeclId.Map.find id !infos in
- self#may_fail info.can_fail;
- stateful := !stateful || info.stateful;
- can_diverge := !can_diverge || info.can_diverge
- | Assumed id ->
- (* None of the assumed functions can diverge nor are considered stateful *)
- can_fail := !can_fail || Assumed.assumed_can_fail id);
+ | FnOpMove _ ->
+ (* Ignoring this: we lookup the called function upon creating
+ the closure *)
+ ()
+ | FnOpRegular func -> (
+ match func.func with
+ | FunId (FRegular id) -> self#visit_fid id
+ | FunId (FAssumed id) ->
+ (* 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, 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 =
@@ -102,11 +146,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 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 ->
- (* Opaque function: we consider they fail by default *)
- obj#may_fail true;
- stateful := (not f.is_global_decl_body) && use_state
+ let info_can_fail, info_stateful =
+ match builtin_info with
+ | None -> (true, use_state)
+ | Some { can_fail; stateful } -> (can_fail, stateful)
+ in
+ obj#may_fail info_can_fail;
+ 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;
@@ -114,12 +168,17 @@ 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 !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.
- * 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 :=
+ 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;
@@ -130,7 +189,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
let analyze_fun_decl_group (d : fun_declaration_group) : unit =
(* Retrieve the function declarations *)
- let funs = match d with NonRec id -> [ id ] | Rec ids -> ids in
+ let funs = match d with NonRecGroup id -> [ id ] | RecGroup ids -> ids in
let funs = List.map (fun id -> FunDeclId.Map.find id funs_map) funs in
let fun_ids = List.map (fun (d : fun_decl) -> d.def_id) funs in
let fun_ids = FunDeclId.Set.of_list fun_ids in
@@ -141,14 +200,15 @@ 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'
- | Fun decl :: decls' ->
+ | (TypeGroup _ | TraitDeclGroup _ | TraitImplGroup _) :: decls' ->
+ analyze_decl_groups decls'
+ | FunGroup decl :: decls' ->
analyze_fun_decl_group decl;
analyze_decl_groups decls'
- | Global id :: decls' ->
+ | GlobalGroup id :: decls' ->
(* Analyze a global by analyzing its body function *)
let global = GlobalDeclId.Map.find id globals_map in
- analyze_fun_decl_group (NonRec global.body_id);
+ analyze_fun_decl_group (NonRecGroup global.body);
analyze_decl_groups decls'
in
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 17:39:15 +0000