https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940
Bug ID: 104940
Summary: RFE: integrate analyzer with an SMT solver
Product: gcc
Version: 12.0
Status: UNCONFIRMED
Severity: normal
Priority: P3
Component: analyzer
Assignee: dmalcolm at gcc dot gnu.org
Reporter: dmalcolm at gcc dot gnu.org
Target Milestone: ---
-fanalyzer currently has its own constraint_manager class for tracking the
constraints that hold at a point on an execution path, but it only verifies
some of the interactions between constraints and symbolic values, which can
lead to false positives.
For example, consider:
#include "analyzer-decls.h"
void test (int x, int y)
{
if (y == 3)
if (2 * x == y)
__analyzer_dump_path ();
}
The current constraint_manager code has no knowledge that (2 * x == y) is
impossible for integers, and erroneously outputs:
../../src/gcc/testsuite/gcc.dg/analyzer/t.c: In function ‘test’:
../../src/gcc/testsuite/gcc.dg/analyzer/t.c:7:7: note: path
7 | __analyzer_dump_path ();
| ^~~~~~~~~~~~~~~~~~~~~~~
‘test’: events 1-5
|
| 5 | if (y == 3)
| | ^
| | |
| | (1) following ‘true’ branch (when ‘y == 3’)...
| 6 | if (2 * x == y)
| | ~~~~~~
| | | |
| | | (2) ...to here
| | (3) following ‘true’ branch...
| 7 | __analyzer_dump_path ();
| | ~~~~~~~~~~~~~~~~~~~~~~~
| | |
| | (4) ...to here
| | (5) here
|
Idea: get out of the business of tracking constraints by instead calling out to
an SMT solver.
I have a work-in-progress prototype of the analyzer which can call express
constraints as an SMT-LIB2 script, and call out to an external z3 binary.
Presumably we'd want an option to select between different constraint-tracking
implementations, to avoid depending on z3 (or other smt solvers). Might be
faster to link it in-process, but let's cross that bridge when we come to it.
I'm filing this bug as a tracker bug for other constraint-tracking bugs.
