From 578583f2ab8d6a3f8b25167503647b01c7e8aa15 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Fri, 13 Nov 2020 05:55:27 -0800
Subject: [PATCH] [pulse] check that new arithmetic facts are consistent with
 the heap

Summary:
Communicate new facts from the arithmetic domain to the memory domain to
detect contradictions between the two.

Reviewed By: jberdine

Differential Revision: D24832079

fbshipit-source-id: 2caf8e9af
---
 infer/src/pulse/PulseAbductiveDomain.ml       |  38 +++-
 infer/src/pulse/PulseAbductiveDomain.mli      |   6 +
 infer/src/pulse/PulseArithmetic.ml            |  10 +-
 infer/src/pulse/PulseFormula.ml               | 177 ++++++++++--------
 infer/src/pulse/PulseFormula.mli              |  28 ++-
 infer/src/pulse/PulseInterproc.ml             |   5 +-
 infer/src/pulse/PulsePathCondition.ml         | 107 ++++++-----
 infer/src/pulse/PulsePathCondition.mli        |  22 ++-
 infer/src/pulse/unit/PulseFormulaTest.ml      |   8 +-
 .../codetoanalyze/cpp/pulse/aliasing.cpp      |  32 +++-
 .../tests/codetoanalyze/cpp/pulse/issues.exp  |   1 -
 11 files changed, 277 insertions(+), 157 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index abc3d4f3d..3367aa27a 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -431,11 +431,47 @@ let invalidate_locals pdesc astate : t =
 
 type summary = t [@@deriving yojson_of]
 
+let is_allocated {post; pre} v =
+  let is_heap_allocated base_mem v =
+    BaseMemory.find_opt v base_mem.heap
+    |> Option.exists ~f:(fun edges -> not (BaseMemory.Edges.is_empty edges))
+  in
+  let is_pvar = function Var.ProgramVar _ -> true | Var.LogicalVar _ -> false in
+  let is_stack_allocated base_mem v =
+    BaseStack.exists
+      (fun var (address, _) -> is_pvar var && AbstractValue.equal address v)
+      base_mem.stack
+  in
+  (* OPTIM: the post stack contains at least the pre stack so no need to check both *)
+  is_heap_allocated (post :> BaseDomain.t) v
+  || is_heap_allocated (pre :> BaseDomain.t) v
+  || is_stack_allocated (post :> BaseDomain.t) v
+
+
+let incorporate_new_eqs astate (phi, new_eqs) =
+  List.fold_until new_eqs ~init:phi ~finish:Fn.id ~f:(fun phi (new_eq : PulseFormula.new_eq) ->
+      match new_eq with
+      | EqZero v when is_allocated astate v ->
+          L.d_printfln "CONTRADICTION: %a = 0 but is allocated" AbstractValue.pp v ;
+          Stop PathCondition.false_
+      | Equal (v1, v2)
+        when (not (AbstractValue.equal v1 v2)) && is_allocated astate v1 && is_allocated astate v2
+        ->
+          L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp
+            v1 AbstractValue.pp v2 ;
+          Stop PathCondition.false_
+      | _ ->
+          Continue phi )
+
+
 let summary_of_post pdesc astate =
   let astate = filter_for_summary astate in
   let astate, live_addresses, _ = discard_unreachable astate in
   let astate =
-    {astate with path_condition= PathCondition.simplify ~keep:live_addresses astate.path_condition}
+    { astate with
+      path_condition=
+        PathCondition.simplify ~keep:live_addresses astate.path_condition
+        |> incorporate_new_eqs astate }
   in
   invalidate_locals pdesc astate
 
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 3610bfeec..302a0d4c5 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -172,3 +172,9 @@ val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t
 
 val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t
 (** directly set the edges and attributes for the given address, bypassing abduction altogether *)
+
+val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCondition.t
+(** Check that the new equalities discovered are compatible with the current pre and post heaps,
+    e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x]
+    and [y] being allocated separately. In those cases, the resulting path condition is
+    {!PathCondition.false_}. *)
diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml
index 105a622bc..e2557d5c3 100644
--- a/infer/src/pulse/PulseArithmetic.ml
+++ b/infer/src/pulse/PulseArithmetic.ml
@@ -10,7 +10,9 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 
 let map_path_condition ~f astate =
-  AbductiveDomain.set_path_condition (f astate.AbductiveDomain.path_condition) astate
+  AbductiveDomain.set_path_condition
+    (f astate.AbductiveDomain.path_condition |> AbductiveDomain.incorporate_new_eqs astate)
+    astate
 
 
 let and_nonnegative v astate =
@@ -41,6 +43,7 @@ let eval_unop unop_addr unop addr astate =
 let prune_binop ~negated bop lhs_op rhs_op astate =
   let phi' =
     PathCondition.prune_binop ~negated bop lhs_op rhs_op astate.AbductiveDomain.path_condition
+    |> AbductiveDomain.incorporate_new_eqs astate
   in
   AbductiveDomain.set_path_condition phi' astate
 
@@ -50,7 +53,10 @@ let is_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain.
 let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition
 
 let is_unsat_expensive astate =
-  let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in
+  let phi', is_unsat, new_eqs =
+    PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition
+  in
+  let phi' = AbductiveDomain.incorporate_new_eqs astate (phi', new_eqs) in
   (AbductiveDomain.set_path_condition phi' astate, is_unsat)
 
 
diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index fdd86df2c..5d4f3c31c 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -980,6 +980,10 @@ module VarUF =
     end)
     (Var.Set)
 
+type new_eq = EqZero of Var.t | Equal of Var.t * Var.t
+
+type new_eqs = new_eq list
+
 module Formula = struct
   (* redefined for yojson output *)
   type var_eqs = VarUF.t
@@ -1021,15 +1025,15 @@ module Formula = struct
 
   (** module that breaks invariants more often that the rest, with an interface that is safer to use *)
   module Normalizer : sig
-    val and_var_linarith : Var.t -> LinArith.t -> t -> t normalized
+    val and_var_linarith : Var.t -> LinArith.t -> t * new_eqs -> (t * new_eqs) normalized
 
-    val and_var_var : Var.t -> Var.t -> t -> t normalized
+    val and_var_var : Var.t -> Var.t -> t * new_eqs -> (t * new_eqs) normalized
 
-    val and_atom : Atom.t -> t -> t normalized
+    val and_atom : Atom.t -> t * new_eqs -> (t * new_eqs) normalized
 
     val normalize_atom : t -> Atom.t -> Atom.t option normalized
 
-    val normalize : t -> t normalized
+    val normalize : t -> (t * new_eqs) normalized
 
     val implies_atom : t -> Atom.t -> bool
   end = struct
@@ -1075,44 +1079,53 @@ module Formula = struct
               LinSubst l' )
 
 
-    let rec solve_normalized_eq ~fuel l1 l2 phi =
+    let add_lin_eq_to_new_eqs v l new_eqs =
+      match LinArith.get_as_const l with
+      | Some q when Q.is_zero q ->
+          EqZero v :: new_eqs
+      | _ ->
+          new_eqs
+
+
+    let rec solve_normalized_eq ~fuel new_eqs l1 l2 phi =
       LinArith.solve_eq l1 l2
       >>= function
       | None ->
-          Sat phi
+          Sat (phi, [])
       | Some (v, l) -> (
         match LinArith.get_as_var l with
         | Some v' ->
-            merge_vars ~fuel (v :> Var.t) v' phi
+            merge_vars ~fuel new_eqs (v :> Var.t) v' phi
         | None -> (
           match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with
           | None ->
+              let new_eqs = add_lin_eq_to_new_eqs v l new_eqs in
               (* this can break the (as a result non-)invariant that variables in the domain of
                  [linear_eqs] do not appear in the range of [linear_eqs] *)
-              Sat {phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}
+              Sat ({phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}, new_eqs)
           | Some l' ->
               (* This is the only step that consumes fuel: discovering an equality [l = l']: because we
-                 do not record these anywhere (except when there consequence can be recorded as [y =
+                 do not record these anywhere (except when their consequence can be recorded as [y =
                  l''] or [y = y'], we could potentially discover the same equality over and over and
                  diverge otherwise. Or could we? *)
               (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to
                  normalize it *)
               if fuel > 0 then (
                 L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ;
-                solve_normalized_eq ~fuel:(fuel - 1) l (apply phi l') phi )
+                solve_normalized_eq ~fuel:(fuel - 1) new_eqs l (apply phi l') phi )
               else (
                 (* [fuel = 0]: give up simplifying further for fear of diverging *)
                 L.d_printfln "Ran out of fuel solving linear equality" ;
-                Sat phi ) ) )
+                Sat (phi, new_eqs) ) ) )
 
 
-    and merge_vars ~fuel v1 v2 phi =
+    and merge_vars ~fuel new_eqs v1 v2 phi =
       let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in
       let phi = {phi with var_eqs} in
       match subst_opt with
       | None ->
           (* we already knew the equality *)
-          Sat phi
+          Sat (phi, new_eqs)
       | Some (v_old, v_new) -> (
           (* new equality [v_old = v_new]: we need to update a potential [v_old = l] to be [v_new =
              l], and if [v_new = l'] was known we need to also explore the consequences of [l = l'] *)
@@ -1123,6 +1136,7 @@ module Formula = struct
              normalization steps: when the stronger invariant holds we can normalize in one step (in
              [normalize_linear_eqs]). *)
           let v_new = (v_new :> Var.t) in
+          let new_eqs = Equal (v_old, v_new) :: new_eqs in
           let phi, l_new =
             match Var.Map.find_opt v_new phi.linear_eqs with
             | None ->
@@ -1146,46 +1160,47 @@ module Formula = struct
           in
           match (l_old, l_new) with
           | None, None | None, Some _ ->
-              Sat phi
+              Sat (phi, new_eqs)
           | Some l, None ->
-              Sat {phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs}
+              let new_eqs = add_lin_eq_to_new_eqs v_new l new_eqs in
+              Sat ({phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs}, new_eqs)
           | Some l1, Some l2 ->
               (* no need to consume fuel here as we can only go through this branch finitely many
                  times because there are finitely many variables in a given formula *)
               (* TODO: we may want to keep the "simpler" representative for [v_new] between [l1] and [l2] *)
-              solve_normalized_eq ~fuel l1 l2 phi )
+              solve_normalized_eq ~fuel new_eqs l1 l2 phi )
 
 
     (** an arbitrary value *)
     let base_fuel = 5
 
-    let solve_eq t1 t2 phi = solve_normalized_eq ~fuel:base_fuel (apply phi t1) (apply phi t2) phi
+    let solve_eq new_eqs t1 t2 phi =
+      solve_normalized_eq ~fuel:base_fuel new_eqs (apply phi t1) (apply phi t2) phi
 
-    let and_var_linarith v l phi = solve_eq l (LinArith.of_var v) phi
 
-    let and_var_var v1 v2 phi = merge_vars ~fuel:base_fuel v1 v2 phi
+    let and_var_linarith v l (phi, new_eqs) = solve_eq new_eqs l (LinArith.of_var v) phi
 
-    let rec normalize_linear_eqs ~fuel phi0 =
-      let* changed, phi' =
+    let rec normalize_linear_eqs ~fuel (phi0, new_eqs) =
+      let* changed, phi_new_eqs' =
         (* reconstruct the relation from scratch *)
         Var.Map.fold
           (fun v l acc ->
-            let* changed, phi = acc in
+            let* changed, phi_new_eqs = acc in
             let l' = apply phi0 l in
-            let+ phi' = and_var_linarith v l' phi in
-            (changed || not (phys_equal l l'), phi') )
+            let+ phi_new_eqs' = and_var_linarith v l' phi_new_eqs in
+            (changed || not (phys_equal l l'), phi_new_eqs') )
           phi0.linear_eqs
-          (Sat (false, {phi0 with linear_eqs= Var.Map.empty}))
+          (Sat (false, ({phi0 with linear_eqs= Var.Map.empty}, new_eqs)))
       in
       if changed then
         if fuel > 0 then (
           (* do another pass if we can afford it *)
           L.d_printfln "consuming fuel normalizing linear equalities (from %d)" fuel ;
-          normalize_linear_eqs ~fuel:(fuel - 1) phi' )
+          normalize_linear_eqs ~fuel:(fuel - 1) phi_new_eqs' )
         else (
           L.d_printfln "ran out of fuel normalizing linear equalities" ;
-          Sat phi' )
-      else Sat phi0
+          Sat phi_new_eqs' )
+      else Sat (phi0, new_eqs)
 
 
     let normalize_atom phi (atom : Atom.t) =
@@ -1204,54 +1219,60 @@ module Formula = struct
 
     (** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if
         [phi.linear_eqs] was changed as a result *)
-    let and_atom atom phi =
+    let and_atom atom (phi, new_eqs) =
       normalize_atom phi atom
       >>= function
       | None ->
-          Sat (false, phi)
+          Sat (false, (phi, new_eqs))
       | Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) ->
           (* NOTE: {!normalize_atom} calls {!Atom.eval}, which normalizes linear equalities so
              they end up only on one side, hence only this match case is needed to detect linear
              equalities *)
-          let+ phi' = solve_eq l (LinArith.of_q c) phi in
-          (true, phi')
+          let+ phi', new_eqs = solve_eq new_eqs l (LinArith.of_q c) phi in
+          (true, (phi', new_eqs))
       | Some atom' ->
-          Sat (false, {phi with atoms= Atom.Set.add atom' phi.atoms})
+          Sat (false, ({phi with atoms= Atom.Set.add atom' phi.atoms}, new_eqs))
 
 
-    let normalize_atoms phi =
+    let normalize_atoms (phi, new_eqs) =
       let atoms0 = phi.atoms in
-      let init = Sat (false, {phi with atoms= Atom.Set.empty}) in
+      let init = Sat (false, ({phi with atoms= Atom.Set.empty}, new_eqs)) in
       IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms0 ~init ~f:(fun acc atom ->
-          let* changed, phi = acc in
-          let+ changed', phi = and_atom atom phi in
-          (changed || changed', phi) )
+          let* changed, phi_new_eqs = acc in
+          let+ changed', phi_new_eqs = and_atom atom phi_new_eqs in
+          (changed || changed', phi_new_eqs) )
+
 
+    (* interface *)
 
-    let normalize phi =
+    let normalize phi0 =
       (* NOTE: we may consume a quadratic amount of [fuel] here since the fuel here is not consumed by
          [normalize_linear_eqs] (i.e. [normalize_linear_eqs] does not return the remaining
          fuel). That's ok because there's not much fuel to begin with, and as long as we're making
          progress it's probably worth it anyway. *)
-      let rec normalize_with_fuel ~fuel phi =
+      let rec normalize_with_fuel ~fuel phi_new_eqs =
         if fuel <= 0 then (
           L.d_printfln "ran out of fuel when normalizing" ;
-          Sat phi )
+          Sat phi_new_eqs )
         else
-          let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in
+          let* new_linear_eqs, phi_new_eqs' =
+            normalize_linear_eqs ~fuel phi_new_eqs >>= normalize_atoms
+          in
           if new_linear_eqs then (
             L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
-            normalize_with_fuel ~fuel:(fuel - 1) phi )
-          else Sat phi
+            normalize_with_fuel ~fuel:(fuel - 1) phi_new_eqs' )
+          else Sat phi_new_eqs'
       in
-      normalize_with_fuel ~fuel:base_fuel phi
+      normalize_with_fuel ~fuel:base_fuel (phi0, [])
+
 
+    let and_atom atom phi_new_eqs = and_atom atom phi_new_eqs >>| snd
 
-    let and_atom atom phi = and_atom atom phi >>| snd
+    let and_var_var v1 v2 (phi, new_eqs) = merge_vars ~fuel:base_fuel new_eqs v1 v2 phi
 
     let implies_atom phi atom =
       (* [φ ⊢ a] iff [φ ∧ ¬a] is inconsistent *)
-      match and_atom (Atom.nnot atom) phi with Sat _ -> false | Unsat -> true
+      match and_atom (Atom.nnot atom) (phi, []) with Sat _ -> false | Unsat -> true
   end
 end
 
@@ -1276,9 +1297,9 @@ let pp = pp_with_pp_var Var.pp
 
 let and_known_atom atom phi =
   let open SatUnsatMonad in
-  let* known = Formula.Normalizer.and_atom atom phi.known in
-  let+ both = Formula.Normalizer.and_atom atom phi.both in
-  {phi with known; both}
+  let* known, _ = Formula.Normalizer.and_atom atom (phi.known, []) in
+  let+ both, new_eqs = Formula.Normalizer.and_atom atom (phi.both, []) in
+  ({phi with known; both}, new_eqs)
 
 
 let and_mk_atom mk_atom op1 op2 phi =
@@ -1306,7 +1327,7 @@ let prune_binop ~negated (bop : Binop.t) x y phi =
   let ty = Term.of_operand y in
   let t = Term.of_binop bop tx ty in
   let atom = if negated then Atom.Equal (t, Term.zero) else Atom.NotEqual (t, Term.zero) in
-  let* both = Formula.Normalizer.and_atom atom phi.both in
+  let* both, new_eqs = Formula.Normalizer.and_atom atom (phi.both, []) in
   let+ pruned =
     (* Use [both] to normalize [atom] here to take previous [prune]s into account. This shouldn't
        change whether [known |- pruned] overall, which is what we'll want to ultimately check in
@@ -1314,13 +1335,13 @@ let prune_binop ~negated (bop : Binop.t) x y phi =
     Formula.Normalizer.normalize_atom phi.both atom
     >>| Option.fold ~init:phi.pruned ~f:(fun pruned atom -> Atom.Set.add atom pruned)
   in
-  {phi with pruned; both}
+  ({phi with pruned; both}, new_eqs)
 
 
 let normalize phi =
   let open SatUnsatMonad in
-  let* both = Formula.Normalizer.normalize phi.both in
-  let* known = Formula.Normalizer.normalize phi.known in
+  let* both, new_eqs = Formula.Normalizer.normalize phi.both in
+  let* known, _ = Formula.Normalizer.normalize phi.known in
   let+ pruned =
     Atom.Set.fold
       (fun atom pruned_sat ->
@@ -1334,7 +1355,7 @@ let normalize phi =
             Sat (Atom.Set.add atom pruned) )
       phi.pruned (Sat Atom.Set.empty)
   in
-  {both; known; pruned}
+  ({both; known; pruned}, new_eqs)
 
 
 (** translate each variable in [phi_foreign] according to [f] then incorporate each fact into [phi0] *)
@@ -1348,42 +1369,42 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
   let sat_value_exn (norm : 'a normalized) =
     match norm with Unsat -> raise Contradiction | Sat x -> x
   in
-  let and_var_eqs var_eqs_foreign acc_phi =
-    VarUF.fold_congruences var_eqs_foreign ~init:acc_phi
-      ~f:(fun (acc_f, phi) (repr_foreign, vs_foreign) ->
+  let and_var_eqs var_eqs_foreign acc_phi_new_eqs =
+    VarUF.fold_congruences var_eqs_foreign ~init:acc_phi_new_eqs
+      ~f:(fun (acc_f, phi_new_eqs) (repr_foreign, vs_foreign) ->
         let acc_f, repr = f_var acc_f (repr_foreign :> Var.t) in
-        IContainer.fold_of_pervasives_set_fold Var.Set.fold vs_foreign ~init:(acc_f, phi)
-          ~f:(fun (acc_f, phi) v_foreign ->
+        IContainer.fold_of_pervasives_set_fold Var.Set.fold vs_foreign ~init:(acc_f, phi_new_eqs)
+          ~f:(fun (acc_f, phi_new_eqs) v_foreign ->
             let acc_f, v = f_var acc_f v_foreign in
-            let phi = Formula.Normalizer.and_var_var repr v phi |> sat_value_exn in
-            (acc_f, phi) ) )
+            let phi_new_eqs = Formula.Normalizer.and_var_var repr v phi_new_eqs |> sat_value_exn in
+            (acc_f, phi_new_eqs) ) )
   in
-  let and_linear_eqs linear_eqs_foreign acc_phi =
-    IContainer.fold_of_pervasives_map_fold Var.Map.fold linear_eqs_foreign ~init:acc_phi
-      ~f:(fun (acc_f, phi) (v_foreign, l_foreign) ->
+  let and_linear_eqs linear_eqs_foreign acc_phi_new_eqs =
+    IContainer.fold_of_pervasives_map_fold Var.Map.fold linear_eqs_foreign ~init:acc_phi_new_eqs
+      ~f:(fun (acc_f, phi_new_eqs) (v_foreign, l_foreign) ->
         let acc_f, v = f_var acc_f v_foreign in
         let acc_f, l = LinArith.fold_subst_variables l_foreign ~init:acc_f ~f:f_subst in
-        let phi = Formula.Normalizer.and_var_linarith v l phi |> sat_value_exn in
-        (acc_f, phi) )
+        let phi_new_eqs = Formula.Normalizer.and_var_linarith v l phi_new_eqs |> sat_value_exn in
+        (acc_f, phi_new_eqs) )
   in
-  let and_atoms atoms_foreign acc_phi =
-    IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi
-      ~f:(fun (acc_f, phi) atom_foreign ->
+  let and_atoms atoms_foreign acc_phi_new_eqs =
+    IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi_new_eqs
+      ~f:(fun (acc_f, phi_new_eqs) atom_foreign ->
         let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in
-        let phi = Formula.Normalizer.and_atom atom phi |> sat_value_exn in
-        (acc_f, phi) )
+        let phi_new_eqs = Formula.Normalizer.and_atom atom phi_new_eqs |> sat_value_exn in
+        (acc_f, phi_new_eqs) )
   in
   let and_ phi_foreign acc phi =
     try
       Sat
-        ( and_var_eqs phi_foreign.Formula.var_eqs (acc, phi)
+        ( and_var_eqs phi_foreign.Formula.var_eqs (acc, (phi, []))
         |> and_linear_eqs phi_foreign.Formula.linear_eqs
         |> and_atoms phi_foreign.Formula.atoms )
     with Contradiction -> Unsat
   in
   let open SatUnsatMonad in
-  let* acc, both = and_ phi_foreign.both init phi0.both in
-  let* acc, known = and_ phi_foreign.known acc phi0.known in
+  let* acc, (both, new_eqs) = and_ phi_foreign.both init phi0.both in
+  let* acc, (known, _) = and_ phi_foreign.known acc phi0.known in
   let and_pruned pruned_foreign acc_pruned =
     IContainer.fold_of_pervasives_set_fold Atom.Set.fold pruned_foreign ~init:acc_pruned
       ~f:(fun (acc_f, pruned) atom_foreign ->
@@ -1397,7 +1418,7 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
   let+ acc, pruned =
     try Sat (and_pruned phi_foreign.pruned (acc, phi0.pruned)) with Contradiction -> Unsat
   in
-  (acc, {known; pruned; both})
+  (acc, {known; pruned; both}, new_eqs)
 
 
 (** Intermediate step of [simplify]: build an (undirected) graph between variables where an edge
@@ -1480,7 +1501,7 @@ let get_reachable_from graph vs =
 
 let simplify ~keep phi =
   let open SatUnsatMonad in
-  let+ phi = normalize phi in
+  let+ phi, new_eqs = normalize phi in
   L.d_printfln_escaped "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ;
   (* Get rid of atoms when they contain only variables that do not appear in atoms mentioning
      variables in [keep], or variables appearing in atoms together with variables in [keep], and
@@ -1510,7 +1531,7 @@ let simplify ~keep phi =
   let known = simplify_phi phi.known in
   let both = simplify_phi phi.both in
   let pruned = Atom.Set.filter filter_atom phi.pruned in
-  {known; pruned; both}
+  ({known; pruned; both}, new_eqs)
 
 
 let is_known_zero phi v =
diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli
index 1fece38a5..0b08a34c7 100644
--- a/infer/src/pulse/PulseFormula.mli
+++ b/infer/src/pulse/PulseFormula.mli
@@ -30,29 +30,39 @@ type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t
 
 (** {3 Build formulas} *)
 
+(** some operations will return a set of new facts discovered that are relevant to communicate to
+    the memory domain *)
+type new_eq = EqZero of Var.t | Equal of Var.t * Var.t
+
+type new_eqs = new_eq list
+
 val ttrue : t
 
-val and_equal : operand -> operand -> t -> t normalized
+val and_equal : operand -> operand -> t -> (t * new_eqs) normalized
 
-val and_less_equal : operand -> operand -> t -> t normalized
+val and_less_equal : operand -> operand -> t -> (t * new_eqs) normalized
 
-val and_less_than : operand -> operand -> t -> t normalized
+val and_less_than : operand -> operand -> t -> (t * new_eqs) normalized
 
-val and_equal_unop : Var.t -> Unop.t -> operand -> t -> t normalized
+val and_equal_unop : Var.t -> Unop.t -> operand -> t -> (t * new_eqs) normalized
 
-val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> t normalized
+val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> (t * new_eqs) normalized
 
-val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t normalized
+val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new_eqs) normalized
 
 (** {3 Operations} *)
 
-val normalize : t -> t normalized
+val normalize : t -> (t * new_eqs) normalized
 (** think a bit harder about the formula *)
 
-val simplify : keep:Var.Set.t -> t -> t normalized
+val simplify : keep:Var.Set.t -> t -> (t * new_eqs) normalized
 
 val and_fold_subst_variables :
-  t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t) normalized
+     t
+  -> up_to_f:t
+  -> init:'acc
+  -> f:('acc -> Var.t -> 'acc * Var.t)
+  -> ('acc * t * new_eqs) normalized
 
 val is_known_zero : t -> Var.t -> bool
 
diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml
index 3a3171856..a34fb486c 100644
--- a/infer/src/pulse/PulseInterproc.ml
+++ b/infer/src/pulse/PulseInterproc.ml
@@ -221,10 +221,13 @@ let conjoin_callee_arith pre_post call_state =
     pre_post.AbductiveDomain.path_condition
     (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr))
     call_state.subst ;
-  let subst, path_condition =
+  let subst, path_condition, new_eqs =
     PathCondition.and_callee call_state.subst call_state.astate.path_condition
       ~callee:pre_post.AbductiveDomain.path_condition
   in
+  let path_condition =
+    AbductiveDomain.incorporate_new_eqs call_state.astate (path_condition, new_eqs)
+  in
   if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition)
   else
     let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index 4e0e4a50c..048c70431 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -45,53 +45,61 @@ let true_ = {is_unsat= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula
 
 let false_ = {is_unsat= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
 
-let map_sat phi f = if phi.is_unsat then phi else f phi
+type new_eqs = PulseFormula.new_eqs
+
+let map_sat phi f = if phi.is_unsat then (phi, []) else f phi
 
 let ( let+ ) phi f = map_sat phi f
 
-let map_formula_sat (x : 'a Formula.normalized) f = match x with Unsat -> false_ | Sat x' -> f x'
+let map_formula_sat (x : 'a Formula.normalized) f =
+  match x with Unsat -> (false_, []) | Sat x' -> f x'
+
 
 let ( let+| ) x f = map_formula_sat x f
 
 let and_nonnegative v phi =
   let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-  let+| formula =
+  let+| formula, new_eqs =
     Formula.and_less_equal (LiteralOperand IntLit.zero) (AbstractValueOperand v) formula
   in
-  { is_unsat
-  ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
-  ; citvs= CItvs.add v CItv.zero_inf citvs
-  ; formula }
+  ( { is_unsat
+    ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
+    ; citvs= CItvs.add v CItv.zero_inf citvs
+    ; formula }
+  , new_eqs )
 
 
 let and_positive v phi =
   let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-  let+| formula =
+  let+| formula, new_eqs =
     Formula.and_less_than (LiteralOperand IntLit.zero) (AbstractValueOperand v) formula
   in
-  { is_unsat
-  ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
-  ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
-  ; formula }
+  ( { is_unsat
+    ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
+    ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
+    ; formula }
+  , new_eqs )
 
 
 let and_eq_int v i phi =
   let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-  let+| formula = Formula.and_equal (AbstractValueOperand v) (LiteralOperand i) formula in
-  { is_unsat
-  ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
-  ; citvs= CItvs.add v (CItv.equal_to i) citvs
-  ; formula }
+  let+| formula, new_eqs = Formula.and_equal (AbstractValueOperand v) (LiteralOperand i) formula in
+  ( { is_unsat
+    ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
+    ; citvs= CItvs.add v (CItv.equal_to i) citvs
+    ; formula }
+  , new_eqs )
 
 
 let simplify ~keep phi =
   let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-  let+| formula = Formula.simplify ~keep formula in
+  let+| formula, new_eqs = Formula.simplify ~keep formula in
   let is_in_keep v _ = AbstractValue.Set.mem v keep in
-  { is_unsat
-  ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
-  ; citvs= CItvs.filter is_in_keep citvs
-  ; formula }
+  ( { is_unsat
+    ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
+    ; citvs= CItvs.filter is_in_keep citvs
+    ; formula }
+  , new_eqs )
 
 
 let subst_find_or_new subst addr_callee =
@@ -193,26 +201,27 @@ let and_formula_callee subst formula_caller ~callee:formula_callee =
 
 
 let and_callee subst phi ~callee:phi_callee =
-  if phi.is_unsat || phi_callee.is_unsat then (subst, false_)
+  if phi.is_unsat || phi_callee.is_unsat then (subst, false_, [])
   else
     match and_bo_itvs_callee subst phi.bo_itvs phi_callee.bo_itvs with
     | exception Contradiction ->
         L.d_printfln "contradiction found by inferbo intervals" ;
-        (subst, false_)
+        (subst, false_, [])
     | subst, bo_itvs' -> (
       match and_citvs_callee subst phi.citvs phi_callee.citvs with
       | exception Contradiction ->
           L.d_printfln "contradiction found by concrete intervals" ;
-          (subst, false_)
+          (subst, false_, [])
       | subst, citvs' -> (
         match and_formula_callee subst phi.formula ~callee:phi_callee.formula with
         | Unsat ->
             L.d_printfln "contradiction found by formulas" ;
-            (subst, false_)
-        | Sat (subst, formula') ->
+            (subst, false_, [])
+        | Sat (subst, formula', new_eqs) ->
             (* TODO: normalize here? *)
             L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ;
-            (subst, {is_unsat= false; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) ) )
+            (subst, {is_unsat= false; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}, new_eqs)
+        ) )
 
 
 (** {2 Operations} *)
@@ -255,11 +264,12 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs =
 
 let eval_binop binop_addr binop op_lhs op_rhs phi =
   let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-  let+| formula = Formula.and_equal_binop binop_addr binop op_lhs op_rhs formula in
-  { is_unsat
-  ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
-  ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
-  ; formula }
+  let+| formula, new_eqs = Formula.and_equal_binop binop_addr binop op_lhs op_rhs formula in
+  ( { is_unsat
+    ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
+    ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
+    ; formula }
+  , new_eqs )
 
 
 let eval_citv_unop unop_addr unop operand_addr citvs =
@@ -281,11 +291,14 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs =
 
 let eval_unop unop_addr unop addr phi =
   let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-  let+| formula = Formula.and_equal_unop unop_addr unop (AbstractValueOperand addr) formula in
-  { is_unsat
-  ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
-  ; citvs= eval_citv_unop unop_addr unop addr citvs
-  ; formula }
+  let+| formula, new_eqs =
+    Formula.and_equal_unop unop_addr unop (AbstractValueOperand addr) formula
+  in
+  ( { is_unsat
+    ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
+    ; citvs= eval_citv_unop unop_addr unop addr citvs
+    ; formula }
+  , new_eqs )
 
 
 let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
@@ -318,14 +331,14 @@ let record_citv_abduced addr_opt arith_opt citvs =
 
 
 let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formula} as phi) =
-  if is_unsat then phi
+  if is_unsat then (phi, [])
   else
     let value_lhs_opt, arith_lhs_opt, bo_itv_lhs = eval_operand phi lhs_op in
     let value_rhs_opt, arith_rhs_opt, bo_itv_rhs = eval_operand phi rhs_op in
     match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with
     | Unsatisfiable ->
         L.d_printfln "contradiction detected by concrete intervals" ;
-        false_
+        (false_, [])
     | Satisfiable (abduced_lhs, abduced_rhs) -> (
         let phi =
           let citvs =
@@ -355,9 +368,9 @@ let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formul
         match Formula.prune_binop ~negated bop lhs_op rhs_op formula with
         | Unsat ->
             L.d_printfln "contradiction detected by formulas" ;
-            false_
-        | Sat formula ->
-            {phi with is_unsat; formula} )
+            (false_, [])
+        | Sat (formula, new_eqs) ->
+            ({phi with is_unsat; formula}, new_eqs) )
 
 
 (** {2 Queries} *)
@@ -373,13 +386,13 @@ let is_unsat_cheap phi = phi.is_unsat
 let is_unsat_expensive phi =
   (* note: contradictions are detected eagerly for all sub-domains except formula, so just
      evaluate that one *)
-  if is_unsat_cheap phi then (phi, true)
+  if is_unsat_cheap phi then (phi, true, [])
   else
     match Formula.normalize phi.formula with
     | Unsat ->
-        (false_, true)
-    | Sat formula ->
-        ({phi with formula}, false)
+        (false_, true, [])
+    | Sat (formula, new_eqs) ->
+        ({phi with formula}, false, new_eqs)
 
 
 let as_int phi v =
diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli
index 868d40dbc..0e13de008 100644
--- a/infer/src/pulse/PulsePathCondition.mli
+++ b/infer/src/pulse/PulsePathCondition.mli
@@ -14,20 +14,24 @@ type t [@@deriving yojson_of]
 
 val true_ : t
 
+val false_ : t
+
 val pp : F.formatter -> t -> unit
 
+type new_eqs = PulseFormula.new_eqs
+
 (** {2 Building arithmetic constraints} *)
 
-val and_nonnegative : AbstractValue.t -> t -> t
+val and_nonnegative : AbstractValue.t -> t -> t * new_eqs
 (** [and_nonnegative v phi] is [phi ∧ v≥0] *)
 
-val and_positive : AbstractValue.t -> t -> t
+val and_positive : AbstractValue.t -> t -> t * new_eqs
 (** [and_positive v phi] is [phi ∧ v>0] *)
 
-val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t
+val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t * new_eqs
 (** [and_eq_int v i phi] is [phi ∧ v=i] *)
 
-val simplify : keep:AbstractValue.Set.t -> t -> t
+val simplify : keep:AbstractValue.Set.t -> t -> t * new_eqs
 (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
     possible *)
 
@@ -35,17 +39,17 @@ val and_callee :
      (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t
   -> t
   -> callee:t
-  -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t
+  -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t * new_eqs
 
 (** {2 Operations} *)
 
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
 
-val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t
+val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t * new_eqs
 
-val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> t -> t
+val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> t -> t * new_eqs
 
-val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t
+val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t * new_eqs
 
 (** {2 Queries} *)
 
@@ -55,7 +59,7 @@ val is_known_zero : t -> AbstractValue.t -> bool
 val is_unsat_cheap : t -> bool
 (** whether the state contains a contradiction, call this as often as you want *)
 
-val is_unsat_expensive : t -> t * bool
+val is_unsat_expensive : t -> t * bool * new_eqs
 (** whether the state contains a contradiction, only call this when you absolutely have to *)
 
 val as_int : t -> AbstractValue.t -> int option
diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml
index 67753dd45..ae79619d6 100644
--- a/infer/src/pulse/unit/PulseFormulaTest.ml
+++ b/infer/src/pulse/unit/PulseFormulaTest.ml
@@ -40,7 +40,7 @@ let of_binop bop f1 f2 phi =
   let* phi, op1 = f1 phi in
   let* phi, op2 = f2 phi in
   let v = Var.mk_fresh () in
-  let+ phi = and_equal_binop v bop op1 op2 phi in
+  let+ phi, _new_eqs = and_equal_binop v bop op1 op2 phi in
   (phi, AbstractValueOperand v)
 
 
@@ -59,13 +59,13 @@ let ( mod ) f1 f2 phi = of_binop Mod f1 f2 phi
 let ( = ) f1 f2 phi =
   let* phi, op1 = f1 phi in
   let* phi, op2 = f2 phi in
-  and_equal op1 op2 phi
+  and_equal op1 op2 phi >>| fst
 
 
 let ( < ) f1 f2 phi =
   let* phi, op1 = f1 phi in
   let* phi, op2 = f2 phi in
-  and_less_than op1 op2 phi
+  and_less_than op1 op2 phi >>| fst
 
 
 let ( && ) f1 f2 phi = f1 phi >>= f2
@@ -119,7 +119,7 @@ let normalized_pp fmt = function
 
 let test ~f phi =
   AbstractValue.State.set init_vars_state ;
-  phi ttrue >>= f |> F.printf "%a" normalized_pp
+  phi ttrue >>= f >>| fst |> F.printf "%a" normalized_pp
 
 
 let normalize phi = test ~f:normalize phi
diff --git a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
index 1121a6d0f..40b6559b1 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
@@ -28,11 +28,7 @@ void call_ifnotthenderef_false_null_bad() { ifnotthenderef(false, nullptr); }
 // should be FN given the current "all allocated addresses are assumed
 // disjoint unless specified otherwise" but we detect the bug because
 // we don't propagate pure equalities that we discover to the heap part
-//
-// Well, at the moment it *is* FN but because we mark the issue
-// "latent" because the "if" test is not conclusively true. This is
-// also ok.
-void alias_null_deref_latent(int* x, int* y) {
+void FN_alias_null_deref_latent(int* x, int* y) {
   *x = 32;
   *y = 52;
   if (x == y) {
@@ -54,3 +50,29 @@ void diverge_before_null_deref_ok(int* x) {
   int* p = nullptr;
   *p = 42;
 }
+
+// this test makes more sense in an inter-procedural setting
+void stack_addresses_are_not_null_ok() {
+  int x;
+  if (&x == nullptr) {
+    int* p = nullptr;
+    *p = 42;
+  }
+}
+
+void stack_addresses_are_distinct_ok() {
+  int x;
+  int y;
+  if (&x == &y) {
+    int* p = nullptr;
+    *p = 42;
+  }
+}
+
+void null_test_after_deref_ok(int* x) {
+  *x = 42;
+  if (x == nullptr) {
+    int* p = nullptr;
+    *p = 42;
+  }
+}
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 2db150d4c..2d1585d96 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -1,4 +1,3 @@
-codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_latent, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,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/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, 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,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here]
 codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, 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,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here]
 codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here]