From f8aa139b88547903648c59818efbfee5bb73467a Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Fri, 4 Dec 2020 01:16:13 -0800 Subject: [PATCH] [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 | 51 ++++++++++--------- infer/src/pulse/PulseTopl.mli | 1 + infer/tests/codetoanalyze/java/topl/Makefile | 3 +- .../codetoanalyze/java/topl/taint/Makefile | 13 +++++ .../codetoanalyze/java/topl/taint/Taint.java | 30 +++++++++++ .../codetoanalyze/java/topl/taint/Taint.topl | 20 ++++++++ .../codetoanalyze/java/topl/taint/issues.exp | 1 + 7 files changed, 95 insertions(+), 24 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/topl/taint/Makefile create mode 100644 infer/tests/codetoanalyze/java/topl/taint/Taint.java create mode 100644 infer/tests/codetoanalyze/java/topl/taint/Taint.topl create mode 100644 infer/tests/codetoanalyze/java/topl/taint/issues.exp diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 44257cc31..c37037415 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -219,35 +219,42 @@ 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 = - Binop.( - function - | Eq, l, r -> - (Ne, l, r) - | Ne, l, r -> - (Eq, l, r) - | Ge, l, r -> - (Lt, r, l) - | Gt, l, r -> - (Le, r, l) - | Le, l, r -> - (Gt, r, l) - | Lt, l, r -> - (Ge, r, l) - | _ -> - L.die InternalError - "PulseTopl.negate_predicate should handle all outputs of ToplUtils.binop_to") +let is_unsat_expensive path_condition pruned = + let _path_condition, unsat, _new_eqs = + 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 -> + (Eq, l, r) + | Ge, l, r -> + (Lt, r, l) + | Gt, l, r -> + (Le, r, l) + | Le, l, r -> + (Gt, r, l) + | Lt, l, r -> + (Ge, r, l) + | _ -> + L.die InternalError + "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 = - List.filter ~f:(fun x -> not (is_unsat path_condition x.pruned)) state - +let filter_for_summary path_condition state = drop_infeasible ~expensive:true path_condition state let simplify ~keep state = let simplify_simple_state {pre; post; pruned; last_step} = diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli index 01f4023bd..13efd77c6 100644 --- a/infer/src/pulse/PulseTopl.mli +++ b/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. *) diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile index 7566e8907..7b60e4758 100644 --- a/infer/tests/codetoanalyze/java/topl/Makefile +++ b/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 diff --git a/infer/tests/codetoanalyze/java/topl/taint/Makefile b/infer/tests/codetoanalyze/java/topl/taint/Makefile new file mode 100644 index 000000000..220e5a3a8 --- /dev/null +++ b/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 diff --git a/infer/tests/codetoanalyze/java/topl/taint/Taint.java b/infer/tests/codetoanalyze/java/topl/taint/Taint.java new file mode 100644 index 000000000..98561779b --- /dev/null +++ b/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); + } +} diff --git a/infer/tests/codetoanalyze/java/topl/taint/Taint.topl b/infer/tests/codetoanalyze/java/topl/taint/Taint.topl new file mode 100644 index 000000000..a21bfe54c --- /dev/null +++ b/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 diff --git a/infer/tests/codetoanalyze/java/topl/taint/issues.exp b/infer/tests/codetoanalyze/java/topl/taint/issues.exp new file mode 100644 index 000000000..cd05cbb43 --- /dev/null +++ b/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.(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to StringBuilder.(),call to StringBuilder StringBuilder.append(String),call to String StringBuilder.toString(),call to void Taint.sendToDb(String)]