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

[kristerw at gcc dot gnu.org via Gcc-bugs]

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

Krister Walfridsson  changed:

   What|Removed |Added

 CC||kristerw at gcc dot gnu.org

--- Comment #7 from Krister Walfridsson  ---
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

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

[dmalcolm at gcc dot gnu.org via Gcc-bugs]

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

--- Comment #6 from David Malcolm  ---
https://github.com/kristerw/pysmtgcc

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

[dmalcolm at gcc dot gnu.org via Gcc-bugs]

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

--- Comment #5 from David Malcolm  ---
See also:
  https://kristerw.github.io/2022/11/01/verifying-optimizations/

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

[cvs-commit at gcc dot gnu.org via Gcc-bugs]

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

--- Comment #4 from CVS Commits  ---
The master branch has been updated by David Malcolm :

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

commit r14-2793-g9d804f9b2709b38235a2fe4c6705f2af6784aa2a
Author: David Malcolm 
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

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

[dmalcolm at gcc dot gnu.org via Gcc-bugs]

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

--- Comment #3 from David Malcolm  ---
*** Bug 109195 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 via Gcc-bugs]

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

--- Comment #2 from David Malcolm  ---
*** 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 via Gcc-bugs]

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

David Malcolm  changed:

   What|Removed |Added

 CC||geoffreydgr at icloud dot com

--- Comment #1 from David Malcolm  ---
*** Bug 109193 has been marked as a duplicate of this bug. ***