public inbox for gcc-bugs@sourceware.org
help / color / mirror / Atom feed
* [Bug analyzer/104940] New: RFE: integrate analyzer with an SMT solver
@ 2022-03-15 18:36 dmalcolm at gcc dot gnu.org
  2023-03-20 20:30 ` [Bug analyzer/104940] " dmalcolm at gcc dot gnu.org
                   ` (6 more replies)
  0 siblings, 7 replies; 8+ messages in thread
From: dmalcolm at gcc dot gnu.org @ 2022-03-15 18:36 UTC (permalink / raw)
  To: gcc-bugs

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.

^ permalink raw reply	[flat|nested] 8+ messages in thread
end of thread, other threads:[~2023-09-30  9:19 UTC | newest]

Thread overview: 8+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-03-15 18:36 [Bug analyzer/104940] New: RFE: integrate analyzer with an SMT solver dmalcolm at gcc dot gnu.org
2023-03-20 20:30 ` [Bug analyzer/104940] " dmalcolm at gcc dot gnu.org
2023-03-20 20:31 ` dmalcolm at gcc dot gnu.org
2023-03-20 20:35 ` dmalcolm at gcc dot gnu.org
2023-07-26 14:31 ` cvs-commit at gcc dot gnu.org
2023-09-24 12:56 ` dmalcolm at gcc dot gnu.org
2023-09-24 13:08 ` dmalcolm at gcc dot gnu.org
2023-09-30  9:18 ` kristerw at gcc dot gnu.org

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).