[racerd] skeleton for testing access path stability

Reviewed By: peterogithub

Differential Revision: D6903439

fbshipit-source-id: 299db8e

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

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

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

infer/src/concurrency/RacerD.ml

@@ -962,7 +962,7 @@ 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
@@ -1030,11 +1030,16 @@ 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
+      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 ~default:"") )
+              , 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

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;
+  }
+}
+
+}

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;
+  }
+
+}
+
+}

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

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, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Interprocedural$Field.a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `&a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `&a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Intraprocedural$Field.a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `&a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,<Write trace>,access to `&a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`]