[pulse] new new arithmetic

Summary:
Instead of alternating between a normal form and a tree structure,
always keep a normal form. Except the normal form is not always fully
normalized. Overall, it's a bit faster than the previous iteration,
while being more precise! In particular, linear arithmetic aims at being
much more complete.

Reviewed By: skcho

Differential Revision: D23134209

fbshipit-source-id: 5f9ec6ece

infer/src/IR/IntLit.ml

@@ -72,6 +72,8 @@ let of_int = of_z Z.of_int
 
 let of_string = of_z Z.of_string
 
+let of_big_int = of_z Fn.id
+
 let z_to_int_opt i = try Some (Z.to_int i) with Z.Overflow -> None
 
 let to_int {i} = z_to_int_opt i

infer/src/IR/IntLit.mli

@@ -29,6 +29,8 @@ val eq : t -> t -> bool
 
 val of_int : int -> t
 
+val of_big_int : Z.t -> t
+
 val of_int32 : int32 -> t
 
 val of_int64 : int64 -> t

infer/src/istd/Pp.ml

@@ -202,3 +202,17 @@ let cli_args fmt args = cli_args_with_verbosity ~verbose:true fmt args
 let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b
 
 let in_backticks pp fmt x = F.fprintf fmt "`%a`" pp x
+
+let collection :
+       fold:('t, 'item, _) Container.fold
+    -> sep:string
+    -> pp_item:(F.formatter -> 'item -> unit)
+    -> F.formatter
+    -> 't
+    -> unit =
+ fun ~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)

infer/src/istd/Pp.mli

@@ -105,3 +105,11 @@ val pair :
   -> unit
 
 val in_backticks : (F.formatter -> 'a -> unit) -> F.formatter -> 'a -> unit [@@warning "-32"]
+
+val collection :
+     fold:('t, 'item, bool) Container.fold
+  -> sep:string
+  -> pp_item:(F.formatter -> 'item -> unit)
+  -> F.formatter
+  -> 't
+  -> unit

infer/src/istd/UnionFind.ml

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module F = Format
 
 module type Element = sig
   type t [@@deriving compare]
@@ -13,8 +14,7 @@ module type Element = sig
   val is_simpler_than : t -> t -> bool
 end
 
-module Make (X : Element) = struct
-  module Set = Caml.Set.Make (X)
+module Make (X : Element) (XSet : Caml.Set.S with type elt = X.t) = struct
   module Map = Caml.Map.Make (X)
 
   let equal_x = [%compare.equal: X.t]
@@ -34,6 +34,11 @@ module Make (X : Element) = struct
 
     val merge : t -> repr -> into:repr -> t
 
+    val add_disjoint_class : repr -> XSet.t -> t -> t
+    (** [add_disjoint_class repr xs uf] adds a class [{repr} U xs] with representative [repr] to
+        [uf], assuming the [repr] is correct and the class does not intersect with any existing
+        elements of [uf] *)
+
     module Map : Caml.Map.S with type key = repr
   end = struct
     type repr = X.t
@@ -60,22 +65,24 @@ module Make (X : Element) = struct
 
     let merge reprs x ~into:y = (* TODO: implement path compression *) Map.add x y reprs
 
+    let add_disjoint_class repr xs reprs = XSet.fold (fun x reprs -> Map.add x repr reprs) xs 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 find classes (x : UF.repr) = UF.Map.find_opt x classes |> Option.value ~default:XSet.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
+      let new_class = XSet.union class1 class2 |> XSet.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}
+  type t = {reprs: UF.t; classes: XSet.t UF.Map.t}
 
   let empty = {reprs= UF.empty; classes= UF.Map.empty}
 
@@ -86,16 +93,55 @@ module Make (X : Element) = struct
   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
+    if equal_x (repr1 :> X.t) (repr2 :> X.t) then
+      (* avoid creating loops in the relation *)
+      (uf, None)
     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}
+      ({reprs; classes}, Some ((from :> X.t), into))
 
 
   let fold_congruences {classes} ~init ~f =
     UF.Map.fold (fun repr xs acc -> f acc (repr, xs)) classes init
+
+
+  let pp ~pp_empty pp_item fmt uf =
+    let pp_ts_or_repr repr fmt ts =
+      if XSet.is_empty ts then pp_item fmt repr
+      else
+        Pp.collection ~sep:"="
+          ~fold:(IContainer.fold_of_pervasives_set_fold XSet.fold)
+          ~pp_item fmt ts
+    in
+    let pp_aux fmt uf =
+      let is_empty = ref true in
+      Pp.collection ~sep:" ∧ " ~fold:fold_congruences fmt uf
+        ~pp_item:(fun fmt ((repr : repr), ts) ->
+          is_empty := false ;
+          F.fprintf fmt "%a=%a" pp_item (repr :> X.t) (pp_ts_or_repr (repr :> X.t)) ts ) ;
+      if !is_empty then pp_empty fmt
+    in
+    F.fprintf fmt "@[<hv>%a@]" pp_aux uf
+
+
+  let filter_not_in_closed_set ~keep uf =
+    let classes =
+      UF.Map.filter
+        (fun x _ ->
+          (* here we take advantage of the fact [keep] is transitively closed already to drop
+             entire classes at once iff their representative is not in [keep]: if the class
+             contains *one* item in [keep] then *all* of its items are in [keep] *)
+          XSet.mem (x :> X.t) keep )
+        uf.classes
+    in
+    (* rebuild [reprs] directly from [classes]: does path compression and garbage collection on the
+       old [reprs] *)
+    let reprs =
+      UF.Map.fold (fun repr xs reprs -> UF.add_disjoint_class repr xs reprs) classes UF.empty
+    in
+    {reprs; classes}
 end

infer/src/istd/UnionFind.mli

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module F = Format
 
 (** A union-find data structure. *)
 
@@ -16,23 +17,31 @@ module type Element = sig
   (** will be used to choose a "simpler" representative for a given equivalence class when possible *)
 end
 
-module Make (X : Element) : sig
+module Make (X : Element) (XSet : Caml.Set.S with type elt = X.t) : sig
   type t
 
-  type repr = private X.t
+  val pp :
+    pp_empty:(F.formatter -> unit) -> (F.formatter -> X.t -> unit) -> F.formatter -> t -> unit
 
-  module Set : Caml.Set.S with type elt = X.t
+  type repr = private X.t
 
   val empty : t
 
-  val union : t -> X.t -> X.t -> t
+  val union : t -> X.t -> X.t -> t * (X.t * repr) option
+  (** return the optional new equality added between the old representatives of the two items in the
+      form of "old representative = new representative", [None] if they were already in the same
+      congruence class *)
 
   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
+  val fold_congruences : (t, repr * XSet.t, 'acc) Container.fold
   (** fold over the equivalence classes of the relation, singling out the representative for each
       class *)
+
+  val filter_not_in_closed_set : keep:XSet.t -> t -> t
+  (** only keep items in [keep], assuming that [keep] is closed under the relation, i.e. that if an
+      item [x] is in [keep] then so are all the [y] such that [x=y] according to the relation *)
 end

infer/src/pulse/PulseFormula.mli

@@ -7,69 +7,74 @@
 
 open! IStd
 module F = Format
-module AbstractValue = PulseAbstractValue
+
+(* NOTE: using [Var] for [AbstractValue] here since this is how "abstract values" are interpreted,
+   in particular as far as arithmetic is concerned *)
+module Var = 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 pp : F.formatter -> t -> unit
 
-  val of_absval : AbstractValue.t -> t
+val pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit
+  [@@warning "-32"]
+(** only used for unit tests *)
 
-  val of_intlit : IntLit.t -> t
+type 'a normalized = Unsat | Sat of 'a
 
-  val of_binop : Binop.t -> t -> t -> t
+type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t
 
-  val of_unop : Unop.t -> t -> t
-end
+(** {3 Build formulas} *)
 
-type t
+val ttrue : t
 
-val pp : F.formatter -> t -> unit
+val and_equal : operand -> operand -> t -> t normalized
 
-val pp_with_pp_var : (F.formatter -> AbstractValue.t -> unit) -> F.formatter -> t -> unit
-  [@@warning "-32"]
-(** only used for unit tests *)
+val and_less_equal : operand -> operand -> t -> t normalized
 
-(** {3 Build formulas from non-formulas} *)
+val and_less_than : operand -> operand -> t -> t normalized
 
-val ttrue : t
+val and_equal_unop : Var.t -> Unop.t -> operand -> t -> t normalized
 
-val of_term_binop : Binop.t -> Term.t -> Term.t -> t
+val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> t normalized
 
-val mk_equal : Term.t -> Term.t -> t
+val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t normalized
 
-val mk_less_equal : Term.t -> Term.t -> t
+(** {3 Operations} *)
 
-val mk_less_than : Term.t -> Term.t -> t
+val normalize : t -> t normalized
+(** think a bit harder about the formula *)
 
-(** {3 Combine formulas} *)
+val simplify : keep:Var.Set.t -> t -> t normalized
 
-val aand : t -> t -> t
+val and_fold_map_variables :
+  t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t) normalized
 
-val nnot : t -> t
+val is_known_zero : t -> Var.t -> bool
 
-(** {3 Operations} *)
+(** {3 Notations} *)
+
+include sig
+  [@@@warning "-60"]
 
-val simplify : keep:AbstractValue.Set.t -> t -> t
+  (** Useful notations to deal with normalized formulas *)
+  module SatUnsatMonad : sig
+    [@@@warning "-32"]
 
-val fold_map_variables : t -> init:'a -> f:('a -> AbstractValue.t -> 'a * AbstractValue.t) -> 'a * t
+    val map_normalized : ('a -> 'b) -> 'a normalized -> 'b normalized
 
-val is_literal_false : t -> bool
-(** Call [is_literal_false (normalize phi)] to check satisfiability. *)
+    val ( >>| ) : 'a normalized -> ('a -> 'b) -> 'b normalized
 
-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.
+    val ( let+ ) : 'a normalized -> ('a -> 'b) -> 'b normalized
 
-    (¹) Except it might throw away disjuncts! *)
+    val bind_normalized : ('a -> 'b normalized) -> 'a normalized -> 'b normalized
+
+    val ( >>= ) : 'a normalized -> ('a -> 'b normalized) -> 'b normalized
+
+    val ( let* ) : 'a normalized -> ('a -> 'b normalized) -> 'b normalized
+  end
+end

infer/src/pulse/PulsePathCondition.ml

@@ -29,11 +29,7 @@ module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv)
 (** A mash-up of several arithmetic domains. At the moment they are independent, i.e. we don't use
     facts deduced by one domain to inform another. *)
 type t =
-  { is_unsat: bool
-        (** If [false] then [formula] could still be unsatisfiable (asking that question is
-            expensive).
-
-            If [true] then the other components of the record can be arbitrary. *)
+  { is_unsat: bool  (** if [true] then the other components of the record can be arbitrary *)
   ; bo_itvs: BoItvs.t
   ; citvs: CItvs.t
   ; formula: Formula.t }
@@ -47,39 +43,50 @@ 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 and_nonnegative v ({is_unsat; bo_itvs; citvs; formula} as phi) =
-  if is_unsat then phi
-  else
+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 ( let+| ) x f = map_formula_sat x f
+
+let and_nonnegative v phi =
+  let+ {is_unsat; bo_itvs; citvs; formula} = phi in
+  let+| formula =
+    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= Formula.(aand (mk_less_equal Term.zero (Term.of_absval v)) formula) }
+  ; formula }
 
 
-let and_positive v ({is_unsat; bo_itvs; citvs; formula} as phi) =
-  if is_unsat then phi
-  else
+let and_positive v phi =
+  let+ {is_unsat; bo_itvs; citvs; formula} = phi in
+  let+| formula =
+    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= Formula.(aand (mk_less_than Term.zero (Term.of_absval v)) formula) }
+  ; formula }
 
 
-let and_eq_int v i ({is_unsat; bo_itvs; citvs; formula} as phi) =
-  if is_unsat then phi
-  else
+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= Formula.(aand (mk_equal (Term.of_absval v) (Term.of_intlit i)) formula) }
+  ; formula }
 
 
-let simplify ~keep {is_unsat; bo_itvs; citvs; formula} =
-  if is_unsat then false_
-  else
+let simplify ~keep phi =
+  let+ {is_unsat; bo_itvs; citvs; formula} = phi in
+  let+| formula = Formula.simplify ~keep formula in
   let is_in_keep v _ = AbstractValue.Set.mem v keep in
-    let formula = Formula.simplify ~keep formula in
-    { is_unsat= is_unsat || Formula.is_literal_false formula
+  { is_unsat
   ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
   ; citvs= CItvs.filter is_in_keep citvs
   ; formula }
@@ -179,11 +186,8 @@ let and_citvs_callee subst citvs_caller citvs_callee =
 let and_formula_callee subst formula_caller ~callee:formula_callee =
   (* need to translate callee variables to make sense for the caller, thereby possibly extending
      the current substitution *)
-  let subst, formula_callee_translated =
-    Formula.fold_map_variables formula_callee ~init:subst ~f:subst_find_or_new
-  in
-  L.d_printfln "translated callee formula: %a@\n" Formula.pp formula_callee_translated ;
-  (subst, Formula.aand formula_caller formula_callee_translated)
+  Formula.and_fold_map_variables formula_caller ~up_to_f:formula_callee ~f:subst_find_or_new
+    ~init:subst
 
 
 let and_callee subst phi ~callee:phi_callee =
@@ -198,18 +202,22 @@ let and_callee subst phi ~callee:phi_callee =
       | exception Contradiction ->
           L.d_printfln "contradiction found by concrete intervals" ;
           (subst, false_)
-      | subst, citvs' ->
-          let subst, formula' = and_formula_callee subst phi.formula ~callee:phi_callee.formula in
+      | 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') ->
+            (* TODO: normalize here? *)
             L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ;
-          let formula' = Formula.normalize formula' in
-          let is_unsat = Formula.is_literal_false formula' in
-          if is_unsat then L.d_printfln "contradiction found by formulas" ;
-          (subst, {is_unsat; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) )
+            (subst, {is_unsat= false; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) ) )
 
 
 (** {2 Operations} *)
 
-type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
+type operand = Formula.operand =
+  | LiteralOperand of IntLit.t
+  | AbstractValueOperand of AbstractValue.t
 
 let eval_citv_binop binop_addr bop op_lhs op_rhs citvs =
   let citv_of_op op citvs =
@@ -243,25 +251,13 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs =
   BoItvs.add binop_addr bo_itv bo_itvs
 
 
-let eval_formula_binop binop_addr binop op_lhs op_rhs formula =
-  let open Formula in
-  let term_of_op = function
-    | LiteralOperand i ->
-        Term.of_intlit i
-    | AbstractValueOperand v ->
-        Term.of_absval v
-  in
-  let t_binop = Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) in
-  aand (mk_equal (Term.of_absval binop_addr) t_binop) formula
-
-
-let eval_binop binop_addr binop op_lhs op_rhs ({is_unsat; bo_itvs; citvs; formula} as phi) =
-  if phi.is_unsat then phi
-  else
+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= eval_formula_binop binop_addr binop op_lhs op_rhs formula }
+  ; formula }
 
 
 let eval_citv_unop unop_addr unop operand_addr citvs =
@@ -281,19 +277,13 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs =
       BoItvs.add unop_addr itv bo_itvs
 
 
-let eval_formula_unop unop_addr (unop : Unop.t) addr formula =
-  let open Formula in
-  let t_unop = Term.of_unop unop (Term.of_absval addr) in
-  aand (mk_equal (Term.of_absval unop_addr) t_unop) formula
-
-
-let eval_unop unop_addr unop addr ({is_unsat; bo_itvs; citvs; formula} as phi) =
-  if phi.is_unsat then phi
-  else
+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= eval_formula_unop unop_addr unop addr formula }
+  ; formula }
 
 
 let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
@@ -312,12 +302,9 @@ 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, Formula.Term.of_intlit i)
+      (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i)
   | AbstractValueOperand v ->
-      ( Some v
-      , CItvs.find_opt v phi.citvs
-      , BoItvs.find_or_default v phi.bo_itvs
-      , Formula.Term.of_absval v )
+      (Some v, CItvs.find_opt v phi.citvs, BoItvs.find_or_default v phi.bo_itvs)
 
 
 let record_citv_abduced addr_opt arith_opt citvs =
@@ -328,18 +315,16 @@ let record_citv_abduced addr_opt arith_opt citvs =
       CItvs.add addr arith citvs
 
 
-let bind_is_unsat phi ~f = if phi.is_unsat then phi else f phi
-
 let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formula} as phi) =
   if is_unsat then phi
   else
-    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, t_rhs = eval_operand phi rhs_op in
+    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_
-    | Satisfiable (abduced_lhs, abduced_rhs) ->
+    | Satisfiable (abduced_lhs, abduced_rhs) -> (
         let phi =
           let citvs =
             record_citv_abduced value_lhs_opt abduced_lhs citvs
@@ -359,44 +344,37 @@ let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formul
               true
         in
         if is_unsat then L.d_printfln "contradiction detected by inferbo intervals" ;
-        let phi = {phi with is_unsat} in
-        let phi =
-          bind_is_unsat phi ~f:(fun phi ->
-              prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi )
-        in
-        let phi =
+        let+ phi = {phi with is_unsat} in
+        let+ phi = prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi in
+        let+ phi =
           Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' ->
-              bind_is_unsat phi ~f:(fun phi ->
-                  prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) )
-        in
-        if phi.is_unsat then phi
-        else
-          let f_positive = Formula.of_term_binop bop t_lhs t_rhs in
-          let formula =
-            let f = if negated then Formula.nnot f_positive else f_positive in
-            Formula.aand f formula |> Formula.normalize
+              prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi )
         in
-          let is_unsat = Formula.is_literal_false formula in
-          if is_unsat then L.d_printfln "contradiction detected by formulas" ;
-          {phi with is_unsat; formula}
+        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} )
 
 
 (** {2 Queries} *)
 
 let is_known_zero phi v =
-  (* TODO: ask [Formula] too *)
   CItvs.find_opt v phi.citvs |> Option.value_map ~default:false ~f:CItv.is_equal_to_zero
   || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero
+  || Formula.is_known_zero phi.formula v
 
 
-let is_unsat_cheap phi = phi.is_unsat || Formula.is_literal_false phi.formula
+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)
   else
-    let formula = Formula.normalize phi.formula in
-    let is_unsat = Formula.is_literal_false formula in
-    let phi = {phi with is_unsat; formula} in
-    (phi, is_unsat)
+    match Formula.normalize phi.formula with
+    | Unsat ->
+        (false_, true)
+    | Sat formula ->
+        ({phi with formula}, false)

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -6,26 +6,66 @@
  *)
 
 open! IStd
-module F = Format
 module AbstractValue = PulseAbstractValue
-module Formula = PulseFormula
+open PulseFormula
+open SatUnsatMonad
 
 let%test_module _ =
   ( module struct
-    (** shorthand for defining formulas easily *)
+    (** {2 Utilities for defining formulas easily}
 
-    let i i = Formula.Term.of_intlit (IntLit.of_int i)
+        We want to be able to write something close to [x + y - 42 < z], but the API of
+        {!PulseFormula} doesn't support building arbitrary formulas or even arbitrary terms.
+        Instead, we have to introduce intermediate variables for each sub-expression (this
+        corresponds to how the reste of Pulse interacts with the arithmetic layer too, so it's good
+        that we follow this constraint here too).
 
-    let ( + ) t1 t2 = Formula.Term.of_binop (PlusA None) t1 t2
+        The definitions here make this transparent by passing the formula around. For example,
+        building [x+y] takes in a formula [phi] and returns [(phi ∧ v123 = x+y, v123)], i.e. a
+        pair of the formula with a new intermediate equality and the resulting intermediate
+        variable. This allows us to chain operations: [x+y-42] is a function that takes a formula,
+        passes it to [x+y] returning [(phi',v123)] as we saw with [phi' = phi ∧ v123 = x+y],
+        passes it to "42", which here is also a function returning [(phi',42)] (note the unchanged
+        [phi']), then finally returns [(phi ∧ v123 = x+y ∧ v234 = v123-42, v234)].
 
-    let ( - ) t1 t2 = Formula.Term.of_binop (MinusA None) t1 t2
+        This is convoluted, especially as each step may also return [Unsat] even during "term"
+        construction, but as a result the tests themselves should be straightforward to understand. *)
 
-    let ( = ) t1 t2 = Formula.mk_equal t1 t2
+    (** a literal integer leaves the formula unchanged and returns a [LiteralOperand] *)
+    let i i phi = Sat (phi, LiteralOperand (IntLit.of_int i))
 
-    let ( < ) t1 t2 = Formula.mk_less_than t1 t2
+    (** similarly as for literals; this is not used directly in tests so the name is a bit more
+        descriptive *)
+    let op_of_var x phi = Sat (phi, AbstractValueOperand x)
 
-    let ( && ) phi1 phi2 = Formula.aand phi1 phi2
+    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
+      (phi, AbstractValueOperand v)
 
+
+    let ( + ) f1 f2 phi = of_binop (PlusA None) f1 f2 phi
+
+    let ( - ) f1 f2 phi = of_binop (MinusA None) f1 f2 phi
+
+    let ( = ) f1 f2 phi =
+      let* phi, op1 = f1 phi in
+      let* phi, op2 = f2 phi in
+      and_equal op1 op2 phi
+
+
+    let ( < ) f1 f2 phi =
+      let* phi, op1 = f1 phi in
+      let* phi, op2 = f2 phi in
+      and_less_than op1 op2 phi
+
+
+    let ( && ) f1 f2 phi = f1 phi >>= f2
+
+    (* we remember a mapping [Var.t -> string] to print more readable results that mention the
+       user-defined variables by their readable names instead of [v123] *)
     let var_names = Caml.Hashtbl.create 4
 
     let mk_var name =
@@ -36,21 +76,19 @@ let%test_module _ =
 
     let x_var = mk_var "x"
 
-    let x = Formula.Term.of_absval x_var
+    let x = op_of_var x_var
 
     let y_var = mk_var "y"
 
-    let y = Formula.Term.of_absval y_var
+    let y = op_of_var y_var
 
     let z_var = mk_var "z"
 
-    let z = Formula.Term.of_absval z_var
+    let z = op_of_var z_var
 
-    let w = Formula.Term.of_absval (mk_var "w")
+    let w = op_of_var (mk_var "w")
 
-    let v = Formula.Term.of_absval (mk_var "v")
-
-    (** utilities for writing tests *)
+    let v = op_of_var (mk_var "v")
 
     let pp_var fmt v =
       match Caml.Hashtbl.find_opt var_names v with
@@ -60,75 +98,100 @@ let%test_module _ =
           AbstractValue.pp fmt v
 
 
-    let formula_pp = Formula.pp_with_pp_var pp_var
+    let normalized_pp fmt = function
+      | Unsat ->
+          F.pp_print_string fmt "unsat"
+      | Sat phi ->
+          pp_with_pp_var pp_var fmt phi
+
 
-    let normalize phi = Formula.normalize phi |> F.printf "%a" formula_pp
+    let normalize f = f ttrue >>= normalize |> F.printf "%a" normalized_pp
 
-    let simplify ~keep phi =
-      Formula.simplify ~keep:(AbstractValue.Set.of_list keep) phi |> F.printf "%a" formula_pp
+    let simplify ~keep f =
+      f ttrue >>= simplify ~keep:(AbstractValue.Set.of_list keep) |> F.printf "%a" normalized_pp
 
 
     (** the actual tests *)
 
+    let%expect_test _ =
+      normalize (x < y) ;
+      [%expect {|
+        [true (no var=var) && true (no linear) && {x < y}]|}]
+
     let%expect_test _ =
       normalize (x + i 1 - i 1 < x) ;
       [%expect {|
-        [true && {(x+1)+(-1) < x}]|}]
+        unsat|}]
 
     let%expect_test _ =
       normalize (x + (y - x) < y) ;
       [%expect {|
-        [true && {x+(y-x) < y}]|}]
+        unsat|}]
 
     let%expect_test _ =
       normalize (x = y && y = z && z = i 0 && x = i 1) ;
-      [%expect {|false|}]
+      [%expect {|unsat|}]
 
-    (* should be false (x = w + (y+1) -> 1 = w + z -> 1 = 0) but we don't go and normalize sub-terms
-       in the existing relation when adding new equalities to the relation *)
+    (* should be false (x = w + (y+1) -> 1 = w + z -> 1 = 0)  *)
     let%expect_test _ =
       normalize (x = w + y + i 1 && y + i 1 = z && x = i 1 && w + z = i 0) ;
       [%expect {|
-[0=(w+z) ∧ 1=x=((w+y)+1) ∧ z=(y+1) && true]|}]
+unsat|}]
+
+    (* same as above but atoms are given in the opposite order *)
+    let%expect_test _ =
+      normalize (w + z = i 0 && x = i 1 && y + i 1 = z && x = w + y + i 1) ;
+      [%expect {|
+unsat|}]
 
     let%expect_test _ =
-      normalize (Formula.Term.of_binop Ne x y = i 0 && x = i 0 && y = i 1) ;
+      normalize (of_binop Ne x y = i 0 && x = i 0 && y = i 1) ;
       [%expect {|
-        [0=x=(x≠y) ∧ 1=y && true]|}]
+        unsat|}]
 
     let%expect_test _ =
-      normalize (Formula.Term.of_binop Eq x y = i 0 && x = i 0 && y = i 1) ;
+      normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ;
       [%expect {|
-        [0=x=(x=y) ∧ 1=y && true]|}]
+        [true (no var=var) && x = 0 ∧ y = 1 ∧ v19 = 0 && true (no atoms)]|}]
+
+    let%expect_test _ =
+      normalize (x = i 0 && x < i 0) ;
+      [%expect {|
+        unsat|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ;
       [%expect {|
-0 = x|}]
+[true (no var=var) && x = 0 && true (no atoms)]|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ;
       [%expect {|
-0 = x|}]
+[x=v20 && x = 0 && true (no atoms)]|}]
 
     let%expect_test _ =
       simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ;
       [%expect {|
-0 = y+1|}]
+[true (no var=var) && y = -1 && true (no atoms)]|}]
 
     (* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *)
     let%expect_test _ =
       simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ;
       [%expect {|
-{w = x-y}∧{{x = y+z}∧{0 = w+1}}|}]
+[x=v22 ∧ z=w=v23 && x = y -1 ∧ z = -1 && true (no atoms)]|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ;
-      [%expect {|
-{v = w+1}∧{{x = y+z}∧{0 = (w+x)+y}}|}]
+      [%expect
+        {|
+[x=v25 ∧ v=v28
+ &&
+ x = 1/2·z + -1/2·w ∧ y = -1/2·z + -1/2·w ∧ v = w +1 ∧ v26 = 1/2·z + 1/2·w
+ &&
+ true (no atoms)]|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ;
       [%expect {|
-{y = z}∧{{x = y+4}∧{x = w}}|}]
+[x=w=v29 ∧ y=z && x = y +4 && true (no atoms)]|}]
   end )