[topl] Be more precise in extracting summaries.

Summary:
When extracting summaries, ask PulseFormula to work harder to prove that
path-conditions are unsat. This reduces the number of false positives.

Reviewed By: jvillard

Differential Revision: D25270609

fbshipit-source-id: 61ef5e8ac

infer/src/pulse/PulseTopl.ml

@@ -219,13 +219,19 @@ let conjoin_pruned path_condition pruned =
   List.fold ~init:path_condition ~f pruned
 
 
-let is_unsat path_condition pruned =
+let is_unsat_cheap path_condition pruned =
   PathCondition.is_unsat_cheap (conjoin_pruned path_condition pruned)
 
 
-let negate_predicate =
+let is_unsat_expensive path_condition pruned =
-  Binop.(
+  let _path_condition, unsat, _new_eqs =
-    function
+    PathCondition.is_unsat_expensive (conjoin_pruned path_condition pruned)
+  in
+  unsat
+
+
+let negate_predicate (predicate : predicate) : predicate =
+  match predicate with
   | Eq, l, r ->
       (Ne, l, r)
   | Ne, l, r ->
@@ -240,14 +246,15 @@ let negate_predicate =
       (Ge, r, l)
   | _ ->
       L.die InternalError
-          "PulseTopl.negate_predicate should handle all outputs of ToplUtils.binop_to")
+        "PulseTopl.negate_predicate should handle all outputs of ToplUtils.binop_to"
 
 
 let skip_pruned_of_nonskip_pruned nonskip_list =
   IList.product (List.map ~f:(List.map ~f:negate_predicate) nonskip_list)
 
 
-let drop_infeasible path_condition state =
+let drop_infeasible ?(expensive = false) path_condition state =
+  let is_unsat = if expensive then is_unsat_expensive else is_unsat_cheap in
   let f {pruned} = not (is_unsat path_condition pruned) in
   List.filter ~f state
 
@@ -442,9 +449,7 @@ let large_step ~call_location ~callee_proc_name ~substitution ~condition ~callee
   result
 
 
-let filter_for_summary path_condition state =
+let filter_for_summary path_condition state = drop_infeasible ~expensive:true path_condition state
-  List.filter ~f:(fun x -> not (is_unsat path_condition x.pruned)) state
-
 
 let simplify ~keep state =
   let simplify_simple_state {pre; post; pruned; last_step} =

infer/src/pulse/PulseTopl.mli

@@ -39,6 +39,7 @@ val filter_for_summary : PulsePathCondition.t -> state -> state
     program path condition is updated later.) *)
 
 val simplify : keep:PulseAbstractValue.Set.t -> state -> state
+(** Keep only a subset of abstract values. This is used for extracting summaries. *)
 
 val report_errors : Procdesc.t -> Errlog.t -> state -> unit
 (** Calls [Reporting.log_issue] with error traces, if any. *)

infer/tests/codetoanalyze/java/topl/Makefile

@@ -5,7 +5,8 @@
 
 TESTS_DIR = ../../..
 
-SUBDIRS = baos compareArgs hasnext immutableArray servlet slowIter
+# NOTE: If you wish to deactivate a Topl test, simply remove it from this list
+SUBDIRS = baos compareArgs hasnext immutableArray servlet slowIter taint
 
 test-%:
 	$(MAKE) -C $* test

infer/tests/codetoanalyze/java/topl/taint/Makefile

@@ -0,0 +1,13 @@
+# 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.
+
+TESTS_DIR = ../../../..
+
+INFER_OPTIONS = --topl-properties Taint.topl --pulse-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make

infer/tests/codetoanalyze/java/topl/taint/Taint.java

@@ -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.
+ */
+abstract class Taint {
+  abstract String badString();
+
+  abstract void sendToDb(String arg);
+
+  void fOk() {
+    String s0 = badString();
+    String s1 = "foo";
+    if (s0 == s1) return; // Hint for Pulse.
+    sendToDb(s1);
+  }
+
+  void fBad() {
+    String s0 = badString();
+    if (s0 == null) return;
+    String s1 = "foo" + s0 + "bar";
+    if (s1 == s0) return;
+    String s2 = "oops" + s1;
+    if (s2 == s1 || s2 == s0) return;
+    String s3 = s1 + s1;
+    if (s3 == s0 || s3 == s1 || s3 == s2) return;
+    sendToDb(s2);
+  }
+}

infer/tests/codetoanalyze/java/topl/taint/Taint.topl

@@ -0,0 +1,20 @@
+property TaintTrack
+  prefix "StringBuilder"
+  prefix "Taint"
+  nondet (start building track)
+
+  // We start tracking when we see calls to Taint.badString
+  start -> start: *
+  start -> track: badString(IgnoreThis, Ret) => s := Ret
+
+  // Whatever we track, we'll keep tracking forever ...
+  track -> track: *
+
+  // ... but we also keep an eye for derived strings
+  track -> building:    StringBuilder(Builder, Void) => b := Builder
+  building -> building: *
+  building -> dirty:    append(Builder, S) when S == s
+  dirty -> track:       toString(Builder, S) => s := S
+
+  // If anything we track is sent to Taint.sendToDb, we warn
+  track -> error: sendToDb(IgnoreThis, S, Void) when S == s

infer/tests/codetoanalyze/java/topl/taint/issues.exp

@@ -0,0 +1 @@
+codetoanalyze/java/topl/taint/Taint.java, Taint.fBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to String Taint.badString(),call to StringBuilder.<init>(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to StringBuilder.<init>(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to void Taint.sendToDb(String)]