From 50da07e922b30a34dddb5985ec533187d09496fc Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Tue, 23 Oct 2018 08:52:57 -0700 Subject: [PATCH] [pulse] Invalidate addresses for destructors Summary: Invalidating addresses for destructors to catch use after destructor errors. To pass ownership tests for use after destructor errors, we still need to: (1) fix pointer arithmetic false positives (2) add model for placement new to fix false positives (3) add model for operator= to fix false positives (4) support inter-procedural analysis for destructor_order_bad test Reviewed By: jvillard Differential Revision: D10450912 fbshipit-source-id: 2d9b1ee68 --- infer/src/checkers/Pulse.ml | 32 ++++++++++++++++--- .../tests/codetoanalyze/cpp/pulse/issues.exp | 15 +++++++++ 2 files changed, 42 insertions(+), 5 deletions(-) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 9967fb84e..35e6ceeaa 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -30,6 +30,29 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = Summary.t + let is_destructor = function + | Typ.Procname.ObjC_Cpp clang_pname -> + Typ.Procname.ObjC_Cpp.is_destructor clang_pname + && not + (* Our frontend generates synthetic inner destructors to model invocation of base class + destructors correctly; see D5834555/D7189239 *) + (Typ.Procname.ObjC_Cpp.is_inner_destructor clang_pname) + | _ -> + false + + + let exec_call _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate = + match call with + | Direct callee_pname when is_destructor callee_pname -> ( + match actuals with + | [AccessExpression destroyed_access] -> + PulseDomain.invalidate call_loc destroyed_access astate + | _ -> + Ok astate ) + | _ -> + PulseDomain.read_all call_loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate + + let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate = let model = match call with @@ -41,9 +64,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in match model with | None -> - PulseDomain.havoc (fst ret) astate |> Result.return + exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc (fst ret) | Some model -> - model call_loc ~ret ~actuals astate + PulseDomain.read_all call_loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate + >>= model call_loc ~ret ~actuals let exec_instr (astate : PulseDomain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t) @@ -65,9 +89,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Assume (condition, _, _, loc) -> PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary | Call (ret, call, actuals, flags, loc) -> - PulseDomain.read_all loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate - >>= dispatch_call ret call actuals flags loc - |> check_error summary + dispatch_call ret call actuals flags loc astate |> check_error summary let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 733539526..2c27e9d27 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,5 +1,11 @@ +codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a.str)` here] +codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a.a.str)` here] +codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `s.i` here] codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here] codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here] +codetoanalyze/cpp/ownership/basics.cpp, pointer_arithmetic_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `a` here,accessed `a` here] +codetoanalyze/cpp/ownership/basics.cpp, struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a)` here] +codetoanalyze/cpp/ownership/returns.cpp, returns::FN_return_destructed_pointer_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `x` here,accessed `x` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] @@ -13,5 +19,14 @@ codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad, codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s->f` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing1_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing2_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, destruct_pointer_contents_then_placement_new1_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, placement_new_non_var_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `m.s` here,accessed `m.s` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `*(s.f)` here] +codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(c)` here,accessed `pc->f` here] codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `result` here,accessed `*(result)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(x).__internal_array[_]` here,accessed `*(y)` here]