Skip to content

Commit

Permalink
Merge pull request #3772 from whisperity/fix/doc/z3
Browse files Browse the repository at this point in the history 
[analyzer][doc] Mention that Z3 as the constraint solver is highly unstable
  • Loading branch information
@bruntib
bruntib authored Oct 24, 2022
2 parents 6907145 + fb37f3f commit e918ac4
Show file tree
Hide file tree
Showing 4 changed files with 41 additions and 30 deletions.
15 changes: 9 additions & 6 deletions analyzer/codechecker_analyzer/cmd/analyze.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -454,11 +454,14 @@ def add_arguments_to_parser(parser):
dest='enable_z3',
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.")
help="Enable Z3 as the solver backend. "
"This allows reasoning over more "
"complex queries, but performance is "
"much worse than the default "
"range-based constraint solver "
"system. WARNING: Z3 as the only "
"backend is a highly experimental "
"and likely unstable feature.")

clang_has_z3_refutation = analyzer_types.is_z3_refutation_capable(context)

Expand All @@ -476,7 +479,7 @@ def add_arguments_to_parser(parser):
"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.")
"using only the Z3 solver.")

if analyzer_types.is_ctu_capable(context):
ctu_opts = parser.add_argument_group(
Expand Down
15 changes: 9 additions & 6 deletions analyzer/codechecker_analyzer/cmd/check.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -402,11 +402,14 @@ def add_arguments_to_parser(parser):
dest='enable_z3',
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.")
help="Enable Z3 as the solver backend. "
"This allows reasoning over more "
"complex queries, but performance is "
"much worse than the default "
"range-based constraint solver "
"system. WARNING: Z3 as the only "
"backend is a highly experimental "
"and likely unstable feature.")

clang_has_z3_refutation = analyzer_types.is_z3_refutation_capable(context)

Expand All @@ -424,7 +427,7 @@ def add_arguments_to_parser(parser):
"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.")
"using only the Z3 solver.")

if analyzer_types.is_ctu_capable(context):
ctu_opts = parser.add_argument_group(
Expand Down
15 changes: 9 additions & 6 deletions docs/analyzer/checker_and_analyzer_configuration.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,16 +70,19 @@ If they are needed, they can be switched on using the following command
is for example `-Xclang -analyzer-checker=debug.ExprInspection`.

## Z3 Theorem Prover
The static analyzer supports using the
The _Clang Static Analyzer_ supports using the
[Z3 Theorem Prover](https://github.com/Z3Prover/z3) from Microsoft Research as
an external constraint solver. This allows reasoning over more complex queries,
but performance is `~15x` slower than the default range-based constraint
solver. To enable the Z3 solver backend, Clang must be built with the
`CLANG_ANALYZER_BUILD_Z3=ON` option, and the
but performance is expected to be **15-20 times** slower than the default
range-based constraint solver engine.

To enable the Z3 solver backend, Clang must be built with the
`LLVM_ENABLE_Z3_SOLVER=ON` compile-time option (for versions earlier than
**9.0**, `CLANG_ANALYZER_BUILD_Z3=ON` must be used instead!), and the
`-Xanalyzer -analyzer-constraints=z3` arguments passed at runtime. CodeChecker
will automatically detect that the Clang was built with this option and you
will automatically detect whether Clang was built with this option and you
don't have to pass these arguments to the analyzer command itself when using
CodeChecker, you just have to run the CodeChecker analyze command with the
CodeChecker, you just have to run the `CodeChecker analyze` command with the
`--z3` option.

You can read more about Z3 Theorem Prover
Expand Down
26 changes: 14 additions & 12 deletions docs/analyzer/user_guide.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -304,17 +304,18 @@ 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 {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.
(default: off)
--z3 {on,off} Enable Z3 as the solver backend. This allows reasoning
over more complex queries, but performance is much worse
than the default range-based constraint solver system.
WARNING: Z3 as the only backend is a highly
experimental and likely unstable feature. (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)
cause that much of a slowdown compared to using only the
Z3 solver. (default: on)
cross translation unit analysis arguments:
Expand Down Expand Up @@ -1130,17 +1131,18 @@ 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 {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.
(default: off)
--z3 {on,off} Enable Z3 as the solver backend. This allows reasoning
over more complex queries, but performance is much worse
than the default range-based constraint solver system.
WARNING: Z3 as the only backend is a highly
experimental and likely unstable feature. (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)
cause that much of a slowdown compared to using only the
Z3 solver. (default: on)
```

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

0 comments on commit e918ac4

Please sign in to comment.