Merge pull request #5985 from padhi-aws-forks/smt2_regression_tags

Added new solver-specific tags for SMT regression tests

Author: SaswatPadhi

regression/cbmc/CMakeLists.txt

@@ -20,7 +20,7 @@ add_test_pl_profile(
 add_test_pl_profile(
     "cbmc-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
-    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;${gcc_only_string}-s;cprover-smt2"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2"
     "CORE"
 )
 

regression/cbmc/Makefile

@@ -13,14 +13,25 @@ test:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend -X thorough-smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
+					  -s cprover-smt2 $(GCC_ONLY)
+
+test-z3:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
+					  -s z3 $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
+					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
+					  -s paths-lifo $(GCC_ONLY)
 
 tests.log: ../test.pl test
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.smt2' -execdir $(RM) '{}' \;
-	$(RM) tests.log tests-paths-lifo.log tests-cprover-smt2.log
+	$(RM) tests*.log

regression/readme.md

@@ -1,12 +1,42 @@
-# CProver regression tests
+# CProver Regression Tests
 
 This folder contains the CProver regression test-suite.
 
-## Notes
+## Tags
 
-* Tests marked as `winbug` are currently known to be failing
-  on Windows, but passing on other platforms. The reason for
-  this is not known, and it's currently being investigated.
-  This was discovered during work done to port CI from travis
-  and codebuild to github actions. Worth noting that those tests
-  were not being run on Windows before.
+### Backend
+
+- `smt-backend`:
+  These tests _require_ the SMT backend and do not work with the SAT backend.
+  For example, quantified predicates are not fully supported in SAT.
+- `broken-smt-backend`:
+  These tests are blocked on missing / buggy goto -> SMT translation rules,
+  and therefore do not work with any SMT solver.
+- `thorough-smt-backend`:
+  These tests are too slow to be run in CI with the SMT backend.
+
+### Solver
+
+- `broken-cprover-smt-backend`:
+  These tests are known to not work with CPROVER SMT2.
+- `thorough-cprover-smt-backend`:
+  These tests are too slow to be run in CI with CPROVER SMT2.
+- `broken-z3-smt-backend`:
+  These tests are known to not work with Z3 (the version running on our CI).
+- `thorough-z3-smt-backend`:
+  These tests are too slow to be run in CI with Z3.
+
+### Platform
+
+- `winbug`:
+  These tests are currently known to be failing on Windows,
+  but passing on other platforms.
+  The reason for this is not known, and it's currently being investigated.
+  This was discovered during work done to port CI from [Travis]
+  and [AWS CodeBuild] to [GitHub Actions].
+  Worth noting that those tests were not being run on Windows before.
+
+
+[AWS CodeBuild]: https://aws.amazon.com/codebuild/
+[GitHub Actions]: https://github.com/features/actions
+[Travis]: https://travis-ci.com/