Writing errors for Threadsafe checker

Summary: when a method has writes to a field outside of synchrnoization, issue an appropriate error message identifying the fields

Reviewed By: sblackshear

Differential Revision: D4015612

fbshipit-source-id: 4f697fc

infer/src/base/Config.ml

@@ -1123,6 +1123,11 @@ and unsafe_malloc =
     ~exes:CLOpt.[Analyze]
     "Assume that malloc(3) never returns null."
 
+and thread_safety =
+  CLOpt.mk_bool ~long:"thread-safety"
+    ~exes:CLOpt.[Analyze]
+    "Run the experimental thread safety checker. (In conjunction with -a checkers)"
+
 and use_compilation_database =
   CLOpt.mk_symbol_opt ~long:"use-compilation-database"
     "Buck integration using the compilation database, with or without dependencies."
@@ -1488,6 +1493,7 @@ and trace_join = !trace_join
 and trace_rearrange = !trace_rearrange
 and type_size = !type_size
 and unsafe_malloc = !unsafe_malloc
+and thread_safety = !thread_safety
 and use_compilation_database = !use_compilation_database
 and whole_seconds = !whole_seconds
 and worklist_mode = !worklist_mode

infer/src/base/Config.mli

@@ -261,6 +261,7 @@ val trace_join : bool
 val trace_rearrange : bool
 val type_size : bool
 val unsafe_malloc : bool
+val thread_safety: bool
 val use_compilation_database : [ `Deps | `NoDeps ] option
 val whole_seconds : bool
 val worklist_mode : int

infer/src/checkers/ThreadSafety.ml

@@ -129,25 +129,28 @@ let make_results_table file_env =
   in
   map_post_computation_over_procs compute_post_for_procedure procs_to_analyze
 
+let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate =
+  let report_one_error access_path =
+    let description =
+      F.asprintf "Method %a writes to field %a outside of synchronization"
+        Procname.pp pname
+        AccessPath.pp_access_list access_path
+    in
+    Checkers.ST.report_error tenv
+      pname
+      pdesc
+      "CHECKERS_THREAD_SAFETY_WARNING"
+      (Cfg.Procdesc.get_loc pdesc)
+      description
+  in
+  IList.iter report_one_error (IList.map snd (PathDomain.elements writestate))
+
 (* For now, just checks if there is one active element amongst the posts of the analyzed methods.
    This indicates that the method races with itself. To be refined later. *)
-let process_results_table tab = (
+let process_results_table tab =
-  let finalresult =
+  ResultsTableType.iter   (* report errors for each method *)
-    ResultsTableType.for_all   (* check if writestate is empty for all postconditions*)
+    (fun proc_env ( _,( _, writestate)) -> report_thread_safety_errors proc_env writestate)
-      (fun _ ( _,( _, writestate)) -> (PathDomain.is_empty writestate)
-      )
     tab
-  in
-  if finalresult then
-    begin
-      L.stdout  "\n ***** \n THREADSAFE \n *****\n" ;
-      L.out  "\n ***** \n THREADSAFE \n *****\n"
-    end
-  else  begin
-    L.stdout  "\n ***** \n RACY \n *****\n" ;
-    L.out  "\n ***** \n RACY \n *****\n"
-  end
-)
 
 (* Currently we analyze if there is an @ThreadSafe annotation on at least one of
    the classes in a file. This might be tightened in future or even broadened in future
@@ -163,11 +166,9 @@ let should_analyze_file file_env =
   the results to check (approximation of) thread safety *)
 (* file_env: (Idenv.t * Tenv.t * Procname.t * Cfg.Procdesc.t) list *)
 let file_analysis _ _ _ file_env =
-  begin L.stdout "\n THREAD SAFETY CHECKER \n\n";
   if should_analyze_file file_env then
     process_results_table
       (make_results_table file_env)
-  end
 
       (*
     Todo:
@@ -175,6 +176,5 @@ let file_analysis _ _ _ file_env =
     1. Track line numbers of accesses
     2. Track protected writes and reads, too; if we have a write and a read where
     one is non-protected then we have potential race (including protected write, unprotected read
-    3. Output error message when potential race found
+    3. Lotsa other stuff
-    4. Lotsa other stuff
       *)

infer/src/checkers/accessPath.ml

@@ -148,14 +148,16 @@ let pp_base fmt (pvar, _) =
   Var.pp fmt pvar
 
 let pp_access fmt = function
-  | FieldAccess (field_name, _) -> F.fprintf fmt ".%a" Ident.pp_fieldname field_name
+  | FieldAccess (field_name, _) -> Ident.pp_fieldname fmt field_name
   | ArrayAccess _ -> F.fprintf fmt "[_]"
 
-let pp_raw fmt (base, accesses) =
 let pp_access_list fmt accesses =
-    let pp_sep _ _ = () in
+  let pp_sep _ _ = F.fprintf fmt "." in
-    F.pp_print_list ~pp_sep pp_access fmt accesses in
+  F.pp_print_list ~pp_sep pp_access fmt accesses
-  F.fprintf fmt "%a%a" pp_base base pp_access_list accesses
+
+let pp_raw fmt = function
+  | base, [] ->  pp_base fmt base
+  | base, accesses ->  F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses
 
 let pp fmt = function
   | Exact access_path -> pp_raw fmt access_path

infer/src/checkers/accessPath.mli

@@ -63,6 +63,8 @@ val is_prefix : raw -> raw -> bool
 
 val pp_access : Format.formatter -> access -> unit
 
+val pp_access_list : Format.formatter -> access list -> unit
+
 val pp_raw : Format.formatter -> raw -> unit
 
 val compare : t -> t -> int

infer/src/checkers/annotations.ml

@@ -127,9 +127,12 @@ let integrity_source = "IntegritySource"
 let integrity_sink = "IntegritySink"
 let guarded_by = "GuardedBy"
 let thread_safe = "ThreadSafe"
+let not_thread_safe = "NotThreadSafe"
 
+(* we don't want it to just end with ThreadSafe, because this falls
+   foul of the @NotThreadSafe annotation *)
 let ia_is_thread_safe ia =
-  ia_ends_with ia thread_safe
+  ia_ends_with ia thread_safe && not (ia_ends_with ia not_thread_safe)
 
 let ia_is_nullable ia =
   ia_ends_with ia nullable

infer/src/checkers/registerCheckers.ml

@@ -58,7 +58,7 @@ let active_procedure_checkers () =
 
 let active_cluster_checkers () =
   [(Checkers.callback_check_cluster_access, false, Some Config.Java);
-   (ThreadSafety.file_analysis, false, Some Config.Java)
+   (ThreadSafety.file_analysis, Config.checkers_enabled && Config.thread_safety, Some Config.Java)
   ]
 
 let register () =

infer/tests/codetoanalyze/java/checkers/Makefile

@@ -19,7 +19,9 @@ FILES = \
   FragmentRetainsViewExample.java \
   ImmutableCast.java \
   NoAllocationExample.java \
+  NotThreadSafeExample.java \
   PrintfArgsChecker.java \
+  ThreadSafeExample.java \
   TraceCallSequence.java \
   TwoCheckersExample.java
 
@@ -27,4 +29,4 @@ compile:
 	javac -cp $(CLASSPATH) $(FILES)
 
 analyze:
-	$(call silent_on_success,$(INFER_BIN) -a $(ANALYZER) -- javac -cp $(CLASSPATH) $(FILES))
+	$(call silent_on_success,$(INFER_BIN) --thread-safety -a $(ANALYZER) -- javac -cp $(CLASSPATH) $(FILES))

infer/tests/codetoanalyze/java/checkers/NotThreadSafeExample.java

@@ -0,0 +1,33 @@
+/*
+ * 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.
+ */
+
+package codetoanalyze.java.checkers;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Documented
+@Target(ElementType.TYPE)
+@Retention(RetentionPolicy.CLASS)
+@interface NotThreadSafe {
+}
+
+@NotThreadSafe
+public class NotThreadSafeExample{
+
+  Integer f;
+
+  public void tsBad() { /*Shouldn't report*/
+    f = 24;
+  }
+
+}

infer/tests/codetoanalyze/java/checkers/ThreadSafeExample.java

@@ -0,0 +1,39 @@
+/*
+ * 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.
+ */
+
+package codetoanalyze.java.checkers;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Documented
+@Target(ElementType.TYPE)
+@Retention(RetentionPolicy.CLASS)
+@interface ThreadSafe {
+}
+
+@ThreadSafe
+public class ThreadSafeExample{
+
+  Integer f;
+
+  public void tsOK() {
+    synchronized (this) {
+      f = 42;
+    }
+  }
+
+  public void tsBad() {
+    f = 24;
+  }
+
+}

infer/tests/codetoanalyze/java/checkers/issues.exp

@@ -32,5 +32,6 @@ PrintfArgsChecker.java, void PrintfArgsChecker.formatStringIsNotLiteral(PrintStr
 PrintfArgsChecker.java, void PrintfArgsChecker.notSuppressed(PrintStream), 1, CHECKERS_PRINTF_ARGS
 PrintfArgsChecker.java, void PrintfArgsChecker.stringInsteadOfInteger(PrintStream), 1, CHECKERS_PRINTF_ARGS
 PrintfArgsChecker.java, void PrintfArgsChecker.wrongNumberOfArguments(PrintStream), 1, CHECKERS_PRINTF_ARGS
+ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, CHECKERS_THREAD_SAFETY_WARNING
 TwoCheckersExample.java, List TwoCheckersExample.shouldRaiseImmutableCastError(), 0, CHECKERS_IMMUTABLE_CAST
 TwoCheckersExample.java, List TwoCheckersExample.shouldRaisePerformanceCriticalError(), 1, CHECKERS_CALLS_EXPENSIVE_METHOD