[pudge] only ask unsat when reporting

Summary:
Computing sledge's equality relation and normalising terms is costly. We
can avoid doing that most of the time by keeping the sledge path
condition lazily evaluated and only forcing it down to a value at two
critical points in the analysis:
1. Summary creation, to avoid storing unsatisfiable pre/posts that will have
   to be needlessly executed by callers. This also saves us from having
   to serialise the closures involved in the uncomputed form of lazy
   values inside the pulse summaries.
2. Before reporting errors we check in the state is in fact satisfiable.
   If not we just prune it away at that point.

This yields ~4x speedup on some targets.

Reviewed By: ezgicicek

Differential Revision: D21129759

fbshipit-source-id: a75fdd3bc

infer/src/pulse/Pulse.ml

@@ -22,8 +22,10 @@ let check_error_transform summary ~f = function
   | Ok astate ->
       f astate
   | Error (diagnostic, astate) ->
-      report summary diagnostic ;
-      [ExecutionDomain.AbortProgram astate]
+      if PulseArithmetic.is_unsat astate then []
+      else (
+        report summary diagnostic ;
+        [ExecutionDomain.AbortProgram astate] )
 
 
 let check_error_continue summary result =

infer/src/pulse/PulseAbductiveDomain.ml

@@ -93,8 +93,6 @@ let pp f {post; pre; path_condition; skipped_calls} =
     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 =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -154,8 +154,6 @@ 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

infer/src/pulse/PulseArithmetic.ml

@@ -6,19 +6,19 @@
  *)
 
 open! IStd
-module L = Logging
 open PulseBasicInterface
-open PulseDomainInterface
+module AbductiveDomain = PulseAbductiveDomain
+module AddressAttributes = AbductiveDomain.AddressAttributes
 
 (** {2 Building arithmetic constraints} *)
 
 let and_eq_terms t1 t2 astate =
-  let phi = PathCondition.and_eq t1 t2 (AbductiveDomain.get_path_condition astate) in
+  let phi = PathCondition.and_eq t1 t2 astate.AbductiveDomain.path_condition in
   AbductiveDomain.set_path_condition phi astate
 
 
 let and_term t astate =
-  let phi = PathCondition.and_term t (AbductiveDomain.get_path_condition astate) in
+  let phi = PathCondition.and_term t astate.AbductiveDomain.path_condition in
   AbductiveDomain.set_path_condition phi astate
 
 
@@ -197,49 +197,44 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta
   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 astate =
     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
+      PathCondition.and_term t astate.AbductiveDomain.path_condition
     in
-    let astate = AbductiveDomain.set_path_condition path_condition astate in
-    (astate, path_condition)
+    AbductiveDomain.set_path_condition path_condition astate
   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 =
+  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' ->
           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' ->
-            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_rhs_opt bo_itv_rhs bop' bo_itv_lhs astate ) )
 
 
 (** {2 Queries} *)
@@ -247,6 +242,12 @@ 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
+  || (let phi = astate.AbductiveDomain.path_condition in
       PathCondition.is_known_zero (PathCondition.Term.of_absval v) phi )
   || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv v astate)
+
+
+let is_unsat astate =
+  (* note: contradictions are detected eagerly for all domains except path conditions, so just
+     evaluate that one *)
+  PathCondition.is_unsat astate.AbductiveDomain.path_condition

infer/src/pulse/PulseArithmetic.mli

@@ -7,7 +7,7 @@
 
 open! IStd
 open PulseBasicInterface
-open PulseDomainInterface
+module AbductiveDomain = PulseAbductiveDomain
 
 (** {2 Building arithmetic constraints} *)
 
@@ -56,3 +56,6 @@ val prune_binop :
 
 val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool
 (** [is_known_zero astate t] returns [true] if [astate |- t = 0], [false] if we don't know for sure *)
+
+val is_unsat : AbductiveDomain.t -> bool
+(** returns whether the state contains a contradiction *)

infer/src/pulse/PulseExecutionDomain.ml

@@ -9,13 +9,11 @@ open! IStd
 module F = Format
 module AbductiveDomain = PulseAbductiveDomain
 
-type exec_state =
+type t =
   | AbortProgram of AbductiveDomain.t
   | ContinueProgram of AbductiveDomain.t
   | ExitProgram of AbductiveDomain.t
 
-type t = exec_state
-
 let continue astate = ContinueProgram astate
 
 let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
@@ -49,4 +47,8 @@ let map ~f exec_state =
       ExitProgram (f astate)
 
 
-let of_post pdesc = map ~f:(AbductiveDomain.of_post pdesc)
+let of_posts pdesc posts =
+  List.filter_map posts ~f:(fun exec_state ->
+      let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in
+      if PulseArithmetic.is_unsat astate then None
+      else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) )

infer/src/pulse/PulseExecutionDomain.mli

@@ -6,17 +6,17 @@
  *)
 open! IStd
 
-type exec_state =
+type t =
   | AbortProgram of PulseAbductiveDomain.t
       (** represents the state at the program point that caused an error *)
   | ContinueProgram of PulseAbductiveDomain.t  (** represents the state at the program point *)
   | ExitProgram of PulseAbductiveDomain.t
       (** represents the state originating at exit/divergence. *)
 
-include AbstractDomain.NoJoin with type t = exec_state
+include AbstractDomain.NoJoin with type t := t
 
 val continue : PulseAbductiveDomain.t -> t
 
-val of_post : Procdesc.t -> t -> t
+val of_posts : Procdesc.t -> t list -> t list
 
 val mk_initial : Procdesc.t -> t

infer/src/pulse/PulseInterproc.ml

@@ -73,7 +73,6 @@ 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} ->
@@ -95,8 +94,6 @@ 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
@@ -316,10 +313,9 @@ let conjoin_callee_arith pre_post call_state =
   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
+  (* Don't trigger the computation of [path_condition] by asking for satisfiability here. Instead,
+     (un-)satisfiability is computed lazily when we discover issues. *)
+  {call_state with astate; subst}
 
 
 (* shadowed to take config into account *)

infer/src/pulse/PulseOperations.mli

@@ -13,7 +13,7 @@ type t = AbductiveDomain.t
 
 type 'a access_result = ('a, Diagnostic.t * t) result
 
-val ok_continue : t -> (ExecutionDomain.exec_state list, 'a) result
+val ok_continue : t -> (ExecutionDomain.t list, 'a) result
 
 module Closures : sig
   val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t * t) result

infer/src/pulse/PulseSummary.ml

@@ -11,7 +11,7 @@ open PulseDomainInterface
 
 type t = ExecutionDomain.t list
 
-let of_posts pdesc posts = List.map posts ~f:(ExecutionDomain.of_post pdesc)
+let of_posts pdesc posts = ExecutionDomain.of_posts pdesc posts
 
 let pp fmt summary =
   F.open_vbox 0 ;