[pulse] intervals!

Summary:
This adds a more interesting value domain to pulse: concrete intervals.

There are still two main limitations:
1. arithmetic operations are all over-approximated: any assignment involving arithmetic operations is replaced by non-determinism
2. abstract values that are discovered to be equal are not merged into one

Reviewed By: skcho

Differential Revision: D18058972

fbshipit-source-id: 0492a590f

infer/src/IR/IntLit.ml

@@ -148,6 +148,8 @@ let shift_right intlit1 {i= i2} =
       lift1 (fun i -> Z.shift_right i i2) intlit1
 
 
+let max i1 i2 = if geq i1 i2 then i1 else i2
+
 let min i1 i2 = if leq i1 i2 then i1 else i2
 
 let pp f intlit = if isnull intlit then F.pp_print_string f "null" else Z.pp_print f intlit.i

infer/src/IR/IntLit.mli

@@ -89,6 +89,8 @@ val shift_right : t -> t -> t
 
 val sub : t -> t -> t
 
+val max : t -> t -> t
+
 val min : t -> t -> t
 
 val to_int : t -> int option

infer/src/pulse/PulseAbductiveDomain.ml

@@ -447,26 +447,25 @@ module PrePost = struct
     match Attributes.get_arithmetic attrs_pre with
     | None ->
         call_state
-    | Some _ as arith_callee ->
+    | Some _ as arith_callee -> (
         let addr_caller = fst addr_hist_caller in
         let astate = call_state.astate in
         let arith_caller = Memory.get_arithmetic addr_caller astate in
         (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes
            for that address in the post since abstract values are immutable *)
-        let satisfiable, abduce_caller, _abduce_callee =
+        match Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller arith_callee with
-          Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller arith_callee
+        | Unsatisfiable ->
-        in
+            raise
-        if not satisfiable then
+              (CannotApplyPre
-          raise
+                 (Arithmetic {addr_caller; addr_callee= addr_pre; arith_caller; arith_callee}))
-            (CannotApplyPre
+        | Satisfiable (abduce_caller, _abduce_callee) ->
-               (Arithmetic {addr_caller; addr_callee= addr_pre; arith_caller; arith_callee})) ;
+            let new_astate =
-        let new_astate =
+              Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller ->
-          Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller ->
+                  let attribute = Attribute.Arithmetic abduce_caller in
-              let attribute = Attribute.Arithmetic abduce_caller in
+                  Memory.abduce_attribute addr_caller attribute astate
-              Memory.abduce_attribute addr_caller attribute astate
+                  |> Memory.add_attribute addr_caller attribute )
-              |> Memory.add_attribute addr_caller attribute )
+            in
-        in
+            {call_state with astate= new_astate} )
-        {call_state with astate= new_astate}
 
 
   (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in

infer/src/pulse/PulseArithmetic.ml

@@ -7,62 +7,392 @@
 open! IStd
 module F = Format
 
-type t = EqualTo of Const.t [@@deriving compare]
+module Bound = struct
+  type t = Int of IntLit.t | MinusInfinity | PlusInfinity [@@deriving compare]
 
-let pp fmt = function EqualTo c -> F.fprintf fmt "=%a" (Const.pp Pp.text) c
+  let pp fmt = function
+    | Int i ->
+        IntLit.pp fmt i
+    | MinusInfinity ->
+        F.pp_print_string fmt "-∞"
+    | PlusInfinity ->
+        F.pp_print_string fmt "+∞"
 
-(** booleans with \top *)
+
-module TBool = struct
+  let equal b1 b2 =
-  type t = True | False | Top
+    match (b1, b2) with
+    | MinusInfinity, MinusInfinity | PlusInfinity, PlusInfinity ->
+        true
+    | Int i1, Int i2 ->
+        IntLit.eq i1 i2
+    | _ ->
+        false
+
+
+  let le b1 b2 =
+    match (b1, b2) with
+    | MinusInfinity, _ | _, PlusInfinity ->
+        true
+    | (Int _ | PlusInfinity), MinusInfinity | PlusInfinity, Int _ ->
+        false
+    | Int i1, Int i2 ->
+        IntLit.leq i1 i2
+
+
+  let lt b1 b2 =
+    match (b1, b2) with
+    | MinusInfinity, _ | _, PlusInfinity ->
+        true
+    | (Int _ | PlusInfinity), MinusInfinity | PlusInfinity, Int _ ->
+        false
+    | Int i1, Int i2 ->
+        IntLit.lt i1 i2
+
+
+  let ge b1 b2 =
+    match (b1, b2) with
+    | _, MinusInfinity | PlusInfinity, _ ->
+        true
+    | MinusInfinity, (Int _ | PlusInfinity) | Int _, PlusInfinity ->
+        false
+    | Int i1, Int i2 ->
+        IntLit.geq i1 i2
+
+
+  let gt b1 b2 =
+    match (b1, b2) with
+    | _, MinusInfinity | PlusInfinity, _ ->
+        true
+    | MinusInfinity, (Int _ | PlusInfinity) | Int _, PlusInfinity ->
+        false
+    | Int i1, Int i2 ->
+        IntLit.gt i1 i2
+
+
+  let min b1 b2 = if le b1 b2 then b1 else b2
+
+  let max b1 b2 = if le b1 b2 then b2 else b1
+
+  let add_int b i =
+    match b with MinusInfinity | PlusInfinity -> b | Int i' -> Int (IntLit.add i' i)
+
+
+  let is_interval b1 b2 =
+    match (b1, b2) with
+    | MinusInfinity, MinusInfinity | PlusInfinity, PlusInfinity ->
+        false
+    | _ ->
+        le b1 b2
 end
 
-let flip_abduced (tbool, c1, c2) = (tbool, c2, c1)
+module Unsafe : sig
+  type t = private
+    | Between of Bound.t * Bound.t  (** we write [b1,b2] for these *)
+    | Outside of IntLit.t * IntLit.t  (** we write i1][i2 for these *)
+  [@@deriving compare]
+
+  val between : Bound.t -> Bound.t -> t
+
+  val outside : IntLit.t -> IntLit.t -> t
+
+  val equal_to : IntLit.t -> t
+
+  val not_equal_to : IntLit.t -> t
+end = struct
+  type t = Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t [@@deriving compare]
+
+  let between b1 b2 =
+    assert (Bound.is_interval b1 b2) ;
+    Between (b1, b2)
+
+
+  let outside i1 i2 =
+    assert (IntLit.leq i1 i2) ;
+    Outside (i1, i2)
+
+
+  let equal_to i =
+    let b = Bound.Int i in
+    Between (b, b)
+
+
+  let not_equal_to i = Outside (i, i)
+end
+
+include Unsafe
+
+let pp fmt = function
+  | Between (MinusInfinity, PlusInfinity) ->
+      F.fprintf fmt "∈ℕ"
+  | Between (lower, PlusInfinity) ->
+      F.fprintf fmt "≥%a" Bound.pp lower
+  | Between (MinusInfinity, upper) ->
+      F.fprintf fmt "≤%a" Bound.pp upper
+  | Between (lower, upper) when Bound.equal lower upper ->
+      F.fprintf fmt "=%a" Bound.pp lower
+  | Between (lower, upper) ->
+      F.fprintf fmt "∈[%a,%a]" Bound.pp lower Bound.pp upper
+  | Outside (l, u) when IntLit.eq l u ->
+      F.fprintf fmt "≠%a" IntLit.pp l
+  | Outside (l, u) ->
+      F.fprintf fmt "∉[%a,%a]" IntLit.pp l IntLit.pp u
+
+
+let has_empty_intersection a1 a2 =
+  match (a1, a2) with
+  | Outside _, Outside _ ->
+      false
+  | Between (lower1, upper1), Between (lower2, upper2) ->
+      Bound.lt upper1 lower2 || Bound.lt upper2 lower1
+  | Between (lower1, upper1), Outside (l2, u2) | Outside (l2, u2), Between (lower1, upper1) ->
+      (* is [l1, u1] inside [l2, u2]? *)
+      Bound.le (Int l2) lower1 && Bound.ge (Int u2) upper1
+
 
-let rec abduce_eq a1 a2 =
+let add_int a i =
+  match a with
+  | Between (lower, upper) ->
+      between (Bound.add_int lower i) (Bound.add_int upper i)
+  | Outside (l, u) ->
+      outside (IntLit.add i l) (IntLit.add i u)
+
+
+let to_singleton = function Between (Int l1, Int l2) when IntLit.eq l1 l2 -> Some l1 | _ -> None
+
+(** [remove_element e a] compute [a - {e}] if representable and if it is not [a] *)
+let remove_element e = function
+  | Between (lower, upper) when Bound.equal lower upper ->
+      (* empty sets are not allowed to be represented *) None
+  | Between (Int l, upper) when IntLit.eq l e ->
+      Some (between (Int (IntLit.(add one) l)) upper)
+  | Between (lower, Int u) when IntLit.eq u e ->
+      Some (between lower (Int (IntLit.(add minus_one) u)))
+  | Between (MinusInfinity, PlusInfinity) ->
+      Some (not_equal_to e)
+  | Between _ ->
+      None
+  | Outside (l, u) ->
+      let l_minus_one = IntLit.(add minus_one) l in
+      if IntLit.eq e l_minus_one then Some (outside l_minus_one u)
+      else
+        (* can't have [l-1 = u+1] because [l≤u] *)
+        let u_plus_one = IntLit.(add one) u in
+        if IntLit.eq e u_plus_one then Some (outside l u_plus_one) else None
+
+
+type abduction_result = Unsatisfiable | Satisfiable of t option * t option
+
+let flip_abduced = function
+  | Unsatisfiable ->
+      Unsatisfiable
+  | Satisfiable (lhs, rhs) ->
+      Satisfiable (rhs, lhs)
+
+
+let rec abduce_eq (a1 : t) (a2 : t) =
   match (a1, a2) with
-  | Some (EqualTo c1), Some (EqualTo c2) when Const.equal c1 c2 ->
+  | Between (lower1, upper1), Between (lower2, upper2) ->
-      (TBool.True, None, None)
+      (* ∃x. l1≤x≤u1 ∧ l2≤x≤u2 *)
-  | Some (EqualTo _c1), Some (EqualTo _c2) (* c1≠c2 *) ->
+      (* ⇔ ∃x. max(l1,l2)≤x≤min(u1,u2) *)
-      (TBool.False, None, None)
+      let lower = Bound.max lower1 lower2 in
-  | None, Some _ ->
+      let upper = Bound.min upper1 upper2 in
+      if Bound.lt upper lower then Unsatisfiable
+      else
+        let tighter = Some (between lower upper) in
+        Satisfiable (tighter, tighter)
+  | Outside (l1, u1), Outside (l2, u2) ->
+      (* ∃x. (x<l1 ∨ x>u1) ∧ (x<l2 ∨ x>u2) ∧ li<=ui*)
+      (* all the possible cases:
+            x: --------[   ]---------
+            y: -----[       ]--------
+
+            x: ---[           ]------
+            y: -----[       ]--------
+
+            x: ---[       ]----------
+            y: -----[       ]--------
+
+            x: ---------[       ]----
+            y: -----[       ]--------
+
+         -> SAT, can tighten both to min(l1,l2)][max(u1,u2)
+
+            x: ---------------[   ]--
+            y: -----[       ]--------
+         or symmetrically x<->y => cannot express the 3 intervals that would be needed so return SAT
+         (TODO: we might want to keep only one of these, which would be a kind of recency model of
+         disequalities: remember the last known disequality)
+      *)
+      if IntLit.leq l1 u2 && IntLit.leq l2 u1 then
+        let l = IntLit.min l1 l2 in
+        let u = IntLit.max u1 u2 in
+        let tighter = Some (outside l u) in
+        Satisfiable (tighter, tighter)
+      else Satisfiable (None, None)
+  | Outside _, Between _ ->
       abduce_eq a2 a1 |> flip_abduced
-  | Some (EqualTo _c), None ->
+  | Between (lower1, upper1), Outside (l2, u2) ->
-      (TBool.True, None, a1)
+      (* ∃x. l1≤x≤u1 ∧ (x<l2 ∨ x>u2) *)
-  | None, None ->
+      (* all the possible cases:
-      (TBool.Top, None, None)
+
+            x:  [-------]
+            y: --[   ]---
+
+         case 1 above: SAT, cannot say more unless a1 is [-∞,+∞] (then we can abduce that a1 is
+         the same as a2)
+
+            x:        [--]
+            y: ------[   ]--
 
+         case 2 above: UNSAT
 
-let abduce_ne a1 a2 =
+            x:   [---]
+            y: ------[   ]--
+
+         case 3 above: SAT: x = x\cap y for both
+
+            x:      [----]
+            y: ------[   ]--
+
+         case 4 above: SAT: x\cap y for both
+      *)
+      if Bound.lt lower1 (Int l2) && Bound.gt upper1 (Int u2) then
+        (* case 1 *)
+        match a1 with
+        | Between (MinusInfinity, PlusInfinity) ->
+            Satisfiable (Some a2, None)
+        | _ ->
+            Satisfiable (None, None)
+      else if Bound.ge lower1 (Int l2) && Bound.le upper1 (Int u2) then (* case 2 *)
+        Unsatisfiable
+      else if
+        (* l1≥l2 or u1≤u2 but not both, i.e. x is on only one side of y and their intersection is
+           one interval *)
+        Bound.lt lower1 (Int l2)
+      then
+        (* case 3 & 4: x left of y *)
+        let lower = lower1 in
+        let upper = Bound.min upper1 (Int (IntLit.(add minus_one) l2)) in
+        let tighter = Some (between lower upper) in
+        Satisfiable (tighter, tighter)
+      else
+        (* l1≥l2 ∧ u1>u2*)
+        (* case 3 & 4: x right of y *)
+        let lower = Bound.max lower1 (Int (IntLit.(add one) u2)) in
+        let upper = upper1 in
+        let tighter = Some (between lower upper) in
+        Satisfiable (tighter, tighter)
+
+
+let abduce_ne (a1 : t) (a2 : t) =
+  if has_empty_intersection a1 a2 then Satisfiable (None, None)
+  else
+    match (to_singleton a1, to_singleton a2) with
+    | Some _, Some _ ->
+        (* non-empty intersection between 2 singletons => they are the same singleton and hence the
+           same integer and have the same value, so cannot be disequal *)
+        Unsatisfiable
+    | None, None ->
+        (* non-empty intersection and each predicate can be satisfied by ≥2 elements => we cannot
+           know if they are disequal or not *)
+        Satisfiable (None, None)
+    | Some e1, None -> (
+      match remove_element e1 a2 with
+      | Some _ as abduced2 ->
+          Satisfiable (None, abduced2)
+      | None ->
+          Satisfiable (None, None) )
+    | None, Some e2 -> (
+      match remove_element e2 a1 with
+      | Some _ as abduced1 ->
+          Satisfiable (abduced1, None)
+      | None ->
+          Satisfiable (None, None) )
+
+
+let abduce_le (a1 : t) (a2 : t) =
   match (a1, a2) with
-  | Some (EqualTo c1), Some (EqualTo c2) when Const.equal c1 c2 ->
+  | Between (lower1, upper1), Between (lower2, upper2) ->
-      (TBool.False, None, None)
+      (* ∃x≤y. l1≤x≤u1 ∧ l2≤y≤u2 *)
-  | Some (EqualTo _c1), Some (EqualTo _c2) (* c1≠c2 *) ->
+      (* ⇔ ∃x,y. x≤y ∧ l1≤x≤min(u1,u2) ∧ max(l1,l2)≤y≤u2 *)
-      (TBool.True, None, None)
+      let min_u1u2 = Bound.min upper1 upper2 in
-  | None, Some _ | Some _, None ->
+      let max_l1l2 = Bound.max lower1 lower2 in
-      (* cannot express ≠c so go to Top *)
+      if Bound.lt min_u1u2 lower1 || Bound.lt upper2 max_l1l2 then
-      (TBool.Top, None, None)
+        (* any of these contradict the formula above *)
-  | None, None ->
+        Unsatisfiable
-      (TBool.Top, None, None)
+      else Satisfiable (Some (between lower1 min_u1u2), Some (between max_l1l2 upper2))
+  | Outside _, Outside _ ->
+      Satisfiable (None, None)
+  | Between (lower1, _upper1), Outside (l2, u2) ->
+      (* ∃x≤y. l1≤x≤u1 ∧ y<l2 ∧ y>u2 *)
+      (* two cases:
+         1. l1<l2: we don't know if x≤y for sure and cannot express a good fact to abduce to make
+         it true
+            x:   [----doesn't matter where u1 is
+            y: -----[       ]---------------------
+         2. l1≥l2: we can abduce that y≥max(u2+1, l1) and that makes it SAT
+            x:      [----doesn't matter either
+            y: -----[       ]---------------------
+      *)
+      if Bound.lt lower1 (Int l2) then (* case 1: l1<l2 *) Satisfiable (None, None)
+      else
+        (* case 2: l1≥l2 *)
+        let lower = Bound.max (Int (IntLit.(add one) u2)) lower1 in
+        Satisfiable (None, Some (between lower PlusInfinity))
+  | Outside (l1, u1), Between (_lower2, upper2) ->
+      (* similarly, two cases:
+         1. u1≥u2: can refine to x≤min(l1+1, u2)
+            x: -----[       ]---------------------
+            y: ..-]
+         or y:      ...-----]
+         2. u1<u2: cannot deduce anything 
+            x: -----[       ]---------------------
+            y:          ...---]
+      *)
+      if Bound.ge (Int u1) upper2 then
+        (* case 1: l1>l2 *)
+        let upper = Bound.min (Int (IntLit.(add one) l1)) upper2 in
+        Satisfiable (Some (between MinusInfinity upper), None)
+      else (* case 2: l1≤l2 *)
+        Satisfiable (None, None)
 
 
-let abduce_binop_constraints ~negated (bop : Binop.t) a1 a2 =
+let abduce_lt (a1 : t) (a2 : t) =
+  match abduce_le (add_int a1 IntLit.one) a2 with
+  | Satisfiable (Some abduced1, abduced2_opt) ->
+      Satisfiable (Some (add_int abduced1 IntLit.minus_one), abduced2_opt)
+  | result ->
+      result
+
+
+let abduce_binop_constraints ~negated (bop : Binop.t) (a1 : t) (a2 : t) =
   let open Binop in
   match (bop, negated) with
   | Eq, false | Ne, true ->
       abduce_eq a1 a2
   | Eq, true | Ne, false ->
       abduce_ne a1 a2
+  | Le, false | Gt, true ->
+      abduce_le a1 a2
+  | Ge, false | Lt, true ->
+      abduce_le a2 a1 |> flip_abduced
+  | Lt, false | Ge, true ->
+      abduce_lt a1 a2
+  | Gt, false | Le, true ->
+      abduce_lt a2 a1 |> flip_abduced
   | _ ->
-      (TBool.Top, None, None)
+      Satisfiable (None, None)
-
-
-let abduce_binop_is_true_aux ~negated bop a1_opt a2_opt =
-  Logging.d_printfln "abduce_binop_is_true ~negated:%b %s (%a) (%a)" negated
-    (Binop.str Pp.text bop) (Pp.option pp) a1_opt (Pp.option pp) a2_opt ;
-  abduce_binop_constraints ~negated bop a1_opt a2_opt
 
 
 let abduce_binop_is_true ~negated bop v1 v2 =
-  let result, abduced1, abduced2 = abduce_binop_is_true_aux ~negated bop v1 v2 in
+  Logging.d_printfln "abduce_binop_is_true ~negated:%b %s (%a) (%a)" negated
-  let can_go_through = match result with Top | True -> true | False -> false in
+    (Binop.str Pp.text bop) (Pp.option pp) v1 (Pp.option pp) v2 ;
-  (can_go_through, abduced1, abduced2)
+  match (v1, v2) with
+  | None, None ->
+      (* two existential variables: no way to express in the non-relational domain *)
+      Satisfiable (None, None)
+  | _ ->
+      let unknown = between MinusInfinity PlusInfinity in
+      let a1 = Option.value v1 ~default:unknown in
+      let a2 = Option.value v2 ~default:unknown in
+      abduce_binop_constraints ~negated bop a1 a2

infer/src/pulse/PulseArithmetic.mli

@@ -7,19 +7,31 @@
 open! IStd
 module F = Format
 
-type t = EqualTo of Const.t [@@deriving compare]
+module Bound : sig
+  type t = Int of IntLit.t | MinusInfinity | PlusInfinity
+end
+
+type t = private Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t
+[@@deriving compare]
+
+val equal_to : IntLit.t -> t
 
 val pp : F.formatter -> t -> unit
 
-val abduce_binop_is_true :
+type abduction_result =
-  negated:bool -> Binop.t -> t option -> t option -> bool * t option * t option
+  | Unsatisfiable  (** the assertion is never true given the parameters *)
-(** given [arith_lhs_opt bop arith_rhs_opt], return a triple
+  | Satisfiable of t option * t option
-   [(satisfiable,abduced_lhs_opt,abduced_rhs_opt)] such that (taking lhs=true if lhs_opt is [None],
+      (** the assertion is satisfiable and when it is true then the lhs and rhs can be optionally
-   same for rhs):
+          refined to the given new intervals *)
+
+val abduce_binop_is_true : negated:bool -> Binop.t -> t option -> t option -> abduction_result
+(** given [arith_lhs_opt bop arith_rhs_opt] and if not [negated], return either
 
-   - [satisfiable] iff lhs bop rhs ≠ ∅
+   - [Unsatisfiable] iff lhs bop rhs = ∅
 
-   - [abduced_lhs_opt=Some alhs] if [satisfiable] and (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs)
+   - [Satisfiable (abduced_lhs_opt,abduced_rhs_opt)] iff lhs bop rhs ≠ ∅, such that (taking lhs=true
+    if lhs_opt is [None], same for rhs) [abduced_lhs_opt=Some alhs] if (lhs bop rhs ≠ ∅ => alhs⇔lhs)
+    (and similarly for rhs)
 
-   - likewise if [negated] with (lhs bop rhs = ∅) in the two points above
+    If [negated] then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.
 *)

infer/src/pulse/PulseAttribute.ml

@@ -60,7 +60,7 @@ module Attribute = struct
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 
-  let const_rank = Variants.to_rank (Arithmetic (Arithmetic.EqualTo (Cint IntLit.zero)))
+  let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero))
 
   let pp f attribute =
     let pp_string_if_debug string fmt () =

infer/src/pulse/PulseOperations.ml

@@ -131,12 +131,12 @@ let eval location exp0 astate =
         Closures.record location name (List.rev rev_captured) astate
     | Cast (_, exp') ->
         eval exp' astate
-    | Const c ->
+    | Const (Cint i) ->
         (* TODO: make identical const the same address *)
         let addr = AbstractValue.mk_fresh () in
-        let astate = Memory.add_attribute addr (Arithmetic (Arithmetic.EqualTo c)) astate in
+        let astate = Memory.add_attribute addr (Arithmetic (Arithmetic.equal_to i)) astate in
         Ok (astate, (addr, []))
-    | Sizeof _ | UnOp _ | BinOp _ | Exn _ ->
+    | Const _ | Sizeof _ | UnOp _ | BinOp _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in
   eval exp0 astate
@@ -144,8 +144,8 @@ let eval location exp0 astate =
 
 let eval_arith location exp astate =
   match (exp : Exp.t) with
-  | Const c ->
+  | Const (Cint i) ->
-      Ok (astate, None, Some (Arithmetic.EqualTo c))
+      Ok (astate, None, Some (Arithmetic.equal_to i))
   | exp -> (
       eval location exp astate
       >>| fun (astate, (addr, _)) ->
@@ -167,14 +167,17 @@ let record_abduced addr_opt arith_opt astate =
 
 let rec eval_cond ~negated location exp astate =
   match (exp : Exp.t) with
-  | BinOp (bop, e1, e2) ->
+  | BinOp (bop, e1, e2) -> (
       eval_arith location e1 astate
       >>= fun (astate, addr1, eval1) ->
       eval_arith location e2 astate
       >>| fun (astate, addr2, eval2) ->
-      let result, abduced1, abduced2 = Arithmetic.abduce_binop_is_true ~negated bop eval1 eval2 in
+      match Arithmetic.abduce_binop_is_true ~negated bop eval1 eval2 with
-      let astate = record_abduced addr1 abduced1 astate |> record_abduced addr2 abduced2 in
+      | Unsatisfiable ->
-      (astate, result)
+          (astate, false)
+      | Satisfiable (abduced1, abduced2) ->
+          let astate = record_abduced addr1 abduced1 astate |> record_abduced addr2 abduced2 in
+          (astate, true) )
   | UnOp (LNot, exp', _) ->
       eval_cond ~negated:(not negated) location exp' astate
   | exp ->

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

@@ -15,8 +15,7 @@ void unreachable_eq_then_ne_ok(int* x, int y) {
   }
 }
 
-// pulse only tracks equality for now, not disequality
+void unreachable_ne_then_eq_ok(int* x, int y) {
-void FP_unreachable_ne_then_eq_ok(int* x, int y) {
   if (y != 0) {
     free(x);
   }
@@ -32,6 +31,7 @@ bool equal_explicit(size_t x, size_t y) {
   return false;
 }
 
+// need relational domain to give this a good spec
 bool equal(size_t x, size_t y) {
   return x == y;
 }

infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp

@@ -30,7 +30,7 @@ struct LikeFBString {
   int category_;
   char* buffer_;
   size_t size_;
-  unsigned int refcount;
+  unsigned int* refcount_;
 
   LikeFBString() {}
 
@@ -64,18 +64,20 @@ struct LikeFBString {
   }
 
   void copyLarge(const LikeFBString& src) {
-    refcount++;
     buffer_ = src.buffer_;
     size_ = src.size_;
+    refcount_ = src.refcount_;
+    *refcount_ = *refcount_ + 1;
   }
 
   int category() const { return category_; }
 
-  void incr_ref_count() { refcount++; }
-
   void decr_ref_count() {
-    refcount--;
+    if (*refcount_ <= 0) {
-    if (refcount == 0) {
+      exit(1);
+    }
+    *refcount_ = *refcount_ - 1;
+    if (*refcount_ == 0) {
       free(buffer_);
     }
   }
@@ -89,10 +91,7 @@ void copy_fbstring(LikeFBString& s) {
   LikeFBString t = s;
 }
 
-void FP_pass_to_copy_ok() {
+void pass_to_copy_ok() {
-  // Currently pulse follows impossible control flow and thinks the
-  // underlying buffer of s is freed twice: once per copy. That is
-  // caused by manual ref-counting in the case of large strings.
   LikeFBString s;
   copy_fbstring(s);
 }

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

@@ -6,12 +6,10 @@ codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6
 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, FP_unreachable_ne_then_eq_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,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]
 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]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function<int>` here,parameter `a` of deduplication::templated_delete_function<int>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<int>` here,parameter `a` of deduplication::templated_access_function<int>,invalid access occurs here]
-codetoanalyze/cpp/pulse/fbstring.cpp, FP_pass_to_copy_ok, 6, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `copy_fbstring` here,parameter `s` of copy_fbstring,passed as argument to `LikeFBString::LikeFBString`,parameter `src` of LikeFBString::LikeFBString,passed as argument to `LikeFBString::copyLarge`,parameter `src` of LikeFBString::copyLarge,assigned,return from call to `LikeFBString::copyLarge`,return from call to `LikeFBString::LikeFBString`,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,when calling `LikeFBString::decr_ref_count` here,parameter `this` of LikeFBString::decr_ref_count,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,when calling `LikeFBString::decr_ref_count` here,parameter `this` of LikeFBString::decr_ref_count,invalid access occurs here]
 codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/frontend.cpp, deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `some::thing::bad_ptr` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `some::thing::bad_ptr`,return from call to `some::thing::bad_ptr`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,assigned,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
@@ -52,7 +50,6 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,invalid access occurs here]
-codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_no_free_if_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_no_free_if_ok,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/values.cpp

@@ -48,7 +48,7 @@ void free_if(int* x, int b) {
   }
 }
 
-void FP_no_free_if_ok(int* x) {
+void no_free_if_ok(int* x) {
   free_if(x, 0);
   *x = 42;
 }