From 4799fb6b82269455f8b82767c5a9243f1d61f70a Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 21 Feb 2018 20:40:59 -0800 Subject: [PATCH] [racerd] skeleton for testing access path stability Reviewed By: peterogithub Differential Revision: D6903439 fbshipit-source-id: 299db8e --- Makefile | 2 +- infer/src/base/Config.ml | 7 ++ infer/src/base/Config.mli | 2 + infer/src/concurrency/RacerD.ml | 27 +++--- .../Interprocedural.java | 96 +++++++++++++++++++ .../Intraprocedural.java | 91 ++++++++++++++++++ .../java/racerd_path_stability/Makefile | 15 +++ .../java/racerd_path_stability/issues.exp | 5 + 8 files changed, 233 insertions(+), 12 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/racerd_path_stability/Interprocedural.java create mode 100644 infer/tests/codetoanalyze/java/racerd_path_stability/Intraprocedural.java create mode 100644 infer/tests/codetoanalyze/java/racerd_path_stability/Makefile create mode 100644 infer/tests/codetoanalyze/java/racerd_path_stability/issues.exp diff --git a/Makefile b/Makefile index 8029e168e..71db60f00 100644 --- a/Makefile +++ b/Makefile @@ -89,7 +89,7 @@ BUILD_SYSTEMS_TESTS += \ DIRECT_TESTS += \ java_checkers java_eradicate java_infer java_lab java_tracing java_quandary \ - java_racerd java_crashcontext + java_racerd java_racerd_path_stability java_crashcontext ifneq ($(ANT),no) BUILD_SYSTEMS_TESTS += ant endif diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index c50b8f4b8..5b7eeed76 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1644,6 +1644,11 @@ and quiet = "Do not print specs on standard output (default: only print for the $(b,report) command)" +and racerd_use_path_stability = + CLOpt.mk_bool ~long:"racerd-use-path-stability" ~default:false + "Use access path stability to prune RacerD false positives" + + and reactive = CLOpt.mk_bool ~deprecated:["reactive"] ~long:"reactive" ~short:'r' ~in_help:InferCommand.([(Analyze, manual_generic)]) @@ -2522,6 +2527,8 @@ and quiet = !quiet and racerd = !racerd +and racerd_use_path_stability = !racerd_use_path_stability + and reactive_mode = !reactive || InferCommand.(equal Diff) command and reactive_capture = !reactive_capture diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index b209797b9..3427efaaa 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -534,6 +534,8 @@ val quandary_sinks : Yojson.Basic.json val quiet : bool +val racerd_use_path_stability : bool + val reactive_mode : bool val reactive_capture : bool diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 9f8a6061a..391f8d860 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -962,13 +962,13 @@ let make_trace ~report_kind original_path pdesc = let ignore_var v = Var.is_global v || Var.is_return v (* Checking for a wobbly path *) -let contaminated_race_msg access wobbly_paths = +let get_contaminated_race_message access wobbly_paths = let open RacerDDomain in let wobbly_path_opt = match TraceElem.kind access with | TraceElem.Kind.Read access_path | Write access_path - (* Access paths rooted in static variables are always race-prone, + (* Access paths rooted in static variables are always race-prone, hence do not complain about contamination. *) when not (access_path |> fst |> fst |> ignore_var) -> let proper_prefix_path = AccessPath.truncate access_path in @@ -1030,15 +1030,20 @@ let report_thread_safety_violation tenv pdesc ~make_description ~report_kind acc (* why we are reporting it *) let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in let error_message = F.sprintf "%s%s" description explanation in - let contaminated = contaminated_race_msg access wobbly_paths in - let exn = - Exceptions.Checkers - ( issue_type - , Localise.verbatim_desc (error_message ^ Option.value contaminated ~default:"") ) - in - let end_locs = Option.to_list original_end @ Option.to_list conflict_end in - let access = IssueAuxData.encode (pname, access, end_locs) in - Reporting.log_error_deprecated ~store_summary:true pname ~loc ~ltr ~access exn + match get_contaminated_race_message access wobbly_paths with + | Some _ when Config.racerd_use_path_stability -> + (* don't report races on unstable paths when use_path_stability is on *) + () + | contaminated_message_opt -> + let exn = + Exceptions.Checkers + ( issue_type + , Localise.verbatim_desc + (error_message ^ Option.value contaminated_message_opt ~default:"") ) + in + let end_locs = Option.to_list original_end @ Option.to_list conflict_end in + let access = IssueAuxData.encode (pname, access, end_locs) in + Reporting.log_error_deprecated ~store_summary:true pname ~loc ~ltr ~access exn in let trace_of_pname = trace_of_pname access pdesc in Option.iter ~f:report_one_path (PathDomain.get_reportable_sink_path access ~trace_of_pname) diff --git a/infer/tests/codetoanalyze/java/racerd_path_stability/Interprocedural.java b/infer/tests/codetoanalyze/java/racerd_path_stability/Interprocedural.java new file mode 100644 index 000000000..c1d12a446 --- /dev/null +++ b/infer/tests/codetoanalyze/java/racerd_path_stability/Interprocedural.java @@ -0,0 +1,96 @@ +/* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package codetoanalyze.java.checkers; + +import com.facebook.infer.annotation.ThreadSafe; + +class Interprocedural { + +static class A { + B f = new B(); + int h = 0; +} + +static class B { + int g = 0; +} + +@ThreadSafe +static class Field { + private A a = new A(); + + private void destabilize() { + B b = a.f; + } + + public void unstable_ok() { + int x = 42; + destabilize(); + synchronized (this){ + a.f.g = 101; + } + x = a.f.g; + } + + public void stable_bad() { + int x = 42; + synchronized (this){ + a.f.g = 101; + } + x = a.f.g; + } + +} + +@ThreadSafe +static class Param { + + private void destabilize(A z) { + B b1 = z.f; + System.out.println(b1); + } + + public void unstable_ok(A a) { + int x = 42; + destabilize(a); + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } + + public void stable_bad(A a) { + int x = 42; + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } + +} + +@ThreadSafe +static class Param2 { + + private void destabilize(A z) { + // Do nothing + } + + public void stable_bad(A a) { + int x = 42; + destabilize(a); // a leaks, but shouldn't be de-stabilized because callee does nothing + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } +} + +} diff --git a/infer/tests/codetoanalyze/java/racerd_path_stability/Intraprocedural.java b/infer/tests/codetoanalyze/java/racerd_path_stability/Intraprocedural.java new file mode 100644 index 000000000..a419c020d --- /dev/null +++ b/infer/tests/codetoanalyze/java/racerd_path_stability/Intraprocedural.java @@ -0,0 +1,91 @@ +/* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package codetoanalyze.java.checkers; + +import com.facebook.infer.annotation.ThreadSafe; + +class Intraprocedural { + +static class B { + int g = 0; +} + +static class A { + B f = new B(); + int h = 0; +} + +@ThreadSafe +static class Field { + private A a = new A(); + + public void unstable_ok() { + int x = 42; + B b = a.f; // destabilizes + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } + + public void stable_bad() { + int x = 42; + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } +} + +static class Param { + + public void unstable_ok(A a) { + int x = 42; + B b = a.f; // destabilizes + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } + + public void stable_bad(A a) { + int x = 42; + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } + +} + +@ThreadSafe +static class Global { + private static A a = new A(); + + synchronized public A getA() { + return a; + } + + synchronized public void setA(A newA) { + a = newA; + } + + public void unstable_ok() { + int x = 42; + A a = getA(); // destabilizes + synchronized (this) { + a.f.g = 101; + } + x = a.f.g; + } + +} + +} diff --git a/infer/tests/codetoanalyze/java/racerd_path_stability/Makefile b/infer/tests/codetoanalyze/java/racerd_path_stability/Makefile new file mode 100644 index 000000000..476e5f2c3 --- /dev/null +++ b/infer/tests/codetoanalyze/java/racerd_path_stability/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2016 - present Facebook, Inc. +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +INFER_OPTIONS = --racerd-only --debug-exceptions --racerd-use-path-stability +INFERPRINT_OPTIONS = --issues-tests +SOURCES = $(wildcard *.java) + +include $(TESTS_DIR)/javac.make diff --git a/infer/tests/codetoanalyze/java/racerd_path_stability/issues.exp b/infer/tests/codetoanalyze/java/racerd_path_stability/issues.exp new file mode 100644 index 000000000..8c7ec92a1 --- /dev/null +++ b/infer/tests/codetoanalyze/java/racerd_path_stability/issues.exp @@ -0,0 +1,5 @@ +codetoanalyze/java/racerd_path_stability/Interprocedural.java, void Interprocedural$Field.stable_bad(), 5, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Interprocedural$Field.a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,,access to `&this.codetoanalyze.java.checkers.Interprocedural$Field.a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`] +codetoanalyze/java/racerd_path_stability/Interprocedural.java, void Interprocedural$Param.stable_bad(Interprocedural$A), 5, THREAD_SAFETY_VIOLATION, [,access to `&a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,,access to `&a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`] +codetoanalyze/java/racerd_path_stability/Interprocedural.java, void Interprocedural$Param2.stable_bad(Interprocedural$A), 6, THREAD_SAFETY_VIOLATION, [,access to `&a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,,access to `&a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`] +codetoanalyze/java/racerd_path_stability/Intraprocedural.java, void Intraprocedural$Field.stable_bad(), 5, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Intraprocedural$Field.a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,,access to `&this.codetoanalyze.java.checkers.Intraprocedural$Field.a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`] +codetoanalyze/java/racerd_path_stability/Intraprocedural.java, void Intraprocedural$Param.stable_bad(Intraprocedural$A), 5, THREAD_SAFETY_VIOLATION, [,access to `&a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,,access to `&a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`]