Skip to content

Commit

Permalink
Merge pull request Ericsson#2222 from bruntib/fix_z3
Browse files Browse the repository at this point in the history 
Switching z3 refutation on by default.
  • Loading branch information
Gyorgy Orban authored Jul 11, 2019
2 parents b8c9a4a + 0c09402 commit 28cb139
Show file tree
Hide file tree
Showing 5 changed files with 63 additions and 29 deletions.
20 changes: 19 additions & 1 deletion analyzer/codechecker_analyzer/analyzers/analyzer_types.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,26 @@ def is_z3_capable(context):
check_supported_analyzers([ClangSA.ANALYZER_NAME], context)
analyzer_binary = context.analyzer_binaries.get(ClangSA.ANALYZER_NAME)

analyzer_env = env.extend(context.path_env_extra,
context.ld_lib_path_extra)

return host_check.has_analyzer_option(analyzer_binary,
['-analyzer-constraints=z3'])
['-Xclang',
'-analyzer-constraints=z3'],
analyzer_env)


def is_z3_refutation_capable(context):
""" Detects if the current clang is Z3 refutation compatible. """
check_supported_analyzers([ClangSA.ANALYZER_NAME], context)
analyzer_binary = context.analyzer_binaries.get(ClangSA.ANALYZER_NAME)

analyzer_env = env.extend(context.path_env_extra,
context.ld_lib_path_extra)

return host_check.has_analyzer_config_option(analyzer_binary,
'crosscheck-with-z3',
analyzer_env)


def check_supported_analyzers(analyzers, context):
Expand Down
4 changes: 2 additions & 2 deletions analyzer/codechecker_analyzer/analyzers/clangsa/analyzer.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -333,10 +333,10 @@ def construct_config_handler(cls, args, context):
handler.report_hash = args.report_hash \
if 'report_hash' in args else None

handler.enable_z3 = 'enable_z3' in args and args.enable_z3
handler.enable_z3 = 'enable_z3' in args and args.enable_z3 == 'on'

handler.enable_z3_refutation = 'enable_z3_refutation' in args and \
args.enable_z3_refutation
args.enable_z3_refutation == 'on'

if 'ctu_phases' in args:
handler.ctu_dir = os.path.join(args.output_path,
Expand Down
18 changes: 12 additions & 6 deletions analyzer/codechecker_analyzer/cmd/analyze.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -290,23 +290,29 @@ def add_arguments_to_parser(parser):
"one.")

context = analyzer_context.get_context()
clang_has_z3 = analyzer_types.is_z3_capable(context)

if analyzer_types.is_z3_capable(context):
if clang_has_z3:
analyzer_opts.add_argument('--z3',
action='store_true',
dest='enable_z3',
default=argparse.SUPPRESS,
choices=['on', 'off'],
default='off',
help="Enable the z3 solver backend. This "
"allows reasoning over more complex "
"queries, but performance is worse "
"than the default range-based "
"constraint solver.")

clang_has_z3_refutation = analyzer_types.is_z3_refutation_capable(context)

if clang_has_z3_refutation:
analyzer_opts.add_argument('--z3-refutation',
action='store_true',
dest='enable_z3_refutation',
default=argparse.SUPPRESS,
help="Enable the Z3 SMT Solver backend to "
choices=['on', 'off'],
default='on' if clang_has_z3_refutation
else 'off',
help="Switch on/off the Z3 SMT Solver "
"backend to "
"reduce false positives. The results "
"of the ranged based constraint "
"solver in the Clang Static Analyzer "
Expand Down
18 changes: 12 additions & 6 deletions analyzer/codechecker_analyzer/cmd/check.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -319,23 +319,29 @@ def add_arguments_to_parser(parser):
"one.")

context = analyzer_context.get_context()
clang_has_z3 = analyzer_types.is_z3_capable(context)

if analyzer_types.is_z3_capable(context):
if clang_has_z3:
analyzer_opts.add_argument('--z3',
action='store_true',
dest='enable_z3',
default=argparse.SUPPRESS,
choices=['on', 'off'],
default='off',
help="Enable the z3 solver backend. This "
"allows reasoning over more complex "
"queries, but performance is worse "
"than the default range-based "
"constraint solver.")

clang_has_z3_refutation = analyzer_types.is_z3_refutation_capable(context)

if clang_has_z3_refutation:
analyzer_opts.add_argument('--z3-refutation',
action='store_true',
dest='enable_z3_refutation',
default=argparse.SUPPRESS,
help="Enable the Z3 SMT Solver backend to "
choices=['on', 'off'],
default='on' if clang_has_z3_refutation
else 'off',
help="Switch on/off the Z3 SMT Solver "
"backend to "
"reduce false positives. The results "
"of the ranged based constraint "
"solver in the Clang Static Analyzer "
Expand Down
32 changes: 18 additions & 14 deletions docs/analyzer/user_guide.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -199,15 +199,17 @@ analyzer arguments:
analysis of a particular file takes longer than this
time, the analyzer is killed and the analysis is
considered as a failed one.
--z3 Enable the z3 solver backend. This allows reasoning
--z3 {on,off} Enable the z3 solver backend. This allows reasoning
over more complex queries, but performance is worse
than the default range-based constraint solver.
--z3-refutation Enable the Z3 SMT Solver backend to reduce false
positives. The results of the ranged based constraint
solver in the Clang Static Analyzer will be cross
checked with the Z3 SMT solver. This should not cause
that much of a slowdown compared to using the Z3
solver only.
(default: off)
--z3-refutation {on,off}
Switch on/off the Z3 SMT Solver backend to reduce
false positives. The results of the ranged based
constraint solver in the Clang Static Analyzer will be
cross checked with the Z3 SMT solver. This should not
cause that much of a slowdown compared to using the Z3
solver only. (default: on)
checker configuration:
Expand Down Expand Up @@ -551,15 +553,17 @@ analyzer arguments:
analysis of a particular file takes longer than this
time, the analyzer is killed and the analysis is
considered as a failed one.
--z3 Enable the z3 solver backend. This allows reasoning
--z3 {on,off} Enable the z3 solver backend. This allows reasoning
over more complex queries, but performance is worse
than the default range-based constraint solver.
--z3-refutation Enable the Z3 SMT Solver backend to reduce false
positives. The results of the ranged based constraint
solver in the Clang Static Analyzer will be cross
checked with the Z3 SMT solver. This should not cause
that much of a slowdown compared to using the Z3
solver only.
(default: off)
--z3-refutation {on,off}
Switch on/off the Z3 SMT Solver backend to reduce
false positives. The results of the ranged based
constraint solver in the Clang Static Analyzer will be
cross checked with the Z3 SMT solver. This should not
cause that much of a slowdown compared to using the Z3
solver only. (default: on)
```

CodeChecker supports several analyzer tools. Currently, these analyzers are
Expand Down

0 comments on commit 28cb139

Please sign in to comment.