[pulse] refactor incorporate_new_eqs

Summary:
Pretty minor, it's more convenient to make it return the state and will
be used in a later diff when that function will actually sometimes
modify the state.

Reviewed By: skcho

Differential Revision: D26488376

fbshipit-source-id: a21eaf008

infer/src/pulse/PulseAbductiveDomain.ml

@@ -687,21 +687,23 @@ let is_allocated {post; pre} v =
 
 
 let incorporate_new_eqs astate new_eqs =
-  List.fold_until new_eqs ~init:()
-    ~finish:(fun () -> Sat ())
-    ~f:(fun () (new_eq : PulseFormula.new_eq) ->
+  List.fold_until new_eqs ~init:astate
+    ~finish:(fun astate -> Sat astate)
+    ~f:(fun astate (new_eq : PulseFormula.new_eq) ->
       match new_eq with
       | EqZero v when is_allocated astate v ->
           L.d_printfln "CONTRADICTION: %a = 0 but is allocated" AbstractValue.pp v ;
           Stop Unsat
-      | Equal (v1, v2)
-        when (not (AbstractValue.equal v1 v2)) && is_allocated astate v1 && is_allocated astate v2
-        ->
-          L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp
-            v1 AbstractValue.pp v2 ;
-          Stop Unsat
+      | Equal (v1, v2) when AbstractValue.equal v1 v2 ->
+          Continue astate
+      | Equal (v1, v2) ->
+          if is_allocated astate v1 && is_allocated astate v2 then (
+            L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp
+              v1 AbstractValue.pp v2 ;
+            Stop Unsat )
+          else Continue astate
       | _ ->
-          Continue () )
+          Continue astate )
 
 
 (** it's a good idea to normalize the path condition before calling this function *)
@@ -744,7 +746,7 @@ let summary_of_post pdesc astate =
   if is_unsat then Unsat
   else
     let astate = {astate with path_condition} in
-    let* () = incorporate_new_eqs astate new_eqs in
+    let* astate = incorporate_new_eqs astate new_eqs in
     L.d_printfln "Canonicalizing...@\n" ;
     let* astate = canonicalize astate in
     L.d_printfln "Canonicalized state: %a@\n" pp astate ;
@@ -756,7 +758,7 @@ let summary_of_post pdesc astate =
     let* path_condition, new_eqs =
       PathCondition.simplify ~keep:live_addresses astate.path_condition
     in
-    let+ () = incorporate_new_eqs astate new_eqs in
+    let+ astate = incorporate_new_eqs astate new_eqs in
     let astate =
       {astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl}
     in
@@ -768,9 +770,14 @@ let get_pre {pre} = (pre :> BaseDomain.t)
 let get_post {post} = (post :> BaseDomain.t)
 
 (* re-exported for mli *)
-let incorporate_new_eqs astate (phi, new_eqs) =
-  if PathCondition.is_unsat_cheap phi then phi
-  else match incorporate_new_eqs astate new_eqs with Unsat -> PathCondition.false_ | Sat () -> phi
+let incorporate_new_eqs new_eqs astate =
+  if PathCondition.is_unsat_cheap astate.path_condition then astate
+  else
+    match incorporate_new_eqs astate new_eqs with
+    | Unsat ->
+        {astate with path_condition= PathCondition.false_}
+    | Sat astate ->
+        astate
 
 
 module Topl = struct

infer/src/pulse/PulseAbductiveDomain.mli

@@ -202,7 +202,7 @@ val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t
 val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t
 (** directly set the edges and attributes for the given address, bypassing abduction altogether *)
 
-val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCondition.t
+val incorporate_new_eqs : PathCondition.new_eqs -> t -> t
 (** Check that the new equalities discovered are compatible with the current pre and post heaps,
     e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x]
     and [y] being allocated separately. In those cases, the resulting path condition is

infer/src/pulse/PulseArithmetic.ml

@@ -10,9 +10,8 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 
 let map_path_condition ~f astate =
-  AbductiveDomain.set_path_condition
-    (f astate.AbductiveDomain.path_condition |> AbductiveDomain.incorporate_new_eqs astate)
-    astate
+  let phi, new_eqs = f astate.AbductiveDomain.path_condition in
+  AbductiveDomain.set_path_condition phi astate |> AbductiveDomain.incorporate_new_eqs new_eqs
 
 
 let and_nonnegative v astate =
@@ -41,11 +40,8 @@ let eval_unop unop_addr unop addr astate =
 
 
 let prune_binop ~negated bop lhs_op rhs_op astate =
-  let phi' =
-    PathCondition.prune_binop ~negated bop lhs_op rhs_op astate.AbductiveDomain.path_condition
-    |> AbductiveDomain.incorporate_new_eqs astate
-  in
-  AbductiveDomain.set_path_condition phi' astate
+  map_path_condition astate ~f:(fun phi ->
+      PathCondition.prune_binop ~negated bop lhs_op rhs_op phi )
 
 
 let prune_eq_zero v astate =

infer/src/pulse/PulseInterproc.ml

@@ -270,13 +270,10 @@ let conjoin_callee_arith pre_post call_state =
     PathCondition.and_callee call_state.subst call_state.astate.path_condition
       ~callee:pre_post.AbductiveDomain.path_condition
   in
-  let path_condition =
-    AbductiveDomain.incorporate_new_eqs call_state.astate (path_condition, new_eqs)
-  in
-  if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition)
-  else
-    let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in
-    {call_state with astate; subst}
+  let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in
+  let astate = AbductiveDomain.incorporate_new_eqs new_eqs astate in
+  if PathCondition.is_unsat_cheap astate.path_condition then raise (Contradiction PathCondition)
+  else {call_state with astate; subst}
 
 
 let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state =