Several inconsistenties in regression test build scripts

[SaswatPadhi]

CBMC version: abba3d7
Operating system: Mac OS 10.15.7

PR #5985 exposed some issues with the existing Makefiles and CMakeLists.txt in regression/ subdirectories:

1. make and cmake sometimes run different regression tests

One example is regression/cbmc:

• make only builds the test target. Although test-cprover-smt2 and test-paths-lifo are defined, they are not built as part of the default target.
• cmake builds (the equivalents of) all three targets: test and test-cprover-smt2 and test-paths-lifo.

There might be similar instances in other subdirectories under regression/. You can notice this difference in the *cmake* (and Ubuntu 18.04) CI jobs vs *make* CI jobs. They don't run the same set of regression tests!

I am not sure if there is a good / automated solution to ensuring that make and cmake always build the same targets. An immediate step for now is to update all the default targets and make sure they run the same tests as added in the CMakeLists.txt file.

2. Inconsistent behavior of make command within regression/

The make command under regression/ runs the default target in each subdirectory:

cbmc/regression/Makefile

Lines 72 to 75 in abba3d7

	test:
	@for dir in $(DIRS); do \
	$(MAKE) "$$dir" || exit 1; \
	done;

However, the make X command under regression/ runs the test target under X subdirectory:

cbmc/regression/Makefile

Lines 79 to 81 in abba3d7

	$(DIRS):
	@echo "Running $@..." ;
	$(MAKE) -C "$@" test || exit 1;

Line 81 should be fixed to also build the default target instead.

[SaswatPadhi]

Some more comments:

3. Missing CMakeLists.txt

For instance, within regression/array-refinement.

4. test vs test.log targets

In almost all Makefiles these two targets look like duplicates, the only difference being test.log checks that the test.pl file actually exists before running any tests.

I think this is related to point 2 above -- the test target can probably just be removed now, and default target could use test.log instead.

5. Missing -s flag for test.pl in Makefiles

In regression/cbmc the test-paths-lifo and test-cprover-smt2 targets do not call test.pl with a -s. The CMakeLists.txt does. I think without this flag, the tests.log file would be overwritten by these targets, and these targets cannot be run concurrently.
I fixed regression/cbmc/Makefile in #5985, but there might be such instances in other regression/ subdirectories.

[tautschnig]

3. Missing CMakeLists.txt

For instance, within regression/array-refinement.

This is work in progress: #5936, among others.

[SaswatPadhi]

Adding one more:

6. Tags (e.g. smt-backend) are ignored in many directories

For instance, within regression/contracts.
I noticed this when I added regression/contracts/quantifiers-loop-02/test.desc as part of #6012.

It looks like many subdirectories have their own chain.sh variant and at least for the contracts directory it wasn't straightforward for me to update the Makefile so the right flags (--z3 or --cprover-smt2) could be passed to CBMC for all tests.

[feliperodri]

@TGWDB can we close this issue?

[TGWDB]

Yes, I believe we can (closing now).