[pulse] back to sounder joins

Summary:
Now that arrays are dealt with separately (see previous diff), we can
turn the join back into an over-approximation as far as invalid
locations are concerned.

Reviewed By: skcho

Differential Revision: D12881989

fbshipit-source-id: fd85e49c0

infer/src/checkers/PulseDomain.ml

@@ -61,6 +61,8 @@ module Memory : sig
 
   val fold : (AbstractAddress.t -> edges -> 'accum -> 'accum) -> t -> 'accum -> 'accum
 
+  val mem : AbstractAddress.t -> t -> bool
+
   val pp : F.formatter -> t -> unit
 
   val add_edge : AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddress.t -> t -> t
@@ -89,6 +91,8 @@ end = struct
 
   let fold = Graph.fold
 
+  let mem = Graph.mem
+
   let pp = Graph.pp ~pp_value:(Edges.pp ~pp_value:AbstractAddress.pp)
 
   (* {3 Helper functions to traverse the two maps at once } *)
@@ -150,16 +154,15 @@ module InvalidAddressesDomain : sig
 
   val add : AbstractAddress.t -> Invalidation.t -> astate -> astate
 
+  val fold :
+    (AbstractAddress.t -> Invalidation.t -> 'accum -> 'accum) -> astate -> 'accum -> 'accum
+
   val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option
   (** None denotes a valid location *)
-
-  val is_invalid : AbstractAddress.t -> astate -> bool
 end = struct
   include AbstractDomain.Map (AbstractAddress) (Invalidation)
 
   let get_invalidation address invalids = find_opt address invalids
-
-  let is_invalid address invalids = mem address invalids
 end
 
 (** the domain *)
@@ -299,39 +302,43 @@ module Domain : AbstractDomain.S with type astate = t = struct
 
 
     (** compute new set of invalid addresses for a given join state *)
-    let to_invalids {subst; astate= {invalids= old_invalids}} =
+    let to_invalids {subst; astate= {invalids= old_invalids} as astate} =
-      (* iterate over all discovered equivalence classes *)
+      (* Is the address reachable from the stack variables? Since the new heap only has addresses
-      AddressUF.fold_sets subst ~init:InvalidAddressesDomain.empty
+         reachable from stack variables it suffices to check if the address appears in either the
-        ~f:(fun new_invalids (repr, set) ->
+         heap or the stack. *)
-          (* Add [repr] as an invalid address if *all* the addresses it represents were known to
+      let address_is_live astate address =
-             be invalid. This is unsound but avoids false positives for now. *)
+        Memory.mem address astate.heap
-          if
+        || AliasingDomain.exists (fun _ value -> AbstractAddress.equal value address) astate.stack
-            AddressUnionSet.Set.for_all
+      in
-              (fun addr -> InvalidAddressesDomain.is_invalid addr old_invalids)
+      (* given a previously known invalid address [old_address], add the new address that
-              !set
+         represents it to [new_invalids] *)
-          then
+      let add_old_invalid astate old_address old_invalid new_invalids =
-            (* join the invalidation reasons for all the invalidations of the representative *)
+        (* the address has to make sense for the new heap *)
-            let reason =
+        let repr = AddressUF.find subst old_address in
-              AddressUnionSet.Set.fold
+        let new_address = (repr :> AbstractAddress.t) in
-                (fun address reason ->
+        match InvalidAddressesDomain.get_invalidation new_address new_invalids with
-                  (* this is safe because of [for_all] above *)
+        | Some new_invalid ->
-                  let reason' =
+            (* We have seen a representative of this address already: join. This can happen when
-                    Option.value_exn (InvalidAddressesDomain.get_invalidation address old_invalids)
+               several previously invalid addresses correspond to the same representative in
-                  in
+               [subst]. Doing the join of all known invalidation reasons to make results more
-                  match reason with
+               deterministic(?).  *)
-                  | None ->
+            InvalidAddressesDomain.add new_address
-                      Some reason'
+              (Invalidation.join new_invalid old_invalid)
-                  | Some reason ->
-                      Some (Invalidation.join reason reason') )
-                !set None
-            in
-            InvalidAddressesDomain.add
-              (repr :> AbstractAddress.t)
-              ((* safe because [!set] cannot be empty so there is at least one address to join from
-                  *)
-               Option.value_exn reason)
               new_invalids
-          else new_invalids )
+        | None ->
+            (* only record the old invalidation fact if the address is still reachable (helps
+               convergence) *)
+            if address_is_live astate new_address then
+              InvalidAddressesDomain.add new_address old_invalid new_invalids
+            else
+              (* we can forget about the fact that this location is invalid since nothing can
+                   refer to it anymore *)
+              new_invalids
+      in
+      InvalidAddressesDomain.fold
+        (fun old_address old_invalid new_invalids ->
+          add_old_invalid astate old_address old_invalid new_invalids )
+        old_invalids InvalidAddressesDomain.empty
 
 
     let rec normalize state =

infer/src/checkers/PulseModels.ml

@@ -88,7 +88,6 @@ module StdVector = struct
         let array_elements = deref_internal_array vector in
         let invalidation = PulseInvalidation.StdVectorPushBack (vector, location) in
         PulseDomain.invalidate invalidation location array_elements astate
-        >>= PulseDomain.invalidate invalidation location array
         >>= PulseDomain.havoc location array
     | _ ->
         Ok astate

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

@@ -14,7 +14,7 @@ struct Aggregate {
   ~Aggregate() {}
 };
 
-void aggregate_reassign_ok() {
+void FP_aggregate_reassign_ok() {
   const int len = 5;
   Aggregate arr[len];
   for (int i = 0; i < len; i++) {
@@ -29,7 +29,7 @@ struct AggregateWithConstructedField {
   std::string str;
 };
 
-void aggregate_reassign2_ok() {
+void FP_aggregate_reassign2_ok() {
   AggregateWithConstructedField arr[10];
   for (int i = 0; i < 10; i++) {
     // this is translated as string(&(a.str), "hi"). need to make sure this is
@@ -43,7 +43,7 @@ struct NestedAggregate {
   AggregateWithConstructedField a;
 };
 
-void aggregate_reassign3_ok() {
+void FP_aggregate_reassign3_ok() {
   NestedAggregate arr[10];
   for (int i = 0; i < 10; i++) {
     // this is translated as std::basic_string(&(a.str), "hi"). need to make
@@ -62,7 +62,7 @@ int multiple_invalidations_branch_bad(int n, int* ptr) {
   return *ptr;
 }
 
-int FN_multiple_invalidations_loop_bad(int n, int* ptr) {
+int multiple_invalidations_loop_bad(int n, int* ptr) {
   for (int i = 0; i < n; i++) {
     if (i == 7) {
       delete ptr;

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,6 +1,15 @@
+codetoanalyze/cpp/pulse/basics.cpp, FP_aggregate_reassign2_ok, 5, USE_AFTER_DESTRUCTOR, 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_DESTRUCTOR, 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_DESTRUCTOR, 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, 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, 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]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 50, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 37, column 3 here,accessed `s->f` here]
@@ -14,6 +23,8 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing3_bad, 6
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 61, column 3 here,accessed `*(s.f)` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 194, column 3 here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 55, column 5 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_loop_ok, 7, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 46, column 5 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, column 3 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here]

infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp

@@ -51,7 +51,7 @@ void double_delete_bad() {
   delete s;
 }
 
-Simple* FN_delete_in_branch_bad(bool b) {
+Simple* delete_in_branch_bad(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;
@@ -76,7 +76,7 @@ void use_in_branch_bad(bool b) {
   }
 }
 
-void FN_delete_in_loop_bad() {
+void delete_in_loop_bad() {
   auto s = new Simple{1};
   for (int i = 0; i < 10; i++) {
     delete s;
@@ -105,7 +105,7 @@ void use_in_loop_bad() {
   }
 }
 
-Simple* gated_delete_abort_ok(bool b) {
+Simple* FP_gated_delete_abort_ok(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;
@@ -114,7 +114,7 @@ Simple* gated_delete_abort_ok(bool b) {
   return s;
 }
 
-Simple* gated_exit_abort_ok(bool b) {
+Simple* FP_gated_exit_abort_ok(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;
@@ -123,7 +123,7 @@ Simple* gated_exit_abort_ok(bool b) {
   return s;
 }
 
-Simple* gated_delete_throw_ok(bool b) {
+Simple* FP_gated_delete_throw_ok(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -38,7 +38,7 @@ void FP_reserve_then_push_back_ok(std::vector<int>& vec) {
   std::cout << *elt << "\n";
 }
 
-void reserve_then_push_back_loop_ok(std::vector<int>& vec,
+void FP_reserve_then_push_back_loop_ok(std::vector<int>& vec,
                                     std::vector<int>& vec_other) {
   vec.reserve(vec.size() + vec_other.size());
   int* elt = &vec[1];
@@ -48,7 +48,7 @@ void reserve_then_push_back_loop_ok(std::vector<int>& vec,
   std::cout << *elt << "\n";
 }
 
-void init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
+void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
   std::vector<int> vec(vec_other.size());
   int* elt = &vec[1];
   for (const auto& i : vec_other) {