From 8b54879b0792ab3ee8c1e775941d4fc5283b0e77 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Wed, 31 Oct 2018 06:37:22 -0700 Subject: [PATCH] [pulse] Constructors Summary: Similarly as for destructors, we provide an address of an object as a first parameter to constructors. When constructor is called we want to create a fresh location for a new object. Reviewed By: jvillard Differential Revision: D10868433 fbshipit-source-id: b60f32953 --- infer/src/checkers/Pulse.ml | 14 +++++++++++++- infer/tests/codetoanalyze/cpp/pulse/basics.cpp | 2 +- infer/tests/codetoanalyze/cpp/pulse/issues.exp | 7 ++----- .../cpp/pulse/use_after_destructor.cpp | 4 ++-- 4 files changed, 18 insertions(+), 9 deletions(-) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 7cac412b8..ffdb5ff1f 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -42,6 +42,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_call _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate = + let read_all args astate = + PulseDomain.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate + in match call with | Direct callee_pname when is_destructor callee_pname -> ( match actuals with @@ -54,8 +57,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct call_loc destroyed_object astate | _ -> Ok astate ) + | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> ( + match actuals with + | AccessExpression constructor_access :: rest -> + let constructed_object = + AccessExpression.normalize (AccessExpression.Dereference constructor_access) + in + PulseDomain.havoc call_loc constructed_object astate >>= read_all rest + | _ -> + Ok astate ) | _ -> - PulseDomain.read_all call_loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate + read_all actuals astate let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate = diff --git a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp index b7cb80546..78e2ce3b0 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp @@ -92,7 +92,7 @@ struct A { A getA(); -int FP_struct_inside_loop_ok(std::vector numbers) { +int struct_inside_loop_ok(std::vector numbers) { int sum; for (auto number : numbers) { A a = getA(); diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 1fb54e9a5..2b0796cd8 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,7 +1,6 @@ -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(a)` at line 39, column 3 here,accessed `&(a.str)` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(a)` at line 53, column 3 here,accessed `&(a.a.str)` here] +codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(a)` at line 39, column 3 here,accessed `a.str` here] +codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(a)` at line 53, column 3 here,accessed `a.a.str` here] codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(s)` at line 25, column 3 here,accessed `s.i` here] -codetoanalyze/cpp/pulse/basics.cpp, FP_struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `A_~A(a)` at line 100, column 3 here,accessed `&(a)` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60, column 5 here,accessed `*(ptr)` here] 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, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here] @@ -18,8 +17,6 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 103, column 3 here,accessed `s->f` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 162, column 3 here,accessed `&(s)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_placement_new_explicit_destructor_ok, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(*(s))` at line 43, column 5 here,accessed `&(buf)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 34, column 3 here,accessed `&(s)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 54, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 132, column 3 here,accessed `s` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 0c974db3c..675d843f2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -36,7 +36,7 @@ int FP_reinit_after_explicit_destructor_ok() { return *s.f; } -void FP_placement_new_explicit_destructor_ok() { +void placement_new_explicit_destructor_ok() { char buf[sizeof(S)]; { S* s = new (buf) S(1); @@ -156,7 +156,7 @@ void return_placement_new_ok() { return new (mem) S(2); } -void FP_destructor_in_loop_ok() { +void destructor_in_loop_ok() { for (int i = 0; i < 10; i++) { S s(1); }