[Bug analyzer/104940] New: RFE: integrate analyzer with an SMT solver

[Bug analyzer/104940] New: RFE: integrate analyzer with an SMT solver

[dmalcolm at gcc dot gnu.org]

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.

[Bug analyzer/104940] RFE: integrate analyzer with an SMT solver

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940

David Malcolm <dmalcolm at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |geoffreydgr at icloud dot com

--- Comment #1 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
*** Bug 109193 has been marked as a duplicate of this bug. ***

[Bug analyzer/104940] RFE: integrate analyzer with an SMT solver

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940

--- Comment #2 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
*** Bug 109194 has been marked as a duplicate of this bug. ***

[Bug analyzer/104940] RFE: integrate analyzer with an SMT solver

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940

--- Comment #3 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
*** Bug 109195 has been marked as a duplicate of this bug. ***

[Bug analyzer/104940] RFE: integrate analyzer with an SMT solver

[cvs-commit at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940

--- Comment #4 from CVS Commits <cvs-commit at gcc dot gnu.org> ---
The master branch has been updated by David Malcolm <dmalcolm@gcc.gnu.org>:

https://gcc.gnu.org/g:9d804f9b2709b38235a2fe4c6705f2af6784aa2a

commit r14-2793-g9d804f9b2709b38235a2fe4c6705f2af6784aa2a
Author: David Malcolm <dmalcolm@redhat.com>
Date:   Wed Jul 26 10:29:20 2023 -0400

    analyzer: add symbol base class, moving region id to there [PR104940]

    This patch introduces a "symbol" base class that region and svalue
    both inherit from, generalizing the ID from the region class so it's
    also used by svalues.  This gives a way of sorting regions and svalues
    into creation order, which I've found useful in my experiments with
    adding SMT support (PR analyzer/104940).

    gcc/ChangeLog:
            PR analyzer/104940
            * Makefile.in (ANALYZER_OBJS): Add analyzer/symbol.o.

    gcc/analyzer/ChangeLog:
            PR analyzer/104940
            * region-model-manager.cc
            (region_model_manager::region_model_manager): Update for
            generalizing region ids to also cover svalues.
            (region_model_manager::get_or_create_constant_svalue): Likewise.
            (region_model_manager::get_or_create_unknown_svalue): Likewise.
            (region_model_manager::create_unique_svalue): Likewise.
            (region_model_manager::get_or_create_initial_value): Likewise.
            (region_model_manager::get_or_create_setjmp_svalue): Likewise.
            (region_model_manager::get_or_create_poisoned_svalue): Likewise.
            (region_model_manager::get_ptr_svalue): Likewise.
            (region_model_manager::get_or_create_unaryop): Likewise.
            (region_model_manager::get_or_create_binop): Likewise.
            (region_model_manager::get_or_create_sub_svalue): Likewise.
            (region_model_manager::get_or_create_repeated_svalue): Likewise.
            (region_model_manager::get_or_create_bits_within): Likewise.
            (region_model_manager::get_or_create_unmergeable): Likewise.
            (region_model_manager::get_or_create_widening_svalue): Likewise.
            (region_model_manager::get_or_create_compound_svalue): Likewise.
            (region_model_manager::get_or_create_conjured_svalue): Likewise.
            (region_model_manager::get_or_create_asm_output_svalue): Likewise.
            (region_model_manager::get_or_create_const_fn_result_svalue):
            Likewise.
            (region_model_manager::get_region_for_fndecl): Likewise.
            (region_model_manager::get_region_for_label): Likewise.
            (region_model_manager::get_region_for_global): Likewise.
            (region_model_manager::get_field_region): Likewise.
            (region_model_manager::get_element_region): Likewise.
            (region_model_manager::get_offset_region): Likewise.
            (region_model_manager::get_sized_region): Likewise.
            (region_model_manager::get_cast_region): Likewise.
            (region_model_manager::get_frame_region): Likewise.
            (region_model_manager::get_symbolic_region): Likewise.
            (region_model_manager::get_region_for_string): Likewise.
            (region_model_manager::get_bit_range): Likewise.
            (region_model_manager::get_var_arg_region): Likewise.
            (region_model_manager::get_region_for_unexpected_tree_code):
            Likewise.
            (region_model_manager::get_or_create_region_for_heap_alloc):
            Likewise.
            (region_model_manager::create_region_for_alloca): Likewise.
            (region_model_manager::log_stats): Likewise.
            * region-model-manager.h (region_model_manager::get_num_regions):
            Replace with...
            (region_model_manager::get_num_symbols): ...this.
            (region_model_manager::alloc_region_id): Replace with...
            (region_model_manager::alloc_symbol_id): ...this.
            (region_model_manager::m_next_region_id): Replace with...
            (region_model_manager::m_next_symbol_id): ...this.
            * region-model.cc (selftest::test_get_representative_tree): Update
            for generalizing region ids to also cover svalues.
            (selftest::test_binop_svalue_folding): Likewise.
            (selftest::test_state_merging): Likewise.
            * region.cc (region::cmp_ids): Delete, in favor of
            symbol::cmp_ids.
            (region::region): Update for introduction of symbol base class.
            (frame_region::get_region_for_local): Likewise.
            (root_region::root_region): Likewise.
            (symbolic_region::symbolic_region): Likewise.
            * region.h: Replace include of "analyzer/complexity.h" with
            "analyzer/symbol.h".
            (class region): Make a subclass of symbol.
            (region::get_id): Delete in favor of symbol::get_id.
            (region::cmp_ids): Delete in favor of symbol::cmp_ids.
            (region::get_complexity): Delete in favor of
            symbol::get_complexity.
            (region::region): Use symbol::id_t for "id" param.
            (region::m_complexity): Move field to symbol base class.
            (region::m_id): Likewise.
            (space_region::space_region): Use symbol::id_t for "id" param.
            (frame_region::frame_region): Likewise.
            (globals_region::globals_region): Likewise.
            (code_region::code_region): Likewise.
            (function_region::function_region): Likewise.
            (label_region::label_region): Likewise.
            (stack_region::stack_region): Likewise.
            (heap_region::heap_region): Likewise.
            (thread_local_region::thread_local_region): Likewise.
            (root_region::root_region): Likewise.
            (symbolic_region::symbolic_region): Likewise.
            (decl_region::decl_region): Likewise.
            (field_region::field_region): Likewise.
            (element_region::element_region): Likewise.
            (offset_region::offset_region): Likewise.
            (sized_region::sized_region): Likewise.
            (cast_region::cast_region): Likewise.
            (heap_allocated_region::heap_allocated_region): Likewise.
            (alloca_region::alloca_region): Likewise.
            (string_region::string_region): Likewise.
            (bit_range_region::bit_range_region): Likewise.
            (var_arg_region::var_arg_region): Likewise.
            (errno_region::errno_region): Likewise.
            (unknown_region::unknown_region): Likewise.
            * svalue.cc (sub_svalue::sub_svalue): Add symbol::id_t param.
            (repeated_svalue::repeated_svalue): Likewise.
            (bits_within_svalue::bits_within_svalue): Likewise.
            (compound_svalue::compound_svalue): Likewise.
            * svalue.h: Replace include of "analyzer/complexity.h" with
            "analyzer/symbol.h".
            (class svalue): Make a subclass of symbol.
            (svalue::get_complexity): Delete in favor of
            symbol::get_complexity.
            (svalue::svalue): Add symbol::id_t param.  Update for new base
            class.
            (svalue::m_complexity): Delete in favor of
            symbol::m_complexity.
            (region_svalue::region_svalue): Add symbol::id_t param
            (constant_svalue::constant_svalue): Likewise.
            (unknown_svalue::unknown_svalue): Likewise.
            (poisoned_svalue::poisoned_svalue): Likewise.
            (setjmp_svalue::setjmp_svalue): Likewise.
            (initial_svalue::initial_svalue): Likewise.
            (unaryop_svalue::unaryop_svalue): Likewise.
            (binop_svalue::binop_svalue): Likewise.
            (sub_svalue::sub_svalue): Likewise.
            (repeated_svalue::repeated_svalue): Likewise.
            (bits_within_svalue::bits_within_svalue): Likewise.
            (unmergeable_svalue::unmergeable_svalue): Likewise.
            (placeholder_svalue::placeholder_svalue): Likewise.
            (widening_svalue::widening_svalue): Likewise.
            (compound_svalue::compound_svalue): Likewise.
            (conjured_svalue::conjured_svalue): Likewise.
            (asm_output_svalue::asm_output_svalue): Likewise.
            (const_fn_result_svalue::const_fn_result_svalue): Likewise.
            * symbol.cc: New file.
            * symbol.h: New file.

    Signed-off-by: David Malcolm <dmalcolm@redhat.com>

[Bug analyzer/104940] RFE: integrate analyzer with an SMT solver

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940

--- Comment #5 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
See also:
  https://kristerw.github.io/2022/11/01/verifying-optimizations/

[Bug analyzer/104940] RFE: integrate analyzer with an SMT solver

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940

--- Comment #6 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
https://github.com/kristerw/pysmtgcc

[Bug analyzer/104940] RFE: integrate analyzer with an SMT solver

[kristerw at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940

Krister Walfridsson <kristerw at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |kristerw at gcc dot gnu.org

--- Comment #7 from Krister Walfridsson <kristerw at gcc dot gnu.org> ---
I have released a new version of my tool doing GIMPLE IR to SMT conversion.
This is now written in C++, and converts a bigger subset of GIMPLE. The code is
available at https://github.com/kristerw/smtgcc