[pulse] arithmetic domain: take 4!

Summary:
This time it's personal.

Roll out pulse's own arithmetic domain to be fast and be able to add
precision as needed. Formulas are precise representations of the path
condition to allow for good inter-procedural precision. Reasoning on
these is somewhat ad-hoc (except for equalities, but even these aren't
quite properly saturated in general), so expect lots of holes.

Skipping dead code in the interest of readability as this (at least
temporarily) doesn't use pudge anymore. This may make a come-back as
pudge has/will have better precision: the proposed implementation of
`PulseFormula` is very cheap so can be used any time we could want to
prune paths (see following commits), but this comes at the price of some
precision. Calling into pudge at reporting time still sounds like a good
idea to reduce false positives due to infeasible paths.

#skipdeadcode

Reviewed By: skcho

Differential Revision: D22576004

fbshipit-source-id: c91793256

infer/src/istd/IContainer.ml

@@ -68,6 +68,10 @@ let filter ~fold ~filter t ~init ~f =
   fold t ~init ~f:(fun acc item -> if filter item then f acc item else acc)
 
 
+let fold_of_pervasives_set_fold fold collection ~init ~f =
+  fold (fun elt accum -> f accum elt) collection init
+
+
 let map ~f:g fold t ~init ~f = fold t ~init ~f:(fun acc item -> f acc (g item))
 
 let fold_of_pervasives_map_fold fold collection ~init ~f =

infer/src/istd/IContainer.mli

@@ -45,6 +45,9 @@ val filter :
 
 val map : f:('a -> 'b) -> ('t, 'a, 'accum) Container.fold -> ('t, 'b, 'accum) Container.fold
 
+val fold_of_pervasives_set_fold :
+  (('elt -> 'accum -> 'accum) -> 't -> 'accum -> 'accum) -> ('t, 'elt, 'accum) Container.fold
+
 val fold_of_pervasives_map_fold :
      (('key -> 'value -> 'accum -> 'accum) -> 't -> 'accum -> 'accum)
   -> ('t, 'key * 'value, 'accum) Container.fold

infer/src/istd/UnionFind.ml

@@ -0,0 +1,101 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+module type Element = sig
+  type t [@@deriving compare]
+
+  val is_simpler_than : t -> t -> bool
+end
+
+module Make (X : Element) = struct
+  module Set = Caml.Set.Make (X)
+  module Map = Caml.Map.Make (X)
+
+  let equal_x = [%compare.equal: X.t]
+
+  (** the union-find backing data structure: maps elements to their representatives *)
+  module UF : sig
+    (** to get a little bit of type safety *)
+    type repr = private X.t
+
+    type t
+
+    val empty : t
+
+    val find_opt : t -> X.t -> repr option
+
+    val find : t -> X.t -> repr
+
+    val merge : t -> repr -> into:repr -> t
+
+    module Map : Caml.Map.S with type key = repr
+  end = struct
+    type repr = X.t
+
+    type t = X.t Map.t
+
+    let empty = Map.empty
+
+    let find_opt reprs x =
+      let rec find_opt_aux candidate_repr =
+        (* [x] is in the relation and now we are climbing up to the final representative *)
+        match Map.find_opt candidate_repr reprs with
+        | None ->
+            (* [candidate_repr] is the representative *)
+            candidate_repr
+        | Some candidate_repr' ->
+            (* keep climbing *)
+            find_opt_aux candidate_repr'
+      in
+      Map.find_opt x reprs |> Option.map ~f:find_opt_aux
+
+
+    let find reprs x = find_opt reprs x |> Option.value ~default:x
+
+    let merge reprs x ~into:y = (* TODO: implement path compression *) Map.add x y reprs
+
+    module Map = Map
+  end
+
+  type repr = UF.repr
+
+  module Classes = struct
+    let find classes (x : UF.repr) = UF.Map.find_opt x classes |> Option.value ~default:Set.empty
+
+    let merge classes (x1 : UF.repr) ~into:(x2 : UF.repr) =
+      let class1 = find classes x1 in
+      let class2 = find classes x2 in
+      let new_class = Set.union class1 class2 |> Set.add (x1 :> X.t) in
+      UF.Map.remove x1 classes |> UF.Map.add x2 new_class
+  end
+
+  type t = {reprs: UF.t; classes: Set.t UF.Map.t}
+
+  let empty = {reprs= UF.empty; classes= UF.Map.empty}
+
+  let find_opt uf x = UF.find_opt uf.reprs x
+
+  let find uf x = UF.find uf.reprs x
+
+  let union uf x1 x2 =
+    let repr1 = find uf x1 in
+    let repr2 = find uf x2 in
+    if equal_x (repr1 :> X.t) (repr2 :> X.t) then (* avoid creating loops in the relation *) uf
+    else
+      let from, into =
+        if X.is_simpler_than (repr1 :> X.t) (repr2 :> X.t) then (repr2, repr1) else (repr1, repr2)
+      in
+      let reprs = UF.merge uf.reprs from ~into in
+      let classes = Classes.merge uf.classes from ~into in
+      {reprs; classes}
+
+
+  let fold_congruences {classes} ~init ~f =
+    UF.Map.fold (fun repr xs acc -> f acc (repr, xs)) classes init
+end

infer/src/istd/UnionFind.mli

@@ -0,0 +1,38 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** A union-find data structure. *)
+
+module type Element = sig
+  type t [@@deriving compare]
+
+  val is_simpler_than : t -> t -> bool
+  (** will be used to choose a "simpler" representative for a given equivalence class when possible *)
+end
+
+module Make (X : Element) : sig
+  type t
+
+  type repr = private X.t
+
+  module Set : Caml.Set.S with type elt = X.t
+
+  val empty : t
+
+  val union : t -> X.t -> X.t -> t
+
+  val find_opt : t -> X.t -> repr option
+
+  val find : t -> X.t -> repr
+  (** like [find_opt] but returns the element given if it wasn't found in the relation *)
+
+  val fold_congruences : (t, repr * Set.t, 'acc) Container.fold
+  (** fold over the equivalence classes of the relation, singling out the representative for each
+      class *)
+end

infer/src/pulse/PulseFormula.ml

@@ -0,0 +1,780 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module F = Format
+module L = Logging
+module AbstractValue = PulseAbstractValue
+
+module Term = struct
+  type t =
+    | Const of Const.t
+    | Var of AbstractValue.t
+    | Add of t * t
+    | Minus of t
+    | LessThan of t * t
+    | LessEqual of t * t
+    | Equal of t * t
+    | NotEqual of t * t
+    | Mult of t * t
+    | Div of t * t
+    | And of t * t
+    | Or of t * t
+    | Not of t
+    | Mod of t * t
+    | BitAnd of t * t
+    | BitOr of t * t
+    | BitNot of t
+    | BitShiftLeft of t * t
+    | BitShiftRight of t * t
+    | BitXor of t * t
+  [@@deriving compare]
+
+  let equal_syntax = [%compare.equal: t]
+
+  let rec pp fmt = function
+    | Var v ->
+        AbstractValue.pp fmt v
+    | Const c ->
+        Const.pp Pp.text fmt c
+    | Minus t ->
+        F.fprintf fmt "-(%a)" pp t
+    | BitNot t ->
+        F.fprintf fmt "BitNot(%a)" pp t
+    | Not t ->
+        F.fprintf fmt "¬(%a)" pp t
+    | Add (t1, t2) ->
+        F.fprintf fmt "(%a)+(%a)" pp t1 pp t2
+    | Mult (t1, t2) ->
+        F.fprintf fmt "(%a)×(%a)" pp t1 pp t2
+    | Div (t1, t2) ->
+        F.fprintf fmt "(%a)÷(%a)" pp t1 pp t2
+    | Mod (t1, t2) ->
+        F.fprintf fmt "(%a) mod (%a)" pp t1 pp t2
+    | BitAnd (t1, t2) ->
+        F.fprintf fmt "(%a)&(%a)" pp t1 pp t2
+    | BitOr (t1, t2) ->
+        F.fprintf fmt "(%a)|(%a)" pp t1 pp t2
+    | BitShiftLeft (t1, t2) ->
+        F.fprintf fmt "(%a)<<(%a)" pp t1 pp t2
+    | BitShiftRight (t1, t2) ->
+        F.fprintf fmt "(%a)>>(%a)" pp t1 pp t2
+    | BitXor (t1, t2) ->
+        F.fprintf fmt "(%a) xor (%a)" pp t1 pp t2
+    | And (t1, t2) ->
+        F.fprintf fmt "(%a)∧(%a)" pp t1 pp t2
+    | Or (t1, t2) ->
+        F.fprintf fmt "(%a)∨(%a)" pp t1 pp t2
+    | LessThan (t1, t2) ->
+        F.fprintf fmt "(%a)<(%a)" pp t1 pp t2
+    | LessEqual (t1, t2) ->
+        F.fprintf fmt "(%a)≤(%a)" pp t1 pp t2
+    | Equal (t1, t2) ->
+        F.fprintf fmt "(%a)=(%a)" pp t1 pp t2
+    | NotEqual (t1, t2) ->
+        F.fprintf fmt "(%a)≠(%a)" pp t1 pp t2
+
+
+  let of_absval v = Var v
+
+  let of_intlit i = Const (Cint i)
+
+  let one = of_intlit IntLit.one
+
+  let zero = of_intlit IntLit.zero
+
+  let of_unop (unop : Unop.t) t =
+    match unop with Neg -> Minus t | BNot -> BitNot t | LNot -> Not t
+
+
+  let of_binop (bop : Binop.t) t1 t2 =
+    match bop with
+    | PlusA _ | PlusPI ->
+        Add (t1, t2)
+    | MinusA _ | MinusPI | MinusPP ->
+        Add (t1, Minus t2)
+    | Mult _ ->
+        Mult (t1, t2)
+    | Div ->
+        Div (t1, t2)
+    | Mod ->
+        Mod (t1, t2)
+    | Shiftlt ->
+        BitShiftLeft (t1, t2)
+    | Shiftrt ->
+        BitShiftRight (t1, t2)
+    | Lt ->
+        LessThan (t1, t2)
+    | Gt ->
+        LessThan (t2, t1)
+    | Le ->
+        LessEqual (t1, t2)
+    | Ge ->
+        LessEqual (t2, t1)
+    | Eq ->
+        Equal (t1, t2)
+    | Ne ->
+        NotEqual (t1, t2)
+    | BAnd ->
+        BitAnd (t1, t2)
+    | BXor ->
+        BitXor (t1, t2)
+    | BOr ->
+        BitOr (t1, t2)
+    | LAnd ->
+        And (t1, t2)
+    | LOr ->
+        Or (t1, t2)
+
+
+  let is_zero = function Const c -> Const.iszero_int_float c | _ -> false
+
+  let is_non_zero_const = function Const c -> not (Const.iszero_int_float c) | _ -> false
+
+  (** Fold [f] on the strict sub-terms of [t], if any. Preserve physical equality if [f] does. *)
+  let fold_map_direct_subterms t ~init ~f =
+    match t with
+    | Var _ | Const _ ->
+        (init, t)
+    | Minus t_not | BitNot t_not | Not t_not ->
+        let acc, t_not' = f init t_not in
+        let t' =
+          if phys_equal t_not t_not' then t
+          else
+            match t with
+            | Minus _ ->
+                Minus t_not'
+            | BitNot _ ->
+                BitNot t_not'
+            | Not _ ->
+                Not t_not'
+            | Var _
+            | Const _
+            | Add _
+            | Mult _
+            | Div _
+            | Mod _
+            | BitAnd _
+            | BitOr _
+            | BitShiftLeft _
+            | BitShiftRight _
+            | BitXor _
+            | And _
+            | Or _
+            | LessThan _
+            | LessEqual _
+            | Equal _
+            | NotEqual _ ->
+                assert false
+        in
+        (acc, t')
+    | Add (t1, t2)
+    | Mult (t1, t2)
+    | Div (t1, t2)
+    | Mod (t1, t2)
+    | BitAnd (t1, t2)
+    | BitOr (t1, t2)
+    | BitShiftLeft (t1, t2)
+    | BitShiftRight (t1, t2)
+    | BitXor (t1, t2)
+    | And (t1, t2)
+    | Or (t1, t2)
+    | LessThan (t1, t2)
+    | LessEqual (t1, t2)
+    | Equal (t1, t2)
+    | NotEqual (t1, t2) ->
+        let acc, t1' = f init t1 in
+        let acc, t2' = f acc t2 in
+        let t' =
+          if phys_equal t1 t1' && phys_equal t2 t2' then t
+          else
+            match t with
+            | Add _ ->
+                Add (t1', t2')
+            | Mult _ ->
+                Mult (t1', t2')
+            | Div _ ->
+                Div (t1', t2')
+            | Mod _ ->
+                Mod (t1', t2')
+            | BitAnd _ ->
+                BitAnd (t1', t2')
+            | BitOr _ ->
+                BitOr (t1', t2')
+            | BitShiftLeft _ ->
+                BitShiftLeft (t1', t2')
+            | BitShiftRight _ ->
+                BitShiftRight (t1', t2')
+            | BitXor _ ->
+                BitXor (t1', t2')
+            | And _ ->
+                And (t1', t2')
+            | Or _ ->
+                Or (t1', t2')
+            | LessThan _ ->
+                LessThan (t1', t2')
+            | LessEqual _ ->
+                LessEqual (t1', t2')
+            | Equal _ ->
+                Equal (t1', t2')
+            | NotEqual _ ->
+                NotEqual (t1', t2')
+            | Var _ | Const _ | Minus _ | BitNot _ | Not _ ->
+                assert false
+        in
+        (acc, t')
+
+
+  let map_direct_subterms t ~f =
+    fold_map_direct_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd
+
+
+  let rec fold_map_variables t ~init ~f =
+    match t with
+    | Var v ->
+        let acc, v' = f init v in
+        let t' = if phys_equal v v' then t else Var v' in
+        (acc, t')
+    | _ ->
+        fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_map_variables t' ~init:acc ~f)
+end
+
+(** Basically boolean terms, used to build formulas. *)
+module Atom = struct
+  type t =
+    | LessEqual of Term.t * Term.t
+    | LessThan of Term.t * Term.t
+    | Equal of Term.t * Term.t
+    | NotEqual of Term.t * Term.t
+  [@@deriving compare]
+
+  type atom = t
+
+  let pp fmt = function
+    | LessEqual (t1, t2) ->
+        F.fprintf fmt "%a ≤ %a" Term.pp t1 Term.pp t2
+    | LessThan (t1, t2) ->
+        F.fprintf fmt "%a < %a" Term.pp t1 Term.pp t2
+    | Equal (t1, t2) ->
+        F.fprintf fmt "%a = %a" Term.pp t1 Term.pp t2
+    | NotEqual (t1, t2) ->
+        F.fprintf fmt "%a ≠ %a" Term.pp t1 Term.pp t2
+
+
+  let nnot = function
+    | LessEqual (t1, t2) ->
+        LessThan (t2, t1)
+    | LessThan (t1, t2) ->
+        LessEqual (t2, t1)
+    | Equal (t1, t2) ->
+        NotEqual (t1, t2)
+    | NotEqual (t1, t2) ->
+        Equal (t1, t2)
+
+
+  let get_terms atom =
+    let (LessEqual (t1, t2) | LessThan (t1, t2) | Equal (t1, t2) | NotEqual (t1, t2)) = atom in
+    (t1, t2)
+
+
+  (** preserve physical equality if [f] does *)
+  let fold_map_terms atom ~init ~f =
+    let t1, t2 = get_terms atom in
+    let acc, t1' = f init t1 in
+    let acc, t2' = f acc t2 in
+    let t' =
+      if phys_equal t1' t1 && phys_equal t2' t2 then atom
+      else
+        match atom with
+        | LessEqual _ ->
+            LessEqual (t1', t2')
+        | LessThan _ ->
+            LessThan (t1', t2')
+        | Equal _ ->
+            Equal (t1', t2')
+        | NotEqual _ ->
+            NotEqual (t1', t2')
+    in
+    (acc, t')
+
+
+  let map_terms atom ~f = fold_map_terms atom ~init:() ~f:(fun () t -> ((), f t)) |> snd
+
+  let to_term : t -> Term.t = function
+    | LessEqual (t1, t2) ->
+        LessEqual (t1, t2)
+    | LessThan (t1, t2) ->
+        LessThan (t1, t2)
+    | Equal (t1, t2) ->
+        Equal (t1, t2)
+    | NotEqual (t1, t2) ->
+        NotEqual (t1, t2)
+
+
+  type eval_result = True | False | Atom of t
+
+  let eval_result_of_bool b = if b then True else False
+
+  let term_of_eval_result = function
+    | True ->
+        Term.one
+    | False ->
+        Term.zero
+    | Atom atom ->
+        to_term atom
+
+
+  (* other simplifications TODO:
+     - push Minus inwards
+     - (t1+i1)+((i2+t2)+i3) -> (t1+t2)+(i1+i2+i3): need to flatten trees of additions (and Minus)
+     - same for multiplications, possibly others too
+  *)
+  let rec eval_term t =
+    let open Term in
+    let t_norm_subterms = map_direct_subterms ~f:eval_term t in
+    match t_norm_subterms with
+    | Var _ | Const _ ->
+        t
+    | Minus (Minus t) ->
+        (* [--t = t] *)
+        t
+    | Minus (Const (Cint i)) ->
+        (* [-i = -1*i] *)
+        Const (Cint (IntLit.(mul minus_one) i))
+    | BitNot (BitNot t) ->
+        (* [~~t = t] *)
+        t
+    | Not (Const c) when Const.iszero_int_float c ->
+        (* [!0 = 1]  *)
+        one
+    | Not (Const c) when Const.isone_int_float c ->
+        (* [!1 = 0]  *)
+        zero
+    | Add (Const (Cint i1), Const (Cint i2)) ->
+        (* constants *)
+        Const (Cint (IntLit.add i1 i2))
+    | Add (Const c, t) when Const.iszero_int_float c ->
+        (* [0 + t = t] *)
+        t
+    | Add (t, Const c) when Const.iszero_int_float c ->
+        (* [t + 0 = t] *)
+        t
+    | Mult (Const c, t) when Const.isone_int_float c ->
+        (* [1 × t = t] *)
+        t
+    | Mult (t, Const c) when Const.isone_int_float c ->
+        (* [t × 1 = t] *)
+        t
+    | Mult (Const c, _) when Const.iszero_int_float c ->
+        (* [0 × t = 0] *)
+        zero
+    | Mult (_, Const c) when Const.iszero_int_float c ->
+        (* [t × 0 = 0] *)
+        zero
+    | Div (Const c, _) when Const.iszero_int_float c ->
+        (* [0 / t = 0] *)
+        zero
+    | Div (t, Const c) when Const.isone_int_float c ->
+        (* [t / 1 = t] *)
+        t
+    | Div (t, Const c) when Const.isminusone_int_float c ->
+        (* [t / (-1) = -t] *)
+        eval_term (Minus t)
+    | Div (Minus t1, Minus t2) ->
+        (* [(-t1) / (-t2) = t1 / t2] *)
+        eval_term (Div (t1, t2))
+    | Mod (Const c, _) when Const.iszero_int_float c ->
+        (* [0 % t = 0] *)
+        zero
+    | Mod (_, Const (Cint i)) when IntLit.isone i ->
+        (* [t % 1 = 0] *)
+        zero
+    | Mod (t1, t2) when equal_syntax t1 t2 ->
+        (* [t % t = 0] *)
+        zero
+    | And (t1, t2) when is_zero t1 || is_zero t2 ->
+        (* [false ∧ t = t ∧ false = false] *) zero
+    | And (t1, t2) when is_non_zero_const t1 ->
+        (* [true ∧ t = t] *) t2
+    | And (t1, t2) when is_non_zero_const t2 ->
+        (* [t ∧ true = t] *) t1
+    | Or (t1, t2) when is_non_zero_const t1 || is_non_zero_const t2 ->
+        (* [true ∨ t = t ∨ true = true] *) one
+    | Or (t1, t2) when is_zero t1 ->
+        (* [false ∨ t = t] *) t2
+    | Or (t1, t2) when is_zero t2 ->
+        (* [t ∨ false = t] *) t1
+    (* terms that are atoms can be simplified in [eval_atom] *)
+    | LessEqual (t1, t2) ->
+        eval_atom (LessEqual (t1, t2) : atom) |> term_of_eval_result
+    | LessThan (t1, t2) ->
+        eval_atom (LessThan (t1, t2) : atom) |> term_of_eval_result
+    | Equal (t1, t2) ->
+        eval_atom (Equal (t1, t2) : atom) |> term_of_eval_result
+    | NotEqual (t1, t2) ->
+        eval_atom (NotEqual (t1, t2) : atom) |> term_of_eval_result
+    | _ ->
+        t_norm_subterms
+
+
+  (** This assumes that the terms in the atom have been normalized/evaluated already.
+
+      TODO: probably a better way to implement this would be to rely entirely on
+      [eval_term (term_of_atom (atom))], possibly implementing it as something about observing the
+      sign/zero-ness of [t1 - t2]. *)
+  and eval_atom (atom : t) =
+    let t1, t2 = get_terms atom in
+    match (t1, t2) with
+    | Const (Cint i1), Const (Cint i2) -> (
+      match atom with
+      | Equal _ ->
+          eval_result_of_bool (IntLit.eq i1 i2)
+      | NotEqual _ ->
+          eval_result_of_bool (IntLit.neq i1 i2)
+      | LessEqual _ ->
+          eval_result_of_bool (IntLit.leq i1 i2)
+      | LessThan _ ->
+          eval_result_of_bool (IntLit.lt i1 i2) )
+    | _ ->
+        if Term.equal_syntax t1 t2 then
+          match atom with
+          | Equal _ ->
+              True
+          | NotEqual _ ->
+              False
+          | LessEqual _ ->
+              True
+          | LessThan _ ->
+              False
+        else Atom atom
+
+
+  let eval (atom : t) = map_terms atom ~f:eval_term |> eval_atom
+
+  let fold_map_variables a ~init ~f =
+    fold_map_terms a ~init ~f:(fun acc t -> Term.fold_map_variables t ~init:acc ~f)
+
+
+  module Set = Caml.Set.Make (struct
+    type nonrec t = t [@@deriving compare]
+  end)
+end
+
+module UnionFind = UnionFind.Make (struct
+  type t = Term.t [@@deriving compare]
+
+  let is_simpler_than (t1 : Term.t) (t2 : Term.t) =
+    match (t1, t2) with
+    | Const _, _ ->
+        true
+    | _, Const _ ->
+        false
+    | Var _, _ ->
+        true
+    | _, Var _ ->
+        false
+    | _ ->
+        false
+end)
+
+(** The main datatype is either in a normal form [True | False | NormalForm _], or in a
+    not-yet-normalized form [Atom _ | And _], or a mix of both.
+
+    Note the absence of disjunction and negation: negations are interpreted eagerly and
+    under-approximately by only remembering the first produced disjunct, and disjunctions are kept
+    in {!Term.t} form. *)
+type t =
+  | True
+  | False
+  | NormalForm of
+      { congruences: UnionFind.t
+            (** equality relation between terms represented by a union-find data structure with
+                canonical representatives for each class of congruent terms *)
+      ; facts: Atom.Set.t
+            (** atoms not of the form [Equal _], normalized with respect to the congruence relation
+                and the {!Atom.eval} function *) }
+  | And of t * t
+  | Atom of Atom.t
+
+let ffalse = False
+
+let is_literal_false = function False -> true | _ -> false
+
+let ttrue = True
+
+let rec pp fmt = function
+  | True ->
+      F.fprintf fmt "true"
+  | False ->
+      F.fprintf fmt "false"
+  | Atom atom ->
+      Atom.pp fmt atom
+  | NormalForm {congruences; facts} ->
+      let pp_collection ~fold ~sep ~pp_item fmt coll =
+        let pp_coll_aux is_first item =
+          F.fprintf fmt "@[<h>%s%a@]" (if is_first then "" else sep) pp_item item ;
+          (* is_first not true anymore *) false
+        in
+        F.fprintf fmt "@[<hv>%t@]" (fun _fmt -> fold coll ~init:true ~f:pp_coll_aux |> ignore)
+      in
+      let pp_ts_or_repr repr fmt ts =
+        if UnionFind.Set.is_empty ts then Term.pp fmt repr
+        else
+          pp_collection ~sep:"="
+            ~fold:(IContainer.fold_of_pervasives_set_fold UnionFind.Set.fold)
+            ~pp_item:Term.pp fmt ts
+      in
+      let pp_congruences fmt congruences =
+        pp_collection ~sep:"∧" ~fold:UnionFind.fold_congruences fmt congruences
+          ~pp_item:(fun fmt ((repr : UnionFind.repr), ts) ->
+            F.fprintf fmt "%a=%a" Term.pp (repr :> Term.t) (pp_ts_or_repr (repr :> Term.t)) ts )
+      in
+      let pp_atoms fmt atoms =
+        pp_collection ~sep:"∧"
+          ~fold:(IContainer.fold_of_pervasives_set_fold Atom.Set.fold)
+          ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" Atom.pp atom)
+          fmt atoms
+      in
+      F.fprintf fmt "[%a@;&&@ %a]" pp_congruences congruences pp_atoms facts
+  | And (phi1, phi2) ->
+      F.fprintf fmt "{%a}∧{%a}" pp phi1 pp phi2
+
+
+module NormalForm : sig
+  val of_formula : t -> t
+  (** This computes equivalence classes between terms induced by the given conjunctive formula, then
+      symbolically evaluates the resulting terms and atoms to form a [NormalForm _] term equivalent
+      to the input formula, or [True] or [False]. *)
+
+  val to_formula : UnionFind.t -> Atom.Set.t -> t
+  (** transforms a congruence relation and set of atoms into a formula without [NormalForm _]
+      sub-formulas *)
+end = struct
+  (* NOTE: throughout this module some cases that are never supposed to happen at the moment are
+     handled nonetheless to avoid hassle and surprises in the future. *)
+
+  let to_formula uf facts =
+    let phi = Atom.Set.fold (fun atom phi -> And (Atom atom, phi)) facts True in
+    let phi =
+      UnionFind.fold_congruences uf ~init:phi ~f:(fun conjuncts (repr, terms) ->
+          L.d_printf "@\nEquivalence class of %a: " Term.pp (repr :> Term.t) ;
+          UnionFind.Set.fold
+            (fun t conjuncts ->
+              L.d_printf "%a," Term.pp t ;
+              if phys_equal t (repr :> Term.t) then conjuncts
+              else And (Atom (Equal ((repr :> Term.t), t)), conjuncts) )
+            terms conjuncts )
+    in
+    L.d_ln () ;
+    phi
+
+
+  (** used for quickly detecting contradictions *)
+  exception Contradiction
+
+  (** normalize term by replacing every (sub-)term by its canonical representative *)
+  let rec apply_term uf t =
+    match (UnionFind.find_opt uf t :> Term.t option) with
+    | None ->
+        (* no representative found for [t], look for substitution opportunities in its sub-terms *)
+        Term.map_direct_subterms t ~f:(fun t' -> apply_term uf t')
+    | Some t_repr ->
+        t_repr
+
+
+  let apply_atom uf (atom : Atom.t) =
+    let atom' = Atom.map_terms atom ~f:(fun t -> apply_term uf t) in
+    match Atom.eval atom' with
+    | True ->
+        None
+    | False ->
+        (* early exit on contradictions *)
+        L.d_printfln "Contradiction detected! %a ~> %a is False" Atom.pp atom Atom.pp atom' ;
+        raise_notrace Contradiction
+    | Atom atom ->
+        Some atom
+
+
+  (** normalize atomes by replacing every (sub-)term by their canonical representative then
+      symbolically evaluating the result *)
+  let normalize_atoms uf ~add_to:facts0 atoms =
+    List.fold atoms ~init:facts0 ~f:(fun facts atom ->
+        match apply_atom uf atom with None -> facts | Some atom' -> Atom.Set.add atom' facts )
+
+
+  (** Extract [NormalForm _] from the given formula and return the formula without that part
+      (replaced with [True]). If there are several [NormalForm _] sub-formulas, return only one of
+      them and leave the others in. *)
+  let split_normal_form phi =
+    let rec find_normal_form normal_form phi =
+      match phi with
+      | NormalForm _ when Option.is_some normal_form ->
+          (normal_form, phi)
+      | NormalForm {congruences; facts} ->
+          (Some (congruences, facts), ttrue)
+      | True | False | Atom _ ->
+          (normal_form, phi)
+      | And (phi1, phi2) ->
+          let normal_form, phi1' = find_normal_form normal_form phi1 in
+          let normal_form, phi2' = find_normal_form normal_form phi2 in
+          let phi' =
+            if phys_equal phi1' phi && phys_equal phi2' phi2 then phi else And (phi1', phi2')
+          in
+          (normal_form, phi')
+    in
+    find_normal_form None phi
+
+
+  (** split the given formula into [(uf, facts, atoms)] where [phi] is equivalent to
+      [uf ∧ facts ∧ atoms], [facts] are in normal form w.r.t. [uf], but [atoms] are not and need
+      to be normalized *)
+  let rec gather_congruences_and_facts ((uf, facts, atoms) as acc) phi =
+    match phi with
+    | True ->
+        acc
+    | False ->
+        raise Contradiction
+    | Atom (Equal (t1, t2)) ->
+        (* NOTE: this should also normalize sub-terms of [t1] and [t2] according to the equality
+           relation. We don't do that yet. *)
+        let uf = UnionFind.union uf t1 t2 in
+        (* change facts into atoms when the equality relation changes so they will be normalized
+           again later using the new equality relation *)
+        let atoms_with_facts = Atom.Set.fold (fun atom atoms -> atom :: atoms) facts atoms in
+        (uf, Atom.Set.empty, atoms_with_facts)
+    | Atom atom ->
+        (uf, facts, atom :: atoms)
+    | And (phi1, phi2) ->
+        let acc' = gather_congruences_and_facts acc phi1 in
+        gather_congruences_and_facts acc' phi2
+    | NormalForm {congruences; facts} ->
+        gather_congruences_and_facts acc (to_formula congruences facts)
+
+
+  let of_formula phi =
+    (* start from a pre-existing normal form if any *)
+    let (uf, facts), phi =
+      match split_normal_form phi with
+      | Some uf_facts, phi ->
+          (uf_facts, phi)
+      | None, phi ->
+          ((UnionFind.empty, Atom.Set.empty), phi)
+    in
+    try
+      let uf, facts, new_facts = gather_congruences_and_facts (uf, facts, []) phi in
+      let facts = normalize_atoms uf ~add_to:facts new_facts in
+      NormalForm {congruences= uf; facts}
+    with Contradiction -> ffalse
+end
+
+let mk_less_than t1 t2 = Atom (LessThan (t1, t2))
+
+let mk_less_equal t1 t2 = Atom (LessEqual (t1, t2))
+
+let mk_equal t1 t2 = Atom (Equal (t1, t2))
+
+let mk_not_equal t1 t2 = Atom (NotEqual (t1, t2))
+
+(** propagates literal [False] *)
+let aand phi1 phi2 =
+  if is_literal_false phi1 || is_literal_false phi2 then ffalse else And (phi1, phi2)
+
+
+let rec nnot phi =
+  match phi with
+  | True ->
+      False
+  | False ->
+      True
+  | Atom a ->
+      Atom (Atom.nnot a)
+  | NormalForm {congruences; facts} ->
+      NormalForm.to_formula congruences facts |> nnot
+  | And (phi1, _phi2) ->
+      (* HACK/TODO: this keeps only one disjunct of the negation, which is ok for
+         under-approximation even though it's quite incomplete (especially for [And (True,
+         phi)]!). We could work harder at disjunctions if that proves to be an issue. *)
+      nnot phi1
+
+
+(** Detects terms that look like formulas, but maybe the logic in here would be better in
+    [Atom.eval_term] to avoid duplicating reasoning steps. *)
+let rec of_term (t : Term.t) =
+  match t with
+  | And (t1, t2) ->
+      aand (of_term t1) (of_term t2)
+  | LessThan (t1, t2) ->
+      mk_less_than t1 t2
+  | LessEqual (t1, t2) ->
+      mk_less_equal t1 t2
+  | Equal (t1, t2) ->
+      mk_equal t1 t2
+  | NotEqual (t1, t2) ->
+      mk_not_equal t1 t2
+  | Const (Cint i) ->
+      if IntLit.iszero i then ffalse else ttrue
+  | Const (Cfloat f) ->
+      if Float.equal f Float.zero then ffalse else ttrue
+  | Const (Cstr _ | Cfun _ | Cclass _) ->
+      ttrue
+  | Mult (t1, t2) ->
+      (* [t1 × t2 ≠ 0] iff [t1 ≠ 0] && [t2 ≠ 0] *)
+      aand (of_term t1) (of_term t2)
+  | Div (t1, t2) when Term.equal_syntax t1 t2 ->
+      (* [t ÷ t = 1] *)
+      ttrue
+  | Div (t1, t2) ->
+      (* [t1 ÷ t2 ≠ 0] iff [t1 ≠ 0 ∧ t1 ≥ t2] *)
+      aand (of_term t1) (mk_less_equal t2 t1)
+  | Not t ->
+      nnot (of_term t)
+  | Minus t ->
+      (* [-t ≠ 0] iff [t ≠ 0] *)
+      of_term t
+  | Add (t1, Minus t2) | Add (Minus t1, t2) ->
+      (* [t1 - t2 ≠ 0] iff [t1 ≠ t2] *)
+      mk_not_equal t1 t2
+  | Or _
+  | Add _
+  | Var _
+  | Mod _
+  | BitAnd _
+  | BitOr _
+  | BitNot _
+  | BitShiftLeft _
+  | BitShiftRight _
+  | BitXor _ ->
+      (* default case: we don't know how to change the term itself into a formula so we represent
+         the fact that [t] is "true" by [t ≠ 0] *)
+      Atom (NotEqual (t, Term.zero))
+
+
+let of_term_binop bop t1 t2 =
+  (* be brutal and convert to a term, then trust that [of_term] will restore the formula structure
+     as the conversion is lossless *)
+  Term.of_binop bop t1 t2 |> of_term
+
+
+let normalize phi = NormalForm.of_formula phi
+
+let simplify ~keep:_ phi = (* TODO: actually remove variables not in [keep] *) normalize phi
+
+let rec fold_map_variables phi ~init ~f =
+  match phi with
+  | True | False ->
+      (init, phi)
+  | NormalForm {congruences; facts} ->
+      NormalForm.to_formula congruences facts |> fold_map_variables ~init ~f
+  | Atom atom ->
+      let acc, atom' = Atom.fold_map_variables atom ~init ~f in
+      let phi' = if phys_equal atom atom' then phi else Atom atom' in
+      (acc, phi')
+  | And (phi1, phi2) ->
+      let acc, phi1' = fold_map_variables phi1 ~init ~f in
+      let acc, phi2' = fold_map_variables phi2 ~init:acc ~f in
+      if phys_equal phi1' phi1 && phys_equal phi2' phi2 then (acc, phi)
+      else (acc, And (phi1', phi2'))

infer/src/pulse/PulseFormula.mli

@@ -0,0 +1,71 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module F = Format
+module AbstractValue = PulseAbstractValue
+
+(** {2 Arithmetic solver}
+
+    Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable. *)
+
+module Term : sig
+  (** Similar to {!Exp.t} but with no memory operations and with {!AbstractValue.t} instead of SIL
+      variables. The rich structure allows us to represent all of SIL but is not a promise that we
+      are able to meaningfully reason about all of it. *)
+  type t
+
+  val zero : t
+
+  val of_absval : AbstractValue.t -> t
+
+  val of_intlit : IntLit.t -> t
+
+  val of_binop : Binop.t -> t -> t -> t
+
+  val of_unop : Unop.t -> t -> t
+end
+
+type t
+
+val pp : F.formatter -> t -> unit
+
+(** {3 Build formulas from non-formulas} *)
+
+val ttrue : t
+
+val of_term_binop : Binop.t -> Term.t -> Term.t -> t
+
+val mk_equal : Term.t -> Term.t -> t
+
+val mk_less_equal : Term.t -> Term.t -> t
+
+val mk_less_than : Term.t -> Term.t -> t
+
+(** {3 Combine formulas} *)
+
+val aand : t -> t -> t
+
+val nnot : t -> t
+
+(** {3 Operations} *)
+
+val simplify : keep:AbstractValue.Set.t -> t -> t
+
+val fold_map_variables : t -> init:'a -> f:('a -> AbstractValue.t -> 'a * AbstractValue.t) -> 'a * t
+
+val is_literal_false : t -> bool
+(** Call [is_literal_false (normalize phi)] to check satisfiability. *)
+
+val normalize : t -> t
+(** Produces a semantically-equivalent formula¹ where all consequences of equalities have been
+    applied and some ad-hoc arithmetic and logical reasoning has been performed. In particular, the
+    canonical representation of a known-false formula is [ffalse], and [is_literal_false ffalse] is
+    [true]. Probably a good idea to not throw away the result of calling this if you are going to
+    re-use the formula.
+
+    (¹) Except it might throw away disjuncts! *)

infer/src/pulse/PulsePathCondition.ml

@@ -10,6 +10,7 @@ module F = Format
 module L = Logging
 module AbstractValue = PulseAbstractValue
 module CItv = PulseCItv
+module Formula = PulseFormula
 module ValueHistory = PulseValueHistory
 
 module BoItvs = struct
@@ -29,57 +30,58 @@ module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv)
     facts deduced by one domain to inform another. *)
 type t =
   { satisfiable: bool
-        (** If [true] then [pudge] could still be unsatisfiable (asking that question is expensive).
+        (** If [true] then [formula] could still be unsatisfiable (asking that question is
+            expensive).
 
             If [false] then the other components of the record can be arbitrary. *)
   ; bo_itvs: BoItvs.t
   ; citvs: CItvs.t
-  ; pudge: Pudge.t }
+  ; formula: Formula.t }
 
-let pp fmt {satisfiable; bo_itvs; citvs; pudge} =
+let pp fmt {satisfiable; bo_itvs; citvs; formula} =
-  F.fprintf fmt "@[<hv>sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;pudge: @[%a@]@]" satisfiable BoItvs.pp
+  F.fprintf fmt "@[<hv>sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" satisfiable BoItvs.pp
-    bo_itvs CItvs.pp citvs Pudge.pp pudge
+    bo_itvs CItvs.pp citvs Formula.pp formula
 
 
-let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; pudge= Pudge.true_}
+let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
 
-let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; pudge= Pudge.true_}
+let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
 
-let and_nonnegative v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
+let and_nonnegative v ({satisfiable; bo_itvs; citvs; formula} as phi) =
   if not satisfiable then phi
   else
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
     ; citvs= CItvs.add v CItv.zero_inf citvs
-    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
+    ; formula= Formula.(aand (mk_less_equal Term.zero (Term.of_absval v)) formula) }
 
 
-let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
+let and_positive v ({satisfiable; bo_itvs; citvs; formula} as phi) =
   if not satisfiable then phi
   else
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
     ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
-    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
+    ; formula= Formula.(aand (mk_less_than Term.zero (Term.of_absval v)) formula) }
 
 
-let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) =
+let and_eq_int v i ({satisfiable; bo_itvs; citvs; formula} as phi) =
   if not satisfiable then phi
   else
     { satisfiable
     ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
     ; citvs= CItvs.add v (CItv.equal_to i) citvs
-    ; pudge= Pudge.(and_formula (Formula.eq (Term.of_absval v) (Term.of_intlit i)) pudge) }
+    ; formula= Formula.(aand (mk_equal (Term.of_absval v) (Term.of_intlit i)) formula) }
 
 
-let simplify ~keep {satisfiable; bo_itvs; citvs; pudge} =
+let simplify ~keep {satisfiable; bo_itvs; citvs; formula} =
   if not satisfiable then false_
   else
     let is_in_keep v _ = AbstractValue.Set.mem v keep in
     { satisfiable
     ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
     ; citvs= CItvs.filter is_in_keep citvs
-    ; pudge= Pudge.simplify ~keep pudge }
+    ; formula= Formula.simplify ~keep formula }
 
 
 let subst_find_or_new subst addr_callee =
@@ -173,19 +175,14 @@ let and_citvs_callee subst citvs_caller citvs_callee =
   (subst, citvs')
 
 
-let and_pudge_callee subst pudge_caller pudge_callee =
+let and_formula_callee subst formula_caller formula_callee =
   (* need to translate callee variables to make sense for the caller, thereby possibly extending
      the current substitution *)
-  let subst, pudge_callee_translated =
+  let subst, formula_callee_translated =
-    Pudge.fold_map_variables pudge_callee ~init:subst ~f:(fun subst v_callee_arith ->
+    Formula.fold_map_variables formula_callee ~init:subst ~f:subst_find_or_new
-        let v_callee = Pudge.Var.to_absval v_callee_arith in
-        let subst', v_caller = subst_find_or_new subst v_callee in
-        (subst', Pudge.Var.of_absval v_caller) )
   in
-  (* Don't trigger the computation of the underlying Sledge data structure by asking for
+  L.d_printfln "translated callee formula: %a@\n" Formula.pp formula_callee_translated ;
-     satisfiability here. Instead, pudge (un-)satisfiability is computed lazily when we discover
+  (subst, Formula.aand formula_caller formula_callee_translated)
-     issues. *)
-  (subst, Pudge.and_ pudge_caller pudge_callee_translated)
 
 
 let and_callee subst phi ~callee:phi_callee =
@@ -201,8 +198,9 @@ let and_callee subst phi ~callee:phi_callee =
           L.d_printfln "contradiction found by concrete intervals" ;
           (subst, false_)
       | subst, citvs' ->
-          let subst, pudge' = and_pudge_callee subst phi.pudge phi_callee.pudge in
+          let subst, formula' = and_formula_callee subst phi.formula phi_callee.formula in
-          (subst, {satisfiable= true; bo_itvs= bo_itvs'; citvs= citvs'; pudge= pudge'}) )
+          L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ;
+          (subst, {satisfiable= true; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) )
 
 
 (** {2 Operations} *)
@@ -241,28 +239,25 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs =
   BoItvs.add binop_addr bo_itv bo_itvs
 
 
-let eval_pudge_binop binop_addr binop op_lhs op_rhs pudge =
+let eval_formula_binop binop_addr binop op_lhs op_rhs formula =
-  let open Pudge in
+  let open Formula in
   let term_of_op = function
     | LiteralOperand i ->
         Term.of_intlit i
     | AbstractValueOperand v ->
         Term.of_absval v
   in
-  match Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) with
+  let t_binop = Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) in
-  | None ->
+  aand (mk_equal (Term.of_absval binop_addr) t_binop) formula
-      pudge
-  | Some t_binop ->
-      and_formula (Formula.eq (Term.of_absval binop_addr) t_binop) pudge
 
 
-let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pudge} as phi) =
+let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; formula} as phi) =
   if not phi.satisfiable then phi
   else
     { satisfiable
     ; 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
-    ; pudge= eval_pudge_binop binop_addr binop op_lhs op_rhs pudge }
+    ; formula= eval_formula_binop binop_addr binop op_lhs op_rhs formula }
 
 
 let eval_citv_unop unop_addr unop operand_addr citvs =
@@ -282,22 +277,19 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs =
       BoItvs.add unop_addr itv bo_itvs
 
 
-let eval_pudge_unop unop_addr (unop : Unop.t) addr pudge =
+let eval_formula_unop unop_addr (unop : Unop.t) addr formula =
-  let open Pudge in
+  let open Formula in
-  match Term.of_unop unop (Term.of_absval addr) with
+  let t_unop = Term.of_unop unop (Term.of_absval addr) in
-  | None ->
+  aand (mk_equal (Term.of_absval unop_addr) t_unop) formula
-      pudge
-  | Some t_unop ->
-      and_formula (Formula.eq (Term.of_absval unop_addr) t_unop) pudge
 
 
-let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi) =
+let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; formula} as phi) =
   if not phi.satisfiable then phi
   else
     { satisfiable
     ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
     ; citvs= eval_citv_unop unop_addr unop addr citvs
-    ; pudge= eval_pudge_unop unop_addr unop addr pudge }
+    ; formula= eval_formula_unop unop_addr unop addr formula }
 
 
 let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
@@ -316,12 +308,12 @@ let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
 
 let eval_operand phi = function
   | LiteralOperand i ->
-      (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, Pudge.Term.of_intlit i)
+      (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, Formula.Term.of_intlit i)
   | AbstractValueOperand v ->
       ( Some v
       , CItvs.find_opt v phi.citvs
       , BoItvs.find_or_default v phi.bo_itvs
-      , Pudge.Term.of_absval v )
+      , Formula.Term.of_absval v )
 
 
 let record_citv_abduced addr_opt arith_opt citvs =
@@ -334,21 +326,18 @@ let record_citv_abduced addr_opt arith_opt citvs =
 
 let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi
 
-let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; pudge} as phi) =
+let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; formula} as phi) =
   if not satisfiable then phi
   else
-    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, pudge_lhs = eval_operand phi lhs_op in
+    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, t_lhs = eval_operand phi lhs_op in
-    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, pudge_rhs = eval_operand phi rhs_op in
+    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, t_rhs = eval_operand phi rhs_op in
     let phi =
-      match Pudge.Formula.term_binop bop pudge_lhs pudge_rhs with
+      let f_positive = Formula.of_term_binop bop t_lhs t_rhs in
-      | None ->
+      let formula =
-          phi
+        let f = if negated then Formula.nnot f_positive else f_positive in
-      | Some f_positive ->
+        Formula.aand f formula
-          let pudge =
+      in
-            let f = if negated then Pudge.Formula.not_ f_positive else f_positive in
+      {phi with formula}
-            Pudge.and_formula f pudge
-          in
-          {phi with pudge}
     in
     match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with
     | Unsatisfiable ->
@@ -392,9 +381,9 @@ let is_known_zero phi v =
   || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero
 
 
-let is_unsat_cheap phi = not phi.satisfiable
+let is_unsat_cheap phi = (not phi.satisfiable) || Formula.is_literal_false phi.formula
 
 let is_unsat_expensive phi =
-  (* note: contradictions are detected eagerly for all sub-domains except pudge, so just
+  (* note: contradictions are detected eagerly for all sub-domains except formula, so just
      evaluate that one *)
-  is_unsat_cheap phi || Pudge.is_unsat phi.pudge
+  is_unsat_cheap phi || Formula.normalize phi.formula |> Formula.is_literal_false

infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp

@@ -45,7 +45,7 @@ void diverge_if_alias_ok(int* x, int* y) {
   }
 }
 
-void FP_diverge_before_null_deref_ok(int* x) {
+void diverge_before_null_deref_ok(int* x) {
   diverge_if_alias_ok(x, x);
   int* p = nullptr;
   *p = 42;

infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp

@@ -36,7 +36,7 @@ bool equal(size_t x, size_t y) {
   return x == y;
 }
 
-void FP_unreachable_interproc_compare_ok(int* x, size_t y) {
+void unreachable_interproc_compare_ok(int* x, size_t y) {
   if (equal(y, 0)) {
     free(x);
   }

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

@@ -1,4 +1,3 @@
-codetoanalyze/cpp/pulse/aliasing.cpp, FP_diverge_before_null_deref_ok, 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/aliasing.cpp, alias_null_deref_bad, 6, 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/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]
@@ -11,7 +10,6 @@ codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_b
 codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
-codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_interproc_compare_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_unreachable_interproc_compare_ok,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_unreachable_interproc_compare_ok,invalid access occurs here]
 codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_bad, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test3_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test5_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok,invalid access occurs here]