[pulse] apply discovered variable equalities eagerly

Summary:
This resolves a few instances of false negatives; typically:

```
  if (x == y) {
    // HERE
    *x = 10;
    *y = 44;
    // THERE
  }
```

We used to get
```
HERE:  &x->v * &y ->v' * v == v'
THERE: &x->v * &y ->v' * v == v' * v |-> 10 * v' |-> 44
```

The state at THERE was thus inconsistent and detected as such (v` and
`v'` are allocated separately in the heap hence cannot be equal).

Now we normalize the state more eagerly and so we get:
```
HERE:  &x->v * &y->v
THERE: &x->v * &y->v * v |-> 44
```

Reviewed By: skcho

Differential Revision: D26488377

fbshipit-source-id: 568e685f0

infer/src/istd/RecencyMap.ml

@@ -29,6 +29,8 @@ module type S = sig
 
   val bindings : t -> (key * value) list
 
+  val exists : t -> f:(key * value -> bool) -> bool
+
   val filter : t -> f:(key * value -> bool) -> t
 
   val find_opt : key -> t -> value option
@@ -39,6 +41,8 @@ module type S = sig
 
   val is_empty : t -> bool
 
+  val map : t -> f:(value -> value) -> t
+
   val mem : t -> key -> bool
 
   val union_left_biased : t -> t -> t
@@ -144,6 +148,12 @@ module Make
 
   let bindings map = fold ~init:[] ~f:(fun bindings binding -> binding :: bindings) map
 
+  let exists map ~f =
+    List.exists map.new_ ~f
+    || List.exists map.old ~f:(fun binding ->
+           if List.Assoc.mem ~equal:Key.equal map.new_ (fst binding) then false else f binding )
+
+
   let filter map ~f =
     let count_new = ref map.count_new in
     let f_update_count_new binding =

infer/src/istd/RecencyMap.mli

@@ -32,6 +32,8 @@ module type S = sig
 
   val bindings : t -> (key * value) list
 
+  val exists : t -> f:(key * value -> bool) -> bool
+
   val filter : t -> f:(key * value -> bool) -> t
 
   val find_opt : key -> t -> value option
@@ -42,6 +44,8 @@ module type S = sig
 
   val is_empty : t -> bool
 
+  val map : t -> f:(value -> value) -> t
+
   val mem : t -> key -> bool
 
   val union_left_biased : t -> t -> t

infer/src/pulse/PulseAbductiveDomain.ml

@@ -34,6 +34,8 @@ module type BaseDomainSig = sig
   (** compute new state containing only reachable addresses in its heap and attributes, as well as
       the list of discarded unreachable addresses *)
 
+  val subst_var : AbstractValue.t * AbstractValue.t -> t -> t SatUnsat.t
+
   val pp : F.formatter -> t -> unit
 end
 
@@ -686,6 +688,12 @@ let is_allocated {post; pre} v =
   || is_stack_allocated (post :> BaseDomain.t) v
 
 
+let subst_var subst astate =
+  let open SatUnsat.Import in
+  let+ post = PostDomain.subst_var subst astate.post in
+  if phys_equal astate.post post then astate else {astate with post}
+
+
 let incorporate_new_eqs astate new_eqs =
   List.fold_until new_eqs ~init:astate
     ~finish:(fun astate -> Sat astate)
@@ -696,12 +704,17 @@ let incorporate_new_eqs astate new_eqs =
           Stop Unsat
       | Equal (v1, v2) when AbstractValue.equal v1 v2 ->
           Continue astate
-      | Equal (v1, v2) ->
+      | Equal (v1, v2) -> (
           if is_allocated astate v1 && is_allocated astate v2 then (
             L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp
               v1 AbstractValue.pp v2 ;
             Stop Unsat )
-          else Continue astate
+          else
+            match subst_var (v1, v2) astate with
+            | Unsat ->
+                Stop Unsat
+            | Sat astate' ->
+                Continue astate' )
       | _ ->
           Continue astate )
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -39,6 +39,8 @@ module type BaseDomainSig = sig
   (** compute new state containing only reachable addresses in its heap and attributes, as well as
       the list of discarded unreachable addresses *)
 
+  val subst_var : AbstractValue.t * AbstractValue.t -> t -> t SatUnsat.t
+
   val pp : F.formatter -> t -> unit
 end
 

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -172,3 +172,10 @@ let canonicalize ~get_var_repr attrs_map =
         let addr' = get_var_repr addr in
         add addr' attrs g )
     attrs_map Graph.empty
+
+
+let subst_var (v, v') attrs_map =
+  if Graph.mem v attrs_map then
+    canonicalize attrs_map ~get_var_repr:(fun addr ->
+        if AbstractValue.equal addr v then v' else addr )
+  else attrs_map

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -66,3 +66,5 @@ val initialize : AbstractValue.t -> t -> t
 val canonicalize : get_var_repr:(AbstractValue.t -> AbstractValue.t) -> t -> t
 (** merge the attributes of all the variables that are equal according to [get_var_repr] and remove
     non-canonical variables in favor of their rerpresentative *)
+
+val subst_var : AbstractValue.t * AbstractValue.t -> t -> t

infer/src/pulse/PulseBaseDomain.ml

@@ -301,3 +301,12 @@ let reachable_addresses_from addresses astate =
   GraphVisit.fold_from_addresses addresses astate ~init:() ~finish:Fn.id ~f:(fun () _ _ ->
       Continue () )
   |> fst
+
+
+let subst_var subst ({heap; stack; attrs} as astate) =
+  let open SatUnsat.Import in
+  let+ heap' = Memory.subst_var subst heap in
+  let stack' = Stack.subst_var subst stack in
+  let attrs' = AddressAttributes.subst_var subst attrs in
+  if phys_equal heap heap' && phys_equal stack stack' && phys_equal attrs attrs' then astate
+  else {heap= heap'; stack= stack'; attrs= attrs'}

infer/src/pulse/PulseBaseDomain.mli

@@ -38,3 +38,5 @@ val is_isograph : lhs:t -> rhs:t -> mapping -> bool
 val find_cell_opt : AbstractValue.t -> t -> cell option
 
 val pp : F.formatter -> t -> unit
+
+val subst_var : AbstractValue.t * AbstractValue.t -> t -> t SatUnsat.t

infer/src/pulse/PulseBaseMemory.ml

@@ -55,6 +55,11 @@ module Edges = struct
         M.add access' (addr', hist) edges' )
 
 
+  let subst_var (v, v') edges =
+    M.map edges ~f:(fun ((addr, hist) as addr_hist) ->
+        if AbstractValue.equal addr v then (v', hist) else addr_hist )
+
+
   include M
 end
 
@@ -103,6 +108,36 @@ let canonicalize ~get_var_repr memory =
   with AliasingContradiction -> Unsat
 
 
+let subst_var (v, v') memory =
+  (* subst in edges *)
+  let memory =
+    let v_appears_in_edges =
+      Graph.exists
+        (fun _ edges -> Edges.exists ~f:(fun (_, (dest, _)) -> AbstractValue.equal v dest) edges)
+        memory
+    in
+    if v_appears_in_edges then Graph.map (Edges.subst_var (v, v')) memory else memory
+  in
+  (* subst in the domain of the graph, already substituted in edges above *)
+  match Graph.find_opt v memory with
+  | None ->
+      Sat memory
+  | Some edges -> (
+      let memory = Graph.remove v memory in
+      match Graph.find_opt v' memory with
+      | None ->
+          Sat (Graph.add v' edges memory)
+      | Some edges' ->
+          if Edges.is_empty edges then Sat memory
+          else if Edges.is_empty edges' then Sat (Graph.add v' edges memory)
+          else (
+            (* both set of edges being non-empty means that [v] and [v'] have been treated as
+               disjoint memory locations until now, contradicting the fact they are equal *)
+            L.d_printfln "CONTRADICTION: %a = %a, which is already allocated in %a@\n"
+              AbstractValue.pp v AbstractValue.pp v' Graph.pp memory ;
+            Unsat ) )
+
+
 include Graph
 
 let compare = Graph.compare Edges.compare

infer/src/pulse/PulseBaseMemory.mli

@@ -43,3 +43,5 @@ val canonicalize : get_var_repr:(AbstractValue.t -> AbstractValue.t) -> t -> t S
 (** replace each address in the heap by its canonical representative according to the current
     equality relation, represented by [get_var_repr]; also remove addresses that point to empty
     edges *)
+
+val subst_var : AbstractValue.t * AbstractValue.t -> t -> t SatUnsat.t

infer/src/pulse/PulseBaseStack.ml

@@ -47,6 +47,10 @@ let canonicalize ~get_var_repr stack =
   if !changed then stack' else stack
 
 
+let subst_var (v, v') stack =
+  canonicalize stack ~get_var_repr:(fun addr -> if AbstractValue.equal v addr then v' else addr)
+
+
 include M
 
 let compare = M.compare AddrHistPair.compare

infer/src/pulse/PulseBaseStack.mli

@@ -24,3 +24,5 @@ val yojson_of_t : t -> Yojson.Safe.t
 val canonicalize : get_var_repr:(AbstractValue.t -> AbstractValue.t) -> t -> t
 (** replace each address in the stack by its canonical representative according to the current
     equality relation, represented by [get_var_repr] *)
+
+val subst_var : AbstractValue.t * AbstractValue.t -> t -> t

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

@@ -116,9 +116,15 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `use_after_destructor::S::S`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `c` declared here,is the address of a stack variable `c` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, assumed_aliasing2_latent, 4, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of assumed_aliasing2_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing2_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, assumed_aliasing3_latent, 4, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of assumed_aliasing3_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing3_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, assumed_aliasing_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of assumed_aliasing_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of double_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of double_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, free_null_then_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, trigger_assumed_aliasing2_bad, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `assumed_aliasing2_latent`,invalidation part of the trace starts here,parameter `x` of assumed_aliasing2_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing2_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, trigger_assumed_aliasing3_bad, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `assumed_aliasing3_latent`,invalidation part of the trace starts here,parameter `x` of assumed_aliasing3_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing3_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, trigger_assumed_aliasing_bad, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `assumed_aliasing_latent`,invalidation part of the trace starts here,parameter `x` of assumed_aliasing_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp

@@ -31,38 +31,32 @@ void free_null_then_deref_bad() {
   *x = 1;
 }
 
-void FN_assumed_aliasing_latent(int* x, int* y) {
+void assumed_aliasing_latent(int* x, int* y) {
   if (x == y) {
     free(x);
     free(y);
   }
 }
 
-void FN_trigger_assumed_aliasing_bad(int* x) {
+void trigger_assumed_aliasing_bad(int* x) { assumed_aliasing_latent(x, x); }
-  FN_assumed_aliasing_latent(x, x);
-}
 
-void FN_assumed_aliasing2_latent(int* x, int* y) {
+void assumed_aliasing2_latent(int* x, int* y) {
   if (x == y)
     ;
   free(x);
   free(y);
 }
 
-void FN_trigger_assumed_aliasing2_bad(int* x) {
+void trigger_assumed_aliasing2_bad(int* x) { assumed_aliasing2_latent(x, x); }
-  FN_assumed_aliasing2_latent(x, x);
-}
 
-void FN_assumed_aliasing3_latent(int* x, int* y) {
+void assumed_aliasing3_latent(int* x, int* y) {
   free(x);
   if (x == y)
     ;
   free(y);
 }
 
-void FN_trigger_assumed_aliasing3_bad(int* x) {
+void trigger_assumed_aliasing3_bad(int* x) { assumed_aliasing3_latent(x, x); }
-  FN_assumed_aliasing3_latent(x, x);
-}
 
 void FN_assumed_aliasing4_latent(int* x, int* y) {
   free(x);