diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index eb79155a337..023ccfc81c7 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -399,7 +399,7 @@ jobs: run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}} # This job takes approximately 14 to 46 minutes - check-ubuntu-24_04-cmake-gcc-13: + check-ubuntu-24_04-cmake-gcc-14: runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 @@ -412,13 +412,13 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-13 gdb g++-13 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 + sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-14 gdb g++-14 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 # Update symlinks so that any use of gcc (including our regression - # tests) will use GCC 13. - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-13 110 \ - --slave /usr/bin/g++ g++ /usr/bin/g++-13 \ - --slave /usr/bin/gcov gcov /usr/bin/gcov-13 - sudo ln -sf cpp-13 /usr/bin/cpp + # tests) will use GCC 14. + sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-14 110 \ + --slave /usr/bin/g++ g++ /usr/bin/g++-14 \ + --slave /usr/bin/gcov gcov /usr/bin/gcov-14 + sudo ln -sf cpp-14 /usr/bin/cpp - name: Confirm z3 solver is available and log the version installed run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed @@ -432,10 +432,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-24.04-Release-gcc-13-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-24.04-Release-gcc-13-${{ github.ref }} - ${{ runner.os }}-24.04-Release-gcc-13 + ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }} + ${{ runner.os }}-24.04-Release-gcc-14 - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 117aeb49c17..d4e3f6e7308 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -641,8 +641,9 @@ static code_with_references_listt assign_enum_from_json( dereference_exprt values_struct{ info.symbol_table.lookup_ref(values_name).symbol_expr()}; - const auto &values_struct_type = namespacet{info.symbol_table}.follow_tag( - to_struct_tag_type(values_struct.type())); + const namespacet ns{info.symbol_table}; + const auto &values_struct_type = + ns.follow_tag(to_struct_tag_type(values_struct.type())); PRECONDITION(is_valid_java_array(values_struct_type)); const member_exprt values_data = member_exprt{ values_struct, "data", values_struct_type.components()[2].type()}; diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index c07e2a716aa..4deb6183cde 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -164,7 +164,11 @@ bool is_non_null_library_global(const irep_idt &); extern const std::unordered_set cprover_methods_to_ignore; -symbolt &fresh_java_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +symbolt & +fresh_java_symbol( const typet &type, const std::string &basename_prefix, const source_locationt &source_location, diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 559acb80b04..8fa28b18159 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -444,7 +444,11 @@ void create_invokedynamic_synthetic_classes( } } -static const symbolt &get_or_create_method_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +static const symbolt & +get_or_create_method_symbol( const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 81248f7b8e8..f95bbcff992 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -381,7 +381,7 @@ get_ultimate_source_symbol( /// \return The identifier of the ultimate source symbol assigned to the field, /// which will be used for future calls to /// `require_struct_component_assignment`. -const irep_idt &require_goto_statements::require_struct_component_assignment( +irep_idt require_goto_statements::require_struct_component_assignment( const irep_idt &structure_name, const std::optional &superclass_name, const irep_idt &component_name, @@ -514,8 +514,7 @@ require_goto_statements::require_struct_array_component_assignment( /// \param argument_name: Name of the input argument of method under test /// \param entry_point_statements: The statements to look through /// \return The identifier of the variable assigned to the input argument -const irep_idt & -require_goto_statements::require_entry_point_argument_assignment( +irep_idt require_goto_statements::require_entry_point_argument_assignment( const irep_idt &argument_name, const std::vector &entry_point_statements) { diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.h b/jbmc/unit/java-testing-utils/require_goto_statements.h index ebd78d9d7e4..991286e7c2a 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.h +++ b/jbmc/unit/java-testing-utils/require_goto_statements.h @@ -72,7 +72,7 @@ const code_declt &require_declaration_of_name( const irep_idt &variable_name, const std::vector &entry_point_instructions); -const irep_idt &require_struct_component_assignment( +irep_idt require_struct_component_assignment( const irep_idt &structure_name, const std::optional &superclass_name, const irep_idt &component_name, @@ -89,7 +89,7 @@ const irep_idt &require_struct_array_component_assignment( const std::vector &entry_point_instructions, const symbol_table_baset &symbol_table); -const irep_idt &require_entry_point_argument_assignment( +irep_idt require_entry_point_argument_assignment( const irep_idt &argument_name, const std::vector &entry_point_statements); diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index 513593fb7cc..84f3b51015e 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -24,6 +24,9 @@ namespace require_type pointer_typet require_pointer(const typet &type, const std::optional &subtype); +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif const struct_tag_typet & require_struct_tag(const typet &type, const irep_idt &identifier = ""); diff --git a/scripts/cadical-1.7.2-patch b/scripts/cadical-2.0.0-patch similarity index 100% rename from scripts/cadical-1.7.2-patch rename to scripts/cadical-2.0.0-patch diff --git a/scripts/cadical_CMakeLists.txt b/scripts/cadical_CMakeLists.txt index 9dcb6d27230..c3c0343920e 100644 --- a/scripts/cadical_CMakeLists.txt +++ b/scripts/cadical_CMakeLists.txt @@ -9,7 +9,7 @@ add_library(cadical ${sources}) # Pass -DNBUILD to disable including the version information, which is not # needed since cbmc doesn't run the cadical binary -target_compile_options(cadical PUBLIC -DNBUILD) +target_compile_options(cadical PUBLIC -DNBUILD -DNFLEXIBLE) set_target_properties( cadical diff --git a/src/Makefile b/src/Makefile index e9181a2e039..4b3c4eb5cc7 100644 --- a/src/Makefile +++ b/src/Makefile @@ -186,14 +186,14 @@ glucose-download: @(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch) @$(RM) $(glucose_rev).tar.gz -cadical_release = rel-1.7.2 +cadical_release = rel-2.0.0 cadical-download: @echo "Downloading CaDiCaL $(cadical_release)" @$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz @$(TAR) xfz $(cadical_release).tar.gz @rm -Rf ../cadical @mv cadical-$(cadical_release) ../cadical - @(cd ../cadical; patch -p1 < ../scripts/cadical-1.7.2-patch) + @(cd ../cadical; patch -p1 < ../scripts/cadical-2.0.0-patch) @(cd ../cadical && ./configure CXX="$(CXX)") # Need to rename VERSION so that it isn't picked up by `#include` on # macOS which is case insensitive diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h index 4c938502530..8920a952f1d 100644 --- a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h +++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h @@ -32,8 +32,12 @@ typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16))); typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32))); typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64))); typedef unsigned short __gcc_v32uhi __attribute__ ((__vector_size__ (64))); +typedef unsigned int __gcc_v4usi __attribute__ ((__vector_size__ (16))); +typedef unsigned int __gcc_v8usi __attribute__ ((__vector_size__ (32))); typedef unsigned int __gcc_v16usi __attribute__ ((__vector_size__ (64))); typedef unsigned long long __gcc_di; +typedef unsigned long long __gcc_v2udi __attribute__ ((__vector_size__ (16))); +typedef unsigned long long __gcc_v4udi __attribute__ ((__vector_size__ (32))); typedef unsigned long long __gcc_v8udi __attribute__ ((__vector_size__ (64))); enum __gcc_atomic_memmodels { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h index 7923947bd4f..f7f57896123 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h @@ -72,7 +72,11 @@ struct dfcc_utilst const bool no_nondet_initialization = true); /// Creates a new parameter symbol for the given function_id - static const symbolt &create_new_parameter_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 + [[gnu::no_dangling]] +#endif + static const symbolt & + create_new_parameter_symbol( symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, @@ -100,7 +104,11 @@ struct dfcc_utilst /// The cloned function symbol has `new_function_id` as name /// The cloned parameters symbols have `new_function_id::name` as name /// Returns the new function symbol - static const symbolt &clone_and_rename_function( +#if defined(__GNUC__) && __GNUC__ >= 14 + [[gnu::no_dangling]] +#endif + static const symbolt & + clone_and_rename_function( goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 29d0f766f56..3104f1d9de8 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -607,7 +607,7 @@ exprt interpretert::get_value( { // We want the symbol pointed to mp_integer address = rhs[numeric_cast_v(offset)]; - const symbol_exprt &symbol_expr = address_to_symbol(address); + const symbol_exprt symbol_expr = address_to_symbol(address); mp_integer offset_from_address = address_to_offset(address); if(offset_from_address == 0) @@ -751,7 +751,7 @@ void interpretert::execute_function_call() #if 0 const memory_cellt &cell=memory[address]; #endif - const irep_idt &identifier = address_to_symbol(address).get_identifier(); + const irep_idt identifier = address_to_symbol(address).get_identifier(); trace_step.called_function = identifier; const goto_functionst::function_mapt::const_iterator f_it= diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index ad6d0753e01..0db64f9e5aa 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -54,15 +54,14 @@ mm_iot::mm_iot(symbol_table_baset &symbol_table) { mm_io_r = mm_io_r_symbol->symbol_expr(); - const auto &value_symbol = get_fresh_aux_symbol( - to_code_type(mm_io_r.type()).return_type(), - id2string(id_r) + "$value", - id2string(id_r) + "$value", - mm_io_r_symbol->location, - mm_io_r_symbol->mode, - symbol_table); - - mm_io_r_value = value_symbol.symbol_expr(); + mm_io_r_value = get_fresh_aux_symbol( + to_code_type(mm_io_r.type()).return_type(), + id2string(id_r) + "$value", + id2string(id_r) + "$value", + mm_io_r_symbol->location, + mm_io_r_symbol->mode, + symbol_table) + .symbol_expr(); } if(const auto mm_io_w_symbol = symbol_table.lookup(id_w)) diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index f2c88ae4b1b..375a681b83c 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -347,16 +347,18 @@ void goto_symext::associate_array_to_pointer( const function_application_exprt array_to_pointer_app{ function_symbol.symbol_expr(), {new_char_array, string_data}}; - const symbolt &return_symbol = get_fresh_aux_symbol( - to_mathematical_function_type(function_symbol.type).codomain(), - "", - "return_value", - source_locationt(), - function_symbol.mode, - ns, - state.symbol_table); - - const ssa_exprt ssa_expr(return_symbol.symbol_expr()); + symbol_exprt return_symbol_expr = + get_fresh_aux_symbol( + to_mathematical_function_type(function_symbol.type).codomain(), + "", + "return_value", + source_locationt(), + function_symbol.mode, + ns, + state.symbol_table) + .symbol_expr(); + + const ssa_exprt ssa_expr(return_symbol_expr); symex_assign.assign_symbol( ssa_expr, expr_skeletont{}, array_to_pointer_app, {}); diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index b5f5b0358d4..fe7b2005d53 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -71,17 +71,19 @@ const symbol_exprt &shadow_memoryt::add_field( const typet &field_type) { const auto &function_symbol = ns.lookup(state.source.function_id); - const symbolt &new_symbol = get_fresh_aux_symbol( - field_type, - id2string(state.source.function_id), - SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name), - state.source.pc->source_location(), - function_symbol.mode, - state.symbol_table); + symbol_exprt new_symbol_expr = + get_fresh_aux_symbol( + field_type, + id2string(state.source.function_id), + SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name), + state.source.pc->source_location(), + function_symbol.mode, + state.symbol_table) + .symbol_expr(); auto &addresses = state.shadow_memory.address_fields[field_name]; addresses.push_back( - shadow_memory_statet::shadowed_addresst{expr, new_symbol.symbol_expr()}); + shadow_memory_statet::shadowed_addresst{expr, new_symbol_expr}); return addresses.back().shadow; } diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index f4beccfb669..25a61e2f74e 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -215,14 +215,15 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state) return *cached; } - auto const &cache_symbol = get_fresh_aux_symbol( - cache_key.type(), - "symex", - "dereference_cache", - dereference_result.source_location(), - language_mode, - ns, - state.symbol_table); + auto cache_symbol_expr = get_fresh_aux_symbol( + cache_key.type(), + "symex", + "dereference_cache", + dereference_result.source_location(), + language_mode, + ns, + state.symbol_table) + .symbol_expr(); // we need to lift possible lets // (come from the value set to avoid repeating complex pointer comparisons) @@ -237,7 +238,6 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state) symex_config, target}; - auto cache_symbol_expr = cache_symbol.symbol_expr(); assign.assign_symbol( to_ssa_expr(state.rename(cache_symbol_expr, ns).get()), expr_skeletont{}, diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index f17e389a7e8..003a0d957b1 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -121,11 +121,11 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building solvers with cadical") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch + URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt COMMAND ./configure - URL_MD5 be646831a017f81b300664e58deba1b5 + URL_MD5 9fc2a66196b86adceb822a583318cc35 ) add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) @@ -144,10 +144,10 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building with IPASIR solver linking against: CaDiCaL") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch + URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch COMMAND ./configure - URL_MD5 be646831a017f81b300664e58deba1b5 + URL_MD5 9fc2a66196b86adceb822a583318cc35 ) message(STATUS "Building CaDiCaL") diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 6c46d6e048f..ad1b777b6a8 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -281,7 +281,7 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB) $(LINKLIB) ../../cadical/build/libcadical$(LIBEXT): - $(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS)" + $(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS) -DNFLEXIBLE" -include smt2/smt2_solver$(DEPEXT) diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h index 0bab21812be..72d2ca22ac7 100644 --- a/src/util/fresh_symbol.h +++ b/src/util/fresh_symbol.h @@ -22,7 +22,11 @@ class symbolt; class symbol_table_baset; class typet; -symbolt &get_fresh_aux_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +symbolt & +get_fresh_aux_symbol( const typet &type, const std::string &name_prefix, const std::string &basename_prefix, @@ -30,7 +34,11 @@ symbolt &get_fresh_aux_symbol( const irep_idt &symbol_mode, symbol_table_baset &symbol_table); -symbolt &get_fresh_aux_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +symbolt & +get_fresh_aux_symbol( const typet &type, const std::string &name_prefix, const std::string &basename_prefix, diff --git a/src/util/irep.h b/src/util/irep.h index 97fea5e9c4a..28f87062c48 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -37,7 +37,11 @@ typedef dstringt irep_idt; // NOLINTNEXTLINE(readability/identifiers) typedef dstring_hash irep_id_hash; -inline const std::string &id2string(const irep_idt &d) +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +inline const std::string & +id2string(const irep_idt &d) { return as_string(d); } diff --git a/unit/testing-utils/require_symbol.h b/unit/testing-utils/require_symbol.h index 8bd9d65a3d5..846b17d10df 100644 --- a/unit/testing-utils/require_symbol.h +++ b/unit/testing-utils/require_symbol.h @@ -20,7 +20,11 @@ class symbolt; // NOLINTNEXTLINE(readability/namespace) namespace require_symbol { -const symbolt &require_symbol_exists( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +const symbolt & +require_symbol_exists( const symbol_tablet &symbol_table, const irep_idt &symbol_identifier); } diff --git a/unit/util/graph.cpp b/unit/util/graph.cpp index 30afb8f2441..ef64dbf4207 100644 --- a/unit/util/graph.cpp +++ b/unit/util/graph.cpp @@ -70,7 +70,15 @@ static bool contains_hole( continue; } + // Work around spurious GCC 14 warning about __builtin_memmove accessing + // elements out-of-bounds +#pragma GCC diagnostic push +#ifndef __clang__ +# pragma GCC diagnostic ignored "-Warray-bounds" +# pragma GCC diagnostic ignored "-Wstringop-overflow" +#endif std::vector::node_indext> extended_cycle = cycle_so_far; +#pragma GCC diagnostic pop extended_cycle.push_back(successor.first); if(contains_hole(g, extended_cycle)) return true; @@ -88,7 +96,7 @@ static bool contains_hole(const grapht &g) for(typename grapht::node_indext i = 0; i < g.size(); ++i) { - std::vector::node_indext> start_node {i}; + std::vector::node_indext> start_node(1, i); if(contains_hole(g, start_node)) return true; }