[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

@@ -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)

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).

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).

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"

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"

infer/src/base/Checker.mli

@@ -32,6 +32,7 @@ type t =
   | SIOF
   | SelfInBlock
   | Starvation
+  | TOPL
   | Uninit
 [@@deriving equal, enumerate]
 

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 =

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

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)

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)

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)

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
 

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)

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)