[pulse] filter out unsat states earlier

Summary:
See comments added in the code: there's always a chance some unsat
states make it to the end of the execution of an instructions. Before
this diff they would get propagated and executed until some code path
actually bothers to check their satifiability. After this diff we throw
them out at the end of the execution of the first instruction they get
generated in.

An alternative design would be to return Unsat explicitly everywhere we
currently might return `false_`. This would be good too but there's
still a chance we'd generate `false_` and so even if we did that more
significant refactoring, the detection in this diff would still be a
good last line of defense.

Reviewed By: ezgicicek

Differential Revision: D25336042

fbshipit-source-id: a24693596

infer/src/pulse/Pulse.ml

@@ -255,7 +255,7 @@ module PulseTransferFunctions = struct
     (astates, ret_vars)
 
 
-  let exec_instr (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
+  let exec_instr_aux (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
       _cfg_node (instr : Sil.instr) : Domain.t list =
     match astate with
     | AbortProgram _ | LatentAbortProgram _ ->
@@ -345,6 +345,13 @@ module PulseTransferFunctions = struct
           [Domain.ContinueProgram astate] )
 
 
+  let exec_instr astate analysis_data cfg_node instr =
+    (* Sometimes instead of stopping on contradictions a false path condition is recorded
+       instead. Prune these early here so they don't spuriously count towards the disjunct limit. *)
+    exec_instr_aux astate analysis_data cfg_node instr
+    |> List.filter ~f:(fun exec_state -> not (Domain.is_unsat_cheap exec_state))
+
+
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
 end
 

infer/src/pulse/PulseExecutionDomain.ml

@@ -59,6 +59,17 @@ let pp fmt = function
         (astate :> AbductiveDomain.t)
 
 
+(* do not export this function as there lies wickedness: clients should generally care about what
+   kind of state they are manipulating so let's not encourage them not to *)
+let get_astate : t -> AbductiveDomain.t = function
+  | ContinueProgram astate ->
+      astate
+  | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} ->
+      (astate :> AbductiveDomain.t)
+
+
+let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_state).path_condition
+
 type summary = AbductiveDomain.summary base_t [@@deriving yojson_of]
 
 let summary_of_posts pdesc posts =

infer/src/pulse/PulseExecutionDomain.mli

@@ -26,6 +26,9 @@ val continue : AbductiveDomain.t -> t
 
 val mk_initial : Procdesc.t -> t
 
+val is_unsat_cheap : t -> bool
+(** see {!PulsePathCondition.is_unsat_cheap} *)
+
 type summary = AbductiveDomain.summary base_t [@@deriving yojson_of]
 
 val summary_of_posts : Procdesc.t -> t list -> summary list