[formula] remember results of normalization

Summary:
Normalization is potentially expensive and its result should be
remembered if the formula keeps being used. In the future we might use
this to make normalization more incremental.

Also rename PathCondition.satisfiable -> is_unsat to match
PulseFormula.is_unsat.

Reviewed By: skcho

Differential Revision: D22728264

fbshipit-source-id: 7759b33ac

infer/src/pulse/Pulse.ml

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

infer/src/pulse/PulseArithmetic.ml

@@ -50,4 +50,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 =
-  PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition
+  let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in
+  (AbductiveDomain.set_path_condition phi' astate, is_unsat)

infer/src/pulse/PulseArithmetic.mli

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

infer/src/pulse/PulseExecutionDomain.ml

@@ -52,5 +52,10 @@ let of_posts pdesc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
       let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
-      if PulseArithmetic.is_unsat_expensive astate then None
-      else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) )
+      let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
+      if is_unsat then None
+      else
+        Some
+          (map exec_state ~f:(fun _astate ->
+               (* prefer [astate] since it is an equivalent state that has been normalized *)
+               AbductiveDomain.of_post pdesc astate )) )

infer/src/pulse/PulsePathCondition.ml

@@ -29,59 +29,60 @@ module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv)
 (** A mash-up of several arithmetic domains. At the moment they are independent, i.e. we don't use
     facts deduced by one domain to inform another. *)
 type t =
-  { satisfiable: bool
-        (** If [true] then [formula] could still be unsatisfiable (asking that question is
+  { is_unsat: bool
+        (** If [false] then [formula] could still be unsatisfiable (asking that question is
             expensive).
 
-            If [false] then the other components of the record can be arbitrary. *)
+            If [true] then the other components of the record can be arbitrary. *)
   ; bo_itvs: BoItvs.t
   ; citvs: CItvs.t
   ; formula: Formula.t }
 
-let pp fmt {satisfiable; bo_itvs; citvs; formula} =
-  F.fprintf fmt "@[<hv>sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" satisfiable BoItvs.pp
+let pp fmt {is_unsat; bo_itvs; citvs; formula} =
+  F.fprintf fmt "@[<hv>unsat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" is_unsat BoItvs.pp
     bo_itvs CItvs.pp citvs Formula.pp formula
 
 
-let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
+let true_ = {is_unsat= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
 
-let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
+let false_ = {is_unsat= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
 
-let and_nonnegative v ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not satisfiable then phi
+let and_nonnegative v ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
     ; citvs= CItvs.add v CItv.zero_inf citvs
     ; formula= Formula.(aand (mk_less_equal Term.zero (Term.of_absval v)) formula) }
 
 
-let and_positive v ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not satisfiable then phi
+let and_positive v ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
     ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
     ; formula= Formula.(aand (mk_less_than Term.zero (Term.of_absval v)) formula) }
 
 
-let and_eq_int v i ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not satisfiable then phi
+let and_eq_int v i ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
     ; citvs= CItvs.add v (CItv.equal_to i) citvs
     ; formula= Formula.(aand (mk_equal (Term.of_absval v) (Term.of_intlit i)) formula) }
 
 
-let simplify ~keep {satisfiable; bo_itvs; citvs; formula} =
-  if not satisfiable then false_
+let simplify ~keep {is_unsat; bo_itvs; citvs; formula} =
+  if is_unsat then false_
   else
     let is_in_keep v _ = AbstractValue.Set.mem v keep in
-    { satisfiable
+    let formula = Formula.simplify ~keep formula in
+    { is_unsat= is_unsat || Formula.is_literal_false formula
     ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
     ; citvs= CItvs.filter is_in_keep citvs
-    ; formula= Formula.simplify ~keep formula }
+    ; formula }
 
 
 let subst_find_or_new subst addr_callee =
@@ -186,7 +187,7 @@ let and_formula_callee subst formula_caller formula_callee =
 
 
 let and_callee subst phi ~callee:phi_callee =
-  if (not phi.satisfiable) || not phi_callee.satisfiable then (subst, false_)
+  if phi.is_unsat || phi_callee.is_unsat then (subst, false_)
   else
     match and_bo_itvs_callee subst phi.bo_itvs phi_callee.bo_itvs with
     | exception Contradiction ->
@@ -201,9 +202,9 @@ let and_callee subst phi ~callee:phi_callee =
           let subst, formula' = and_formula_callee subst phi.formula phi_callee.formula in
           L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ;
           let formula' = Formula.normalize formula' in
-          let satisfiable = not (Formula.is_literal_false formula') in
-          if not satisfiable then L.d_printfln "contradiction found by formulas" ;
-          (subst, {satisfiable; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) )
+          let is_unsat = Formula.is_literal_false formula' in
+          if is_unsat then L.d_printfln "contradiction found by formulas" ;
+          (subst, {is_unsat; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) )
 
 
 (** {2 Operations} *)
@@ -254,10 +255,10 @@ let eval_formula_binop binop_addr binop op_lhs op_rhs formula =
   aand (mk_equal (Term.of_absval binop_addr) t_binop) formula
 
 
-let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not phi.satisfiable then phi
+let eval_binop binop_addr binop op_lhs op_rhs ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if phi.is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
     ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
     ; formula= eval_formula_binop binop_addr binop op_lhs op_rhs formula }
@@ -286,10 +287,10 @@ let eval_formula_unop unop_addr (unop : Unop.t) addr formula =
   aand (mk_equal (Term.of_absval unop_addr) t_unop) formula
 
 
-let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; formula} as phi) =
-  if not phi.satisfiable then phi
+let eval_unop unop_addr unop addr ({is_unsat; bo_itvs; citvs; formula} as phi) =
+  if phi.is_unsat then phi
   else
-    { satisfiable
+    { is_unsat
     ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
     ; citvs= eval_citv_unop unop_addr unop addr citvs
     ; formula= eval_formula_unop unop_addr unop addr formula }
@@ -304,7 +305,7 @@ let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
   | None ->
       phi
   | Some (_, Bottom) ->
-      {phi with satisfiable= false}
+      {phi with is_unsat= true}
   | Some (v, NonBottom arith_pruned) ->
       {phi with bo_itvs= BoItvs.add v arith_pruned phi.bo_itvs}
 
@@ -327,10 +328,10 @@ let record_citv_abduced addr_opt arith_opt citvs =
       CItvs.add addr arith citvs
 
 
-let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi
+let bind_is_unsat phi ~f = if phi.is_unsat then phi else f phi
 
-let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; formula} as phi) =
-  if not satisfiable then phi
+let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formula} as phi) =
+  if is_unsat then phi
   else
     let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, t_lhs = eval_operand phi lhs_op in
     let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, t_rhs = eval_operand phi rhs_op in
@@ -346,38 +347,38 @@ let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; for
           in
           {phi with citvs}
         in
-        let satisfiable =
+        let is_unsat =
           match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with
           | False ->
-              negated
-          | True ->
               not negated
+          | True ->
+              negated
           | Top ->
-              true
-          | Bottom ->
               false
+          | Bottom ->
+              true
         in
-        if not satisfiable then L.d_printfln "contradiction detected by inferbo intervals" ;
-        let phi = {phi with satisfiable} in
+        if is_unsat then L.d_printfln "contradiction detected by inferbo intervals" ;
+        let phi = {phi with is_unsat} in
         let phi =
-          bind_satisfiable phi ~f:(fun phi ->
+          bind_is_unsat phi ~f:(fun phi ->
               prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi )
         in
         let phi =
           Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' ->
-              bind_satisfiable phi ~f:(fun phi ->
+              bind_is_unsat phi ~f:(fun phi ->
                   prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) )
         in
-        if not phi.satisfiable then phi
+        if phi.is_unsat then phi
         else
           let f_positive = Formula.of_term_binop bop t_lhs t_rhs in
           let formula =
             let f = if negated then Formula.nnot f_positive else f_positive in
             Formula.aand f formula |> Formula.normalize
           in
-          let satisfiable = not (Formula.is_literal_false formula) in
-          if not satisfiable then L.d_printfln "contradiction detected by formulas" ;
-          {phi with satisfiable; formula}
+          let is_unsat = Formula.is_literal_false formula in
+          if is_unsat then L.d_printfln "contradiction detected by formulas" ;
+          {phi with is_unsat; formula}
 
 
 (** {2 Queries} *)
@@ -388,9 +389,14 @@ let is_known_zero phi v =
   || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero
 
 
-let is_unsat_cheap phi = (not phi.satisfiable) || Formula.is_literal_false phi.formula
+let is_unsat_cheap phi = phi.is_unsat || Formula.is_literal_false phi.formula
 
 let is_unsat_expensive phi =
   (* note: contradictions are detected eagerly for all sub-domains except formula, so just
      evaluate that one *)
-  is_unsat_cheap phi || Formula.normalize phi.formula |> Formula.is_literal_false
+  if is_unsat_cheap phi then (phi, true)
+  else
+    let formula = Formula.normalize phi.formula in
+    let is_unsat = Formula.is_literal_false formula in
+    let phi = {phi with is_unsat; formula} in
+    (phi, is_unsat)

infer/src/pulse/PulsePathCondition.mli

@@ -55,5 +55,5 @@ val is_known_zero : t -> AbstractValue.t -> bool
 val is_unsat_cheap : t -> bool
 (** whether the state contains a contradiction, call this as often as you want *)
 
-val is_unsat_expensive : t -> bool
+val is_unsat_expensive : t -> t * bool
 (** whether the state contains a contradiction, only call this when you absolutely have to *)