зеркало из https://github.com/mozilla/gecko-dev.git
Bug 1479503: Check infer in ./mach static-analysis autotest. r=nalexander
Now autotest does not require java to be installed, but it will let the user know that infer is not being tested if java is missing. Differential Revision: https://phabricator.services.mozilla.com/D7326 --HG-- extra : moz-landing-system : lando
This commit is contained in:
Robert Bartlensky
Родитель
d7bcabf70a
Коммит
6cf2bd98ec
1
.flake8
1
.flake8
|
|
@ -22,3 +22,4 @@ exclude =
|
|||
testing/mochitest/pywebsocket,
|
||||
tools/lint/test/files,
|
||||
build/build-infer/build-infer.py,
|
||||
tools/infer/test/*.configure, tools/infer/test/*.configure,
|
||||
|
|
@ -74,6 +74,7 @@ _OPT\.OBJ/
|
|||
|
||||
# Gradle cache.
|
||||
^.gradle/
|
||||
^tools/infer/test/.gradle/
|
||||
|
||||
# Local Gradle configuration properties.
|
||||
^local.properties$
|
||||
|
|
|
|||
|
|
@ -1704,14 +1704,8 @@ class StaticAnalysis(MachCommandBase):
|
|||
self.log_manager.enable_all_structured_loggers()
|
||||
|
||||
rc = self._build_compile_db(verbose=verbose)
|
||||
if rc != 0:
|
||||
return rc
|
||||
|
||||
rc = self._build_export(jobs=jobs, verbose=verbose)
|
||||
if rc != 0:
|
||||
return rc
|
||||
|
||||
rc = self._get_clang_tools(verbose=verbose)
|
||||
rc = rc or self._build_export(jobs=jobs, verbose=verbose)
|
||||
rc = rc or self._get_clang_tools(verbose=verbose)
|
||||
if rc != 0:
|
||||
return rc
|
||||
|
||||
|
|
@ -1776,6 +1770,9 @@ class StaticAnalysis(MachCommandBase):
|
|||
self.log(logging.WARNING, 'static-analysis', {},
|
||||
'Cannot check java source code unless you are building for android!')
|
||||
return 1
|
||||
rc = self._check_for_java()
|
||||
if rc != 0:
|
||||
return 1
|
||||
# if source contains the whole mobile folder, then we just have to
|
||||
# analyze everything
|
||||
check_all = any(i.rstrip(os.sep).split(os.sep)[-1] == 'mobile' for i in source)
|
||||
|
|
@ -1800,21 +1797,15 @@ class StaticAnalysis(MachCommandBase):
|
|||
checks=checks or all_checkers,
|
||||
third_party_path=third_party_path
|
||||
)
|
||||
gradlew = mozpath.join(self.topsrcdir, 'gradlew')
|
||||
rc = rc or self._gradle(['clean']) # clean so that we can recompile
|
||||
# infer capture command
|
||||
capture_cmd = [self._infer_path, 'capture'] + excludes + \
|
||||
['--', gradlew, task]
|
||||
capture_cmd = [self._infer_path, 'capture'] + excludes + ['--']
|
||||
rc = rc or self._gradle([task], infer_args=capture_cmd, verbose=verbose)
|
||||
tmp_file, args = self._get_infer_source_args(java_sources)
|
||||
# infer analyze command
|
||||
analysis_cmd = [self._infer_path, 'analyze', '--keep-going'] + \
|
||||
checkers + args
|
||||
# capture, then analyze the sources
|
||||
for args in [[gradlew, 'clean'], capture_cmd, analysis_cmd]:
|
||||
rc = self.run_process(args=args, cwd=self.topsrcdir,
|
||||
pass_thru=True)
|
||||
# if a command fails, break and close the tmp file before returning
|
||||
if rc != 0:
|
||||
break
|
||||
rc = rc or self.run_process(args=analysis_cmd, cwd=self.topsrcdir, pass_thru=True)
|
||||
if tmp_file:
|
||||
tmp_file.close()
|
||||
return rc
|
||||
|
|
@ -1918,6 +1909,47 @@ class StaticAnalysis(MachCommandBase):
|
|||
str(jobs), '-p', self._compilation_commands_path
|
||||
] + common_args + sources
|
||||
|
||||
def _check_for_java(self):
|
||||
'''Check if javac can be found.'''
|
||||
import distutils
|
||||
java = self.substs.get('JAVA')
|
||||
java = java or os.getenv('JAVA_HOME')
|
||||
java = java or distutils.spawn.find_executable('javac')
|
||||
error = 'javac was not found! Please install javac and either add it to your PATH, '
|
||||
error += 'set JAVA_HOME, or add the following to your mozconfig:\n'
|
||||
error += ' --with-java-bin-path=/path/to/java/bin/'
|
||||
if not java:
|
||||
self.log(logging.ERROR, 'ERROR: static-analysis', {}, error)
|
||||
return 1
|
||||
return 0
|
||||
|
||||
def _gradle(self, args, infer_args=None, verbose=False, autotest=False,
|
||||
suppress_output=True):
|
||||
infer_args = infer_args or []
|
||||
if autotest:
|
||||
cwd = mozpath.join(self.topsrcdir, 'tools', 'infer', 'test')
|
||||
gradle = mozpath.join(cwd, 'gradlew')
|
||||
else:
|
||||
gradle = self.substs['GRADLE']
|
||||
cwd = self.topsrcdir
|
||||
extra_env = {
|
||||
'GRADLE_OPTS': '-Dfile.encoding=utf-8', # see mobile/android/mach_commands.py
|
||||
'JAVA_TOOL_OPTIONS': '-Dfile.encoding=utf-8',
|
||||
}
|
||||
if suppress_output:
|
||||
devnull = open(os.devnull, 'w')
|
||||
return subprocess.call(
|
||||
infer_args + [gradle] + args,
|
||||
env=dict(os.environ, **extra_env),
|
||||
cwd=cwd, stdout=devnull, stderr=subprocess.STDOUT, close_fds=True)
|
||||
else:
|
||||
return self.run_process(
|
||||
infer_args + [gradle] + args,
|
||||
append_env=extra_env,
|
||||
pass_thru=True, # Allow user to run gradle interactively.
|
||||
ensure_exit_code=False, # Don't throw on non-zero exit code.
|
||||
cwd=cwd)
|
||||
|
||||
@StaticAnalysisSubCommand('static-analysis', 'autotest',
|
||||
'Run the auto-test suite in order to determine that'
|
||||
' the analysis did not regress.')
|
||||
|
|
@ -1935,10 +1967,7 @@ class StaticAnalysis(MachCommandBase):
|
|||
self._set_log_level(verbose)
|
||||
self._dump_results = dump_results
|
||||
|
||||
force_download = True
|
||||
|
||||
if self._dump_results:
|
||||
force_download = False
|
||||
force_download = not self._dump_results
|
||||
|
||||
# Function return codes
|
||||
self.TOOLS_SUCCESS = 0
|
||||
|
|
@ -1951,6 +1980,7 @@ class StaticAnalysis(MachCommandBase):
|
|||
self.TOOLS_CHECKER_NOT_FOUND = 7
|
||||
self.TOOLS_CHECKER_FAILED_FILE = 8
|
||||
self.TOOLS_CHECKER_LIST_EMPTY = 9
|
||||
self.TOOLS_GRADLE_FAILED = 10
|
||||
|
||||
# Configure the tree or download clang-tidy package, depending on the option that we choose
|
||||
if intree_tool:
|
||||
|
|
@ -2058,7 +2088,7 @@ class StaticAnalysis(MachCommandBase):
|
|||
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 _run_analysis(self, checks, header_filter, sources, jobs=1, fix=False, print_out=False):
|
||||
cmd = self._get_clang_tidy_command(
|
||||
|
|
@ -2111,7 +2141,7 @@ class StaticAnalysis(MachCommandBase):
|
|||
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)
|
||||
|
||||
|
|
@ -2120,6 +2150,129 @@ class StaticAnalysis(MachCommandBase):
|
|||
|
||||
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':
|
||||
rc = self._check_for_java()
|
||||
if rc != 0:
|
||||
return 1
|
||||
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
|
||||
self.__infer_tool = mozpath.join(self.topsrcdir, 'tools', 'infer')
|
||||
self.__infer_test_folder = mozpath.join(self.__infer_tool, 'test')
|
||||
|
||||
import concurrent.futures
|
||||
import multiprocessing
|
||||
max_workers = multiprocessing.cpu_count()
|
||||
self.log(logging.INFO, 'static-analysis', {},
|
||||
"RUNNING: infer autotest for platform {0} with {1} workers.".format(
|
||||
self.platform[0], max_workers))
|
||||
# clean previous autotest if it exists
|
||||
rc = self._gradle(['autotest:clean'], autotest=True)
|
||||
if rc != 0:
|
||||
return rc
|
||||
import yaml
|
||||
with open(mozpath.join(self.__infer_tool, '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.")
|
||||
else:
|
||||
self.log(logging.WARNING, 'static-analysis', {},
|
||||
"Skipping infer autotest, because it is only available on linux64!")
|
||||
return self.TOOLS_SUCCESS
|
||||
|
||||
def _verify_infer_checker(self, item):
|
||||
'''Given a checker, this method verifies the following:
|
||||
1. if there is a `checker`.json and `checker`.java file in
|
||||
`tools/infer/test/autotest/src`
|
||||
2. if running infer on `checker`.java yields the same result as `checker`.json
|
||||
An `item` is simply a dictionary, which needs to have a `name` field set, which is the
|
||||
name of the checker.
|
||||
'''
|
||||
def to_camelcase(str):
|
||||
return ''.join([s.capitalize() for s in str.split('-')])
|
||||
check = item['name']
|
||||
test_file_path = mozpath.join(self.__infer_tool, 'test', 'autotest', 'src',
|
||||
'main', 'java', 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
|
||||
out_folder = mozpath.join(self.__infer_test_folder, 'test-infer-{}'.format(check))
|
||||
if check == 'checkers':
|
||||
check_arg = ['-a', 'checkers']
|
||||
else:
|
||||
check_arg = ['--{}-only'.format(check)]
|
||||
infer_args = [self._infer_path, 'run'] + check_arg + ['-o', out_folder, '--']
|
||||
gradle_args = ['autotest:compileInferTest{}'.format(to_camelcase(check))]
|
||||
rc = self._gradle(gradle_args, infer_args=infer_args, autotest=True)
|
||||
if rc != 0:
|
||||
self.log(logging.ERROR, 'static-analysis', {},
|
||||
"ERROR: infer failed to execute gradle {}.".format(gradle_args))
|
||||
return self.TOOLS_GRADLE_FAILED
|
||||
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):
|
||||
error_str = "ERROR: in check {} Expected: ".format(check)
|
||||
error_str += '\n' + json.dumps(baseline_issues, indent=2)
|
||||
error_str += '\n Got:\n' + json.dumps(issues, indent=2)
|
||||
self.log(logging.ERROR, 'static-analysis', {},
|
||||
'ERROR: infer autotest for check {} failed, check stdout for more details'
|
||||
.format(check))
|
||||
print(error_str)
|
||||
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,
|
||||
|
|
@ -2413,7 +2566,6 @@ class StaticAnalysis(MachCommandBase):
|
|||
"run-clang-tidy.py")
|
||||
self._clang_format_diff = mozpath.join(clang_tools_path, "clang-tidy", "share", "clang",
|
||||
"clang-format-diff.py")
|
||||
|
||||
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 \
|
||||
|
|
@ -2514,15 +2666,17 @@ class StaticAnalysis(MachCommandBase):
|
|||
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:
|
||||
|
|
|
|||
|
|
@ -86,9 +86,9 @@ jobs:
|
|||
fetch:
|
||||
symbol: I(fetch)
|
||||
parent: debian9-base
|
||||
infer-build:
|
||||
symbol: I(infer)
|
||||
parent: debian9-base
|
||||
static-analysis-build:
|
||||
symbol: I(static-analysis-build)
|
||||
parent: android-build
|
||||
mingw32-build:
|
||||
symbol: I(mingw)
|
||||
parent: debian9-base
|
||||
|
|
|
|||
|
|
@ -40,10 +40,12 @@ jobs:
|
|||
platform: linux64/debug
|
||||
worker-type: aws-provisioner-v1/gecko-t-linux-large
|
||||
worker:
|
||||
docker-image: {in-tree: static-analysis-build}
|
||||
env:
|
||||
# clang-tidy needs a recent libstdc++, which can be found in the clang
|
||||
# toolchain.
|
||||
LD_LIBRARY_PATH: /builds/worker/workspace/build/src/clang/lib
|
||||
PERFHERDER_EXTRA_OPTIONS: static-analysis-autotest
|
||||
run:
|
||||
config:
|
||||
- builds/releng_base_firefox.py
|
||||
|
|
|
|||
|
|
@ -185,7 +185,7 @@ linux64-infer:
|
|||
tier: 1
|
||||
worker-type: aws-provisioner-v1/gecko-{level}-b-linux
|
||||
worker:
|
||||
docker-image: {in-tree: infer-build}
|
||||
docker-image: {in-tree: static-analysis-build}
|
||||
max-run-time: 3600
|
||||
run:
|
||||
using: toolchain-script
|
||||
|
|
|
|||
|
|
@ -0,0 +1,58 @@
|
|||
# %ARG DOCKER_IMAGE_PARENT
|
||||
FROM $DOCKER_IMAGE_PARENT
|
||||
MAINTAINER Robert Bartlensky <rbartlensky@mozilla.com>
|
||||
|
||||
VOLUME /builds/worker/checkouts
|
||||
VOLUME /builds/worker/workspace
|
||||
VOLUME /builds/worker/tooltool-cache
|
||||
|
||||
ENV XZ_OPT=-T0
|
||||
|
||||
RUN apt-get update && \
|
||||
apt-get install \
|
||||
autoconf2.13 \
|
||||
automake \
|
||||
bison \
|
||||
bzip2 \
|
||||
cmake \
|
||||
flex \
|
||||
curl \
|
||||
opam \
|
||||
libsqlite3-dev \
|
||||
file \
|
||||
gawk \
|
||||
gcc-multilib \
|
||||
gnupg \
|
||||
libc6-dev \
|
||||
openjdk-8-jdk-headless \
|
||||
pkg-config \
|
||||
patch \
|
||||
p7zip-full \
|
||||
procps \
|
||||
python-pip \
|
||||
python-setuptools \
|
||||
python-virtualenv \
|
||||
rsync \
|
||||
screen \
|
||||
tar \
|
||||
unzip \
|
||||
uuid \
|
||||
valgrind \
|
||||
wget \
|
||||
yasm \
|
||||
zip \
|
||||
zlib1g-dev \
|
||||
x11-utils \
|
||||
xvfb \
|
||||
linux-libc-dev \
|
||||
libdbus-glib-1-dev \
|
||||
libfontconfig1-dev \
|
||||
libfreetype6-dev \
|
||||
libgconf2-dev \
|
||||
libgtk-3-dev \
|
||||
libgtk2.0-dev \
|
||||
libpango1.0-dev \
|
||||
libpulse-dev \
|
||||
libx11-xcb-dev \
|
||||
libxt-dev \
|
||||
lib32z1
|
||||
|
|
@ -1097,7 +1097,10 @@ or run without that action (ie: --no-{action})"
|
|||
def static_analysis_autotest(self):
|
||||
"""Run mach static-analysis autotest, in order to make sure we dont regress"""
|
||||
self.preflight_build()
|
||||
self._run_mach_command_in_build_env(['static-analysis', 'autotest', '--intree-tool'])
|
||||
self._run_mach_command_in_build_env(['configure'])
|
||||
self._run_mach_command_in_build_env(['static-analysis', 'autotest',
|
||||
'--intree-tool'],
|
||||
use_subprocess=True)
|
||||
|
||||
def _query_mach(self):
|
||||
dirs = self.query_abs_dirs()
|
||||
|
|
@ -1114,7 +1117,7 @@ or run without that action (ie: --no-{action})"
|
|||
mach = [sys.executable, 'mach']
|
||||
return mach
|
||||
|
||||
def _run_mach_command_in_build_env(self, args):
|
||||
def _run_mach_command_in_build_env(self, args, use_subprocess=False):
|
||||
"""Run a mach command in a build context."""
|
||||
env = self.query_build_env()
|
||||
env.update(self.query_mach_build_env())
|
||||
|
|
@ -1123,12 +1126,21 @@ or run without that action (ie: --no-{action})"
|
|||
|
||||
mach = self._query_mach()
|
||||
|
||||
return_code = self.run_command(
|
||||
command=mach + ['--log-no-times'] + args,
|
||||
cwd=dirs['abs_src_dir'],
|
||||
env=env,
|
||||
output_timeout=self.config.get('max_build_output_timeout', 60 * 40)
|
||||
)
|
||||
# XXX See bug 1483883
|
||||
# Work around an interaction between Gradle and mozharness
|
||||
# Not using `subprocess` causes gradle to hang
|
||||
if use_subprocess:
|
||||
import subprocess
|
||||
return_code = subprocess.call(mach + ['--log-no-times'] + args,
|
||||
env=env, cwd=dirs['abs_src_dir'])
|
||||
else:
|
||||
return_code = self.run_command(
|
||||
command=mach + ['--log-no-times'] + args,
|
||||
cwd=dirs['abs_src_dir'],
|
||||
env=env,
|
||||
output_timeout=self.config.get('max_build_output_timeout',
|
||||
60 * 40)
|
||||
)
|
||||
|
||||
if return_code:
|
||||
self.return_code = self.worst_level(
|
||||
|
|
|
|||
|
|
@ -5,19 +5,27 @@ target: obj-x86_64-pc-linux-gnu
|
|||
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
|
||||
|
|
|
|||
|
|
@ -0,0 +1,25 @@
|
|||
buildDir "${topobjdir}/gradle/build/tools/infer/test/autotest"
|
||||
|
||||
apply plugin: 'java'
|
||||
|
||||
repositories {
|
||||
mavenCentral()
|
||||
}
|
||||
|
||||
dependencies {
|
||||
compile "com.google.code.findbugs:jsr305:3.0.2"
|
||||
}
|
||||
|
||||
def createSingleTask = { name ->
|
||||
task("compileInferTest${name}", type: JavaCompile) {
|
||||
source = fileTree(dir: '.', include: "src/main/java/${name}.java")
|
||||
classpath = project.configurations.compileClasspath
|
||||
destinationDir = file("${topobjdir}/gradle/build/tools/infer/test/autotest")
|
||||
}
|
||||
}
|
||||
|
||||
createSingleTask('Biabduction')
|
||||
createSingleTask('Checkers')
|
||||
createSingleTask('Eradicate')
|
||||
createSingleTask('Racerd')
|
||||
createSingleTask('Starvation')
|
||||
|
|
@ -0,0 +1,22 @@
|
|||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
||||
|
||||
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) {
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,114 @@
|
|||
[
|
||||
{
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "start of procedure f1()",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 0,
|
||||
"line_number": 11
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 0,
|
||||
"line_number": 12
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "start of procedure get()",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 1,
|
||||
"line_number": 9
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "return from a call to String Biabduction.get()",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 1,
|
||||
"line_number": 9
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 0,
|
||||
"line_number": 12
|
||||
}
|
||||
],
|
||||
"bug_type": "NULL_DEREFERENCE",
|
||||
"bug_type_hum": "Null Dereference",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Biabduction.java",
|
||||
"hash": "918d7eaedf45f651f04c55554c72478c",
|
||||
"key": "Biabduction.java|f1|NULL_DEREFERENCE",
|
||||
"kind": "ERROR",
|
||||
"line": 12,
|
||||
"node_key": "9afcdcc9d4253c36267a0d34b98c337d",
|
||||
"procedure": "void Biabduction.f1()",
|
||||
"procedure_id": "Biabduction.f1():void.4b49520e7621606a0d5661886ff0b098",
|
||||
"procedure_start_line": 11,
|
||||
"qualifier": "object returned by `get(this)` could be null and is dereferenced at line 12.",
|
||||
"severity": "HIGH",
|
||||
"visibility": "user"
|
||||
},
|
||||
{
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "start of procedure f2()",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 0,
|
||||
"line_number": 15
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 0,
|
||||
"line_number": 17
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "start of procedure get()",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 1,
|
||||
"line_number": 9
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "return from a call to String Biabduction.get()",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 1,
|
||||
"line_number": 9
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Biabduction.java",
|
||||
"level": 0,
|
||||
"line_number": 17
|
||||
}
|
||||
],
|
||||
"bug_type": "NULL_DEREFERENCE",
|
||||
"bug_type_hum": "Null Dereference",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Biabduction.java",
|
||||
"hash": "bc952ce8bad58dac5cb6672dc3150524",
|
||||
"key": "Biabduction.java|f2|NULL_DEREFERENCE",
|
||||
"kind": "ERROR",
|
||||
"line": 17,
|
||||
"node_key": "9afcdcc9d4253c36267a0d34b98c337d",
|
||||
"procedure": "void Biabduction.f2()",
|
||||
"procedure_id": "Biabduction.f2():void.41c05a632eb912a458482c1e2e4dcbb4",
|
||||
"procedure_start_line": 15,
|
||||
"qualifier": "object returned by `get(this)` could be null and is dereferenced at line 17.",
|
||||
"severity": "HIGH",
|
||||
"visibility": "user"
|
||||
}
|
||||
]
|
||||
|
|
@ -0,0 +1,34 @@
|
|||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
||||
|
||||
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
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -0,0 +1,121 @@
|
|||
[
|
||||
{
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "start of procedure leak()",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 10
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 12
|
||||
}
|
||||
],
|
||||
"bug_type": "RESOURCE_LEAK",
|
||||
"bug_type_hum": "Resource Leak",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Checkers.java",
|
||||
"hash": "56806153823413731f2e2166ed8d30a0",
|
||||
"key": "Checkers.java|leak|RESOURCE_LEAK",
|
||||
"kind": "ERROR",
|
||||
"line": 12,
|
||||
"node_key": "3a2af627d5d1f10e1994f6259cf18e4c",
|
||||
"procedure": "void Checkers.leak()",
|
||||
"procedure_id": "Checkers.leak():void.e21648e10d3037f4559cdb7c08642c84",
|
||||
"procedure_start_line": 10,
|
||||
"qualifier": "resource of type `java.io.FileReader` acquired by call to `new()` at line 12 is not released after line 12.",
|
||||
"severity": "HIGH",
|
||||
"visibility": "user"
|
||||
},
|
||||
{
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "start of procedure error1()",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 20
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 21
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 23
|
||||
}
|
||||
],
|
||||
"bug_type": "NULL_DEREFERENCE",
|
||||
"bug_type_hum": "Null Dereference",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Checkers.java",
|
||||
"hash": "6de26e7c66c71b1114ad233679d55640",
|
||||
"key": "Checkers.java|error1|NULL_DEREFERENCE",
|
||||
"kind": "ERROR",
|
||||
"line": 23,
|
||||
"node_key": "c281f77c6dae544ee5fb7d5e2bb35118",
|
||||
"procedure": "void Checkers.error1()",
|
||||
"procedure_id": "Checkers.error1():void.59417424d80960700a32012973e98db5",
|
||||
"procedure_start_line": 20,
|
||||
"qualifier": "object `str` last assigned on line 21 could be null and is dereferenced at line 23.",
|
||||
"severity": "HIGH",
|
||||
"visibility": "user"
|
||||
},
|
||||
{
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "start of procedure error2()",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 29
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 30
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "",
|
||||
"filename": "autotest/src/main/java/Checkers.java",
|
||||
"level": 0,
|
||||
"line_number": 31
|
||||
}
|
||||
],
|
||||
"bug_type": "NULL_DEREFERENCE",
|
||||
"bug_type_hum": "Null Dereference",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Checkers.java",
|
||||
"hash": "39e021b634ab428af7be2034688491a7",
|
||||
"key": "Checkers.java|error2|NULL_DEREFERENCE",
|
||||
"kind": "ERROR",
|
||||
"line": 31,
|
||||
"node_key": "c281f77c6dae544ee5fb7d5e2bb35118",
|
||||
"procedure": "void Checkers.error2()",
|
||||
"procedure_id": "Checkers.error2():void.e9146d80ba20c908c11d08947cd89d06",
|
||||
"procedure_start_line": 29,
|
||||
"qualifier": "object `str` last assigned on line 30 could be null and is dereferenced at line 31.",
|
||||
"severity": "HIGH",
|
||||
"visibility": "user"
|
||||
}
|
||||
]
|
||||
|
|
@ -0,0 +1,57 @@
|
|||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
||||
|
||||
import javax.annotation.Nullable;
|
||||
|
||||
// Examples taken from the infer website.
|
||||
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
|
||||
}
|
||||
|
|
@ -0,0 +1,40 @@
|
|||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
||||
|
||||
import javax.annotation.concurrent.ThreadSafe;
|
||||
|
||||
// Examples taken from the infer website.
|
||||
@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;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,146 @@
|
|||
[
|
||||
{
|
||||
"access": "hJWmvgAAAJMAAAApAAAAfgAAAHSwkNAnZGVwb3NpdKCgQCNpbnRAk6AnQWNjb3VudECQoEAkdm9pZECgoJKgIECwXAD/kgkiYXV0b3Rlc3Qvc3JjL21haW4vamF2YS9SYWNlcmQuamF2YZGgoJGwAjafTBegJHRoaXNAkAQcoKOglJOgBBpAsEBAQEAEAaCRkTBBY2NvdW50Lm1CYWxhbmNlQKAEF0A=",
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "access to `this.Account.mBalance`",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 0,
|
||||
"line_number": 28
|
||||
}
|
||||
],
|
||||
"bug_type": "THREAD_SAFETY_VIOLATION",
|
||||
"bug_type_hum": "Thread Safety Violation",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Racerd.java",
|
||||
"hash": "6b62cb17008a3135d218108fa3123402",
|
||||
"key": "Racerd.java|deposit|THREAD_SAFETY_VIOLATION",
|
||||
"kind": "ERROR",
|
||||
"line": 28,
|
||||
"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": "hJWmvgAAAKYAAAApAAAAhQAAAHqwkNAqbWFrZURpbm5lckCToCZSYWNlcmRAkKBAJHZvaWRAoKCQ0Clib2lsV2F0ZXJAk6AEC0AECkCwTQD/kgkiYXV0b3Rlc3Qvc3JjL21haW4vamF2YS9SYWNlcmQuamF2YZGgoJGwAjafTBegJHRoaXNAkAQboKOglJOgBBxAsEBAQEAEAaCRkTNSYWNlcmQubVRlbXBlcmF0dXJlQKCwUQD/BBdA",
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "call to void Racerd.boilWater()",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 0,
|
||||
"line_number": 13
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "access to `this.Racerd.mTemperature`",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 1,
|
||||
"line_number": 17
|
||||
}
|
||||
],
|
||||
"bug_type": "THREAD_SAFETY_VIOLATION",
|
||||
"bug_type_hum": "Thread Safety Violation",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Racerd.java",
|
||||
"hash": "2882383086ab102a88144ae3c2cc4701",
|
||||
"key": "Racerd.java|makeDinner|THREAD_SAFETY_VIOLATION",
|
||||
"kind": "ERROR",
|
||||
"line": 13,
|
||||
"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": "hJWmvgAAAJgAAAAqAAAAgwAAAHqwkNAod2l0aGRyYXegoEAjaW50QJOgJ0FjY291bnRAkKBABAZAoKCSoCBAsGMA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmGQoKCRsAI2n0wXoCR0aGlzQJAEG6CjoJSToAQZQLBAQEBABAGgkZEwQWNjb3VudC5tQmFsYW5jZUCgBBegsGIA/wQYQA==",
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "<Read trace>",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 0,
|
||||
"line_number": 35
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "access to `this.Account.mBalance`",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 0,
|
||||
"line_number": 35
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "<Write trace>",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 0,
|
||||
"line_number": 34
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "access to `this.Account.mBalance`",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 0,
|
||||
"line_number": 34
|
||||
}
|
||||
],
|
||||
"bug_type": "THREAD_SAFETY_VIOLATION",
|
||||
"bug_type_hum": "Thread Safety Violation",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Racerd.java",
|
||||
"hash": "5665f12d2392f93f11f556cd1b1e238a",
|
||||
"key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION",
|
||||
"kind": "ERROR",
|
||||
"line": 35,
|
||||
"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": "hJWmvgAAAJEAAAAoAAAAfAAAAHOwkNAod2l0aGRyYXegoEAjaW50QJOgJ0FjY291bnRAkKBABAZAoKCSoCBAsGIA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmGRoKCRsAI2n0wXoCR0aGlzQJAEG6CjoJSToAQZQLBAQEBABAGgkZEwQWNjb3VudC5tQmFsYW5jZUCgBBdA",
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "access to `this.Account.mBalance`",
|
||||
"filename": "autotest/src/main/java/Racerd.java",
|
||||
"level": 0,
|
||||
"line_number": 34
|
||||
}
|
||||
],
|
||||
"bug_type": "THREAD_SAFETY_VIOLATION",
|
||||
"bug_type_hum": "Thread Safety Violation",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Racerd.java",
|
||||
"hash": "a7c30fd1b251d9e16750fc7e5913b885",
|
||||
"key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION",
|
||||
"kind": "ERROR",
|
||||
"line": 34,
|
||||
"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"
|
||||
}
|
||||
]
|
||||
|
|
@ -0,0 +1,25 @@
|
|||
/* This Source Code Form is subject to the terms of the Mozilla Public
|
||||
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
||||
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
||||
|
||||
// Examples taken from the infer website.
|
||||
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
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,65 @@
|
|||
[
|
||||
{
|
||||
"bug_class": "PROVER",
|
||||
"bug_trace": [
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "[Trace 1] `void Starvation.lockAThenB()`",
|
||||
"filename": "autotest/src/main/java/Starvation.java",
|
||||
"level": 0,
|
||||
"line_number": 11
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "locks `this.Starvation.lockA` in class `Starvation*`",
|
||||
"filename": "autotest/src/main/java/Starvation.java",
|
||||
"level": 0,
|
||||
"line_number": 11
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "locks `this.Starvation.lockB` in class `Starvation*`",
|
||||
"filename": "autotest/src/main/java/Starvation.java",
|
||||
"level": 1,
|
||||
"line_number": 12
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "[Trace 2] `void Starvation.lockBThenA()`",
|
||||
"filename": "autotest/src/main/java/Starvation.java",
|
||||
"level": 0,
|
||||
"line_number": 19
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "locks `this.Starvation.lockB` in class `Starvation*`",
|
||||
"filename": "autotest/src/main/java/Starvation.java",
|
||||
"level": 0,
|
||||
"line_number": 19
|
||||
},
|
||||
{
|
||||
"column_number": -1,
|
||||
"description": "locks `this.Starvation.lockA` in class `Starvation*`",
|
||||
"filename": "autotest/src/main/java/Starvation.java",
|
||||
"level": 1,
|
||||
"line_number": 20
|
||||
}
|
||||
],
|
||||
"bug_type": "DEADLOCK",
|
||||
"bug_type_hum": "Deadlock",
|
||||
"censored_reason": "",
|
||||
"column": -1,
|
||||
"file": "autotest/src/main/java/Starvation.java",
|
||||
"hash": "043d28a94431b4c573b949b8570fb318",
|
||||
"key": "Starvation.java|lockAThenB|DEADLOCK",
|
||||
"kind": "ERROR",
|
||||
"line": 11,
|
||||
"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 11 in `void Starvation.lockAThenB()`) and then locks `this.Starvation.lockB` in class `Starvation*` (line 12 in `void Starvation.lockAThenB()`).\nTrace 2 (starts at `void Starvation.lockBThenA()`), first locks `this.Starvation.lockB` in class `Starvation*` (line 19 in `void Starvation.lockBThenA()`) and then locks `this.Starvation.lockA` in class `Starvation*` (line 20 in `void Starvation.lockBThenA()`).",
|
||||
"severity": "HIGH",
|
||||
"visibility": "user"
|
||||
}
|
||||
]
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
allprojects {
|
||||
// Expose the per-object-directory configuration to all projects.
|
||||
ext {
|
||||
topobjdir = gradle.mozconfig.topobjdir
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
org.gradle.parallel=true
|
||||
org.gradle.daemon=true
|
||||
org.gradle.jvmargs=-Xmx2560M
|
||||
Двоичный файл не отображается.
|
|
@ -0,0 +1,6 @@
|
|||
distributionBase=GRADLE_USER_HOME
|
||||
distributionPath=wrapper/dists
|
||||
zipStoreBase=GRADLE_USER_HOME
|
||||
zipStorePath=wrapper/dists
|
||||
distributionUrl=https\://services.gradle.org/distributions/gradle-4.4-all.zip
|
||||
distributionSha256Sum=7a2c66d1a78f811d5f37d14630ad21cec5e77a2a4dc61e787e2257a6341016ce
|
||||
|
|
@ -0,0 +1,172 @@
|
|||
#!/usr/bin/env sh
|
||||
|
||||
##############################################################################
|
||||
##
|
||||
## Gradle start up script for UN*X
|
||||
##
|
||||
##############################################################################
|
||||
|
||||
# Attempt to set APP_HOME
|
||||
# Resolve links: $0 may be a link
|
||||
PRG="$0"
|
||||
# Need this for relative symlinks.
|
||||
while [ -h "$PRG" ] ; do
|
||||
ls=`ls -ld "$PRG"`
|
||||
link=`expr "$ls" : '.*-> \(.*\)$'`
|
||||
if expr "$link" : '/.*' > /dev/null; then
|
||||
PRG="$link"
|
||||
else
|
||||
PRG=`dirname "$PRG"`"/$link"
|
||||
fi
|
||||
done
|
||||
SAVED="`pwd`"
|
||||
cd "`dirname \"$PRG\"`/" >/dev/null
|
||||
APP_HOME="`pwd -P`"
|
||||
cd "$SAVED" >/dev/null
|
||||
|
||||
APP_NAME="Gradle"
|
||||
APP_BASE_NAME=`basename "$0"`
|
||||
|
||||
# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
|
||||
DEFAULT_JVM_OPTS=""
|
||||
|
||||
# Use the maximum available, or set MAX_FD != -1 to use that value.
|
||||
MAX_FD="maximum"
|
||||
|
||||
warn () {
|
||||
echo "$*"
|
||||
}
|
||||
|
||||
die () {
|
||||
echo
|
||||
echo "$*"
|
||||
echo
|
||||
exit 1
|
||||
}
|
||||
|
||||
# OS specific support (must be 'true' or 'false').
|
||||
cygwin=false
|
||||
msys=false
|
||||
darwin=false
|
||||
nonstop=false
|
||||
case "`uname`" in
|
||||
CYGWIN* )
|
||||
cygwin=true
|
||||
;;
|
||||
Darwin* )
|
||||
darwin=true
|
||||
;;
|
||||
MINGW* )
|
||||
msys=true
|
||||
;;
|
||||
NONSTOP* )
|
||||
nonstop=true
|
||||
;;
|
||||
esac
|
||||
|
||||
CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar
|
||||
|
||||
# Determine the Java command to use to start the JVM.
|
||||
if [ -n "$JAVA_HOME" ] ; then
|
||||
if [ -x "$JAVA_HOME/jre/sh/java" ] ; then
|
||||
# IBM's JDK on AIX uses strange locations for the executables
|
||||
JAVACMD="$JAVA_HOME/jre/sh/java"
|
||||
else
|
||||
JAVACMD="$JAVA_HOME/bin/java"
|
||||
fi
|
||||
if [ ! -x "$JAVACMD" ] ; then
|
||||
die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME
|
||||
|
||||
Please set the JAVA_HOME variable in your environment to match the
|
||||
location of your Java installation."
|
||||
fi
|
||||
else
|
||||
JAVACMD="java"
|
||||
which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
|
||||
|
||||
Please set the JAVA_HOME variable in your environment to match the
|
||||
location of your Java installation."
|
||||
fi
|
||||
|
||||
# Increase the maximum file descriptors if we can.
|
||||
if [ "$cygwin" = "false" -a "$darwin" = "false" -a "$nonstop" = "false" ] ; then
|
||||
MAX_FD_LIMIT=`ulimit -H -n`
|
||||
if [ $? -eq 0 ] ; then
|
||||
if [ "$MAX_FD" = "maximum" -o "$MAX_FD" = "max" ] ; then
|
||||
MAX_FD="$MAX_FD_LIMIT"
|
||||
fi
|
||||
ulimit -n $MAX_FD
|
||||
if [ $? -ne 0 ] ; then
|
||||
warn "Could not set maximum file descriptor limit: $MAX_FD"
|
||||
fi
|
||||
else
|
||||
warn "Could not query maximum file descriptor limit: $MAX_FD_LIMIT"
|
||||
fi
|
||||
fi
|
||||
|
||||
# For Darwin, add options to specify how the application appears in the dock
|
||||
if $darwin; then
|
||||
GRADLE_OPTS="$GRADLE_OPTS \"-Xdock:name=$APP_NAME\" \"-Xdock:icon=$APP_HOME/media/gradle.icns\""
|
||||
fi
|
||||
|
||||
# For Cygwin, switch paths to Windows format before running java
|
||||
if $cygwin ; then
|
||||
APP_HOME=`cygpath --path --mixed "$APP_HOME"`
|
||||
CLASSPATH=`cygpath --path --mixed "$CLASSPATH"`
|
||||
JAVACMD=`cygpath --unix "$JAVACMD"`
|
||||
|
||||
# We build the pattern for arguments to be converted via cygpath
|
||||
ROOTDIRSRAW=`find -L / -maxdepth 1 -mindepth 1 -type d 2>/dev/null`
|
||||
SEP=""
|
||||
for dir in $ROOTDIRSRAW ; do
|
||||
ROOTDIRS="$ROOTDIRS$SEP$dir"
|
||||
SEP="|"
|
||||
done
|
||||
OURCYGPATTERN="(^($ROOTDIRS))"
|
||||
# Add a user-defined pattern to the cygpath arguments
|
||||
if [ "$GRADLE_CYGPATTERN" != "" ] ; then
|
||||
OURCYGPATTERN="$OURCYGPATTERN|($GRADLE_CYGPATTERN)"
|
||||
fi
|
||||
# Now convert the arguments - kludge to limit ourselves to /bin/sh
|
||||
i=0
|
||||
for arg in "$@" ; do
|
||||
CHECK=`echo "$arg"|egrep -c "$OURCYGPATTERN" -`
|
||||
CHECK2=`echo "$arg"|egrep -c "^-"` ### Determine if an option
|
||||
|
||||
if [ $CHECK -ne 0 ] && [ $CHECK2 -eq 0 ] ; then ### Added a condition
|
||||
eval `echo args$i`=`cygpath --path --ignore --mixed "$arg"`
|
||||
else
|
||||
eval `echo args$i`="\"$arg\""
|
||||
fi
|
||||
i=$((i+1))
|
||||
done
|
||||
case $i in
|
||||
(0) set -- ;;
|
||||
(1) set -- "$args0" ;;
|
||||
(2) set -- "$args0" "$args1" ;;
|
||||
(3) set -- "$args0" "$args1" "$args2" ;;
|
||||
(4) set -- "$args0" "$args1" "$args2" "$args3" ;;
|
||||
(5) set -- "$args0" "$args1" "$args2" "$args3" "$args4" ;;
|
||||
(6) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" ;;
|
||||
(7) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" ;;
|
||||
(8) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" ;;
|
||||
(9) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" "$args8" ;;
|
||||
esac
|
||||
fi
|
||||
|
||||
# Escape application args
|
||||
save () {
|
||||
for i do printf %s\\n "$i" | sed "s/'/'\\\\''/g;1s/^/'/;\$s/\$/' \\\\/" ; done
|
||||
echo " "
|
||||
}
|
||||
APP_ARGS=$(save "$@")
|
||||
|
||||
# Collect all arguments for the java command, following the shell quoting and substitution rules
|
||||
eval set -- $DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS "\"-Dorg.gradle.appname=$APP_BASE_NAME\"" -classpath "\"$CLASSPATH\"" org.gradle.wrapper.GradleWrapperMain "$APP_ARGS"
|
||||
|
||||
# by default we should be in the correct project dir, but when run from Finder on Mac, the cwd is wrong
|
||||
if [ "$(uname)" = "Darwin" ] && [ "$HOME" = "$PWD" ]; then
|
||||
cd "$(dirname "$0")"
|
||||
fi
|
||||
|
||||
exec "$JAVACMD" "$@"
|
||||
|
|
@ -0,0 +1,84 @@
|
|||
@if "%DEBUG%" == "" @echo off
|
||||
@rem ##########################################################################
|
||||
@rem
|
||||
@rem Gradle startup script for Windows
|
||||
@rem
|
||||
@rem ##########################################################################
|
||||
|
||||
@rem Set local scope for the variables with windows NT shell
|
||||
if "%OS%"=="Windows_NT" setlocal
|
||||
|
||||
set DIRNAME=%~dp0
|
||||
if "%DIRNAME%" == "" set DIRNAME=.
|
||||
set APP_BASE_NAME=%~n0
|
||||
set APP_HOME=%DIRNAME%
|
||||
|
||||
@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
|
||||
set DEFAULT_JVM_OPTS=
|
||||
|
||||
@rem Find java.exe
|
||||
if defined JAVA_HOME goto findJavaFromJavaHome
|
||||
|
||||
set JAVA_EXE=java.exe
|
||||
%JAVA_EXE% -version >NUL 2>&1
|
||||
if "%ERRORLEVEL%" == "0" goto init
|
||||
|
||||
echo.
|
||||
echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
|
||||
echo.
|
||||
echo Please set the JAVA_HOME variable in your environment to match the
|
||||
echo location of your Java installation.
|
||||
|
||||
goto fail
|
||||
|
||||
:findJavaFromJavaHome
|
||||
set JAVA_HOME=%JAVA_HOME:"=%
|
||||
set JAVA_EXE=%JAVA_HOME%/bin/java.exe
|
||||
|
||||
if exist "%JAVA_EXE%" goto init
|
||||
|
||||
echo.
|
||||
echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
|
||||
echo.
|
||||
echo Please set the JAVA_HOME variable in your environment to match the
|
||||
echo location of your Java installation.
|
||||
|
||||
goto fail
|
||||
|
||||
:init
|
||||
@rem Get command-line arguments, handling Windows variants
|
||||
|
||||
if not "%OS%" == "Windows_NT" goto win9xME_args
|
||||
|
||||
:win9xME_args
|
||||
@rem Slurp the command line arguments.
|
||||
set CMD_LINE_ARGS=
|
||||
set _SKIP=2
|
||||
|
||||
:win9xME_args_slurp
|
||||
if "x%~1" == "x" goto execute
|
||||
|
||||
set CMD_LINE_ARGS=%*
|
||||
|
||||
:execute
|
||||
@rem Setup the command line
|
||||
|
||||
set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
|
||||
|
||||
@rem Execute Gradle
|
||||
"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %CMD_LINE_ARGS%
|
||||
|
||||
:end
|
||||
@rem End local scope for the variables with windows NT shell
|
||||
if "%ERRORLEVEL%"=="0" goto mainEnd
|
||||
|
||||
:fail
|
||||
rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
|
||||
rem the _cmd.exe /c_ return code!
|
||||
if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
|
||||
exit /b 1
|
||||
|
||||
:mainEnd
|
||||
if "%OS%"=="Windows_NT" endlocal
|
||||
|
||||
:omega
|
||||
|
|
@ -0,0 +1,24 @@
|
|||
// Check out root/settings.gradle for more information
|
||||
|
||||
rootProject.name = 'infer'
|
||||
|
||||
def topsrcdir = rootProject.projectDir.absolutePath + '/../../..'
|
||||
|
||||
def commandLine = ["${topsrcdir}/mach", "environment", "--format", "json", "--verbose"]
|
||||
def proc = commandLine.execute(null, new File(topsrcdir))
|
||||
def standardOutput = new ByteArrayOutputStream()
|
||||
proc.consumeProcessOutput(standardOutput, standardOutput)
|
||||
proc.waitFor()
|
||||
|
||||
if (proc.exitValue() != 0) {
|
||||
throw new GradleException("Process '${commandLine}' finished with non-zero exit value ${proc.exitValue()}:\n\n${standardOutput.toString()}")
|
||||
}
|
||||
|
||||
import groovy.json.JsonSlurper
|
||||
def slurper = new JsonSlurper()
|
||||
def json = slurper.parseText(standardOutput.toString())
|
||||
|
||||
include 'autotest'
|
||||
project(':autotest').projectDir = new File("${json.topsrcdir}/tools/infer/test/autotest")
|
||||
|
||||
gradle.ext.mozconfig = json
|
||||
Загрузка…
Ссылка в новой задаче