diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 204bb492b..420cc0d95 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -89,18 +89,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct read_all actuals astate - let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate = + let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) flags call_loc astate = let model = match call with | Indirect _ -> (* function pointer, etc.: skip for now *) None | Direct callee_pname -> - PulseModels.dispatch callee_pname + PulseModels.dispatch callee_pname flags in match model with | None -> - exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc_var (fst ret) + exec_call ret call actuals flags call_loc astate >>| PulseDomain.havoc_var (fst ret) | Some model -> model call_loc ~ret ~actuals astate diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index 850d683be..570d68542 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -17,6 +17,10 @@ type exec_fun = type model = exec_fun +module Misc = struct + let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok PulseDomain.initial +end + module C = struct let free : model = fun location ~ret:_ ~actuals astate -> @@ -119,7 +123,10 @@ let builtins_dispatcher = [ (BuiltinDecl.__delete, Cplusplus.delete) ; (BuiltinDecl.__placement_new, Cplusplus.placement_new) ; (BuiltinDecl.__variable_initialization, C.variable_initialization) - ; (BuiltinDecl.free, C.free) ] + ; (BuiltinDecl.abort, Misc.early_exit) + ; (BuiltinDecl.exit, Misc.early_exit) + ; (BuiltinDecl.free, C.free) + ; (BuiltinDecl.objc_cpp_throw, Misc.early_exit) ] in let builtins_map = Hashtbl.create @@ -137,9 +144,13 @@ let builtins_dispatcher = fun proc_name -> Hashtbl.find builtins_map proc_name -let dispatch proc_name = +let dispatch proc_name flags = match builtins_dispatcher proc_name with | Some _ as result -> result - | None -> - ProcNameDispatcher.dispatch () proc_name + | None -> ( + match ProcNameDispatcher.dispatch () proc_name with + | Some _ as result -> + result + | None -> + if flags.CallFlags.cf_noreturn then Some Misc.early_exit else None ) diff --git a/infer/src/checkers/PulseModels.mli b/infer/src/checkers/PulseModels.mli index dfd9aaee7..f6ddc7070 100644 --- a/infer/src/checkers/PulseModels.mli +++ b/infer/src/checkers/PulseModels.mli @@ -15,4 +15,4 @@ type exec_fun = type model = exec_fun -val dispatch : Typ.Procname.t -> model option +val dispatch : Typ.Procname.t -> CallFlags.t -> model option diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 888540089..229bc12ba 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -2,9 +2,6 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AF codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70, column 7 here,accessed `*(ptr)` here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 26, column 5 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 111, column 5 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_throw_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 129, column 5 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_exit_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 120, column 5 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp index d9a96b6e5..6fd5a084c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp @@ -105,7 +105,7 @@ void use_in_loop_bad() { } } -Simple* FP_gated_delete_abort_ok(bool b) { +Simple* gated_delete_abort_ok(bool b) { auto s = new Simple{1}; if (b) { delete s; @@ -114,7 +114,7 @@ Simple* FP_gated_delete_abort_ok(bool b) { return s; } -Simple* FP_gated_exit_abort_ok(bool b) { +Simple* gated_exit_abort_ok(bool b) { auto s = new Simple{1}; if (b) { delete s; @@ -123,7 +123,7 @@ Simple* FP_gated_exit_abort_ok(bool b) { return s; } -Simple* FP_gated_delete_throw_ok(bool b) { +Simple* gated_delete_throw_ok(bool b) { auto s = new Simple{1}; if (b) { delete s;