[pulse][refactor] extract and reuse a `SatUnsat` module

Summary:
Use the new module to represent both Sat/Unsat from Pulse formulas, and
FeasiblePath/InfeasiblePath from PulseReport.

Reviewed By: jberdine

Differential Revision: D25277566

fbshipit-source-id: 9f8412ca9

infer/src/pulse/Pulse.ml

@@ -15,9 +15,9 @@ open PulseDomainInterface
 let exec_list_of_list_result = function
   | Ok posts ->
       posts
-  | Error PulseReport.InfeasiblePath ->
+  | Error Unsat ->
       []
-  | Error (PulseReport.FeasiblePath post) ->
+  | Error (Sat post) ->
       [post]
 
 

infer/src/pulse/PulseBasicInterface.ml

@@ -16,9 +16,11 @@ module CallEvent = PulseCallEvent
 module Diagnostic = PulseDiagnostic
 module Invalidation = PulseInvalidation
 module PathCondition = PulsePathCondition
+module SatUnsat = PulseSatUnsat
 module SkippedCalls = PulseSkippedCalls
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
+include SatUnsat.Types
 
 (** {2 Enforce short form usage} *)
 
@@ -39,4 +41,5 @@ include struct
   module PulseTrace = PulseTrace [@@deprecated "use the short form Trace instead"]
   module PulseValueHistory = PulseValueHistory
   [@@deprecated "use the short form ValueHistory instead"]
+  module PulseSatUnsat = PulseSatUnsat [@@deprecated "use the short form SatUnsat instead"]
 end

infer/src/pulse/PulseFormula.ml

@@ -8,14 +8,12 @@
 open! IStd
 module F = Format
 module L = Logging
+module SatUnsat = PulseSatUnsat
 module Var = PulseAbstractValue
+open SatUnsat
 
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t
 
-(** "normalized" is not to be taken too seriously, it just means *some* normalization was applied
-    that could result in discovering something is unsatisfiable *)
-type 'a normalized = Unsat | Sat of 'a
-
 (** {!Q} from zarith with a few convenience functions added *)
 module Q = struct
   include Q
@@ -66,7 +64,7 @@ module LinArith : sig
 
   val mult : Q.t -> t -> t
 
-  val solve_eq : t -> t -> (Var.t * t) option normalized
+  val solve_eq : t -> t -> (Var.t * t) option SatUnsat.t
   (** [solve_eq l1 l2] is [Sat (Some (x, l))] if [l1=l2 <=> x=l], [Sat None] if [l1 = l2] is always
       true, and [Unsat] if it is always false *)
 
@@ -953,20 +951,6 @@ module Atom = struct
   end
 end
 
-module SatUnsatMonad = struct
-  let map_normalized f norm = match norm with Unsat -> Unsat | Sat phi -> Sat (f phi)
-
-  let ( >>| ) phi f = map_normalized f phi
-
-  let ( let+ ) phi f = map_normalized f phi
-
-  let bind_normalized f norm = match norm with Unsat -> Unsat | Sat phi -> f phi
-
-  let ( >>= ) x f = bind_normalized f x
-
-  let ( let* ) phi f = bind_normalized f phi
-end
-
 let sat_of_eval_result (eval_result : Atom.eval_result) =
   match eval_result with True -> Sat None | False -> Unsat | Atom atom -> Sat (Some atom)
 
@@ -1025,20 +1009,20 @@ module Formula = struct
 
   (** module that breaks invariants more often that the rest, with an interface that is safer to use *)
   module Normalizer : sig
-    val and_var_linarith : Var.t -> LinArith.t -> t * new_eqs -> (t * new_eqs) normalized
+    val and_var_linarith : Var.t -> LinArith.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t
 
-    val and_var_var : Var.t -> Var.t -> t * new_eqs -> (t * new_eqs) normalized
+    val and_var_var : Var.t -> Var.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t
 
-    val and_atom : Atom.t -> t * new_eqs -> (t * new_eqs) normalized
+    val and_atom : Atom.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t
 
-    val normalize_atom : t -> Atom.t -> Atom.t option normalized
+    val normalize_atom : t -> Atom.t -> Atom.t option SatUnsat.t
 
-    val normalize : t -> (t * new_eqs) normalized
+    val normalize : t -> (t * new_eqs) SatUnsat.t
 
     val implies_atom : t -> Atom.t -> bool
   end = struct
     (* Use the monadic notations when normalizing formulas. *)
-    open SatUnsatMonad
+    open SatUnsat.Import
 
     (** OVERVIEW: the best way to think about this is as a half-assed Shostak technique.
 
@@ -1296,7 +1280,7 @@ let pp_with_pp_var pp_var fmt {known; pruned; both} =
 let pp = pp_with_pp_var Var.pp
 
 let and_known_atom atom phi =
-  let open SatUnsatMonad in
+  let open SatUnsat.Import in
   let* known, _ = Formula.Normalizer.and_atom atom (phi.known, []) in
   let+ both, new_eqs = Formula.Normalizer.and_atom atom (phi.both, []) in
   ({phi with known; both}, new_eqs)
@@ -1322,7 +1306,7 @@ let and_equal_binop v (bop : Binop.t) x y phi =
 
 
 let prune_binop ~negated (bop : Binop.t) x y phi =
-  let open SatUnsatMonad in
+  let open SatUnsat.Import in
   let tx = Term.of_operand x in
   let ty = Term.of_operand y in
   let t = Term.of_binop bop tx ty in
@@ -1339,7 +1323,7 @@ let prune_binop ~negated (bop : Binop.t) x y phi =
 
 
 let normalize phi =
-  let open SatUnsatMonad in
+  let open SatUnsat.Import in
   let* both, new_eqs = Formula.Normalizer.normalize phi.both in
   let* known, _ = Formula.Normalizer.normalize phi.known in
   let+ pruned =
@@ -1366,7 +1350,7 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
   in
   (* propagate [Unsat] faster using this exception *)
   let exception Contradiction in
-  let sat_value_exn (norm : 'a normalized) =
+  let sat_value_exn (norm : 'a SatUnsat.t) =
     match norm with Unsat -> raise Contradiction | Sat x -> x
   in
   let and_var_eqs var_eqs_foreign acc_phi_new_eqs =
@@ -1402,7 +1386,7 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
         |> and_atoms phi_foreign.Formula.atoms )
     with Contradiction -> Unsat
   in
-  let open SatUnsatMonad in
+  let open SatUnsat.Import in
   let* acc, (both, new_eqs) = and_ phi_foreign.both init phi0.both in
   let* acc, (known, _) = and_ phi_foreign.known acc phi0.known in
   let and_pruned pruned_foreign acc_pruned =
@@ -1500,7 +1484,7 @@ let get_reachable_from graph vs =
 
 
 let simplify ~keep phi =
-  let open SatUnsatMonad in
+  let open SatUnsat.Import in
   let+ phi, new_eqs = normalize phi in
   L.d_printfln_escaped "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ;
   (* Get rid of atoms when they contain only variables that do not appear in atoms mentioning

infer/src/pulse/PulseFormula.mli

@@ -7,6 +7,7 @@
 
 open! IStd
 module F = Format
+module SatUnsat = PulseSatUnsat
 
 (* NOTE: using [Var] for [AbstractValue] here since this is how "abstract values" are interpreted,
    in particular as far as arithmetic is concerned *)
@@ -24,8 +25,6 @@ val pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit
   [@@warning "-32"]
 (** only used for unit tests *)
 
-type 'a normalized = Unsat | Sat of 'a
-
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t
 
 (** {3 Build formulas} *)
@@ -38,57 +37,34 @@ type new_eqs = new_eq list
 
 val ttrue : t
 
-val and_equal : operand -> operand -> t -> (t * new_eqs) normalized
+val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
-val and_less_equal : operand -> operand -> t -> (t * new_eqs) normalized
+val and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
-val and_less_than : operand -> operand -> t -> (t * new_eqs) normalized
+val and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
-val and_equal_unop : Var.t -> Unop.t -> operand -> t -> (t * new_eqs) normalized
+val and_equal_unop : Var.t -> Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.t
 
-val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> (t * new_eqs) normalized
+val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
-val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new_eqs) normalized
+val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
 
 (** {3 Operations} *)
 
-val normalize : t -> (t * new_eqs) normalized
+val normalize : t -> (t * new_eqs) SatUnsat.t
 (** think a bit harder about the formula *)
 
-val simplify : keep:Var.Set.t -> t -> (t * new_eqs) normalized
+val simplify : keep:Var.Set.t -> t -> (t * new_eqs) SatUnsat.t
 
 val and_fold_subst_variables :
      t
   -> up_to_f:t
   -> init:'acc
   -> f:('acc -> Var.t -> 'acc * Var.t)
-  -> ('acc * t * new_eqs) normalized
+  -> ('acc * t * new_eqs) SatUnsat.t
 
 val is_known_zero : t -> Var.t -> bool
 
 val as_int : t -> Var.t -> int option
 
 val has_no_assumptions : t -> bool
-
-(** {3 Notations} *)
-
-include sig
-  [@@@warning "-60"]
-
-  (** Useful notations to deal with normalized formulas *)
-  module SatUnsatMonad : sig
-    [@@@warning "-32"]
-
-    val map_normalized : ('a -> 'b) -> 'a normalized -> 'b normalized
-
-    val ( >>| ) : 'a normalized -> ('a -> 'b) -> 'b normalized
-
-    val ( let+ ) : 'a normalized -> ('a -> 'b) -> 'b normalized
-
-    val bind_normalized : ('a -> 'b normalized) -> 'a normalized -> 'b normalized
-
-    val ( >>= ) : 'a normalized -> ('a -> 'b normalized) -> 'b normalized
-
-    val ( let* ) : 'a normalized -> ('a -> 'b normalized) -> 'b normalized
-  end
-end

infer/src/pulse/PulseInterproc.ml

@@ -569,10 +569,10 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post
       (* can't make sense of the pre-condition in the current context: give up on that particular
          pre/post pair *)
       L.d_printfln "Cannot apply precondition: %a" pp_contradiction reason ;
-      PulseReport.InfeasiblePath
+      Unsat
   | Error _ as error ->
       (* error: the function call requires to read some state known to be invalid *)
-      PulseReport.FeasiblePath error
+      Sat error
   | Ok call_state -> (
       L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ;
       match
@@ -595,7 +595,7 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post
         (astate, return_caller)
       with
       | post ->
-          PulseReport.FeasiblePath post
+          Sat post
       | exception Contradiction reason ->
           L.d_printfln "Cannot apply post-condition: %a" pp_contradiction reason ;
-          PulseReport.InfeasiblePath )
+          Unsat )

infer/src/pulse/PulseInterproc.mli

@@ -18,4 +18,4 @@ val apply_prepost :
   -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
   -> AbductiveDomain.t
   -> (AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) option) PulseReport.access_result
-     PulseReport.path_feasibility
+     SatUnsat.t

infer/src/pulse/PulseOperations.ml

@@ -454,9 +454,9 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
       PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals
         ~formals ~actuals astate
     with
-    | (FeasiblePath (Error _) | InfeasiblePath) as path_result ->
+    | (Sat (Error _) | Unsat) as path_result ->
         path_result
-    | FeasiblePath (Ok (post, return_val_opt)) ->
+    | Sat (Ok (post, return_val_opt)) ->
         let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in
         let post =
           match return_val_opt with
@@ -474,23 +474,22 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
         (astate :> AbductiveDomain.t)
         ~f:(fun astate ->
           let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in
-          FeasiblePath (Ok (AbortProgram astate_summary)) )
+          Sat (Ok (AbortProgram astate_summary)) )
   | ContinueProgram astate ->
-      map_call_result astate ~f:(fun astate -> FeasiblePath (Ok (ContinueProgram astate)))
+      map_call_result astate ~f:(fun astate -> Sat (Ok (ContinueProgram astate)))
   | ExitProgram astate ->
-      map_call_result astate ~f:(fun astate -> FeasiblePath (Ok (ExitProgram 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
-          if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then
+          if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Unsat
-            InfeasiblePath
           else
             let latent_issue =
               LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
             in
-            FeasiblePath
+            Sat
               ( if LatentIssue.should_report astate_summary then
                 Error (LatentIssue.to_diagnostic latent_issue, (astate_summary :> AbductiveDomain.t))
               else Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) ) )
@@ -550,14 +549,14 @@ let call ~caller_proc_desc err_log ~(callee_data : (Procdesc.t * PulseSummary.t)
               apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state
                 ~captured_vars_with_actuals ~formals ~actuals ~ret astate
             with
-            | InfeasiblePath ->
+            | Unsat ->
                 (* couldn't apply pre/post pair *)
                 posts
-            | FeasiblePath post -> (
+            | Sat post -> (
               match PulseReport.report_error caller_proc_desc err_log post with
-              | Error InfeasiblePath ->
+              | Error Unsat ->
                   posts
-              | Error (FeasiblePath post) | Ok post ->
+              | Error (Sat post) | Ok post ->
                   post :: posts ) )
   | None ->
       (* no spec found for some reason (unknown function, ...) *)

infer/src/pulse/PulsePathCondition.ml

@@ -11,6 +11,7 @@ module L = Logging
 module AbstractValue = PulseAbstractValue
 module CItv = PulseCItv
 module Formula = PulseFormula
+module SatUnsat = PulseSatUnsat
 module ValueHistory = PulseValueHistory
 
 module BoItvs = struct
@@ -51,9 +52,7 @@ let map_sat phi f = if phi.is_unsat then (phi, []) else f phi
 
 let ( let+ ) phi f = map_sat phi f
 
-let map_formula_sat (x : 'a Formula.normalized) f =
+let map_formula_sat (x : 'a SatUnsat.t) f = match x with Unsat -> (false_, []) | Sat x' -> f x'
-  match x with Unsat -> (false_, []) | Sat x' -> f x'
-
 
 let ( let+| ) x f = map_formula_sat x f
 

infer/src/pulse/PulseReport.ml

@@ -11,8 +11,6 @@ open PulseDomainInterface
 
 type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result
 
-type 'a path_feasibility = InfeasiblePath | FeasiblePath of 'a
-
 let report ?(extra_trace = []) proc_desc err_log diagnostic =
   let open Diagnostic in
   Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic)
@@ -36,13 +34,13 @@ let report_latent_issue proc_desc err_log latent_issue =
 let report_error proc_desc err_log access_result =
   Result.map_error access_result ~f:(fun (diagnostic, astate) ->
       let astate_summary = AbductiveDomain.summary_of_post proc_desc astate in
-      if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then InfeasiblePath
+      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 ;
-            FeasiblePath (ExecutionDomain.AbortProgram astate_summary)
+            Sat (ExecutionDomain.AbortProgram astate_summary)
         | `DelayReport latent_issue ->
             if Config.pulse_report_latent_issues then
               report_latent_issue proc_desc err_log latent_issue ;
-            FeasiblePath (ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}) )
+            Sat (ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}) )

infer/src/pulse/PulseReport.mli

@@ -11,10 +11,5 @@ open PulseDomainInterface
 
 type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result
 
-type 'a path_feasibility = InfeasiblePath | FeasiblePath of 'a
-
 val report_error :
-     Procdesc.t
+  Procdesc.t -> Errlog.t -> 'ok access_result -> ('ok, _ ExecutionDomain.base_t SatUnsat.t) result
-  -> Errlog.t
-  -> 'ok access_result
-  -> ('ok, _ ExecutionDomain.base_t path_feasibility) result

infer/src/pulse/PulseSatUnsat.ml

@@ -0,0 +1,30 @@
+(*
+ * 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
+
+type 'a t = Unsat | Sat of 'a
+
+module Types = struct
+  type nonrec 'a sat_unsat_t = 'a t = Unsat | Sat of 'a
+end
+
+let map f = function Unsat -> Unsat | Sat x -> Sat (f x)
+
+let bind f = function Unsat -> Unsat | Sat x -> f x
+
+module Import = struct
+  include Types
+
+  let ( >>| ) x f = map f x
+
+  let ( >>= ) x f = bind f x
+
+  let ( let+ ) x f = map f x
+
+  let ( let* ) x f = bind f x
+end

infer/src/pulse/PulseSatUnsat.mli

@@ -0,0 +1,33 @@
+(*
+ * 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
+
+[@@@warning "-32-60"]
+
+type 'a t = Unsat | Sat of 'a
+
+(** for [open]ing to get [Sat] and [Unsat] in the namespace *)
+module Types : sig
+  type nonrec 'a sat_unsat_t = 'a t = Unsat | Sat of 'a
+end
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+
+val bind : ('a -> 'b t) -> 'a t -> 'b t
+
+module Import : sig
+  include module type of Types
+
+  val ( >>| ) : 'a t -> ('a -> 'b) -> 'b t
+
+  val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
+
+  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+end

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -8,7 +8,7 @@
 open! IStd
 module AbstractValue = PulseAbstractValue
 open PulseFormula
-open SatUnsatMonad
+open PulseSatUnsat.Import
 
 (** {2 Utilities for defining formulas easily}