Bug 1479503: Check infer in ./mach static-analysis autotest.
authorRobert Bartlensky <rbartlensky@mozilla.com>
Thu, 02 Aug 2018 10:53:15 +0100
changeset 1657237 95e2c5fd3e3c8a8c24ace37a89218029ce17426a
parent 1657236 2cce3174b35b432e951b781accb36beed35cd370
child 1657238 4bfb163099e3c0cc2072a1f3736c268a7f3ed48f
push id288945
push userrbartlensky@mozilla.com
push dateFri, 03 Aug 2018 10:35:38 +0000
treeherdertry@4bfb163099e3 [default view] [failures only]
bugs1479503
milestone63.0a1
Bug 1479503: Check infer in ./mach static-analysis autotest. MozReview-Commit-ID: JxdoprwvXRY
python/mozbuild/mozbuild/mach_commands.py
settings.gradle
taskcluster/ci/static-analysis-autotest/kind.yml
tools/infer/config.yaml
tools/infer/test/Biabduction.java
tools/infer/test/Biabduction.json
tools/infer/test/Checkers.java
tools/infer/test/Checkers.json
tools/infer/test/Eradicate.java
tools/infer/test/Racerd.java
tools/infer/test/Racerd.json
tools/infer/test/Starvation.java
tools/infer/test/Starvation.json
tools/infer/test/build.gradle
--- a/python/mozbuild/mozbuild/mach_commands.py
+++ b/python/mozbuild/mozbuild/mach_commands.py
@@ -1883,72 +1883,47 @@ class StaticAnalysis(MachCommandBase):
     @CommandArgument('checker_names', nargs='*', default=[],
                      help='Checkers that are going to be auto-tested.')
     def autotest(self, verbose=False, dump_results=False, intree_tool=False, checker_names=[]):
         # If 'dump_results' is True than we just want to generate the issues files for each
         # checker in particulat and thus 'force_download' becomes 'False' since we want to
         # do this on a local trusted clang-tidy package.
         self._set_log_level(verbose)
         self._dump_results = dump_results
-
-        force_download = True
-
-        if self._dump_results:
-            force_download = False
+        force_download = False if self._dump_results else True
 
         # Function return codes
         self.TOOLS_SUCCESS = 0
         self.TOOLS_FAILED_DOWNLOAD = 1
         self.TOOLS_UNSUPORTED_PLATFORM = 2
         self.TOOLS_CHECKER_NO_TEST_FILE = 3
         self.TOOLS_CHECKER_RETURNED_NO_ISSUES = 4
         self.TOOLS_CHECKER_RESULT_FILE_NOT_FOUND = 5
         self.TOOLS_CHECKER_DIFF_FAILED = 6
         self.TOOLS_CHECKER_NOT_FOUND = 7
 
-        # Configure the tree or download clang-tidy package, depending on the option that we choose
-        if intree_tool:
-            _, config, _ = self._get_config_environment()
-            clang_tools_path = self.topsrcdir
-            self._clang_tidy_path = mozpath.join(
-                clang_tools_path, "clang", "bin",
-                "clang-tidy" + config.substs.get('BIN_SUFFIX', ''))
-            self._clang_format_path = mozpath.join(
-                clang_tools_path, "clang", "bin",
-                "clang-format" + config.substs.get('BIN_SUFFIX', ''))
-            self._clang_apply_replacements = mozpath.join(
-                clang_tools_path, "clang", "bin",
-                "clang-apply-replacements" + config.substs.get('BIN_SUFFIX', ''))
-            self._run_clang_tidy_path = mozpath.join(clang_tools_path, "clang", "share",
-                                                     "clang", "run-clang-tidy.py")
-            self._clang_format_diff = mozpath.join(clang_tools_path, "clang", "share",
-                                                   "clang", "clang-format-diff.py")
-
-            # Ensure that clang-tidy is present
-            rc = not os.path.exists(self._clang_tidy_path)
-        else:
-            rc = self._get_clang_tools(force=force_download, verbose=verbose)
-
+        rc = self._get_clang_tools(force=force_download, verbose=verbose, intree_tool=intree_tool)
         if rc != 0:
             self.log(logging.ERROR, 'ERROR: static-analysis', {},
                      'clang-tidy unable to locate package.')
             return self.TOOLS_FAILED_DOWNLOAD
 
         self._clang_tidy_base_path = mozpath.join(self.topsrcdir, "tools", "clang-tidy")
 
         # For each checker run it
         f = open(mozpath.join(self._clang_tidy_base_path, "config.yaml"))
         import yaml
         config = yaml.safe_load(f)
         platform, _ = self.platform
 
         if platform not in config['platforms']:
             self.log(logging.ERROR, 'static-analysis', {},
-                     "RUNNING: clang-tidy autotest for platform {} not supported.".format(platform))
-            return TOOLS_UNSUPORTED_PLATFORM
+                     "RUNNING: clang-tidy autotest for platform {} not supported."
+                     .format(platform))
+            return self.TOOLS_UNSUPORTED_PLATFORM
 
         import concurrent.futures
         import multiprocessing
         import shutil
 
         max_workers = multiprocessing.cpu_count()
 
         self.log(logging.INFO, 'static-analysis', {},
@@ -1982,38 +1957,142 @@ class StaticAnalysis(MachCommandBase):
                 if ret_val != self.TOOLS_SUCCESS:
                     # Also delete the tmp folder
                     shutil.rmtree(self._compilation_commands_path)
                     return ret_val
 
         self.log(logging.INFO, 'static-analysis', {}, "SUCCESS: clang-tidy all tests passed.")
         # Also delete the tmp folder
         shutil.rmtree(self._compilation_commands_path)
-        return self.TOOLS_SUCCESS
+        return self._autotest_infer(intree_tool, force_download, verbose)
 
     def _create_temp_compilation_db(self, config):
         directory = tempfile.mkdtemp(prefix='cc')
         with open(mozpath.join(directory, "compile_commands.json"), "wb") as file_handler:
             compile_commands = []
             director = mozpath.join(self.topsrcdir, 'tools', 'clang-tidy', 'test')
             for item in config['clang_checkers']:
                 if item['name'] in ['-*', 'mozilla-*']:
                     continue
                 file = item['name'] + '.cpp'
                 element = {}
                 element["directory"] = director
-                element["command"] = 'cpp '+ file
+                element["command"] = 'cpp ' + file
                 element["file"] = mozpath.join(director, file)
                 compile_commands.append(element)
 
             json.dump(compile_commands, file_handler)
             file_handler.flush()
 
             return directory
 
+    def _autotest_infer(self, intree_tool, force_download, verbose):
+        # infer is not available on other platforms, but autotest should work even without
+        # it being installed
+        if self.platform[0] == 'linux64' and self.substs['MOZ_BUILD_APP'] == 'mobile/android':
+            rc = self._get_infer(force=force_download, verbose=verbose, intree_tool=intree_tool)
+            if rc != 0:
+                self.log(logging.ERROR, 'ERROR: static-analysis', {},
+                         'infer unable to locate package.')
+                return self.TOOLS_FAILED_DOWNLOAD
+            # clean previous autotest if it exists
+            gradlew = mozpath.join(self.topsrcdir, 'gradlew')
+            devnull = open(os.devnull, 'w')
+            subprocess.call([gradlew, 'test_infer:clean'], stdout=devnull,
+                            stderr=subprocess.STDOUT, close_fds=True)
+            import concurrent.futures
+            import multiprocessing
+            max_workers = multiprocessing.cpu_count()
+            import yaml
+            with open(mozpath.join(self.topsrcdir, 'tools', 'infer', 'config.yaml')) as f:
+                config = yaml.safe_load(f)
+            with concurrent.futures.ThreadPoolExecutor(max_workers=max_workers) as executor:
+                futures = []
+                for item in config['infer_checkers']:
+                    if item['publish']:
+                        futures.append(executor.submit(self._verify_infer_checker, item))
+                # this is always included in check-java, but not in config.yaml
+                futures.append(executor.submit(self._verify_infer_checker,
+                                               {'name': 'checkers'}))
+                for future in concurrent.futures.as_completed(futures):
+                    ret_val = future.result()
+                    if ret_val != self.TOOLS_SUCCESS:
+                        return ret_val
+            self.log(logging.INFO, 'static-analysis', {}, "SUCCESS: infer all tests passed.")
+        return self.TOOLS_SUCCESS
+
+    def _verify_infer_checker(self, item):
+        def to_camelcase(str):
+            return ''.join([s.capitalize() for s in str.split('-')])
+        check = item['name']
+        test_file_path = mozpath.join(self.topsrcdir, 'tools',
+                                      'infer', 'test', to_camelcase(check))
+        test_file_path_java = test_file_path + '.java'
+        test_file_path_json = test_file_path + '.json'
+
+        self.log(logging.INFO, 'static-analysis', {},
+                 "RUNNING: infer check {}.".format(check))
+        # Verify if the test file exists for this checker
+        if not os.path.exists(test_file_path_java):
+            self.log(logging.ERROR, 'static-analysis', {},
+                     "ERROR: infer check {} doesn't have a test file.".format(check))
+            return self.TOOLS_CHECKER_NO_TEST_FILE
+        # run infer on a particular test file
+        gradlew = mozpath.join(self.topsrcdir, 'gradlew')
+        out_folder = mozpath.join(self.topsrcdir, 'test-infer-{}'.format(check))
+        if check == 'checkers':
+            check_arg = ['-a', 'checkers']
+        else:
+            check_arg = ['--{}-only'.format(check)]
+        devnull = open(os.devnull, 'w')
+        subprocess.call([self._infer_path, 'run'] + check_arg +
+                        ['-o', out_folder, '--', gradlew,
+                         'compileInferTest{}'.format(to_camelcase(check))],
+                        stdout=devnull, stderr=subprocess.STDOUT, close_fds=True)
+        import json
+        issues = json.load(open(mozpath.join(out_folder, 'report.json')))
+        # remove folder that infer creates because the issues are loaded into memory
+        import shutil
+        shutil.rmtree(out_folder)
+        # Verify to see if we got any issues, if not raise exception
+        if not issues:
+            self.log(
+                logging.ERROR, 'static-analysis', {},
+                "ERROR: infer check {0} did not find any issues in its associated test suite."
+                .format(check)
+            )
+            return self.TOOLS_CHECKER_RETURNED_NO_ISSUES
+        if self._dump_results:
+            self._build_autotest_result(test_file_path_json, issues)
+        else:
+            if not os.path.exists(test_file_path_json):
+                # Result file for test not found maybe regenerate it?
+                self.log(
+                    logging.ERROR, 'static-analysis', {},
+                    "ERROR: infer result file not found for check {0}".format(check)
+                )
+                return self.TOOLS_CHECKER_RESULT_FILE_NOT_FOUND
+            # Read the pre-determined issues
+            baseline_issues = self._get_autotest_stored_issues(test_file_path_json)
+
+            def ordered(obj):
+                if isinstance(obj, dict):
+                    return sorted((k, ordered(v)) for k, v in obj.items())
+                if isinstance(obj, list):
+                    return sorted(ordered(x) for x in obj)
+                return obj
+            # Compare the two lists
+            if ordered(issues) != ordered(baseline_issues):
+                self.log(
+                    logging.ERROR, 'static-analysis', {},
+                    "ERROR: infer auto-test failed for checker {0} Expected: {1} Got: {2}"
+                    .format(check, baseline_issues, issues))
+                return self.TOOLS_CHECKER_DIFF_FAILED
+        return self.TOOLS_SUCCESS
+
     @StaticAnalysisSubCommand('static-analysis', 'install',
                               'Install the static analysis helper tool')
     @CommandArgument('source', nargs='?', type=str,
                      help='Where to fetch a local archive containing the static-analysis and '
                      'format helper tool.'
                           'It will be installed in ~/.mozbuild/clang-tools and ~/.mozbuild/infer.'
                           'Can be omitted, in which case the latest clang-tools and infer '
                           'helper for the platform would be automatically detected and installed.')
@@ -2259,36 +2338,39 @@ class StaticAnalysis(MachCommandBase):
         # Converts all the paths to absolute pathnames
         tmp_path = []
         for f in paths:
             tmp_path.append(os.path.abspath(f))
         return tmp_path
 
     def _get_clang_tools(self, force=False, skip_cache=False,
                          source=None, download_if_needed=True,
-                         verbose=False):
+                         verbose=False, intree_tool=False):
         rc, config, _ = self._get_config_environment()
 
         if rc != 0:
             return rc
 
-        clang_tools_path = mozpath.join(self._mach_context.state_dir, "clang-tools")
+        clang_tools_path = self.topsrcdir if intree_tool else \
+            mozpath.join(self._mach_context.state_dir, "clang-tools")
         self._clang_tidy_path = mozpath.join(clang_tools_path, "clang", "bin",
                                              "clang-tidy" + config.substs.get('BIN_SUFFIX', ''))
         self._clang_format_path = mozpath.join(
             clang_tools_path, "clang", "bin",
             "clang-format" + config.substs.get('BIN_SUFFIX', ''))
         self._clang_apply_replacements = mozpath.join(
             clang_tools_path, "clang", "bin",
             "clang-apply-replacements" + config.substs.get('BIN_SUFFIX', ''))
         self._run_clang_tidy_path = mozpath.join(clang_tools_path, "clang", "share", "clang",
                                                  "run-clang-tidy.py")
         self._clang_format_diff = mozpath.join(clang_tools_path, "clang", "share", "clang",
                                                "clang-format-diff.py")
-
+        if intree_tool:
+            # Ensure that clang-tidy is present
+            return not os.path.exists(self._clang_tidy_path)
         if os.path.exists(self._clang_tidy_path) and \
            os.path.exists(self._clang_format_path) and \
            os.path.exists(self._clang_apply_replacements) and \
            os.path.exists(self._run_clang_tidy_path) and \
            not force:
             return 0
         else:
             if os.path.isdir(clang_tools_path) and download_if_needed:
@@ -2379,25 +2461,27 @@ class StaticAnalysis(MachCommandBase):
                         continue  # empty or comment
                     magics = ['exclude']
                     if pattern.startswith('^'):
                         magics += ['top']
                         pattern = pattern[1:]
                     args += [':({0}){1}'.format(','.join(magics), pattern)]
         return args
 
-    def _get_infer(self, force=False, skip_cache=False,
-                   download_if_needed=True, verbose=False):
+    def _get_infer(self, force=False, skip_cache=False, download_if_needed=True,
+                   verbose=False, intree_tool=False):
         rc, config, _ = self._get_config_environment()
         if rc != 0:
             return rc
-        infer_path = mozpath.join(self._mach_context.state_dir, 'infer')
-        self._infer_path = mozpath.join(infer_path, 'infer', 'bin',
-                                        'infer' +
+        infer_path = self.topsrcdir if intree_tool else \
+            mozpath.join(self._mach_context.state_dir, 'infer')
+        self._infer_path = mozpath.join(infer_path, 'infer', 'bin', 'infer' +
                                         config.substs.get('BIN_SUFFIX', ''))
+        if intree_tool:
+            return not os.path.exists(self._infer_path)
         if os.path.exists(self._infer_path) and not force:
             return 0
         else:
             if os.path.isdir(infer_path) and download_if_needed:
                 # The directory exists, perhaps it's corrupted?  Delete it
                 # and start from scratch.
                 import shutil
                 shutil.rmtree(infer_path)
--- a/settings.gradle
+++ b/settings.gradle
@@ -30,23 +30,25 @@ if (json.substs.MOZ_BUILD_APP != 'mobile
 System.setProperty('android.home', json.substs.ANDROID_SDK_ROOT)
 
 include ':annotations'
 include ':app'
 include ':geckoview'
 include ':geckoview_example'
 include ':omnijar'
 include ':thirdparty'
+// include ':test_infer'
 
 project(':annotations').projectDir = new File("${json.topsrcdir}/mobile/android/annotations")
 project(':app').projectDir = new File("${json.topsrcdir}/mobile/android/app")
 project(':geckoview').projectDir = new File("${json.topsrcdir}/mobile/android/geckoview")
 project(':geckoview_example').projectDir = new File("${json.topsrcdir}/mobile/android/geckoview_example")
 project(':omnijar').projectDir = new File("${json.topsrcdir}/mobile/android/app/omnijar")
 project(':thirdparty').projectDir = new File("${json.topsrcdir}/mobile/android/thirdparty")
+// project(':test_infer').projectDir = new File("${json.topsrcdir}/tools/infer/test")
 
 // The Gradle instance is shared between settings.gradle and all the
 // other build.gradle files (see
 // http://forums.gradle.org/gradle/topics/define_extension_properties_from_settings_xml).
 // We use this ext property to pass the per-object-directory mozconfig
 // between scripts.  This lets us execute set-up code before we gradle
 // tries to configure the project even once, and as a side benefit
 // saves invoking |mach environment| multiple times.
--- a/taskcluster/ci/static-analysis-autotest/kind.yml
+++ b/taskcluster/ci/static-analysis-autotest/kind.yml
@@ -48,16 +48,68 @@ jobs:
         toolchains:
             - linux64-clang
             - linux64-clang-tidy
             - linux64-infer
             - linux64-rust
             - linux64-sccache
             - linux64-node
 
+    android-api-16-st-autotest/debug:
+        description: "Android 4.0 api-16+ Debug"
+        index:
+            product: mobile
+            job-name: android-api-16-st-autotest-debug
+        treeherder:
+            platform: android-4-0-armv7-api16/debug
+            symbol: Sa
+        worker-type: aws-provisioner-v1/gecko-{level}-b-android
+        worker:
+            docker-image: {in-tree: android-build}
+            max-run-time: 7200
+            env:
+                GRADLE_USER_HOME: "/builds/worker/workspace/build/src/mobile/android/gradle/dotgradle-offline"
+                TOOLTOOL_MANIFEST: "mobile/android/config/tooltool-manifests/android/releng.manifest"
+            artifacts:
+                - name: public/android/R
+                  path: /builds/worker/workspace/build/src/obj-firefox/gradle/build/mobile/android/app/R
+                  type: directory
+                - name: public/android/maven
+                  path: /builds/worker/workspace/build/src/obj-firefox/gradle/build/mobile/android/geckoview/maven/
+                  type: directory
+                - name: public/build/geckoview-androidTest.apk
+                  path: /builds/worker/workspace/build/src/obj-firefox/gradle/build/mobile/android/geckoview/outputs/apk/androidTest/officialWithGeckoBinariesNoMinApi/debug/geckoview-official-withGeckoBinaries-noMinApi-debug-androidTest.apk
+                  type: file
+                - name: public/build/geckoview_example.apk
+                  path: /builds/worker/workspace/build/src/obj-firefox/gradle/build/mobile/android/geckoview_example/outputs/apk/officialWithGeckoBinariesNoMinApi/debug/geckoview_example-official-withGeckoBinaries-noMinApi-debug.apk
+                  type: file
+                - name: public/build
+                  path: /builds/worker/artifacts/
+                  type: directory
+        run:
+            using: mozharness
+            actions: [get-secrets build multi-l10n update static-analysis-autotest]
+            config:
+                - builds/releng_base_android_64_builds.py
+            script: "mozharness/scripts/fx_desktop_build.py"
+            secrets: true
+            custom-build-variant-cfg: api-16-debug
+            tooltool-downloads: internal
+        toolchains:
+            - android-gradle-dependencies
+            - android-ndk-linux
+            - android-sdk-linux
+            - linux64-clang
+            - linux64-rust-android
+            - linux64-rust-size
+            - linux64-sccache
+            - linux64-node
+            - linux64-infer
+            - linux64-clang-tidy
+
     win64-st-autotest/debug:
         description: "Win64 Debug Static Analysis Autotest"
         index:
             job-name: win64-st-autotest-debug
         treeherder:
             platform: windows2012-64/debug
             tier: 2
         worker-type: aws-provisioner-v1/gecko-{level}-b-win2012
--- a/tools/infer/config.yaml
+++ b/tools/infer/config.yaml
@@ -1,23 +1,31 @@
 ---
 target: obj-x86_64-pc-linux-gnu
 # It is used by 'mach static-analysis' and 'mozreview static-analysis bot'
 # in order to have consistency across the used checkers.
 platforms:
   - linux64
 infer_checkers:
+  # no issues were ever trigger by this
   - name: check-nullable
+    publish: !!bool no
+  - name: biabduction
     publish: !!bool yes
+  # very very noisy
+  # it could be useful, but it won't be part of the default enabled checkers
   - name: eradicate
     publish: !!bool no
+  # hard to use, not useful
   - name: quandary
-    publish: !!bool yes
+    publish: !!bool no
   - name: starvation
     publish: !!bool yes
+  # experimental
   - name: litho
-    publish: !!bool yes
+    publish: !!bool no
   - name: racerd
     publish: !!bool yes
+  # I think this is only for c++, can't trigger these errors in Java
   - name: liveness
-    publish: !!bool yes
+    publish: !!bool no
 # Third party files from mozilla-central
 third_party: tools/rewriting/ThirdPartyPaths.txt
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Biabduction.java
@@ -0,0 +1,18 @@
+import javax.annotation.Nullable;
+import java.util.List;
+
+public class Biabduction {
+    private String get() { return null; }
+
+    public void f1() {
+        get().length(); // error
+    }
+
+    public void f2() {
+        try {
+            get().length(); // error
+        } catch (NullPointerException e) {
+
+        }
+    }
+}
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Biabduction.json
@@ -0,0 +1,114 @@
+[
+    {
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "start of procedure f1()", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 0, 
+                "line_number": 7
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 0, 
+                "line_number": 8
+            }, 
+            {
+                "column_number": -1, 
+                "description": "start of procedure get()", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 1, 
+                "line_number": 5
+            }, 
+            {
+                "column_number": -1, 
+                "description": "return from a call to String Biabduction.get()", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 1, 
+                "line_number": 5
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 0, 
+                "line_number": 8
+            }
+        ], 
+        "bug_type": "NULL_DEREFERENCE", 
+        "bug_type_hum": "Null Dereference", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Biabduction.java", 
+        "hash": "918d7eaedf45f651f04c55554c72478c", 
+        "key": "Biabduction.java|f1|NULL_DEREFERENCE", 
+        "kind": "ERROR", 
+        "line": 8, 
+        "node_key": "9afcdcc9d4253c36267a0d34b98c337d", 
+        "procedure": "void Biabduction.f1()", 
+        "procedure_id": "Biabduction.f1():void.4b49520e7621606a0d5661886ff0b098", 
+        "procedure_start_line": 7, 
+        "qualifier": "object returned by `get(this)` could be null and is dereferenced at line 8.", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }, 
+    {
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "start of procedure f2()", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 0, 
+                "line_number": 11
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 0, 
+                "line_number": 13
+            }, 
+            {
+                "column_number": -1, 
+                "description": "start of procedure get()", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 1, 
+                "line_number": 5
+            }, 
+            {
+                "column_number": -1, 
+                "description": "return from a call to String Biabduction.get()", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 1, 
+                "line_number": 5
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Biabduction.java", 
+                "level": 0, 
+                "line_number": 13
+            }
+        ], 
+        "bug_type": "NULL_DEREFERENCE", 
+        "bug_type_hum": "Null Dereference", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Biabduction.java", 
+        "hash": "bc952ce8bad58dac5cb6672dc3150524", 
+        "key": "Biabduction.java|f2|NULL_DEREFERENCE", 
+        "kind": "ERROR", 
+        "line": 13, 
+        "node_key": "9afcdcc9d4253c36267a0d34b98c337d", 
+        "procedure": "void Biabduction.f2()", 
+        "procedure_id": "Biabduction.f2():void.41c05a632eb912a458482c1e2e4dcbb4", 
+        "procedure_start_line": 11, 
+        "qualifier": "object returned by `get(this)` could be null and is dereferenced at line 13.", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }
+]
\ No newline at end of file
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Checkers.java
@@ -0,0 +1,30 @@
+import java.io.BufferedReader;
+import java.io.File;
+import java.io.FileReader;
+
+public class Checkers {
+    public static void leak() {
+        try {
+            BufferedReader br = new BufferedReader(
+                new FileReader(new File("some.txt"))
+            );
+        } catch (Exception e) {
+
+        }
+    }
+
+    public static void error1() {
+        String str = null;
+        try {
+            int x = str.length(); // Error: even if exception is caught
+        } catch (NullPointerException e) {
+
+        }
+    }
+
+    public static void error2() {
+        String str = null;
+        int x = str.length(); // Error: not checking for null
+    }
+
+}
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Checkers.json
@@ -0,0 +1,121 @@
+[
+    {
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "start of procedure leak()", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 6
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 8
+            }
+        ], 
+        "bug_type": "RESOURCE_LEAK", 
+        "bug_type_hum": "Resource Leak", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Checkers.java", 
+        "hash": "56806153823413731f2e2166ed8d30a0", 
+        "key": "Checkers.java|leak|RESOURCE_LEAK", 
+        "kind": "ERROR", 
+        "line": 8, 
+        "node_key": "3a2af627d5d1f10e1994f6259cf18e4c", 
+        "procedure": "void Checkers.leak()", 
+        "procedure_id": "Checkers.leak():void.e21648e10d3037f4559cdb7c08642c84", 
+        "procedure_start_line": 6, 
+        "qualifier": "resource of type `java.io.FileReader` acquired by call to `new()` at line 8 is not released after line 8.", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }, 
+    {
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "start of procedure error1()", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 16
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 17
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 19
+            }
+        ], 
+        "bug_type": "NULL_DEREFERENCE", 
+        "bug_type_hum": "Null Dereference", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Checkers.java", 
+        "hash": "6de26e7c66c71b1114ad233679d55640", 
+        "key": "Checkers.java|error1|NULL_DEREFERENCE", 
+        "kind": "ERROR", 
+        "line": 19, 
+        "node_key": "c281f77c6dae544ee5fb7d5e2bb35118", 
+        "procedure": "void Checkers.error1()", 
+        "procedure_id": "Checkers.error1():void.59417424d80960700a32012973e98db5", 
+        "procedure_start_line": 16, 
+        "qualifier": "object `str` last assigned on line 17 could be null and is dereferenced at line 19.", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }, 
+    {
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "start of procedure error2()", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 25
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 26
+            }, 
+            {
+                "column_number": -1, 
+                "description": "", 
+                "filename": "tools/infer/test/Checkers.java", 
+                "level": 0, 
+                "line_number": 27
+            }
+        ], 
+        "bug_type": "NULL_DEREFERENCE", 
+        "bug_type_hum": "Null Dereference", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Checkers.java", 
+        "hash": "39e021b634ab428af7be2034688491a7", 
+        "key": "Checkers.java|error2|NULL_DEREFERENCE", 
+        "kind": "ERROR", 
+        "line": 27, 
+        "node_key": "c281f77c6dae544ee5fb7d5e2bb35118", 
+        "procedure": "void Checkers.error2()", 
+        "procedure_id": "Checkers.error2():void.e9146d80ba20c908c11d08947cd89d06", 
+        "procedure_start_line": 25, 
+        "qualifier": "object `str` last assigned on line 26 could be null and is dereferenced at line 27.", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }
+]
\ No newline at end of file
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Eradicate.java
@@ -0,0 +1,52 @@
+import javax.annotation.Nullable;
+
+public class Eradicate {
+
+    public String f; // Because it is not annoted with nullable -> can never be null!
+
+    public void field(@Nullable Eradicate x) {
+        x.f = "3"; // Error: Eradicate null field access
+    }
+
+    public void method(@Nullable Object x) {
+        String s = x.toString(); // Error: Eradicate null method call
+    }
+
+    public void filedNotNull(@Nullable String s) {
+        f = s; // Error: Eradicate field not nullable
+    }
+
+    public Eradicate() {} // Error: Eradicate field not initialized
+
+    public void str(Eradicate x) {
+        String s = x.toString();
+    }
+
+    public void callStr(@Nullable Eradicate x) {
+        str(x); // Error:  Eradicate parameter not nullable
+    }
+
+    public String shouldNotReturnNullBecauseNotAnnotated() {
+        return null; // Error: Eradicate return not nullable
+    }
+
+    public void redundant() {
+        String s = new String("abc");
+        if (s != null) { // Error: Eradicate condition redundant
+            int n = s.length();
+        }
+    }
+
+    @Nullable
+    public static String someMethod() {
+        return ""; // Error: Eradicate return overannotated
+    }
+}
+
+class B extends Eradicate {
+    @Nullable public String shouldNotReturnNullBecauseNotAnnotated() {
+        return null; // Error: Eradicate inconsistent subclass return annotation
+    }
+
+    public void field(Eradicate x) {} // Error: Inconsistent subclass parameter annotation
+}
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Racerd.java
@@ -0,0 +1,35 @@
+import javax.annotation.concurrent.ThreadSafe;
+
+@ThreadSafe
+public class Racerd {
+    private int mTemperature;
+
+    public void makeDinner() {
+        boilWater();
+    }
+
+    private void boilWater() {
+        mTemperature = 100; //Error: unprotected write.
+    }
+}
+
+@ThreadSafe
+class Account {
+
+    int mBalance = 0;
+
+    public void deposit(int amount) {
+        if (amount > 0) {
+            mBalance += amount; // Error: unsynchronized write
+        }
+    }
+
+    public int withdraw(int amount){
+        if (amount >= 0 && mBalance - amount >= 0) {
+            mBalance -= amount; // Error: unsynchronized write
+            return mBalance; // Error: unsynchronized read
+        } else {
+            return 0;
+        }
+    }
+}
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Racerd.json
@@ -0,0 +1,146 @@
+[
+    {
+        "access": "hJWmvgAAAIwAAAApAAAAfQAAAHOwkNAnZGVwb3NpdKCgQCNpbnRAk6AnQWNjb3VudECQoEAkdm9pZECgoJKgIECwVwD/kjx0b29scy9pbmZlci90ZXN0L1JhY2VyZC5qYXZhkaCgkbACNp9MF6AkdGhpc0CQBBygo6CUk6AEGkCwQEBAQAQBoJGRMEFjY291bnQubUJhbGFuY2VAoAQXQA==", 
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "access to `this.Account.mBalance`", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 0, 
+                "line_number": 23
+            }
+        ], 
+        "bug_type": "THREAD_SAFETY_VIOLATION", 
+        "bug_type_hum": "Thread Safety Violation", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Racerd.java", 
+        "hash": "6b62cb17008a3135d218108fa3123402", 
+        "key": "Racerd.java|deposit|THREAD_SAFETY_VIOLATION", 
+        "kind": "ERROR", 
+        "line": 23, 
+        "node_key": "9c5d6d9028928346cc4fb44cced5dea1", 
+        "procedure": "void Account.deposit(int)", 
+        "procedure_id": "Account.deposit(int):void.a9cc1805c1e3652887a5ee12b55803af", 
+        "procedure_start_line": 0, 
+        "qualifier": "Unprotected write. Non-private method `void Account.deposit(int)` writes to field `this.Account.mBalance` outside of synchronization.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself).", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }, 
+    {
+        "access": "hJWmvgAAAJ8AAAApAAAAhAAAAHmwkNAqbWFrZURpbm5lckCToCZSYWNlcmRAkKBAJHZvaWRAoKCQ0Clib2lsV2F0ZXJAk6AEC0AECkCwSAD/kjx0b29scy9pbmZlci90ZXN0L1JhY2VyZC5qYXZhkaCgkbACNp9MF6AkdGhpc0CQBBugo6CUk6AEHECwQEBAQAQBoJGRM1JhY2VyZC5tVGVtcGVyYXR1cmVAoLBMAP8EF0A=", 
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "call to void Racerd.boilWater()", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 0, 
+                "line_number": 8
+            }, 
+            {
+                "column_number": -1, 
+                "description": "access to `this.Racerd.mTemperature`", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 1, 
+                "line_number": 12
+            }
+        ], 
+        "bug_type": "THREAD_SAFETY_VIOLATION", 
+        "bug_type_hum": "Thread Safety Violation", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Racerd.java", 
+        "hash": "2882383086ab102a88144ae3c2cc4701", 
+        "key": "Racerd.java|makeDinner|THREAD_SAFETY_VIOLATION", 
+        "kind": "ERROR", 
+        "line": 8, 
+        "node_key": "9c5d6d9028928346cc4fb44cced5dea1", 
+        "procedure": "void Racerd.makeDinner()", 
+        "procedure_id": "Racerd.makeDinner():void.2796f75396b30d2d49b24ddfab722306", 
+        "procedure_start_line": 0, 
+        "qualifier": "Unprotected write. Non-private method `void Racerd.makeDinner()` indirectly writes to field `this.Racerd.mTemperature` outside of synchronization.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself).", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }, 
+    {
+        "access": "hJWmvgAAAJEAAAAqAAAAggAAAHmwkNAod2l0aGRyYXegoEAjaW50QJOgJ0FjY291bnRAkKBABAZAoKCSoCBAsF4A/5I8dG9vbHMvaW5mZXIvdGVzdC9SYWNlcmQuamF2YZCgoJGwAjafTBegJHRoaXNAkAQboKOglJOgBBlAsEBAQEAEAaCRkTBBY2NvdW50Lm1CYWxhbmNlQKAEF6CwXQD/BBhA", 
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "<Read trace>", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 0, 
+                "line_number": 30
+            }, 
+            {
+                "column_number": -1, 
+                "description": "access to `this.Account.mBalance`", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 0, 
+                "line_number": 30
+            }, 
+            {
+                "column_number": -1, 
+                "description": "<Write trace>", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 0, 
+                "line_number": 29
+            }, 
+            {
+                "column_number": -1, 
+                "description": "access to `this.Account.mBalance`", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 0, 
+                "line_number": 29
+            }
+        ], 
+        "bug_type": "THREAD_SAFETY_VIOLATION", 
+        "bug_type_hum": "Thread Safety Violation", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Racerd.java", 
+        "hash": "5665f12d2392f93f11f556cd1b1e238a", 
+        "key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION", 
+        "kind": "ERROR", 
+        "line": 30, 
+        "node_key": "9c5d6d9028928346cc4fb44cced5dea1", 
+        "procedure": "int Account.withdraw(int)", 
+        "procedure_id": "Account.withdraw(int):int.038de5054c5c25e60d169e42e0177a16", 
+        "procedure_start_line": 0, 
+        "qualifier": "Read/Write race. Non-private method `int Account.withdraw(int)` reads without synchronization from `this.Account.mBalance`. Potentially races with write in method `Account.withdraw(...)`.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself).", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }, 
+    {
+        "access": "hJWmvgAAAIoAAAAoAAAAewAAAHKwkNAod2l0aGRyYXegoEAjaW50QJOgJ0FjY291bnRAkKBABAZAoKCSoCBAsF0A/5I8dG9vbHMvaW5mZXIvdGVzdC9SYWNlcmQuamF2YZGgoJGwAjafTBegJHRoaXNAkAQboKOglJOgBBlAsEBAQEAEAaCRkTBBY2NvdW50Lm1CYWxhbmNlQKAEF0A=", 
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "access to `this.Account.mBalance`", 
+                "filename": "tools/infer/test/Racerd.java", 
+                "level": 0, 
+                "line_number": 29
+            }
+        ], 
+        "bug_type": "THREAD_SAFETY_VIOLATION", 
+        "bug_type_hum": "Thread Safety Violation", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Racerd.java", 
+        "hash": "a7c30fd1b251d9e16750fc7e5913b885", 
+        "key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION", 
+        "kind": "ERROR", 
+        "line": 29, 
+        "node_key": "9c5d6d9028928346cc4fb44cced5dea1", 
+        "procedure": "int Account.withdraw(int)", 
+        "procedure_id": "Account.withdraw(int):int.038de5054c5c25e60d169e42e0177a16", 
+        "procedure_start_line": 0, 
+        "qualifier": "Unprotected write. Non-private method `int Account.withdraw(int)` writes to field `this.Account.mBalance` outside of synchronization.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself).", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }
+]
\ No newline at end of file
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Starvation.java
@@ -0,0 +1,20 @@
+public class Starvation {
+
+    String lockA, lockB;
+
+    public void lockAThenB() {
+        synchronized(lockA) {
+            synchronized(lockB) {
+                // do something with both resources
+            }
+        }
+    }
+
+    public void lockBThenA() {
+        synchronized(lockB) {
+            synchronized(lockA) {
+                // do something with both resources
+            }
+        }
+    }
+}
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/Starvation.json
@@ -0,0 +1,65 @@
+[
+    {
+        "bug_class": "PROVER", 
+        "bug_trace": [
+            {
+                "column_number": -1, 
+                "description": "[Trace 1] `void Starvation.lockAThenB()`", 
+                "filename": "tools/infer/test/Starvation.java", 
+                "level": 0, 
+                "line_number": 6
+            }, 
+            {
+                "column_number": -1, 
+                "description": "locks `this.Starvation.lockA` in class `Starvation*`", 
+                "filename": "tools/infer/test/Starvation.java", 
+                "level": 0, 
+                "line_number": 6
+            }, 
+            {
+                "column_number": -1, 
+                "description": "locks `this.Starvation.lockB` in class `Starvation*`", 
+                "filename": "tools/infer/test/Starvation.java", 
+                "level": 1, 
+                "line_number": 7
+            }, 
+            {
+                "column_number": -1, 
+                "description": "[Trace 2] `void Starvation.lockBThenA()`", 
+                "filename": "tools/infer/test/Starvation.java", 
+                "level": 0, 
+                "line_number": 14
+            }, 
+            {
+                "column_number": -1, 
+                "description": "locks `this.Starvation.lockB` in class `Starvation*`", 
+                "filename": "tools/infer/test/Starvation.java", 
+                "level": 0, 
+                "line_number": 14
+            }, 
+            {
+                "column_number": -1, 
+                "description": "locks `this.Starvation.lockA` in class `Starvation*`", 
+                "filename": "tools/infer/test/Starvation.java", 
+                "level": 1, 
+                "line_number": 15
+            }
+        ], 
+        "bug_type": "DEADLOCK", 
+        "bug_type_hum": "Deadlock", 
+        "censored_reason": "", 
+        "column": -1, 
+        "file": "tools/infer/test/Starvation.java", 
+        "hash": "043d28a94431b4c573b949b8570fb318", 
+        "key": "Starvation.java|lockAThenB|DEADLOCK", 
+        "kind": "ERROR", 
+        "line": 6, 
+        "node_key": "9c5d6d9028928346cc4fb44cced5dea1", 
+        "procedure": "void Starvation.lockAThenB()", 
+        "procedure_id": "Starvation.lockAThenB():void.b7eb3955306c498af42d6336f52a796f", 
+        "procedure_start_line": 0, 
+        "qualifier": "Potential deadlock.\nTrace 1 (starts at `void Starvation.lockAThenB()`) first locks `this.Starvation.lockA` in class `Starvation*` (line 6 in `void Starvation.lockAThenB()`) and then locks `this.Starvation.lockB` in class `Starvation*` (line 7 in `void Starvation.lockAThenB()`).\nTrace 2 (starts at `void Starvation.lockBThenA()`), first locks `this.Starvation.lockB` in class `Starvation*` (line 14 in `void Starvation.lockBThenA()`) and then locks `this.Starvation.lockA` in class `Starvation*` (line 15 in `void Starvation.lockBThenA()`).", 
+        "severity": "HIGH", 
+        "visibility": "user"
+    }
+]
\ No newline at end of file
new file mode 100644
--- /dev/null
+++ b/tools/infer/test/build.gradle
@@ -0,0 +1,43 @@
+apply plugin: 'java'
+
+buildDir "${topobjdir}/gradle/build/test-infer"
+
+repositories {
+    maven {
+        url "https://maven.google.com"
+    }
+}
+
+dependencies {
+    compile "com.google.code.findbugs:jsr305:3.0.2"
+}
+
+task compileInferTestBiabduction(type: JavaCompile) {
+    source = fileTree(dir: '.', include: 'Biabduction.java')
+    classpath = project.configurations.compileClasspath
+    destinationDir = file("${project.buildDir}")
+}
+
+task compileInferTestCheckers(type: JavaCompile) {
+    source = fileTree(dir: '.', include: 'Checkers.java')
+    classpath = project.configurations.compileClasspath
+    destinationDir = file("${project.buildDir}")
+}
+
+task compileInferTestEradicate(type: JavaCompile) {
+    source = fileTree(dir: '.', include: 'Eradicate.java')
+    classpath = project.configurations.compileClasspath
+    destinationDir = file("${project.buildDir}")
+}
+
+task compileInferTestRacerd(type: JavaCompile) {
+    source = fileTree(dir: '.', include: 'Racerd.java')
+    classpath = project.configurations.compileClasspath
+    destinationDir = file("${project.buildDir}")
+}
+
+task compileInferTestStarvation(type: JavaCompile) {
+    source = fileTree(dir: '.', include: 'Starvation.java')
+    classpath = project.configurations.compileClasspath
+    destinationDir = file("${project.buildDir}")
+}
\ No newline at end of file