[pulse] make sure we checked satisfiability on summaries

Summary:
Made `AbductiveDomain.summary_of_post` return a Sat/Unsat to make sure
callers filter unsat summaries. Also made `ExitProgram` take a summary
instead of a non-normalized abstract state, which was wrong (mostly
could litter the disjuncts with infeasible paths).

Reviewed By: skcho

Differential Revision: D25277565

fbshipit-source-id: 72dacb944

infer/src/checkers/impurity.ml

@@ -158,7 +158,7 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur
   let astate, exited =
     match exec_state with
     | ExitProgram astate ->
-        (astate, true)
+        ((astate :> AbductiveDomain.t), true)
     | ContinueProgram astate ->
         (astate, false)
     | AbortProgram astate | LatentAbortProgram {astate} ->

infer/src/pulse/PulseAbductiveDomain.ml

@@ -456,31 +456,34 @@ let is_allocated {post; pre} v =
   || is_stack_allocated (post :> BaseDomain.t) v
 
 
-let incorporate_new_eqs astate (phi, new_eqs) =
+let incorporate_new_eqs astate new_eqs =
-  List.fold_until new_eqs ~init:phi ~finish:Fn.id ~f:(fun phi (new_eq : PulseFormula.new_eq) ->
+  List.fold_until new_eqs ~init:()
+    ~finish:(fun () -> Sat ())
+    ~f:(fun () (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 PathCondition.false_
+          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 PathCondition.false_
+          Stop Unsat
       | _ ->
-          Continue phi )
+          Continue () )
 
 
 let summary_of_post pdesc astate =
+  let open SatUnsat.Import in
   let astate = filter_for_summary astate in
   let astate, live_addresses, _ = discard_unreachable astate in
-  let astate =
+  let* path_condition, new_eqs =
-    { astate with
-      path_condition=
     PathCondition.simplify ~keep:live_addresses astate.path_condition
-        |> incorporate_new_eqs astate
+  in
-    ; topl= PulseTopl.simplify ~keep:live_addresses astate.topl }
+  let+ () = incorporate_new_eqs astate new_eqs in
+  let astate =
+    {astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl}
   in
   invalidate_locals pdesc astate
 
@@ -489,6 +492,12 @@ 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
+
+
 module Topl = struct
   let small_step loc event astate =
     {astate with topl= PulseTopl.small_step loc astate.path_condition event astate.topl}

infer/src/pulse/PulseAbductiveDomain.mli

@@ -164,7 +164,7 @@ val set_path_condition : PathCondition.t -> t -> t
 (** private type to make sure {!summary_of_post} is always called when creating summaries *)
 type summary = private t [@@deriving yojson_of]
 
-val summary_of_post : Procdesc.t -> t -> summary
+val summary_of_post : Procdesc.t -> t -> summary SatUnsat.t
 (** trim the state down to just the procedure's interface (formals and globals), and simplify and
     normalize the state *)
 

infer/src/pulse/PulseArithmetic.ml

@@ -52,13 +52,5 @@ let is_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain.
 
 let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition
 
-let is_unsat_expensive astate =
-  let phi', is_unsat, new_eqs =
-    PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition
-  in
-  let phi' = AbductiveDomain.incorporate_new_eqs astate (phi', new_eqs) in
-  (AbductiveDomain.set_path_condition phi' astate, is_unsat)
-
-
 let has_no_assumptions astate =
   PathCondition.has_no_assumptions astate.AbductiveDomain.path_condition

infer/src/pulse/PulseArithmetic.mli

@@ -34,6 +34,4 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool
 
 val is_unsat_cheap : AbductiveDomain.t -> bool
 
-val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool
-
 val has_no_assumptions : AbductiveDomain.t -> bool

infer/src/pulse/PulseExecutionDomain.ml

@@ -18,7 +18,7 @@ module LatentIssue = PulseLatentIssue
    normalized them and don't need to normalize them again. *)
 type 'abductive_domain_t base_t =
   | ContinueProgram of 'abductive_domain_t
-  | ExitProgram of 'abductive_domain_t
+  | ExitProgram of AbductiveDomain.summary
   | AbortProgram of AbductiveDomain.summary
   | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
 [@@deriving yojson_of]
@@ -31,10 +31,10 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
 
 let leq ~lhs ~rhs =
   match (lhs, rhs) with
-  | AbortProgram astate1, AbortProgram astate2 ->
+  | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 ->
-      AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
-  | ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram astate2 ->
       AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
+  | ContinueProgram astate1, ContinueProgram astate2 ->
+      AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
   | ( LatentAbortProgram {astate= astate1; latent_issue= issue1}
     , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) ->
       LatentIssue.equal issue1 issue2
@@ -59,34 +59,22 @@ let pp fmt = function
         (astate :> AbductiveDomain.t)
 
 
-let map ~f exec_state =
-  match exec_state with
-  | ContinueProgram astate ->
-      ContinueProgram (f astate)
-  | ExitProgram astate ->
-      ExitProgram (f astate)
-  | AbortProgram astate ->
-      AbortProgram astate
-  | LatentAbortProgram {astate; latent_issue} ->
-      LatentAbortProgram {astate; latent_issue}
-
-
 type summary = AbductiveDomain.summary base_t [@@deriving yojson_of]
 
 let summary_of_posts pdesc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
-      let astate =
-        match exec_state with
-        | AbortProgram astate | LatentAbortProgram {astate} ->
-            (astate :> AbductiveDomain.t)
-        | ContinueProgram astate | ExitProgram astate ->
-            astate
-      in
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
-      let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
+      match exec_state with
-      if is_unsat then None
+      | ContinueProgram astate -> (
-      else
+        match AbductiveDomain.summary_of_post pdesc astate with
-        Some
+        | Unsat ->
-          (map exec_state ~f:(fun _astate ->
+            None
-               (* prefer [astate] since it is an equivalent state that has been normalized *)
+        | Sat astate ->
-               AbductiveDomain.summary_of_post pdesc astate )) )
+            Some (ContinueProgram astate) )
+      (* already a summary but need to reconstruct the variants to make the type system happy *)
+      | AbortProgram astate ->
+          Some (AbortProgram astate)
+      | ExitProgram astate ->
+          Some (ExitProgram astate)
+      | LatentAbortProgram {astate; latent_issue} ->
+          Some (LatentAbortProgram {astate; latent_issue}) )

infer/src/pulse/PulseExecutionDomain.mli

@@ -11,7 +11,8 @@ module LatentIssue = PulseLatentIssue
 
 type 'abductive_domain_t base_t =
   | ContinueProgram of 'abductive_domain_t  (** represents the state at the program point *)
-  | ExitProgram of 'abductive_domain_t  (** represents the state originating at exit/divergence. *)
+  | ExitProgram of AbductiveDomain.summary
+      (** represents the state originating at exit/divergence. *)
   | AbortProgram of AbductiveDomain.summary
       (** represents the state at the program point that caused an error *)
   | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}

infer/src/pulse/PulseModels.ml

@@ -48,7 +48,12 @@ module Misc = struct
 
 
   let early_exit : model =
-   fun _ ~callee_procname:_ _ ~ret:_ astate -> Ok [ExecutionDomain.ExitProgram astate]
+   fun {proc_desc} ~callee_procname:_ _ ~ret:_ astate ->
+    match AbductiveDomain.summary_of_post proc_desc astate with
+    | Unsat ->
+        Ok []
+    | Sat astate ->
+        Ok [ExecutionDomain.ExitProgram astate]
 
 
   let return_int : Int64.t -> model =

infer/src/pulse/PulseOperations.ml

@@ -468,31 +468,31 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
         f post
   in
   let open ExecutionDomain in
+  let open SatUnsat.Import in
   match callee_exec_state with
-  | AbortProgram astate ->
-      map_call_result
-        (astate :> AbductiveDomain.t)
-        ~f:(fun astate ->
-          let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in
-          Sat (Ok (AbortProgram astate_summary)) )
   | ContinueProgram astate ->
       map_call_result astate ~f:(fun astate -> Sat (Ok (ContinueProgram astate)))
-  | ExitProgram astate ->
+  | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} ->
-      map_call_result astate ~f:(fun astate -> Sat (Ok (ExitProgram astate)))
-  | LatentAbortProgram {astate; latent_issue} ->
       map_call_result
         (astate :> AbductiveDomain.t)
         ~f:(fun astate ->
-          let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in
+          let+ astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in
-          if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Unsat
+          match callee_exec_state with
-          else
+          | ContinueProgram _ ->
+              assert false
+          | AbortProgram _ ->
+              Ok (AbortProgram astate_summary)
+          | ExitProgram _ ->
+              Ok (ExitProgram astate_summary)
+          | LatentAbortProgram {latent_issue} ->
               let latent_issue =
                 LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
               in
-            Sat
+              if LatentIssue.should_report astate_summary then
-              ( if LatentIssue.should_report astate_summary then
+                Error
-                Error (LatentIssue.to_diagnostic latent_issue, (astate_summary :> AbductiveDomain.t))
+                  ( LatentIssue.to_diagnostic latent_issue
-              else Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) ) )
+                  , (astate_summary : AbductiveDomain.summary :> AbductiveDomain.t) )
+              else Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) )
 
 
 let get_captured_actuals location ~captured_vars ~actual_closure astate =

infer/src/pulse/PulsePathCondition.ml

@@ -13,6 +13,7 @@ module CItv = PulseCItv
 module Formula = PulseFormula
 module SatUnsat = PulseSatUnsat
 module ValueHistory = PulseValueHistory
+open SatUnsat.Types
 
 module BoItvs = struct
   include PrettyPrintable.MakePPMonoMap (AbstractValue) (Itv.ItvPure)
@@ -100,6 +101,7 @@ let and_eq_vars v1 v2 phi =
 
 
 let simplify ~keep phi =
+  let result =
     let+ {is_unsat; bo_itvs; citvs; formula} = phi in
     let+| formula, new_eqs = Formula.simplify ~keep formula in
     let is_in_keep v _ = AbstractValue.Set.mem v keep in
@@ -108,6 +110,8 @@ let simplify ~keep phi =
       ; citvs= CItvs.filter is_in_keep citvs
       ; formula }
     , new_eqs )
+  in
+  if (fst result).is_unsat then Unsat else Sat result
 
 
 let subst_find_or_new subst addr_callee =

infer/src/pulse/PulsePathCondition.mli

@@ -8,6 +8,7 @@
 open! IStd
 module F = Format
 module AbstractValue = PulseAbstractValue
+module SatUnsat = PulseSatUnsat
 module ValueHistory = PulseValueHistory
 
 type t [@@deriving yojson_of]
@@ -33,7 +34,7 @@ val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t * new_eqs
 
 val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
 
-val simplify : keep:AbstractValue.Set.t -> t -> t * new_eqs
+val simplify : keep:AbstractValue.Set.t -> t -> (t * new_eqs) SatUnsat.t
 (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
     possible *)
 
@@ -65,6 +66,7 @@ val is_unsat_cheap : t -> bool
 (** whether the state contains a contradiction, call this as often as you want *)
 
 val is_unsat_expensive : t -> t * bool * new_eqs
+  [@@warning "-32"]
 (** whether the state contains a contradiction, only call this when you absolutely have to *)
 
 val as_int : t -> AbstractValue.t -> int option

infer/src/pulse/PulseReport.ml

@@ -32,15 +32,14 @@ let report_latent_issue proc_desc err_log latent_issue =
 
 
 let report_error proc_desc err_log access_result =
+  let open SatUnsat.Import in
   Result.map_error access_result ~f:(fun (diagnostic, astate) ->
-      let astate_summary = AbductiveDomain.summary_of_post proc_desc astate in
+      let+ astate_summary = AbductiveDomain.summary_of_post proc_desc astate in
-      if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Unsat
-      else
       match LatentIssue.should_report_diagnostic astate_summary diagnostic with
       | `ReportNow ->
           report proc_desc err_log diagnostic ;
-            Sat (ExecutionDomain.AbortProgram astate_summary)
+          ExecutionDomain.AbortProgram astate_summary
       | `DelayReport latent_issue ->
           if Config.pulse_report_latent_issues then
             report_latent_issue proc_desc err_log latent_issue ;
-            Sat (ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}) )
+          ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue} )