diff options
author | Sidney Congard | 2022-06-30 12:22:14 +0200 |
---|---|---|
committer | Sidney Congard | 2022-06-30 12:22:14 +0200 |
commit | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (patch) | |
tree | 06ac570c7f9eee49987d716e043415ae31c681d0 /src/FunsAnalysis.ml | |
parent | da118da3e590fbea4e880121837da2ee938837f6 (diff) |
Traduct globals body separately (WIP)
Diffstat (limited to 'src/FunsAnalysis.ml')
-rw-r--r-- | src/FunsAnalysis.ml | 77 |
1 files changed, 43 insertions, 34 deletions
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index dc205eb9..ca20352f 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -1,6 +1,6 @@ (** Compute various information, including: - can a function fail (by having `Fail` in its body, or transitively - calling a function which can fail) + calling a function which can fail), false for globals - can a function diverge (bu being recursive, containing a loop or transitively calling a function which can diverge) - does a function perform stateful operations (i.e., do we need a state @@ -49,47 +49,56 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) let stateful = ref false in let divergent = ref false in - let obj = - object - inherit [_] iter_statement as super - - method! visit_Assert env a = - can_fail := true; - super#visit_Assert env a - - method! visit_Call env call = - (match call.func with - | Regular id -> - if FunDeclId.Set.mem id fun_ids then divergent := true - else - let info = FunDeclId.Map.find id !infos in - can_fail := !can_fail || info.can_fail; - stateful := !stateful || info.stateful; - divergent := !divergent || info.divergent - | Assumed id -> - (* None of the assumed functions is stateful for now *) - can_fail := !can_fail || Assumed.assumed_can_fail id); - super#visit_Call env call - - method! visit_Panic env = - can_fail := true; - super#visit_Panic env - - method! visit_Loop env loop = - divergent := true; - super#visit_Loop env loop - end - in - let visit_fun (f : fun_decl) : unit = + print_endline ("@ fun: " ^ Print.fun_name_to_string f.name); + let obj = + object (self) + inherit [_] iter_statement as super + + method may_fail b = + if f.is_global then () else + can_fail := !can_fail || b + + method! visit_Assert env a = + self#may_fail true; + super#visit_Assert env a + + method! visit_Call env call = + print_string "@ dep: "; + pp_fun_id Format.std_formatter call.func; + print_newline (); + + (match call.func with + | Regular id -> + if FunDeclId.Set.mem id fun_ids then divergent := true + else + let info = FunDeclId.Map.find id !infos in + self#may_fail info.can_fail; + stateful := !stateful || info.stateful; + divergent := !divergent || info.divergent + | Assumed id -> + (* None of the assumed functions is stateful for now *) + can_fail := !can_fail || Assumed.assumed_can_fail id); + super#visit_Call env call + + method! visit_Panic env = + self#may_fail true; + super#visit_Panic env + + method! visit_Loop env loop = + divergent := true; + super#visit_Loop env loop + end + in match f.body with | None -> (* Opaque function *) - can_fail := true; + obj#may_fail true; stateful := use_state | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; + print_endline ("@ can_fail: " ^ Bool.to_string !can_fail); { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } in |