[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

@@ -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 =

infer/tests/codetoanalyze/cpp/pulse/basics.cpp

@@ -92,7 +92,7 @@ struct A {
 
 A getA();
 
-int FP_struct_inside_loop_ok(std::vector<int> numbers) {
+int struct_inside_loop_ok(std::vector<int> numbers) {
   int sum;
   for (auto number : numbers) {
     A a = getA();

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_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_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]

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);
   }