From f8e71ceb1ef851b1c0c6de6b846063f0751d53db Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 19 May 2020 03:56:28 -0700 Subject: [PATCH] [topl] make TOPL its own checker Summary: This seems to make sense as it's a separate analysis (that depends on biabduction). This introduces unpleasant `|| is_checker_enabled TOPL` whenever we try to figure out if biabduction will run. I think this is a more general problem that deserves a more general solution to express the fact that checkers can depend on others, so that, eg, `is_checker_enabled Purity` is true when we pass `--loop-hoisting`. Will address in another diff. Reviewed By: ngorogiannis Differential Revision: D21618460 fbshipit-source-id: 8b0c9a015 --- infer/man/man1/infer-analyze.txt | 7 +++++++ infer/man/man1/infer-full.txt | 7 +++++++ infer/man/man1/infer.txt | 7 +++++++ infer/src/backend/registerCheckers.ml | 6 ++++-- infer/src/base/Checker.ml | 8 ++++++++ infer/src/base/Checker.mli | 1 + infer/src/base/Config.ml | 2 +- infer/src/biabduction/errdesc.ml | 2 +- infer/tests/codetoanalyze/java/topl/baos/Makefile | 2 +- infer/tests/codetoanalyze/java/topl/compareArgs/Makefile | 2 +- infer/tests/codetoanalyze/java/topl/hasnext/Makefile | 2 +- infer/tests/codetoanalyze/java/topl/servlet/Makefile | 2 +- infer/tests/codetoanalyze/java/topl/skip/Makefile | 2 +- infer/tests/codetoanalyze/java/topl/slowIter/Makefile | 2 +- 14 files changed, 42 insertions(+), 10 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 94f4ad9e4..388da23e0 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -328,6 +328,13 @@ OPTIONS Activates: Enable --starvation and disable all other checkers (Conversely: --no-starvation-only) + --topl + Activates: TOPL (Conversely: --no-topl) + + --topl-only + Activates: Enable --topl and disable all other checkers + (Conversely: --no-topl-only) + --no-uninit Deactivates: checker for use of uninitialized values (Conversely: --uninit) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 9e8d3fb9d..86fcabb94 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1079,6 +1079,13 @@ OPTIONS Specify custom annotations that should be considered aliases of @ThreadSafe See also infer-analyze(1). + --topl + Activates: TOPL (Conversely: --no-topl) See also infer-analyze(1). + + --topl-only + Activates: Enable --topl and disable all other checkers + (Conversely: --no-topl-only) See also infer-analyze(1). + --no-uninit Deactivates: checker for use of uninitialized values (Conversely: --uninit) See also infer-analyze(1). diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 00b5056fd..4a7d03499 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1079,6 +1079,13 @@ OPTIONS Specify custom annotations that should be considered aliases of @ThreadSafe See also infer-analyze(1). + --topl + Activates: TOPL (Conversely: --no-topl) See also infer-analyze(1). + + --topl-only + Activates: Enable --topl and disable all other checkers + (Conversely: --no-topl-only) See also infer-analyze(1). + --no-uninit Deactivates: checker for use of uninitialized values (Conversely: --uninit) See also infer-analyze(1). diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index 3b6605c34..698761043 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -210,11 +210,13 @@ let all_checkers = in [(bo_analysis, Clang); (bo_analysis, Java)] ) } ; { name= "biabduction" - ; active= Config.is_checker_enabled Biabduction + ; active= Config.(is_checker_enabled Biabduction || is_checker_enabled TOPL) ; callbacks= (let biabduction = dynamic_dispatch Payloads.Fields.biabduction - (Topl.instrument_callback Interproc.analyze_procedure) + ( if Config.is_checker_enabled TOPL then + Topl.instrument_callback Interproc.analyze_procedure + else Interproc.analyze_procedure ) in [(biabduction, Clang); (biabduction, Java)] ) } ; { name= "annotation reachability" diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml index 109c831c0..3cd23f8e6 100644 --- a/infer/src/base/Checker.ml +++ b/infer/src/base/Checker.ml @@ -32,6 +32,7 @@ type t = | SIOF | SelfInBlock | Starvation + | TOPL | Uninit [@@deriving equal, enumerate] @@ -242,6 +243,13 @@ let config checker = ; cli_flag= "starvation" ; enabled_by_default= true ; cli_deprecated_flags= [] } + | TOPL -> + { support= supports_clang_and_java_experimental + ; short_documentation= "TOPL" + ; show_in_help= true + ; cli_flag= "topl" + ; enabled_by_default= false + ; cli_deprecated_flags= [] } | Uninit -> { support= supports_clang ; short_documentation= "checker for use of uninitialized values" diff --git a/infer/src/base/Checker.mli b/infer/src/base/Checker.mli index e4b0178ad..9e5f4ce3f 100644 --- a/infer/src/base/Checker.mli +++ b/infer/src/base/Checker.mli @@ -32,6 +32,7 @@ type t = | SIOF | SelfInBlock | Starvation + | TOPL | Uninit [@@deriving equal, enumerate] diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index edd0e3a78..03b4fe8b3 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -3116,7 +3116,7 @@ let clang_frontend_action_string = a call to unknown code and true triggers lazy dynamic dispatch. The latter mode follows the JVM semantics and creates procedure descriptions during symbolic execution using the type information found in the abstract state *) -let dynamic_dispatch = is_checker_enabled Biabduction +let dynamic_dispatch = is_checker_enabled Biabduction || is_checker_enabled TOPL (** Check if a Java package is external to the repository *) let java_package_is_external package = diff --git a/infer/src/biabduction/errdesc.ml b/infer/src/biabduction/errdesc.ml index 029a9d6c0..2fa42c115 100644 --- a/infer/src/biabduction/errdesc.ml +++ b/infer/src/biabduction/errdesc.ml @@ -135,7 +135,7 @@ let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t opti in Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags)) | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Var id0} - when Config.is_checker_enabled Biabduction + when Config.(is_checker_enabled Biabduction || is_checker_enabled TOPL) && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) -> (* this case is a hack to make bucketing continue to work in the presence of copy diff --git a/infer/tests/codetoanalyze/java/topl/baos/Makefile b/infer/tests/codetoanalyze/java/topl/baos/Makefile index 850a34195..9ecf9d0e5 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/Makefile +++ b/infer/tests/codetoanalyze/java/topl/baos/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 13000 --topl-properties baos.topl --biabduction-only +INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 13000 --topl-properties baos.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile index 625a25205..d4310ee32 100644 --- a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile +++ b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 4000 --topl-properties CompareArgs.topl --biabduction-only +INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 4000 --topl-properties CompareArgs.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile index 96be96b4a..20a3377e6 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile +++ b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 10000 --topl-properties hasnext.topl --biabduction-only +INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 10000 --topl-properties hasnext.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/servlet/Makefile b/infer/tests/codetoanalyze/java/topl/servlet/Makefile index 7e798fdb0..efde7f746 100644 --- a/infer/tests/codetoanalyze/java/topl/servlet/Makefile +++ b/infer/tests/codetoanalyze/java/topl/servlet/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 20 --symops-per-iteration 60000 --topl-properties servlet.topl --biabduction-only +INFER_OPTIONS = --seconds-per-iteration 20 --symops-per-iteration 60000 --topl-properties servlet.topl --topl-only INFERPRINT_OPTIONS = --issues-tests TEST_CLASSPATH = javax.servlet-api-4.0.1.jar diff --git a/infer/tests/codetoanalyze/java/topl/skip/Makefile b/infer/tests/codetoanalyze/java/topl/skip/Makefile index 795e0d705..ba90bf5f9 100644 --- a/infer/tests/codetoanalyze/java/topl/skip/Makefile +++ b/infer/tests/codetoanalyze/java/topl/skip/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 100000 --topl-properties SkipAfterRemove.topl --biabduction-only +INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 100000 --topl-properties SkipAfterRemove.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile index b36e06160..168faf803 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile +++ b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 20000 --topl-properties slowIter.topl --biabduction-only +INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 20000 --topl-properties slowIter.topl --topl-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java)