[pulse] avoid some FPs due to incompleteness in the arihtmetic engine

Summary:
Before, atoms we didn't understand but could be a contradiction became
"true" if they were only about dead variables. This is unsound for
incorrectness logic, and introduces false positives.

Be more conservative and try to identify when that could happen and
prune these paths instead, thus regaining under-approximation.

This is a bit ad-hoc: we expect reasoning on equalities and
disequalities to be precise enough, but we know that inequalities have
very little solving power at the moment (eg we don't detect `x < 0, x >
0 => false`). In addition, we remark that having *one* `<` atom can
never be a contradiction. So, we claim a possible contradiction whenever
we find *two* (>1) atoms containing inequalities and involving the same
variable.

Reviewed By: skcho

Differential Revision: D29232544

fbshipit-source-id: ff91eb1e4

infer/man/man1/infer-analyze.txt

@@ -325,6 +325,15 @@ OPTIONS
            Activates: Enable pulse and disable all other checkers
            (Conversely: --no-pulse-only)
 
+       --pulse-prune-unsupported-arithmetic
+           Activates: The arithmetic engine in Pulse sometimes does not
+           detect that the collection of conditions on the path makes it
+           infeasible, especially outside the well-supported linear
+           arithmetic fragment. To avoid false positives, Pulse tries to
+           detect when there is a possibility of imprecise arithmetic
+           treatment and if so pessimistically assumes the path is
+           infeasible. (Conversely: --no-pulse-prune-unsupported-arithmetic)
+
        --pulse-report-ignore-unknown-java-methods-patterns +string
            On Java, issues that are found on program paths that contain calls
            to unknown methods (those without implementation) are not reported

infer/man/man1/infer-full.txt

@@ -1066,6 +1066,16 @@ OPTIONS
            Activates: Enable pulse and disable all other checkers
            (Conversely: --no-pulse-only)           See also infer-analyze(1).
 
+       --pulse-prune-unsupported-arithmetic
+           Activates: The arithmetic engine in Pulse sometimes does not
+           detect that the collection of conditions on the path makes it
+           infeasible, especially outside the well-supported linear
+           arithmetic fragment. To avoid false positives, Pulse tries to
+           detect when there is a possibility of imprecise arithmetic
+           treatment and if so pessimistically assumes the path is
+           infeasible. (Conversely: --no-pulse-prune-unsupported-arithmetic)       
+    See also infer-analyze(1).
+
        --pulse-report-ignore-unknown-java-methods-patterns +string
            On Java, issues that are found on program paths that contain calls
            to unknown methods (those without implementation) are not reported

infer/man/man1/infer.txt

@@ -1066,6 +1066,16 @@ OPTIONS
            Activates: Enable pulse and disable all other checkers
            (Conversely: --no-pulse-only)           See also infer-analyze(1).
 
+       --pulse-prune-unsupported-arithmetic
+           Activates: The arithmetic engine in Pulse sometimes does not
+           detect that the collection of conditions on the path makes it
+           infeasible, especially outside the well-supported linear
+           arithmetic fragment. To avoid false positives, Pulse tries to
+           detect when there is a possibility of imprecise arithmetic
+           treatment and if so pessimistically assumes the path is
+           infeasible. (Conversely: --no-pulse-prune-unsupported-arithmetic)       
+    See also infer-analyze(1).
+
        --pulse-report-ignore-unknown-java-methods-patterns +string
            On Java, issues that are found on program paths that contain calls
            to unknown methods (those without implementation) are not reported

infer/src/base/Config.ml

@@ -2089,6 +2089,15 @@ and pulse_model_skip_pattern =
     "Regex of methods that should be modelled as \"skip\" in Pulse"
 
 
+and pulse_prune_unsupported_arithmetic =
+  CLOpt.mk_bool ~long:"pulse-prune-unsupported-arithmetic" ~default:false
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "The arithmetic engine in Pulse sometimes does not detect that the collection of conditions on \
+     the path makes it infeasible, especially outside the well-supported linear arithmetic \
+     fragment. To avoid false positives, Pulse tries to detect when there is a possibility of \
+     imprecise arithmetic treatment and if so pessimistically assumes the path is infeasible."
+
+
 and pulse_report_ignore_unknown_java_methods_patterns =
   CLOpt.mk_string_list ~default:[".*<init>.*"]
     ~long:"pulse-report-ignore-unknown-java-methods-patterns"
@@ -3332,6 +3341,8 @@ and pulse_model_return_nonnull = Option.map ~f:Str.regexp !pulse_model_return_no
 
 and pulse_model_skip_pattern = Option.map ~f:Str.regexp !pulse_model_skip_pattern
 
+and pulse_prune_unsupported_arithmetic = !pulse_prune_unsupported_arithmetic
+
 and pulse_report_ignore_unknown_java_methods_patterns =
   match RevList.to_list !pulse_report_ignore_unknown_java_methods_patterns with
   | [] ->

infer/src/base/Config.mli

@@ -520,6 +520,8 @@ val pulse_model_return_nonnull : Str.regexp option
 
 val pulse_model_skip_pattern : Str.regexp option
 
+val pulse_prune_unsupported_arithmetic : bool
+
 val pulse_report_ignore_unknown_java_methods_patterns : Str.regexp option
 
 val pulse_model_transfer_ownership_namespace : (string * string) list

infer/src/pulse/PulseFormula.ml

@@ -886,6 +886,8 @@ module Atom = struct
     (acc, t')
 
 
+  let fold_terms atom ~init ~f = fold_map_terms atom ~init ~f:(fun acc t -> (f acc t, t)) |> fst
+
   let equal t1 t2 = Equal (t1, t2)
 
   let less_equal t1 t2 = LessEqual (t1, t2)
@@ -1866,6 +1868,10 @@ module DeadVariables = struct
     graph
 
 
+  let is_source_of_incompleteness atom =
+    match (atom : Atom.t) with LessEqual _ | LessThan _ -> true | Equal _ | NotEqual _ -> false
+
+
   (** Intermediate step of [simplify]: construct transitive closure of variables reachable from [vs]
       in [graph]. *)
   let get_reachable_from graph vs =
@@ -1906,6 +1912,7 @@ module DeadVariables = struct
     let var_graph = build_var_graph phi.both in
     let vars_to_keep = get_reachable_from var_graph keep in
     L.d_printfln "Reachable vars: %a" Var.Set.pp vars_to_keep ;
+    let exception Contradiction in
     let simplify_phi phi =
       let var_eqs =
         VarUF.filter_morphism ~f:(fun x -> Var.Set.mem x vars_to_keep) phi.Formula.var_eqs
@@ -1922,19 +1929,49 @@ module DeadVariables = struct
          to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive
          closure on the graph above *)
       let atoms =
-        Atom.Set.filter (fun atom -> not (Atom.has_var_notin vars_to_keep atom)) phi.Formula.atoms
+        if Config.pulse_prune_unsupported_arithmetic then
+          Atom.Set.fold
+            (fun atom (atoms_to_keep, discarded_vars_in_atoms) ->
+              let discard_atom = ref false in
+              let discarded_vars_in_atoms =
+                Atom.fold_terms atom ~init:discarded_vars_in_atoms ~f:(fun discarded t ->
+                    Term.fold_variables t ~init:discarded ~f:(fun discarded v ->
+                        if (not (is_source_of_incompleteness atom)) || Var.Set.mem v vars_to_keep
+                        then discarded
+                        else if Var.Set.mem v discarded_vars_in_atoms then (
+                          (* the variable was already involved in *another* atom we discarded, we risk
+                             incompleteness by discarding both (eg [x<y, y≤x]) *)
+                          L.d_printfln ~color:Orange
+                            "%a appears in several atoms that should be discarded; incompleteness \
+                             feared, pruning the path"
+                            Var.pp v ;
+                          raise Contradiction )
+                        else (
+                          discard_atom := true ;
+                          Var.Set.add v discarded ) ) )
+              in
+              let atoms_to_keep =
+                if !discard_atom then atoms_to_keep else Atom.Set.add atom atoms_to_keep
+              in
+              (atoms_to_keep, discarded_vars_in_atoms) )
+            phi.Formula.atoms (Atom.Set.empty, Var.Set.empty)
+          |> fst
+        else
+          Atom.Set.filter (fun atom -> not (Atom.has_var_notin vars_to_keep atom)) phi.Formula.atoms
       in
       {Formula.var_eqs; linear_eqs; term_eqs; atoms}
     in
-    let known = simplify_phi phi.known in
-    let both = simplify_phi phi.both in
-    let pruned =
-      (* discard atoms that callers have no way of influencing, i.e. more or less those that do not
-         contain variables related to variables in the pre *)
-      let closed_prunable_vars = get_reachable_from var_graph can_be_pruned in
-      Atom.Set.filter (fun atom -> not (Atom.has_var_notin closed_prunable_vars atom)) phi.pruned
-    in
-    ({known; pruned; both}, vars_to_keep)
+    try
+      let known = simplify_phi phi.known in
+      let both = simplify_phi phi.both in
+      let pruned =
+        (* discard atoms that callers have no way of influencing, i.e. more or less those that do not
+           contain variables related to variables in the pre *)
+        let closed_prunable_vars = get_reachable_from var_graph can_be_pruned in
+        Atom.Set.filter (fun atom -> not (Atom.has_var_notin closed_prunable_vars atom)) phi.pruned
+      in
+      Sat ({known; pruned; both}, vars_to_keep)
+    with Contradiction -> Unsat
 end
 
 let simplify tenv ~get_dynamic_type ~can_be_pruned ~keep phi =
@@ -1943,10 +1980,10 @@ let simplify tenv ~get_dynamic_type ~can_be_pruned ~keep phi =
   L.d_printfln_escaped "@[Simplifying %a@,wrt %a (keep), with prunables=%a@]" pp phi Var.Set.pp keep
     Var.Set.pp can_be_pruned ;
   (* get rid of as many variables as possible *)
-  let+ phi = QuantifierElimination.eliminate_vars ~keep phi in
+  let* phi = QuantifierElimination.eliminate_vars ~keep phi in
   (* TODO: doing [QuantifierElimination.eliminate_vars; DeadVariables.eliminate] a few times may
      eliminate even more variables *)
-  let phi, live_vars = DeadVariables.eliminate ~can_be_pruned ~keep phi in
+  let+ phi, live_vars = DeadVariables.eliminate ~can_be_pruned ~keep phi in
   (phi, live_vars, new_eqs)