From 6423ec74ad6ea6ac8ff7dc71d35b66a2dda40bdb Mon Sep 17 00:00:00 2001 From: Peter O'Hearn Date: Fri, 14 Oct 2016 11:36:17 -0700 Subject: [PATCH] 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 | 6 +++ infer/src/base/Config.mli | 1 + infer/src/checkers/ThreadSafety.ml | 48 +++++++++---------- infer/src/checkers/accessPath.ml | 14 +++--- infer/src/checkers/accessPath.mli | 2 + infer/src/checkers/annotations.ml | 5 +- infer/src/checkers/registerCheckers.ml | 2 +- .../codetoanalyze/java/checkers/Makefile | 4 +- .../java/checkers/NotThreadSafeExample.java | 33 +++++++++++++ .../java/checkers/ThreadSafeExample.java | 39 +++++++++++++++ .../codetoanalyze/java/checkers/issues.exp | 1 + 11 files changed, 122 insertions(+), 33 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/checkers/NotThreadSafeExample.java create mode 100644 infer/tests/codetoanalyze/java/checkers/ThreadSafeExample.java diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index c92769242..67fcba03a 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 2e88206f6..0c99734a0 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index b7c3c5399..b05e035b8 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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 finalresult = - ResultsTableType.for_all (* check if writestate is empty for all postconditions*) - (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 -) +let process_results_table tab = + ResultsTableType.iter (* report errors for each method *) + (fun proc_env ( _,( _, writestate)) -> report_thread_safety_errors proc_env writestate) + tab (* 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 + if should_analyze_file file_env then + process_results_table + (make_results_table file_env) (* 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 - 4. Lotsa other stuff + 3. Lotsa other stuff *) diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 080734730..bbd86f101 100644 --- a/infer/src/checkers/accessPath.ml +++ b/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 - F.pp_print_list ~pp_sep pp_access fmt accesses in - F.fprintf fmt "%a%a" pp_base base pp_access_list accesses +let pp_access_list fmt accesses = + let pp_sep _ _ = F.fprintf fmt "." in + F.pp_print_list ~pp_sep pp_access fmt 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 diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index 815f0d249..684c4f433 100644 --- a/infer/src/checkers/accessPath.mli +++ b/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 diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index eedcd37f1..c04c9fd6c 100644 --- a/infer/src/checkers/annotations.ml +++ b/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 diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index fbb0de5fe..f42fbff58 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/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 () = diff --git a/infer/tests/codetoanalyze/java/checkers/Makefile b/infer/tests/codetoanalyze/java/checkers/Makefile index 352a57fd1..18cc092ec 100644 --- a/infer/tests/codetoanalyze/java/checkers/Makefile +++ b/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)) diff --git a/infer/tests/codetoanalyze/java/checkers/NotThreadSafeExample.java b/infer/tests/codetoanalyze/java/checkers/NotThreadSafeExample.java new file mode 100644 index 000000000..b97ea872e --- /dev/null +++ b/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; + } + +} diff --git a/infer/tests/codetoanalyze/java/checkers/ThreadSafeExample.java b/infer/tests/codetoanalyze/java/checkers/ThreadSafeExample.java new file mode 100644 index 000000000..46abf778d --- /dev/null +++ b/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; + } + +} diff --git a/infer/tests/codetoanalyze/java/checkers/issues.exp b/infer/tests/codetoanalyze/java/checkers/issues.exp index aa3027d6d..f83baca07 100644 --- a/infer/tests/codetoanalyze/java/checkers/issues.exp +++ b/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