From 3a68d7f6e21959f587f5831e33ee139a1e0a41b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 15 Feb 2023 22:04:26 +0000 Subject: [PATCH] Use CaDiCaL for selected THOROUGH regression tests This is to reduce the overall time of the check-ubuntu-20_04-cmake-gcc-THOROUGH CI task. Test execution times are as follows: * Float-equality1/test_equality.desc: * cadical: 66 seconds * minisat: 695 seconds * VerifStringLastIndexOf/test.desc: * cadical: 49 seconds * minisat: 158 seconds * gcc_popcount2/test.desc: * cadical: 151 seconds * minisat: 3573 seconds * java_easychair/test.desc: * cadical: 19 seconds * minisat: 109 seconds * java_parselong_unknown_radix/test.desc: * cadical: 46 seconds * minisat: 2569 seconds --- .github/workflows/pull-request-checks.yaml | 2 +- .../jbmc-strings/VerifStringLastIndexOf/test.desc | 6 +++++- jbmc/regression/jbmc-strings/java_easychair/test.desc | 5 ++++- .../java_parselong_unknown_radix/test.desc | 5 ++++- regression/cbmc/Float-equality1/test_equality.desc | 6 +++--- regression/cbmc/gcc_popcount2/test.desc | 5 ++++- 6 files changed, 21 insertions(+), 8 deletions(-) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index eb8d0417fa5..b4b4e8b982a 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -411,7 +411,7 @@ jobs: git checkout -- memory_allocation1 printf1 union12 va_list3 ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K - # This job takes approximately 73 to 95 minutes + # This job takes approximately 8 to 30 minutes check-ubuntu-20_04-cmake-gcc-THOROUGH: runs-on: ubuntu-20.04 steps: diff --git a/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc b/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc index 687e50d88e9..c77bffcbc53 100644 --- a/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc +++ b/jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc @@ -1,6 +1,10 @@ THOROUGH Test ---function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +--function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --sat-solver cadical VERIFICATION SUCCESSFUL ^EXIT=0$ ^SIGNAL=0$ +-- +-- +This test takes approximately 3 minutes when using MiniSat, and less than 1 +minute when using CaDiCaL. diff --git a/jbmc/regression/jbmc-strings/java_easychair/test.desc b/jbmc/regression/jbmc-strings/java_easychair/test.desc index 7e95317417f..66fc69a62bb 100644 --- a/jbmc/regression/jbmc-strings/java_easychair/test.desc +++ b/jbmc/regression/jbmc-strings/java_easychair/test.desc @@ -1,7 +1,10 @@ THOROUGH easychair ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --sat-solver cadical ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 30.* FAILURE$ -- +-- +This test takes approximately 2 minutes when using MiniSat, and just 20 seconds +when using CaDiCaL. diff --git a/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc index 5718bca4ef8..4c584fc9355 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc @@ -1,9 +1,12 @@ THOROUGH Test ---max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --sat-solver cadical ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 12.* FAILURE$ ^\[.*assertion.2\].* line 14.* SUCCESS$ -- non equal types +-- +This test takes approximately 45 minutes when using MiniSat, but less than 1 +minute when using CaDiCaL. diff --git a/regression/cbmc/Float-equality1/test_equality.desc b/regression/cbmc/Float-equality1/test_equality.desc index 1c46f5f4365..e8bfd526fe1 100644 --- a/regression/cbmc/Float-equality1/test_equality.desc +++ b/regression/cbmc/Float-equality1/test_equality.desc @@ -1,6 +1,6 @@ THOROUGH main.c --DEQUALITY +-DEQUALITY --sat-solver cadical ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ @@ -8,5 +8,5 @@ main.c ^warning: ignoring -- Takes approximately 1000 seconds to complete when using the SAT back-end (and -Minisat2). The SMT solver completes this task in less than 0.1 seconds. -See #4337. +Minisat2). CaDiCaL solves the problem in less than 2 minutes. The SMT solver +completes this task in less than 0.1 seconds. See #4337. diff --git a/regression/cbmc/gcc_popcount2/test.desc b/regression/cbmc/gcc_popcount2/test.desc index d20959b7f67..1635e61d96a 100644 --- a/regression/cbmc/gcc_popcount2/test.desc +++ b/regression/cbmc/gcc_popcount2/test.desc @@ -1,6 +1,6 @@ THOROUGH main.c - +--sat-solver cadical ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ @@ -8,3 +8,6 @@ main.c ^\*\* 1 of 3 failed -- ^warning: ignoring +-- +MiniSat takes approximately 1 hour on this test while CaDiCaL completes in under +3 minutes.