From d5d54c6663d993545c4a6e768c573140f646b0cf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 2 Apr 2025 10:44:13 +0000 Subject: [PATCH 1/5] Library test no longer fails on Ubuntu 24.04 It would still fail on older platforms, hence marking it `FUTURE` rather than `CORE` or `KNOWNBUG`. --- regression/cbmc-library/fgets-01/__fgets_chk.desc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-library/fgets-01/__fgets_chk.desc b/regression/cbmc-library/fgets-01/__fgets_chk.desc index 8fe85e38cb2..ac913e72cb5 100644 --- a/regression/cbmc-library/fgets-01/__fgets_chk.desc +++ b/regression/cbmc-library/fgets-01/__fgets_chk.desc @@ -1,4 +1,4 @@ -KNOWNBUG +FUTURE main.c --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2 --unwindset fgets:0 ^EXIT=10$ @@ -11,4 +11,6 @@ main.c ^warning: ignoring -- Our asm renaming results in fgets and its alias being one and the same function -to us, so we end up recursing in glibc's fgets wrapper. +to us, so we end up recursing in glibc's fgets wrapper on some platforms. On +Ubuntu 24.04, however, this appears to work fine. Given this disparity this test +is now marked `FUTURE` instead of `KNOWNBUG`. From 30bd93dae5b5990314ea34130ef56e9ce51138b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Apr 2025 08:34:34 +0000 Subject: [PATCH 2/5] Apply use-after-free and empty-symbol-table fixes to Linux 5.10 We cannot compile Linux 5.10 with toolchains involving GCC 12 or newer without these patches. --- integration/linux/compile_linux.sh | 81 ++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) diff --git a/integration/linux/compile_linux.sh b/integration/linux/compile_linux.sh index 45438968ea5..1993dda1744 100755 --- a/integration/linux/compile_linux.sh +++ b/integration/linux/compile_linux.sh @@ -32,6 +32,87 @@ ln -s goto-cc src/goto-cc/goto-g++ configure_linux () { pushd linux_5_10 + # GCC >= 12 correctly reports (and fails with) use-after-free, which was + # eventually fixed in 5.16.11 (and 5.17+) + curl https://github.com/torvalds/linux/commit/52a9dab6d892763b2a8334a568bd4e2c1a6fde66.patch | patch -p1 + # Some versions of binutils fail to generate a symbol table, pick up fix that + # eventually landed in 6.0, see + # https://github.com/torvalds/linux/commit/de979c83574abf6e78f3fa65b716515c91b2613d + cat > de979c83574abf6e78f3fa65b716515c91b2613d-adjusted.patch << "EOF" +diff --git a/arch/x86/entry/Makefile b/arch/x86/entry/Makefile +index 08bf95dbc..83c98dae7 100644 +--- a/arch/x86/entry/Makefile ++++ b/arch/x86/entry/Makefile +@@ -21,12 +21,13 @@ CFLAGS_syscall_64.o += $(call cc-option,-Wno-override-init,) + CFLAGS_syscall_32.o += $(call cc-option,-Wno-override-init,) + CFLAGS_syscall_x32.o += $(call cc-option,-Wno-override-init,) + +-obj-y := entry_$(BITS).o thunk_$(BITS).o syscall_$(BITS).o ++obj-y := entry_$(BITS).o syscall_$(BITS).o + obj-y += common.o + + obj-y += vdso/ + obj-y += vsyscall/ + ++obj-$(CONFIG_PREEMPTION) += thunk_$(BITS).o + obj-$(CONFIG_IA32_EMULATION) += entry_64_compat.o syscall_32.o + obj-$(CONFIG_X86_X32_ABI) += syscall_x32.o + +diff --git a/arch/x86/entry/thunk_32.S b/arch/x86/entry/thunk_32.S +index f1f96d4d8..5997ec0b4 100644 +--- a/arch/x86/entry/thunk_32.S ++++ b/arch/x86/entry/thunk_32.S +@@ -29,10 +29,8 @@ SYM_CODE_START_NOALIGN(\name) + SYM_CODE_END(\name) + .endm + +-#ifdef CONFIG_PREEMPTION + THUNK preempt_schedule_thunk, preempt_schedule + THUNK preempt_schedule_notrace_thunk, preempt_schedule_notrace + EXPORT_SYMBOL(preempt_schedule_thunk) + EXPORT_SYMBOL(preempt_schedule_notrace_thunk) +-#endif + +diff --git a/arch/x86/entry/thunk_64.S b/arch/x86/entry/thunk_64.S +index ccd32877a..c7cf79be7 100644 +--- a/arch/x86/entry/thunk_64.S ++++ b/arch/x86/entry/thunk_64.S +@@ -36,14 +36,11 @@ SYM_FUNC_END(\name) + _ASM_NOKPROBE(\name) + .endm + +-#ifdef CONFIG_PREEMPTION + THUNK preempt_schedule_thunk, preempt_schedule + THUNK preempt_schedule_notrace_thunk, preempt_schedule_notrace + EXPORT_SYMBOL(preempt_schedule_thunk) + EXPORT_SYMBOL(preempt_schedule_notrace_thunk) +-#endif + +-#ifdef CONFIG_PREEMPTION + SYM_CODE_START_LOCAL_NOALIGN(.L_restore) + popq %r11 + popq %r10 +@@ -58,4 +55,3 @@ SYM_CODE_START_LOCAL_NOALIGN(.L_restore) + ret + _ASM_NOKPROBE(.L_restore) + SYM_CODE_END(.L_restore) +-#endif +diff --git a/arch/x86/um/Makefile b/arch/x86/um/Makefile +index 77f70b969..3113800da 100644 +--- a/arch/x86/um/Makefile ++++ b/arch/x86/um/Makefile +@@ -27,7 +27,8 @@ else + + obj-y += syscalls_64.o vdso/ + +-subarch-y = ../lib/csum-partial_64.o ../lib/memcpy_64.o ../entry/thunk_64.o ++subarch-y = ../lib/csum-partial_64.o ../lib/memcpy_64.o ++subarch-$(CONFIG_PREEMPTION) += ../entry/thunk_64.o + + endif + +EOF + patch -p1 < de979c83574abf6e78f3fa65b716515c91b2613d-adjusted.patch cat > kvm-config < Date: Thu, 3 Apr 2025 19:21:01 +0000 Subject: [PATCH 3/5] Address include-what-you-use warnings More recent versions of iwyu identified new unused headers. (But struggled to cope with `class C { ... } c;` so that was rewritten as `class C { ... }; C c;`.) --- src/analyses/global_may_alias.h | 1 - src/ansi-c/ansi_c_language.cpp | 2 -- src/goto-checker/solver_factory.h | 1 + src/goto-programs/goto_program.h | 1 - src/goto-programs/goto_trace.cpp | 2 -- src/goto-programs/show_goto_functions_json.cpp | 2 -- src/goto-programs/show_goto_functions_xml.cpp | 2 -- src/goto-programs/validate_goto_model.h | 2 +- src/goto-symex/goto_symex_state.h | 1 - src/pointer-analysis/value_set.cpp | 2 -- src/solvers/sat/dimacs_cnf.cpp | 2 -- src/solvers/smt2/smt2_dec.cpp | 2 ++ src/solvers/smt2/smt2_dec.h | 2 -- .../smt2_incremental/smt2_incremental_decision_procedure.h | 3 ++- 14 files changed, 6 insertions(+), 19 deletions(-) diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index e2209cdd331..91935163ad6 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H #define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H -#include #include #include diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 4a434bb2f69..87a196298eb 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -23,8 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2c.h" #include "type2name.h" -#include - std::set ansi_c_languaget::extensions() const { return { "c", "i" }; diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index 98784c45ba2..6359d67bd53 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include #include class cmdlinet; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index fa8eca15353..94d87c8fdfe 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_instruction_code.h" -#include #include #include #include diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 0a7797af2d3..72e8927f7c2 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -27,8 +27,6 @@ Author: Daniel Kroening #include #include -#include - static std::optional get_object_rec(const exprt &src) { if(src.id()==ID_symbol) diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index eb2b2c8443e..850424001e0 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -16,8 +16,6 @@ Author: Thomas Kiley #include "goto_functions.h" -#include - /// For outputting the GOTO program in a readable JSON format. /// \param _list_only: output only list of functions, but not their bodies show_goto_functions_jsont::show_goto_functions_jsont(bool _list_only) diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index 32bc23f9464..b38a12badf1 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -16,8 +16,6 @@ Author: Thomas Kiley #include "goto_functions.h" -#include - /// For outputting the GOTO program in a readable xml format. /// \param _list_only: output only list of functions, but not their bodies show_goto_functions_xmlt::show_goto_functions_xmlt(bool _list_only) diff --git a/src/goto-programs/validate_goto_model.h b/src/goto-programs/validate_goto_model.h index 6e399af6692..67439604801 100644 --- a/src/goto-programs/validate_goto_model.h +++ b/src/goto-programs/validate_goto_model.h @@ -10,7 +10,7 @@ Date: Oct 2018 #ifndef CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H #define CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H -#include +#include // IWYU pragma: keep class goto_model_validation_optionst final { diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index fa7c06895f5..939279b8ef2 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -26,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "shadow_memory_state.h" #include -#include class incremental_dirtyt; class symex_target_equationt; diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index b2d7a4fd867..2c41b0484b6 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -27,8 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #ifdef DEBUG #include #include diff --git a/src/solvers/sat/dimacs_cnf.cpp b/src/solvers/sat/dimacs_cnf.cpp index 66b2587287b..2141ef82031 100644 --- a/src/solvers/sat/dimacs_cnf.cpp +++ b/src/solvers/sat/dimacs_cnf.cpp @@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : cnf_clause_listt(message_handler), break_lines(false) { diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 9263ae2834c..e467db8e5ba 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "smt2irep.h" +#include + std::string smt2_dect::decision_procedure_text() const { // clang-format off diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index ddb499e27fa..e362e6f0109 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "smt2_conv.h" -#include - class message_handlert; class smt2_stringstreamt diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 4bd6b21eba8..8872a191af4 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -143,7 +143,8 @@ class smt2_incremental_decision_proceduret final { return next_id++; } - } handle_sequence, array_sequence, index_sequence, padding_sequence; + }; + sequencet handle_sequence, array_sequence, index_sequence, padding_sequence; /// When the `handle(exprt)` member function is called, the decision procedure /// commands the SMT solver to define a new function corresponding to the /// given expression. The mapping of the expressions to the function From 850dfa57a12741e77bd4d0aefb858527de053a2e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 2 Apr 2025 09:00:11 +0000 Subject: [PATCH 4/5] CI: Remove use of Ubuntu 20.04 GitHub will no longer support ubuntu-20.04 runners after 2025-04-15. Use ubuntu-24.04 or ubuntu-latest instead. This implies that we will no longer release pre-built packages for Ubuntu 20.04. --- .github/workflows/README.md | 15 ++-- .github/workflows/build-and-test-Linux.yaml | 10 +-- .github/workflows/build-and-test-Xen.yaml | 14 ++-- .github/workflows/coverage.yaml | 8 +-- .github/workflows/csmith.yaml | 10 +-- .github/workflows/doxygen-check.yaml | 2 +- .github/workflows/performance.yaml | 8 +-- .github/workflows/publish.yaml | 2 +- .github/workflows/pull-request-checks.yaml | 70 +++++++++---------- .github/workflows/regular-release.yaml | 6 +- .github/workflows/release-packages.yaml | 76 +-------------------- .github/workflows/syntax-checks.yaml | 4 +- CMakeLists.txt | 4 +- 13 files changed, 79 insertions(+), 150 deletions(-) diff --git a/.github/workflows/README.md b/.github/workflows/README.md index 49898733076..c474eec8396 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -25,19 +25,22 @@ The files in this folder correspond to: We are currently building and testing CBMC under the following configurations: -* `make` * `gcc` * `linux` (ubuntu 20.04) -* `make` * `clang` * `linux` (ubuntu 20.04) -* `cmake` * `gcc` * `linux` (ubuntu 20.04) -* `make` * `clang` * `macos` (10.15) -* `cmake` * `clang` * `macos` (10.15) +* `make` * `gcc` * `linux` (ubuntu 24.04) +* `make` * `clang` * `linux` (ubuntu 22.04, 24.04) +* `cmake` * `gcc` * `linux` (ubuntu 22.04, 24.04) +* `cmake` * `gcc-14` * `linux` (ubuntu 24.04) +* `cmake` * `gcc` * `linux` (ubuntu 22.04 32-bit) +* `make` * `clang` * `macos` (13) +* `cmake` * `clang` * `macos` (14) * `cmake` * `vs` * `windows` (vs2019) +* `make` * `vs` * `windows` (vs2022) Aside from the main platform builds for testing, we are also performing some auxiliary builds that test packaging support to be up-to-date. We do that for: * a `docker` image -* an `ubuntu-20.04` package +* a `ubuntu-24.04` package * a `windows-msi` installer package Last but not least, we are also performing a coverage statistics collection diff --git a/.github/workflows/build-and-test-Linux.yaml b/.github/workflows/build-and-test-Linux.yaml index 108b225acf3..4fe377b9988 100644 --- a/.github/workflows/build-and-test-Linux.yaml +++ b/.github/workflows/build-and-test-Linux.yaml @@ -8,7 +8,7 @@ on: jobs: # This job takes approximately 18 minutes CompileLinux: - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -20,7 +20,7 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -y clang-10 clang++-10 flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache + sudo apt-get install --no-install-recommends -y clang-19 clang++-19 flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache sudo apt-get install --no-install-recommends -y libssl-dev libelf-dev libudev-dev libpci-dev libiberty-dev autoconf sudo apt-get install --no-install-recommends -y gawk jq @@ -29,10 +29,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-KERNEL + key: ${{ runner.os }}-24.04-make-clang-${{ github.ref }}-${{ github.sha }}-KERNEL restore-keys: | - ${{ runner.os }}-20.04-make-clang-${{ github.ref }} - ${{ runner.os }}-20.04-make-clang + ${{ runner.os }}-24.04-make-clang-${{ github.ref }} + ${{ runner.os }}-24.04-make-clang - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 31ccb2598c6..63ce990a0fd 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -7,7 +7,7 @@ on: jobs: # This job takes approximately 33 minutes CompileXen: - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -19,19 +19,19 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -y build-essential git flex bison software-properties-common curl python - sudo apt-get install --no-install-recommends -y bin86 gdb bcc liblzma-dev python-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config - sudo apt-get install --no-install-recommends -y libgtk2.0-dev libyajl-dev time ccache clang-10 clang++-10 + sudo apt-get install --no-install-recommends -y build-essential git flex bison software-properties-common curl python3 + sudo apt-get install --no-install-recommends -y bin86 gdb bcc liblzma-dev python3-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config + sudo apt-get install --no-install-recommends -y libgtk2.0-dev libyajl-dev time ccache clang-19 clang++-19 - name: Prepare ccache uses: actions/cache@v4 with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-XEN + key: ${{ runner.os }}-24.04-make-clang-${{ github.ref }}-${{ github.sha }}-XEN restore-keys: | - ${{ runner.os }}-20.04-make-clang-${{ github.ref }} - ${{ runner.os }}-20.04-make-clang + ${{ runner.os }}-24.04-make-clang-${{ github.ref }} + ${{ runner.os }}-24.04-make-clang - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV diff --git a/.github/workflows/coverage.yaml b/.github/workflows/coverage.yaml index 9b549598846..c549eb52f9b 100644 --- a/.github/workflows/coverage.yaml +++ b/.github/workflows/coverage.yaml @@ -12,7 +12,7 @@ env: jobs: # This job takes approximately 22 to 75 minutes Linux: - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 steps: - name: Clone repository uses: actions/checkout@v4 @@ -45,10 +45,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-Coverage-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-Coverage-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-Coverage-${{ github.ref }} - ${{ runner.os }}-20.04-Coverage + ${{ runner.os }}-24.04-Coverage-${{ github.ref }} + ${{ runner.os }}-24.04-Coverage - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV diff --git a/.github/workflows/csmith.yaml b/.github/workflows/csmith.yaml index 564464938bb..47889708db4 100644 --- a/.github/workflows/csmith.yaml +++ b/.github/workflows/csmith.yaml @@ -7,7 +7,7 @@ on: jobs: # This job takes approximately 18 minutes run-10-random-tests: - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -19,7 +19,7 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -y build-essential flex bison maven ccache clang-10 clang++-10 + sudo apt-get install --no-install-recommends -y build-essential flex bison maven ccache clang-19 clang++-19 sudo apt-get install --no-install-recommends -y csmith libcsmith-dev make -C src minisat2-download - name: Prepare ccache @@ -27,10 +27,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-CSMITH + key: ${{ runner.os }}-24.04-make-clang-${{ github.ref }}-${{ github.sha }}-CSMITH restore-keys: | - ${{ runner.os }}-20.04-make-clang-${{ github.ref }} - ${{ runner.os }}-20.04-make-clang + ${{ runner.os }}-24.04-make-clang-${{ github.ref }} + ${{ runner.os }}-24.04-make-clang - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV diff --git a/.github/workflows/doxygen-check.yaml b/.github/workflows/doxygen-check.yaml index aee60708d63..5395b0be7b1 100644 --- a/.github/workflows/doxygen-check.yaml +++ b/.github/workflows/doxygen-check.yaml @@ -8,7 +8,7 @@ jobs: check-doxygen: # Note that the versions used for this `check-doxygen` job should be kept in # sync with the `publish` job. - runs-on: ubuntu-24.04 + runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - name: Fetch dependencies diff --git a/.github/workflows/performance.yaml b/.github/workflows/performance.yaml index f054fd6bf73..7dafd5b94cb 100644 --- a/.github/workflows/performance.yaml +++ b/.github/workflows/performance.yaml @@ -8,7 +8,7 @@ on: jobs: perf-benchcomp: - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 steps: - name: Save push event HEAD and HEAD~ to environment variables if: ${{ github.event_name == 'push' }} @@ -51,10 +51,10 @@ jobs: uses: actions/cache/restore@v4 with: path: .ccache - key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-Release-${{ github.ref }} - ${{ runner.os }}-20.04-Release + ${{ runner.os }}-24.04-Release-${{ github.ref }} + ${{ runner.os }}-24.04-Release - name: ccache environment run: echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - name: Zero ccache stats and limit in size diff --git a/.github/workflows/publish.yaml b/.github/workflows/publish.yaml index 488f04bc949..227040f1f39 100644 --- a/.github/workflows/publish.yaml +++ b/.github/workflows/publish.yaml @@ -6,7 +6,7 @@ jobs: publish: # Note that the versions used for this `publish` job should be kept in sync # with the `check-doxygen` job. - runs-on: ubuntu-24.04 + runs-on: ubuntu-latest steps: - name: Checkout repository uses: actions/checkout@v4 diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 266da10a0d2..e77bd396b88 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -11,8 +11,8 @@ env: jobs: # This job takes approximately 15 to 40 minutes - check-ubuntu-20_04-make-gcc: - runs-on: ubuntu-20.04 + check-ubuntu-24_04-make-gcc: + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -38,10 +38,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-make-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-make-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-make-${{ github.ref }} - ${{ runner.os }}-20.04-make + ${{ runner.os }}-24.04-make-${{ github.ref }} + ${{ runner.os }}-24.04-make - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV @@ -92,8 +92,8 @@ jobs: fi # This job takes approximately 25 to 34 minutes - check-ubuntu-20_04-make-clang: - runs-on: ubuntu-20.04 + check-ubuntu-24_04-make-clang: + runs-on: ubuntu-24.04 env: CC: "ccache /usr/bin/clang" CXX: "ccache /usr/bin/clang++" @@ -108,7 +108,7 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 make -C src minisat2-download cadical-download cpanm Thread::Pool::Simple - name: Confirm z3 solver is available and log the version installed @@ -124,10 +124,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-make-clang-${{ github.ref }} - ${{ runner.os }}-20.04-make-clang + ${{ runner.os }}-24.04-make-clang-${{ github.ref }} + ${{ runner.os }}-24.04-make-clang - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV @@ -165,8 +165,8 @@ jobs: # The reason we opted for a new job is that adding a `test-z3` step to the current # jobs increases the job runtime to unacceptable levels (over 2hrs). # This job takes approximately 3 to 18 minutes - check-ubuntu-20_04-make-clang-smt-z3: - runs-on: ubuntu-20.04 + check-ubuntu-24_04-make-clang-smt-z3: + runs-on: ubuntu-24.04 env: CC: "ccache /usr/bin/clang" CXX: "ccache /usr/bin/clang++" @@ -179,7 +179,7 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 make -C src minisat2-download cpanm Thread::Pool::Simple - name: Confirm z3 solver is available and log the version installed @@ -189,10 +189,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-make-clang-${{ github.ref }} - ${{ runner.os }}-20.04-make-clang + ${{ runner.os }}-24.04-make-clang-${{ github.ref }} + ${{ runner.os }}-24.04-make-clang - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV @@ -207,8 +207,8 @@ jobs: run: make -C regression/cbmc test-z3 # This job takes approximately 17 to 42 minutes - check-ubuntu-20_04-cmake-gcc: - runs-on: ubuntu-20.04 + check-ubuntu-24_04-cmake-gcc: + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -234,10 +234,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-Release-${{ github.ref }} - ${{ runner.os }}-20.04-Release + ${{ runner.os }}-24.04-Release-${{ github.ref }} + ${{ runner.os }}-24.04-Release - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV @@ -499,8 +499,8 @@ jobs: run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}} # This job takes approximately 2 to 24 minutes - check-ubuntu-20_04-cmake-gcc-KNOWNBUG: - runs-on: ubuntu-20.04 + check-ubuntu-24_04-cmake-gcc-KNOWNBUG: + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -518,10 +518,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-Release-${{ github.ref }} - ${{ runner.os }}-20.04-Release + ${{ runner.os }}-24.04-Release-${{ github.ref }} + ${{ runner.os }}-24.04-Release - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV @@ -546,8 +546,8 @@ jobs: ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K # This job takes approximately 7 to 30 minutes - check-ubuntu-20_04-cmake-gcc-THOROUGH: - runs-on: ubuntu-20.04 + check-ubuntu-24_04-cmake-gcc-THOROUGH: + runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -565,10 +565,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-20.04-Release-${{ github.ref }} - ${{ runner.os }}-20.04-Release + ${{ runner.os }}-24.04-Release-${{ github.ref }} + ${{ runner.os }}-24.04-Release - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV @@ -877,7 +877,7 @@ jobs: # This job takes approximately 2 to 3 minutes check-string-table: - runs-on: ubuntu-20.04 + runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - name: Check for unused irep ids @@ -885,7 +885,7 @@ jobs: # This job takes approximately 23 to 29 minutes check-docker-image: - runs-on: ubuntu-20.04 + runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 with: @@ -909,7 +909,7 @@ jobs: # This job takes approximately 22 to 41 minutes include-what-you-use: - runs-on: ubuntu-22.04 + runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 with: diff --git a/.github/workflows/regular-release.yaml b/.github/workflows/regular-release.yaml index 92fdff936d3..a15e1fc59be 100644 --- a/.github/workflows/regular-release.yaml +++ b/.github/workflows/regular-release.yaml @@ -8,7 +8,7 @@ name: Create Release jobs: get-version-information: name: Get Version Information - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 outputs: version: ${{ steps.split-version.outputs._1 }} steps: @@ -24,7 +24,7 @@ jobs: separator: '-' perform-release: name: Perform Release - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 needs: get-version-information steps: - name: Checkout code @@ -62,7 +62,7 @@ jobs: ```sh # Ubuntu 20: - $ dpkg -i ubuntu-20.04-cbmc-${{ env.CBMC_VERSION }}-Linux.deb + $ dpkg -i ubuntu-24.04-cbmc-${{ env.CBMC_VERSION }}-Linux.deb ``` ## Windows diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml index 0e7fab7e1b3..576e97c2ed4 100644 --- a/.github/workflows/release-packages.yaml +++ b/.github/workflows/release-packages.yaml @@ -148,80 +148,6 @@ jobs: SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 22.04 package built and uploaded successfully' || 'Ubuntu 22.04 package build failed' }}" - ubuntu-20_04-package: - runs-on: ubuntu-20.04 - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Fetch dependencies - run: | - sudo apt-get update - sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 - - 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 - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip - cvc5 --version - - name: Prepare ccache - uses: actions/cache@v4 - with: - save-always: true - path: .ccache - key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-RELEASEPKG - restore-keys: | - ${{ runner.os }}-20.04-Release-${{ github.ref }} - ${{ runner.os }}-20.04-Release - - name: ccache environment - run: | - echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV - echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - - name: Configure CMake - run: | - mkdir build - cd build - cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl="minisat2;cadical" - - name: Zero ccache stats and limit in size - run: ccache -z --max-size=500M - - name: Build using Ninja - run: ninja -C build -j4 - - name: Print ccache stats - run: ccache -s - - name: Run CTest - run: cd build; ctest . -V -L CORE -C Release -j4 - - name: Create packages - id: create_packages - run: | - cd build - ninja package - deb_package_name="$(ls *.deb)" - echo "deb_package=./build/$deb_package_name" >> $GITHUB_OUTPUT - echo "deb_package_name=ubuntu-20.04-$deb_package_name" >> $GITHUB_OUTPUT - - name: Get release info - id: get_release_info - uses: bruceadams/get-release@v1.3.2 - - name: Upload binary packages - uses: actions/upload-release-asset@v1 - with: - upload_url: ${{ steps.get_release_info.outputs.upload_url }} - asset_path: ${{ steps.create_packages.outputs.deb_package }} - asset_name: ${{ steps.create_packages.outputs.deb_package_name }} - asset_content_type: application/x-deb - - name: Slack notification of CI status - uses: rtCamp/action-slack-notify@v2 - if: success() || failure() - env: - SLACK_CHANNEL: aws-cbmc - SLACK_COLOR: ${{ job.status }} - SLACK_USERNAME: Github Actions CI bot - SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} - SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 20.04 package built and uploaded successfully' || 'Ubuntu 20.04 package build failed' }}" - homebrew-pr: runs-on: macos-13 steps: @@ -350,7 +276,7 @@ jobs: run: go run scripts/slack_notification_action.go push-docker-image-dockerhub: - runs-on: ubuntu-20.04 + runs-on: ubuntu-24.04 steps: - name: Checkout CBMC source uses: actions/checkout@v4 diff --git a/.github/workflows/syntax-checks.yaml b/.github/workflows/syntax-checks.yaml index 5c32a3d3647..e559c31afbc 100644 --- a/.github/workflows/syntax-checks.yaml +++ b/.github/workflows/syntax-checks.yaml @@ -6,7 +6,7 @@ on: jobs: # This job takes approximately 1 minute check-clang-format: - runs-on: ubuntu-24.04 + runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 with: @@ -28,7 +28,7 @@ jobs: # This job takes approximately 1 minute check-cpplint: - runs-on: ubuntu-20.04 + runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 with: diff --git a/CMakeLists.txt b/CMakeLists.txt index 2c1289a121e..0344a94d747 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -156,9 +156,9 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR add_custom_target(coverage COMMAND ${CMAKE_COMMAND} -E make_directory ${CODE_COVERAGE_OUTPUT_DIR} COMMAND ctest -V -L CORE -j${parallel_tests} - COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --capture --directory ${CMAKE_BINARY_DIR} --output-file ${CODE_COVERAGE_INFO_FILE} + COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --ignore-errors mismatch --capture --directory ${CMAKE_BINARY_DIR} --output-file ${CODE_COVERAGE_INFO_FILE} COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --remove ${CODE_COVERAGE_INFO_FILE} '/usr/*' --output-file ${CODE_COVERAGE_INFO_FILE} - COMMAND ${CODE_COVERAGE_GENHTML} ${CODE_COVERAGE_INFO_FILE} --output-directory ${CODE_COVERAGE_OUTPUT_DIR} + COMMAND ${CODE_COVERAGE_GENHTML} --ignore-errors unmapped ${CODE_COVERAGE_INFO_FILE} --output-directory ${CODE_COVERAGE_OUTPUT_DIR} DEPENDS "$" "$" From 32d6835856f5f3ec82b2741b1437afa4e8590725 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Apr 2025 19:18:19 +0000 Subject: [PATCH 5/5] Include-what-you-use: use clang to avoid spurious errors iwyu uses clang itself, so is only compatible with compiler command line options that clang takes rather than GCC's. --- .github/workflows/pull-request-checks.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index e77bd396b88..14e187df082 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -921,9 +921,9 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison iwyu + sudo apt-get install --no-install-recommends -yq cmake ninja-build clang-19 clang++-19 gdb maven flex bison iwyu - name: Configure using CMake - run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ - name: Run include-what-you-use run: | iwyu_tool -p build/compile_commands.json -j${{env.linux-vcpus}} | tee includes.txt