From 7a888170e71570b5b8eef08574c81a45cd88ec2b Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Fri, 17 Apr 2020 06:12:32 -0700
Subject: [PATCH] [pudge] it's alive!

Summary:
Add a path condition to each symbolic state, represented in sledge's arithmetic domain. This gives a precise account of arithmetic constraints. In particular, it is relation and thus is more robust in the face of inter-procedural analysis.

This is gated behind a flag for now as there are performance issues with the new arithmetic.

Reviewed By: jberdine

Differential Revision: D20393947

fbshipit-source-id: b780de22a
---
 infer/src/base/Config.ml                      |   9 +
 infer/src/base/Config.mli                     |   2 +
 infer/src/pulse/PulseAbductiveDomain.ml       |  40 +++--
 infer/src/pulse/PulseAbductiveDomain.mli      |  11 +-
 infer/src/pulse/PulseAbstractValue.ml         |   2 +
 infer/src/pulse/PulseAbstractValue.mli        |   2 +
 infer/src/pulse/PulseArithmetic.ml            | 137 ++++++++++----
 infer/src/pulse/PulseBasicInterface.ml        |   7 +
 infer/src/pulse/PulseDummyPathCondition.ml    |  57 ++++++
 infer/src/pulse/PulseDummyPathCondition.mli   |  10 ++
 infer/src/pulse/PulseInterproc.ml             |  62 +++++--
 infer/src/pulse/PulseOperations.ml            |   5 +-
 infer/src/pulse/PulsePathCondition.ml         | 167 ++++++++++++++++++
 infer/src/pulse/PulsePathCondition.mli        |  10 ++
 .../src/pulse/PulsePathConditionModuleType.ml |  69 ++++++++
 .../codetoanalyze/cpp/pulse/conditionals.cpp  |   2 +-
 sledge/lib/equality.mli                       |   3 +
 sledge/lib/term.ml                            |   2 +
 sledge/lib/term.mli                           |   8 +
 19 files changed, 530 insertions(+), 75 deletions(-)
 create mode 100644 infer/src/pulse/PulseDummyPathCondition.ml
 create mode 100644 infer/src/pulse/PulseDummyPathCondition.mli
 create mode 100644 infer/src/pulse/PulsePathCondition.ml
 create mode 100644 infer/src/pulse/PulsePathCondition.mli
 create mode 100644 infer/src/pulse/PulsePathConditionModuleType.ml

diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index 51112db27..ccddc3f30 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -1776,6 +1776,13 @@ and pulse_model_free_pattern =
     "Regex of methods that should be modelled as free in Pulse"
 
 
+and pulse_path_conditions =
+  CLOpt.mk_bool ~long:"" ~deprecated:["-pulse-path-conditions"]
+    ~deprecated_no:["-no-pulse-path-conditions"] ~default:false
+    "Experimental flag to enable arithmetic on path conditions. This is intended for Pulse \
+     development only and will be removed once the feature is stable."
+
+
 and pulse_widen_threshold =
   CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3
     "Under-approximate after $(i,int) loop iterations"
@@ -2848,6 +2855,8 @@ and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_patt
 
 and pulse_model_free_pattern = Option.map ~f:Str.regexp !pulse_model_free_pattern
 
+and pulse_path_conditions = !pulse_path_conditions
+
 and pulse_widen_threshold = !pulse_widen_threshold
 
 and pure_by_default = !pure_by_default
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index e4c652bf5..f928f8d71 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -451,6 +451,8 @@ val pulse_model_alloc_pattern : Str.regexp option
 
 val pulse_model_free_pattern : Str.regexp option
 
+val pulse_path_conditions : bool
+
 val pulse_widen_threshold : int
 
 val pure_by_default : bool
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 277975a75..d3fae80d3 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -85,13 +85,18 @@ module PreDomain : BaseDomainSig = PostDomain
 type t =
   { post: PostDomain.t  (** state at the current program point*)
   ; pre: PreDomain.t  (** inferred pre at the current program point *)
-  ; skipped_calls: SkippedCalls.t  (** set of skipped calls *) }
+  ; skipped_calls: SkippedCalls.t  (** set of skipped calls *)
+  ; path_condition: PathCondition.t }
 
-let pp f {post; pre; skipped_calls} =
-  F.fprintf f "@[<v>%a@;PRE=[%a]@;skipped_calls=%a@]" PostDomain.pp post PreDomain.pp pre
-    SkippedCalls.pp skipped_calls
+let pp f {post; pre; path_condition; skipped_calls} =
+  F.fprintf f "@[<v>%a@;%a@;PRE=[%a]@;skipped_calls=%a@]" PathCondition.pp path_condition
+    PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls
 
 
+let get_path_condition {path_condition} = path_condition
+
+let set_path_condition path_condition astate = {astate with path_condition}
+
 let leq ~lhs ~rhs =
   SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls
   &&
@@ -140,7 +145,8 @@ module Stack = struct
         in
         ( { post= PostDomain.update astate.post ~stack:post_stack
           ; pre
-          ; skipped_calls= astate.skipped_calls }
+          ; skipped_calls= astate.skipped_calls
+          ; path_condition= astate.path_condition }
         , addr_hist )
 
 
@@ -274,7 +280,8 @@ module Memory = struct
         in
         ( { post= PostDomain.update astate.post ~heap:post_heap
           ; pre= PreDomain.update astate.pre ~heap:foot_heap
-          ; skipped_calls= astate.skipped_calls }
+          ; skipped_calls= astate.skipped_calls
+          ; path_condition= astate.path_condition }
         , addr_hist_dst )
 
 
@@ -305,8 +312,7 @@ let mk_initial proc_desc =
     PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty
   in
   let post = PostDomain.update ~stack:initial_stack PostDomain.empty in
-  let skipped_calls = SkippedCalls.empty in
-  {pre; post; skipped_calls}
+  {pre; post; skipped_calls= SkippedCalls.empty; path_condition= PathCondition.true_}
 
 
 let add_skipped_call pname trace astate =
@@ -331,16 +337,17 @@ let discard_unreachable ({pre; post} as astate) =
     PreDomain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address pre_addresses) pre
   in
   let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in
-  let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in
+  let live_addresses = AbstractValue.Set.union pre_addresses post_addresses in
   let (heap_new, attrs_new), (_, attrs_unreachable) =
-    PostDomain.partition_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post
+    PostDomain.partition_addr ~f:(fun address -> AbstractValue.Set.mem address live_addresses) post
   in
   let post_new = PostDomain.update ~heap:heap_new ~attrs:attrs_new post in
+  (* note: we don't call {!PulsePathCondition.simplify} *)
   let astate =
     if phys_equal pre_new pre && phys_equal post_new post then astate
     else {astate with pre= pre_new; post= post_new}
   in
-  (astate, attrs_unreachable)
+  (astate, live_addresses, attrs_unreachable)
 
 
 let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var)
@@ -404,13 +411,16 @@ let invalidate_locals pdesc astate : t =
       attrs attrs
   in
   if phys_equal attrs attrs' then astate
-  else {astate with pre= astate.pre; post= PostDomain.update astate.post ~attrs:attrs'}
+  else {astate with post= PostDomain.update astate.post ~attrs:attrs'}
 
 
 let of_post pdesc astate =
-  let domain = filter_for_summary astate in
-  let domain, _ = discard_unreachable domain in
-  invalidate_locals pdesc domain
+  let astate = filter_for_summary astate in
+  let astate, live_addresses, _ = discard_unreachable astate in
+  let astate =
+    {astate with path_condition= PathCondition.simplify ~keep:live_addresses astate.path_condition}
+  in
+  invalidate_locals pdesc astate
 
 
 let get_pre {pre} = (pre :> BaseDomain.t)
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 717b15fa9..9764331d0 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -55,7 +55,8 @@ module PreDomain : BaseDomainSig
 type t = private
   { post: PostDomain.t  (** state at the current program point*)
   ; pre: PreDomain.t  (** inferred pre at the current program point *)
-  ; skipped_calls: SkippedCalls.t  (** set of skipped calls *) }
+  ; skipped_calls: SkippedCalls.t  (** set of skipped calls *)
+  ; path_condition: PathCondition.t  (** arithmetic facts *) }
 
 val leq : lhs:t -> rhs:t -> bool
 
@@ -145,14 +146,18 @@ val is_local : Var.t -> t -> bool
 
 val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option
 
-val discard_unreachable : t -> t * BaseAddressAttributes.t
+val discard_unreachable : t -> t * AbstractValue.Set.t * BaseAddressAttributes.t
 (** [discard_unreachable astate] garbage collects unreachable addresses in the state to make it
-    smaller, and retuns the new state and the attributes of discarded addresses *)
+    smaller, and retuns the new state, the live addresses, and the attributes of discarded addresses *)
 
 val add_skipped_call : Procname.t -> Trace.t -> t -> t
 
 val add_skipped_calls : SkippedCalls.t -> t -> t
 
+val get_path_condition : t -> PathCondition.t
+
+val set_path_condition : PathCondition.t -> t -> t
+
 val of_post : Procdesc.t -> t -> t
 
 val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t
diff --git a/infer/src/pulse/PulseAbstractValue.ml b/infer/src/pulse/PulseAbstractValue.ml
index 56b5d9c78..0f4e474b5 100644
--- a/infer/src/pulse/PulseAbstractValue.ml
+++ b/infer/src/pulse/PulseAbstractValue.ml
@@ -22,6 +22,8 @@ let pp f l = F.fprintf f "v%d" l
 
 let init () = next_fresh := 1
 
+let of_id v = v
+
 type state = int
 
 let get_state () = !next_fresh
diff --git a/infer/src/pulse/PulseAbstractValue.mli b/infer/src/pulse/PulseAbstractValue.mli
index 30a13c3ac..998105a8e 100644
--- a/infer/src/pulse/PulseAbstractValue.mli
+++ b/infer/src/pulse/PulseAbstractValue.mli
@@ -19,6 +19,8 @@ val pp : F.formatter -> t -> unit
 
 val init : unit -> unit
 
+val of_id : int -> t
+
 type state
 
 val get_state : unit -> state
diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml
index 3f9011b0b..eae5376df 100644
--- a/infer/src/pulse/PulseArithmetic.ml
+++ b/infer/src/pulse/PulseArithmetic.ml
@@ -6,32 +6,46 @@
  *)
 
 open! IStd
+module L = Logging
 open PulseBasicInterface
 open PulseDomainInterface
 
 (** {2 Building arithmetic constraints} *)
 
+let and_eq_terms t1 t2 astate =
+  let phi = PathCondition.and_eq t1 t2 (AbductiveDomain.get_path_condition astate) in
+  AbductiveDomain.set_path_condition phi astate
+
+
+let and_term t astate =
+  let phi = PathCondition.and_term t (AbductiveDomain.get_path_condition astate) in
+  AbductiveDomain.set_path_condition phi astate
+
+
 let and_nonnegative trace v astate =
   AddressAttributes.add_one v (BoItv Itv.ItvPure.nat) astate
   |> AddressAttributes.add_one v (CItv (CItv.zero_inf, trace))
+  |> and_term PathCondition.Term.(le zero (of_absval v))
 
 
 let and_positive trace v astate =
   AddressAttributes.add_one v (BoItv Itv.ItvPure.pos) astate
   |> AddressAttributes.add_one v (CItv (CItv.ge_to IntLit.one, trace))
+  |> and_term PathCondition.Term.(lt zero (of_absval v))
 
 
 let and_eq_int trace v i astate =
   AddressAttributes.add_one v (BoItv (Itv.ItvPure.of_int_lit i)) astate
   |> AddressAttributes.add_one v (CItv (CItv.equal_to i, trace))
+  |> and_eq_terms (PathCondition.Term.of_absval v) (PathCondition.Term.of_intlit i)
 
 
 (** {2 Operations} *)
 
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
 
-let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
-  let arith_of_op op astate =
+let eval_citv_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
+  let citv_of_op op astate =
     match op with
     | LiteralOperand i ->
         Some (CItv.equal_to i)
@@ -39,7 +53,7 @@ let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
         AddressAttributes.get_citv v astate |> Option.map ~f:fst
   in
   match
-    Option.both (arith_of_op op_lhs astate) (arith_of_op op_rhs astate)
+    Option.both (citv_of_op op_lhs astate) (citv_of_op op_rhs astate)
     |> Option.bind ~f:(fun (addr_lhs, addr_rhs) -> CItv.binop bop addr_lhs addr_rhs)
   with
   | None ->
@@ -64,16 +78,30 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs astate =
   AddressAttributes.add_one binop_addr (BoItv bo_itv) astate
 
 
+let eval_path_condition_binop binop_addr binop op_lhs op_rhs astate =
+  let term_of_op = function
+    | LiteralOperand i ->
+        PathCondition.Term.of_intlit i
+    | AbstractValueOperand v ->
+        PathCondition.Term.of_absval v
+  in
+  and_eq_terms
+    (PathCondition.Term.of_absval binop_addr)
+    (PathCondition.Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs))
+    astate
+
+
 let eval_binop location binop op_lhs op_rhs binop_hist astate =
   let binop_addr = AbstractValue.mk_fresh () in
   let astate =
-    eval_arith_operand location binop_addr binop_hist binop op_lhs op_rhs astate
+    eval_path_condition_binop binop_addr binop op_lhs op_rhs astate
+    |> eval_citv_operand location binop_addr binop_hist binop op_lhs op_rhs
     |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs
   in
   (astate, (binop_addr, binop_hist))
 
 
-let eval_unop_arith location unop_addr unop operand_addr unop_hist astate =
+let eval_unop_citv location unop_addr unop operand_addr unop_hist astate =
   match
     AddressAttributes.get_citv operand_addr astate
     |> Option.bind ~f:(function a, _ -> CItv.unop unop a)
@@ -93,10 +121,18 @@ let eval_unop_bo_itv unop_addr unop operand_addr astate =
       AddressAttributes.add_one unop_addr (BoItv itv) astate
 
 
+let eval_path_condition_unop unop_addr unop addr astate =
+  and_eq_terms
+    (PathCondition.Term.of_absval unop_addr)
+    PathCondition.Term.(of_unop unop (of_absval addr))
+    astate
+
+
 let eval_unop location unop addr unop_hist astate =
   let unop_addr = AbstractValue.mk_fresh () in
   let astate =
-    eval_unop_arith location unop_addr unop addr unop_hist astate
+    eval_path_condition_unop unop_addr unop addr astate
+    |> eval_unop_citv location unop_addr unop addr unop_hist
     |> eval_unop_bo_itv unop_addr unop addr
   in
   (astate, (unop_addr, unop_hist))
@@ -126,9 +162,13 @@ let eval_operand location astate = function
       ( None
       , Some
           (CItv.equal_to i, Trace.Immediate {location; history= [ValueHistory.Assignment location]})
-      , Itv.ItvPure.of_int_lit i )
+      , Itv.ItvPure.of_int_lit i
+      , PathCondition.Term.of_intlit i )
   | AbstractValueOperand v ->
-      (Some v, AddressAttributes.get_citv v astate, AddressAttributes.get_bo_itv v astate)
+      ( Some v
+      , AddressAttributes.get_citv v astate
+      , AddressAttributes.get_bo_itv v astate
+      , PathCondition.Term.of_absval v )
 
 
 let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate =
@@ -151,38 +191,55 @@ let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate
 let bind_satisfiable ~satisfiable astate ~f = if satisfiable then f astate else (astate, false)
 
 let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op astate =
-  let value_lhs_opt, arith_lhs_opt, bo_itv_lhs = eval_operand location astate lhs_op in
-  let value_rhs_opt, arith_rhs_opt, bo_itv_rhs = eval_operand location astate rhs_op in
-  match
-    CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
-      (Option.map ~f:fst arith_rhs_opt)
-  with
-  | Unsatisfiable ->
-      (astate, false)
-  | Satisfiable (abduced_lhs, abduced_rhs) ->
-      let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in
-      let astate =
-        record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate
-        |> record_abduced event location value_rhs_opt arith_rhs_opt abduced_rhs
-      in
-      let satisfiable =
-        match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with
-        | False ->
-            negated
-        | True ->
-            not negated
-        | Top ->
-            true
-        | Bottom ->
-            false
-      in
-      let astate, satisfiable =
-        bind_satisfiable ~satisfiable astate ~f:(fun astate ->
-            prune_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs astate )
-      in
-      Option.value_map (Binop.symmetric bop) ~default:(astate, satisfiable) ~f:(fun bop' ->
+  let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs =
+    eval_operand location astate lhs_op
+  in
+  let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs =
+    eval_operand location astate rhs_op
+  in
+  let astate, path_condition =
+    let path_condition =
+      let t_positive = PathCondition.Term.of_binop bop path_cond_lhs path_cond_rhs in
+      let t = if negated then PathCondition.Term.not_ t_positive else t_positive in
+      AbductiveDomain.get_path_condition astate |> PathCondition.and_term t
+    in
+    let astate = AbductiveDomain.set_path_condition path_condition astate in
+    (astate, path_condition)
+  in
+  if PathCondition.is_unsat path_condition then (
+    L.d_printfln "Contradiction detected in path condition" ;
+    (astate, false) )
+  else
+    match
+      CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
+        (Option.map ~f:fst arith_rhs_opt)
+    with
+    | Unsatisfiable ->
+        (astate, false)
+    | Satisfiable (abduced_lhs, abduced_rhs) ->
+        let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in
+        let astate =
+          record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate
+          |> record_abduced event location value_rhs_opt arith_rhs_opt abduced_rhs
+        in
+        let satisfiable =
+          match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with
+          | False ->
+              negated
+          | True ->
+              not negated
+          | Top ->
+              true
+          | Bottom ->
+              false
+        in
+        let astate, satisfiable =
           bind_satisfiable ~satisfiable astate ~f:(fun astate ->
-              prune_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs astate ) )
+              prune_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs astate )
+        in
+        Option.value_map (Binop.symmetric bop) ~default:(astate, satisfiable) ~f:(fun bop' ->
+            bind_satisfiable ~satisfiable astate ~f:(fun astate ->
+                prune_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs astate ) )
 
 
 (** {2 Queries} *)
@@ -190,4 +247,6 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta
 let is_known_zero astate v =
   ( AddressAttributes.get_citv v astate
   |> function Some (arith, _) -> CItv.is_equal_to_zero arith | None -> false )
+  || (let phi = AbductiveDomain.get_path_condition astate in
+      PathCondition.is_known_zero (PathCondition.Term.of_absval v) phi )
   || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv v astate)
diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml
index 1b1ac402d..c93291a26 100644
--- a/infer/src/pulse/PulseBasicInterface.ml
+++ b/infer/src/pulse/PulseBasicInterface.ml
@@ -15,6 +15,11 @@ module CallEvent = PulseCallEvent
 module CItv = PulseCItv
 module Diagnostic = PulseDiagnostic
 module Invalidation = PulseInvalidation
+
+module PathCondition = ( val if Config.pulse_path_conditions then (module PulsePathCondition)
+                             else (module PulseDummyPathCondition) : PulsePathConditionModuleType.S
+                       )
+
 module SkippedCalls = PulseSkippedCalls
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
@@ -32,6 +37,8 @@ include struct
   module PulseDiagnostic = PulseDiagnostic [@@deprecated "use the short form Diagnostic instead"]
   module PulseInvalidation = PulseInvalidation
   [@@deprecated "use the short form Invalidation instead"]
+  module PulsePathCondition = PulsePathCondition
+  [@@deprecated "use the short form PathCondition instead"]
   module PulseSkippedCalls = PulseSkippedCalls
   [@@deprecated "use the short form SkippedCalls instead"]
   module PulseTrace = PulseTrace [@@deprecated "use the short form Trace instead"]
diff --git a/infer/src/pulse/PulseDummyPathCondition.ml b/infer/src/pulse/PulseDummyPathCondition.ml
new file mode 100644
index 000000000..d7cd82a27
--- /dev/null
+++ b/infer/src/pulse/PulseDummyPathCondition.ml
@@ -0,0 +1,57 @@
+(*
+ * 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 Var = struct
+  type t = unit
+
+  let of_absval _ = ()
+
+  let to_absval () = assert false
+end
+
+module Term = struct
+  type t = unit
+
+  let zero = ()
+
+  let le () () = ()
+
+  let lt () () = ()
+
+  let not_ () = ()
+
+  let of_intlit _ = ()
+
+  let of_absval _ = ()
+
+  let of_unop _ () = ()
+
+  let of_binop _ () () = ()
+end
+
+(* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
+type t = {eqs: Sledge.Equality.t; non_eqs: Sledge.Term.t}
+
+let pp _ _ = ()
+
+let true_ = {eqs= Sledge.Equality.true_; non_eqs= Sledge.Term.true_}
+
+let and_eq () () phi = phi
+
+let and_term () phi = phi
+
+let and_ phi1 _ = phi1
+
+let is_known_zero () _ = false
+
+let is_unsat _ = false
+
+let fold_map_variables phi ~init ~f:_ = (init, phi)
+
+let simplify ~keep:_ phi = phi
diff --git a/infer/src/pulse/PulseDummyPathCondition.mli b/infer/src/pulse/PulseDummyPathCondition.mli
new file mode 100644
index 000000000..8e460e1ac
--- /dev/null
+++ b/infer/src/pulse/PulseDummyPathCondition.mli
@@ -0,0 +1,10 @@
+(*
+ * 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
+
+include PulsePathConditionModuleType.S
diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml
index 8da90694c..e26723f98 100644
--- a/infer/src/pulse/PulseInterproc.ml
+++ b/infer/src/pulse/PulseInterproc.ml
@@ -73,6 +73,7 @@ type contradiction =
           state *)
   | FormalActualLength of
       {formals: Var.t list; actuals: ((AbstractValue.t * ValueHistory.t) * Typ.t) list}
+  | UnsatPathCondition of call_state
 
 let pp_contradiction fmt = function
   | Aliasing {addr_caller; addr_callee; addr_callee'; call_state} ->
@@ -94,6 +95,8 @@ let pp_contradiction fmt = function
   | FormalActualLength {formals; actuals} ->
       F.fprintf fmt "formals have length %d but actuals have length %d" (List.length formals)
         (List.length actuals)
+  | UnsatPathCondition call_state ->
+      F.fprintf fmt "UNSAT %a" pp_call_state call_state
 
 
 exception Contradiction of contradiction
@@ -131,7 +134,8 @@ let visit call_state ~addr_callee ~addr_hist_caller =
       ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } )
 
 
-let pp f {AbductiveDomain.pre; post; skipped_calls} =
+let pp f {AbductiveDomain.pre; post; path_condition; skipped_calls} =
+  F.fprintf f "COND:@\n  @[%a@]@\n" PathCondition.pp path_condition ;
   F.fprintf f "PRE:@\n  @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ;
   F.fprintf f "POST:@\n  @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) ;
   F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls
@@ -287,6 +291,42 @@ let add_call_to_attributes proc_name call_location ~addr_callee ~addr_caller cal
   (!subst_ref, attrs)
 
 
+let subst_find_or_new subst addr_callee ~default_hist_caller =
+  match AddressMap.find_opt addr_callee subst with
+  | None ->
+      let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in
+      (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh)
+  | Some addr_hist_caller ->
+      (subst, addr_hist_caller)
+
+
+let conjoin_callee_arith pre_post call_state =
+  L.d_printfln "applying callee path condition: %a[%a]" PathCondition.pp
+    pre_post.AbductiveDomain.path_condition
+    (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr))
+    call_state.subst ;
+  let subst, callee_path_cond =
+    (* need to translate callee variables to make sense for the caller, thereby possibly extending
+       the current substitution *)
+    PathCondition.fold_map_variables pre_post.AbductiveDomain.path_condition ~init:call_state.subst
+      ~f:(fun subst v_callee_arith ->
+        let v_callee = PathCondition.Var.to_absval v_callee_arith in
+        let subst', (v_caller, _) = subst_find_or_new subst v_callee ~default_hist_caller:[] in
+        (subst', PathCondition.Var.of_absval v_caller) )
+  in
+  let path_condition = PathCondition.and_ call_state.astate.path_condition callee_path_cond in
+  let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in
+  let call_state = {call_state with astate; subst} in
+  if PathCondition.is_unsat path_condition then
+    raise (Contradiction (UnsatPathCondition call_state))
+  else call_state
+
+
+(* shadowed to take config into account *)
+let conjoin_callee_arith pre_post call_state =
+  if Config.pulse_path_conditions then conjoin_callee_arith pre_post call_state else call_state
+
+
 let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state =
   let one_address_sat addr_callee callee_attrs (addr_caller, caller_history) call_state =
     let subst, attrs_caller =
@@ -297,6 +337,7 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st
     if phys_equal subst call_state.subst && phys_equal astate call_state.astate then call_state
     else {call_state with subst; astate}
   in
+  let call_state = conjoin_callee_arith pre_post call_state in
   (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *)
   AddressMap.fold
     (fun addr_callee addr_hist_caller call_state ->
@@ -329,15 +370,6 @@ let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals ca
 
 (* {3 applying the post to the current state} *)
 
-let subst_find_or_new subst addr_callee ~default_hist_caller =
-  match AddressMap.find_opt addr_callee subst with
-  | None ->
-      let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in
-      (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh)
-  | Some addr_hist_caller ->
-      (subst, addr_hist_caller)
-
-
 let call_state_subst_find_or_new call_state addr_callee ~default_hist_caller =
   let new_subst, addr_hist_caller =
     subst_find_or_new call_state.subst addr_callee ~default_hist_caller
@@ -473,6 +505,8 @@ let record_post_for_return callee_proc_name call_loc pre_post call_state =
               ( AbstractValue.mk_fresh ()
               , [ (* this could maybe include an event like "returned here" *) ] )
         in
+        L.d_printfln_escaped "Recording POST from [return] <-> %a" AbstractValue.pp
+          (fst return_caller_addr_hist) ;
         let call_state =
           record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee
             ~addr_hist_caller:return_caller_addr_hist call_state
@@ -547,10 +581,10 @@ let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_st
     |> apply_post_for_globals callee_proc_name call_location pre_post
     |> record_post_for_return callee_proc_name call_location pre_post
     |> fun (call_state, return_caller) ->
-    ( record_post_remaining_attributes callee_proc_name call_location pre_post call_state
-      |> record_skipped_calls callee_proc_name call_location pre_post
-    , return_caller )
-    |> fun ({astate; _}, return_caller) -> (astate, return_caller)
+    record_post_remaining_attributes callee_proc_name call_location pre_post call_state
+    |> record_skipped_calls callee_proc_name call_location pre_post
+    |> conjoin_callee_arith pre_post
+    |> fun {astate; _} -> (astate, return_caller)
   in
   PerfEvent.(log (fun logger -> log_end_event logger ())) ;
   r
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index b373e9c34..b1282e879 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -181,8 +181,7 @@ let prune ~is_then_branch if_kind location ~condition astate =
     | UnOp (LNot, exp', _) ->
         prune_aux ~negated:(not negated) exp' astate
     | exp ->
-        let zero = Exp.Const (Cint IntLit.zero) in
-        prune_aux ~negated (Exp.BinOp (Ne, exp, zero)) astate
+        prune_aux ~negated (Exp.BinOp (Ne, exp, Exp.zero)) astate
   in
   prune_aux ~negated:false condition astate
 
@@ -363,7 +362,7 @@ let remove_vars vars location astate =
   let astate' = Stack.remove_vars vars astate in
   if phys_equal astate' astate then Ok astate
   else
-    let astate, unreachable_attrs = AbductiveDomain.discard_unreachable astate' in
+    let astate, _, unreachable_attrs = AbductiveDomain.discard_unreachable astate' in
     let+ () = check_memory_leak_unreachable unreachable_attrs location astate in
     astate
 
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
new file mode 100644
index 000000000..ae3ce980a
--- /dev/null
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -0,0 +1,167 @@
+(*
+ * 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
+
+[@@@warning "+9"]
+
+module Var = struct
+  module Var = Sledge.Var
+
+  let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
+
+  let to_absval v =
+    assert (String.equal (Var.name v) "v") ;
+    Var.id v |> AbstractValue.of_id
+
+
+  include Var
+end
+
+module Term = struct
+  module Term = Sledge.Term
+
+  let of_intlit i = Term.integer (IntLit.to_big_int i)
+
+  let of_absval v = Term.var (Var.of_absval v)
+
+  let of_unop (unop : Unop.t) t = match unop with Neg -> Term.neg t | BNot | LNot -> Term.not_ t
+
+  let of_binop (binop : Binop.t) t1 t2 =
+    let open Term in
+    match binop with
+    | PlusA _ | PlusPI ->
+        add t1 t2
+    | MinusA _ | MinusPI | MinusPP ->
+        sub t1 t2
+    | Mult _ ->
+        mul t1 t2
+    | Div ->
+        div t1 t2
+    | Mod ->
+        rem t1 t2
+    | Shiftlt ->
+        shl t1 t2
+    | Shiftrt ->
+        lshr t1 t2
+    | Lt ->
+        lt t1 t2
+    | Gt ->
+        lt t2 t1
+    | Le ->
+        le t1 t2
+    | Ge ->
+        le t2 t1
+    | Eq ->
+        eq t1 t2
+    | Ne ->
+        dq t1 t2
+    | BAnd | LAnd ->
+        and_ t1 t2
+    | BOr | LOr ->
+        or_ t1 t2
+    | BXor ->
+        xor t1 t2
+
+
+  include Term
+end
+
+module Equality = struct
+  include Sledge.Equality
+
+  let assert_no_new_vars api new_vars =
+    if not (Var.Set.is_empty new_vars) then
+      L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars
+
+
+  let and_eq t1 t2 r =
+    let new_vars, r' = Sledge.Equality.and_eq Var.Set.empty t1 t2 r in
+    assert_no_new_vars "Equality.and_eq" new_vars ;
+    r'
+
+
+  let and_term t r =
+    let new_vars, r' = Sledge.Equality.and_term Var.Set.empty t r in
+    assert_no_new_vars "Equality.and_term" new_vars ;
+    r'
+
+
+  let and_ r1 r2 =
+    let new_vars, r' = Sledge.Equality.and_ Var.Set.empty r1 r2 in
+    assert_no_new_vars "Equality.and_" new_vars ;
+    r'
+
+
+  let apply_subst subst r =
+    let new_vars, r' = Sledge.Equality.apply_subst Var.Set.empty subst r in
+    assert_no_new_vars "Equality.and_" new_vars ;
+    r'
+end
+
+(** We distinguish between what the equality relation of sledge can express and the "non-equalities"
+    terms that this relation ignores. We keep the latter around for completeness: we can still
+    substitute known equalities into these and sometimes get contradictions back. *)
+type t = {eqs: Equality.t; non_eqs: Term.t}
+
+let pp fmt {eqs; non_eqs} = F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs
+
+let true_ = {eqs= Equality.true_; non_eqs= Term.true_}
+
+let and_eq t1 t2 phi = {phi with eqs= Equality.and_eq t1 t2 phi.eqs}
+
+let and_term (t : Term.t) phi =
+  (* add the term to the relation *)
+  let eqs = Equality.and_term t phi.eqs in
+  (* [t] normalizes to [true_] so [non_eqs] never changes, do this regardless for now *)
+  let non_eqs = Term.and_ phi.non_eqs (Equality.normalize eqs t) in
+  {eqs; non_eqs}
+
+
+let and_ phi1 phi2 =
+  {eqs= Equality.and_ phi1.eqs phi2.eqs; non_eqs= Term.and_ phi1.non_eqs phi2.non_eqs}
+
+
+let is_known_zero t phi = Equality.entails_eq phi.eqs t Term.zero
+
+(* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *)
+let is_unsat {eqs; non_eqs} = Equality.is_false eqs || Term.is_false non_eqs
+
+let fv {eqs; non_eqs} = Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs)
+
+let fold_map_variables phi ~init ~f =
+  let term_fold_map t ~init ~f =
+    Term.fold_map_rec_pre t ~init ~f:(fun acc t ->
+        Var.of_term t
+        |> Option.map ~f:(fun v ->
+               let acc', v' = f acc v in
+               (acc', Term.var v') ) )
+  in
+  let acc, eqs' =
+    Equality.classes phi.eqs
+    |> Term.Map.fold ~init:(init, Equality.true_) ~f:(fun ~key:t ~data:equal_ts (acc, eqs') ->
+           let acc, t' = term_fold_map ~init:acc ~f t in
+           List.fold equal_ts ~init:(acc, eqs') ~f:(fun (acc, eqs') equal_t ->
+               let acc, t_mapped = term_fold_map ~init:acc ~f equal_t in
+               (acc, Equality.and_eq t' t_mapped eqs') ) )
+  in
+  let acc, non_eqs' = term_fold_map ~init:acc ~f phi.non_eqs in
+  (acc, {eqs= eqs'; non_eqs= non_eqs'})
+
+
+let simplify ~keep phi =
+  let all_vs = fv phi in
+  let keep_vs =
+    AbstractValue.Set.fold
+      (fun v keep_vs -> Term.Var.Set.add keep_vs (Var.of_absval v))
+      keep Term.Var.Set.empty
+  in
+  let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] phi.eqs in
+  {phi with eqs= Equality.apply_subst simpl_subst phi.eqs}
diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli
new file mode 100644
index 000000000..8e460e1ac
--- /dev/null
+++ b/infer/src/pulse/PulsePathCondition.mli
@@ -0,0 +1,10 @@
+(*
+ * 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
+
+include PulsePathConditionModuleType.S
diff --git a/infer/src/pulse/PulsePathConditionModuleType.ml b/infer/src/pulse/PulsePathConditionModuleType.ml
new file mode 100644
index 000000000..60aba4b24
--- /dev/null
+++ b/infer/src/pulse/PulsePathConditionModuleType.ml
@@ -0,0 +1,69 @@
+(*
+ * 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
+
+module type S = sig
+  type t
+
+  val pp : F.formatter -> t -> unit
+
+  val true_ : t
+
+  module Term : sig
+    type t
+
+    val zero : t
+
+    val le : t -> t -> t
+
+    val lt : t -> t -> t
+
+    val not_ : t -> t
+
+    val of_intlit : IntLit.t -> t
+
+    val of_absval : AbstractValue.t -> t
+
+    val of_unop : Unop.t -> t -> t
+
+    val of_binop : Binop.t -> t -> t -> t
+  end
+
+  module Var : sig
+    type t
+
+    val of_absval : AbstractValue.t -> t
+
+    val to_absval : t -> AbstractValue.t
+    (** use with caution: will crash the program if the given variable wasn't generated from an
+        [AbstractValue.t] using [Var.of_absval] *)
+  end
+
+  val and_eq : Term.t -> Term.t -> t -> t
+
+  val and_term : Term.t -> t -> t
+
+  val and_ : t -> t -> t
+
+  (** queries *)
+
+  val is_unsat : t -> bool
+
+  val is_known_zero : Term.t -> t -> bool
+  (** [is_known_zero phi t] returns [true] if [phi |- t = 0], [false] if we don't know for sure *)
+
+  (** operations *)
+
+  val fold_map_variables : t -> init:'a -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
+
+  val simplify : keep:AbstractValue.Set.t -> t -> t
+  (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
+      possible *)
+end
diff --git a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp
index 12ebc52fc..24fa95d6d 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp
+++ b/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 FP_unreachable_interproc_compare_ok(int* x, size_t y) {
   if (equal(y, 0)) {
     free(x);
   }
diff --git a/sledge/lib/equality.mli b/sledge/lib/equality.mli
index 1cea046a3..8bbb0b806 100644
--- a/sledge/lib/equality.mli
+++ b/sledge/lib/equality.mli
@@ -74,6 +74,9 @@ val difference : t -> Term.t -> Term.t -> Z.t option
 
 val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
 
+val classes : t -> Term.t list Term.Map.t
+(** The equalities that make up the relation. *)
+
 (** Solution Substitutions *)
 module Subst : sig
   type t [@@deriving compare, equal, sexp]
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 3317a2223..54541a8bf 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -381,6 +381,8 @@ module Var = struct
     let x' = Var {name; id= max + 1} in
     (x', Set.add wrt x')
 
+  let identified ~name ~id = Var {name; id}
+
   (** Variable renaming substitutions *)
   module Subst = struct
     type t = T.t Map.t [@@deriving compare, equal, sexp_of]
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index 2d131c414..253067d48 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -131,12 +131,20 @@ module Var : sig
   include Invariant.S with type t := t
 
   val name : t -> string
+  val id : t -> int
   val is_global : t -> bool
   val of_ : term -> t
   val of_term : term -> t option
   val program : ?global:unit -> string -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
+  val identified : name:string -> id:int -> t
+  (** Variable with the given [id]. Variables are compared by [id] alone,
+      [name] is used only for printing. The only way to ensure [identified]
+      variables do not clash with [fresh] variables is to pass the
+      [identified] variables to [fresh] in [wrt]:
+      [Var.fresh name ~wrt:(Var.Set.of_ (Var.identified ~name ~id))]. *)
+
   module Subst : sig
     type var := t
     type t [@@deriving compare, equal, sexp]