From 2591d757b7653ff0df00f4db86f6579f1680b1da Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Aug 2025 20:33:24 +0000 Subject: [PATCH 1/3] Use CBMC's test.pl consistently --- regression/ebmc/test.pl | 163 ------------------------------------ regression/hw-cbmc/Makefile | 6 +- regression/vhdl/Makefile | 6 +- 3 files changed, 8 insertions(+), 167 deletions(-) delete mode 100755 regression/ebmc/test.pl diff --git a/regression/ebmc/test.pl b/regression/ebmc/test.pl deleted file mode 100755 index ca6c77db2..000000000 --- a/regression/ebmc/test.pl +++ /dev/null @@ -1,163 +0,0 @@ -#!/usr/bin/perl - -use subs; -use strict; -use warnings; - -# test.pl -# -# runs a test and check its output - -sub run($$$) { - my ($input, $options, $output) = @_; - my $cmd = "../../../src/ebmc/ebmc $options $input >$output 2>&1"; - - print LOG "Running $cmd\n"; - system $cmd; - my $exit_value = $? >> 8; - my $signal_num = $? & 127; - my $dumped_core = $? & 128; - my $failed = 0; - - print LOG " Exit: $exit_value\n"; - print LOG " Signal: $signal_num\n"; - print LOG " Core: $dumped_core\n"; - - if($signal_num != 0) { - $failed = 1; - print "Killed by signal $signal_num"; - if($dumped_core) { - print " (code dumped)"; - } - } - - system "echo EXIT=$exit_value >>$output"; - system "echo SIGNAL=$signal_num >>$output"; - - return $failed; -} - -sub load($) { - my ($fname) = @_; - - open FILE, "<$fname"; - my @data = ; - close FILE; - - chomp @data; - return @data; -} - -sub test($$) { - my ($name, $test) = @_; - my ($input, $options, @results) = load($test); - - my $output = $input; - $output =~ s/\.smv$/.out/; - $output =~ s/\.v$/.out/; - $output =~ s/\.sv$/.out/; - - if($output eq $input) { - print("Error in test file -- $test\n"); - return 1; - } - - print LOG "Test '$name'\n"; - print LOG " Input: $input\n"; - print LOG " Output: $output\n"; - print LOG " Options: $options\n"; - print LOG " Results:\n"; - foreach my $result (@results) { - print LOG " $result\n"; - } - - my $failed = run($input, $options, $output); - - if(!$failed) { - print LOG "Execution [OK]\n"; - my $included = 1; - foreach my $result (@results) { - if($result eq "--") { - $included = !$included; - } else { - my $r; - system "grep '$result' '$output' >/dev/null"; - $r = ($included ? $? != 0 : $? == 0); - if($r) { - print LOG "$result [FAILED]\n"; - $failed = 1; - } else { - print LOG "$result [OK]\n"; - } - } - } - } else { - print LOG "Execution [FAILED]\n"; - } - - print LOG "\n"; - - return $failed; -} - -sub dirs() { - my @list; - - opendir CWD, "."; - @list = grep { !/^\./ && -d "$_" && !/CVS/ } readdir CWD; - closedir CWD; - - @list = sort @list; - - return @list; -} - -if(@ARGV != 0) { - print "Usage:\n"; - print " test.pl\n"; - exit 1; -} - -open LOG,">tests.log"; - -print "Loading\n"; -my @tests = dirs(); -my $count = @tests; -if($count == 1) { - print " $count test found\n"; -} else { - print " $count tests found\n"; -} -print "\n"; -my $failures = 0; -print "Running tests\n"; -foreach my $test (@tests) { - print " Running $test"; - - chdir $test; - my $failed = test($test, "test.desc"); - chdir ".."; - - if($failed) { - $failures++; - print " [FAILED]\n"; - } else { - print " [OK]\n"; - } -} -print "\n"; - -if($failures == 0) { - print "All tests were successful\n"; -} else { - print "Tests failed\n"; - if($failures == 1) { - print " $failures of $count test failed\n"; - } else { - print " $failures of $count tests failed\n"; - } -} - -close LOG; - -exit $failures; diff --git a/regression/hw-cbmc/Makefile b/regression/hw-cbmc/Makefile index 0ba2e5818..c7742bc8d 100644 --- a/regression/hw-cbmc/Makefile +++ b/regression/hw-cbmc/Makefile @@ -1,10 +1,12 @@ default: tests.log +TEST_PL = ../../lib/cbmc/regression/test.pl + test: - @../test.pl -e -p -c ../../../src/hw-cbmc/hw-cbmc + @$(TEST_PL) -e -p -c ../../../src/hw-cbmc/hw-cbmc tests.log: - @../test.pl -e -p -c ../../../src/hw-cbmc/hw-cbmc + @$(TEST_PL) -e -p -c ../../../src/hw-cbmc/hw-cbmc show: @for dir in *; do \ diff --git a/regression/vhdl/Makefile b/regression/vhdl/Makefile index 3ccabe9cf..812f43f7d 100644 --- a/regression/vhdl/Makefile +++ b/regression/vhdl/Makefile @@ -1,10 +1,12 @@ default: tests.log +TEST_PL = ../../lib/cbmc/regression/test.pl + test: - @../test.pl -e -p -c ../../../src/ebmc/ebmc + @$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc tests.log: - @../test.pl -e -p -c ../../../src/ebmc/ebmc + @$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc show: @for dir in *; do \ From a46bcf924a9018cba502cedf1741063b3169f367 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Aug 2025 20:39:32 +0000 Subject: [PATCH 2/3] Mark passing tests as such --- regression/verilog/enums/enum_in_assert.desc | 3 +-- regression/verilog/enums/enum_name_collision.desc | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/regression/verilog/enums/enum_in_assert.desc b/regression/verilog/enums/enum_in_assert.desc index efe6d4098..7e4dc16d5 100644 --- a/regression/verilog/enums/enum_in_assert.desc +++ b/regression/verilog/enums/enum_in_assert.desc @@ -1,8 +1,7 @@ -KNOWNBUG +CORE enum_in_assert.sv ^EXIT=0$ ^SIGNAL=0$ -- -- -This throws an exception. diff --git a/regression/verilog/enums/enum_name_collision.desc b/regression/verilog/enums/enum_name_collision.desc index 76da42550..364b55ee0 100644 --- a/regression/verilog/enums/enum_name_collision.desc +++ b/regression/verilog/enums/enum_name_collision.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE enum_name_collision.sv ^EXIT=2$ From 8d9bfc08c31f5aa14fe2447308c8ff2d25683bc1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Aug 2025 20:34:40 +0000 Subject: [PATCH 3/3] Add CI job that runs KNOWNBUG tests This is to make sure that we do not spuriously keep tests marked as "KNOWNBUG" when a source change fixes the problem. --- .github/workflows/pull-request-checks.yaml | 60 ++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 08753359b..c28fd7546 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -125,6 +125,12 @@ jobs: name: ebmc-binary retention-days: 5 path: src/ebmc/ebmc + - name: Upload the hw-cbmc binary + uses: actions/upload-artifact@v4 + with: + name: hw-cbmc-binary + retention-days: 5 + path: src/hw-cbmc/hw-cbmc - name: Upload the vlindex binary uses: actions/upload-artifact@v4 with: @@ -457,3 +463,57 @@ jobs: run: make CXX=clcache BUILD_ENV=MSVC -j4 -C unit - name: Print ccache stats run: clcache -s + + # This job takes approximately 2 minutes + check-ubuntu-24_04-make-clang-KNOWNBUG: + runs-on: ubuntu-24.04 + needs: check-ubuntu-24_04-make-clang + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + - name: Fetch dependencies + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq z3 + - name: Confirm z3 solver is available and log the version installed + run: z3 --version + - name: Get the ebmc binary + uses: actions/download-artifact@v4 + with: + name: ebmc-binary + path: bin + - name: Get the hw-cbmc binary + uses: actions/download-artifact@v4 + with: + name: hw-cbmc-binary + path: bin + - name: Get the vlindex binary + uses: actions/download-artifact@v4 + with: + name: vlindex-binary + path: bin + - name: Try the binaries + run: | + chmod a+x ./bin/ebmc ; ./bin/ebmc --version + chmod a+x ./bin/hw-cbmc ; ./bin/hw-cbmc --version + chmod a+x ./bin/vlindex ; ./bin/vlindex --version + echo "PATH=$PATH:$PWD/bin" >> $GITHUB_ENV + - name: Run the ebmc tests with SAT + run: make -C regression/ebmc test TEST_PL="../../lib/cbmc/regression/test.pl -K" + - name: Run the ebmc tests with Z3 + run: make -C regression/ebmc test-z3 TEST_PL="../../lib/cbmc/regression/test.pl -K" + - name: Run the verilog tests + run: make -C regression/verilog test TEST_PL="../../lib/cbmc/regression/test.pl -K" + - name: Run the verilog tests with Z3 + run: make -C regression/verilog test-z3 TEST_PL="../../lib/cbmc/regression/test.pl -K" + - name: Run the smv tests + run: make -C regression/smv test TEST_PL="../../lib/cbmc/regression/test.pl -K" + - name: Run the smv tests with Z3 + run: make -C regression/smv test-z3 TEST_PL="../../lib/cbmc/regression/test.pl -K" + - name: Run the vlindex tests + run: make -C regression/vlindex test TEST_PL="../../lib/cbmc/regression/test.pl -K"