[pulse] underapproximate joins of array values

Summary:
Arrays are the main source of false positives that prevent us from
having a better (less under-approximate) join in general. The next diff
improves join and I split this off to make it easier to review.

Reviewed By: mbouaziz

Differential Revision: D12881986

fbshipit-source-id: 5f52dea27

infer/src/checkers/PulseDomain.ml

@@ -221,10 +221,19 @@ module Domain : AbstractDomain.S with type astate = t = struct
     let union_one_edge subst src_addr access dst_addr union_heap =
       let src_addr = to_canonical_address subst src_addr in
       let dst_addr = to_canonical_address subst dst_addr in
-      match Memory.find_edge_opt src_addr access union_heap with
-      | None ->
+      match
+        (Memory.find_edge_opt src_addr access union_heap, (access : AccessExpression.Access.t))
+      with
+      | Some dst_addr', _ when AbstractAddress.equal dst_addr dst_addr' ->
+          (* same edge *)
+          (union_heap, `No_new_equality)
+      | _, ArrayAccess _ ->
+          (* do not trust array accesses for now, replace the destination of the edge by a fresh location *)
+          ( Memory.add_edge src_addr access (AbstractAddress.mk_fresh ()) union_heap
+          , `No_new_equality )
+      | None, _ ->
           (Memory.add_edge src_addr access dst_addr union_heap, `No_new_equality)
-      | Some dst_addr' ->
+      | Some dst_addr', _ ->
           (* new equality [dst_addr = dst_addr'] found *)
           ignore (AddressUF.union subst dst_addr dst_addr') ;
           (union_heap, `New_equality)

infer/src/checkers/PulseModels.ml

@@ -63,8 +63,10 @@ module StdVector = struct
       "__internal_array"
 
 
+  let to_internal_array vector = AccessExpression.field_offset vector internal_array
+
   let deref_internal_array vector =
-    AccessExpression.(array_offset (dereference (field_offset vector internal_array)) Typ.void [])
+    AccessExpression.(array_offset (dereference (to_internal_array vector)) Typ.void [])
 
 
   let at : model =
@@ -81,9 +83,13 @@ module StdVector = struct
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
-        let deref_array = deref_internal_array vector in
-        PulseDomain.invalidate (StdVectorPushBack (vector, location)) location deref_array astate
-        >>= PulseDomain.havoc location deref_array
+        let array = to_internal_array vector in
+        (* all elements should be invalidated *)
+        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
 end