Restore testing of jbmc

.gitignore

@@ -57,6 +57,7 @@ regression/**/tests.log
 regression/**/*.gb
 regression/**/*.smt2
 jbmc/regression/**/tests.log
+jbmc/regression/**/tests-symex-driven-loading.log
 
 # regression/coverage file
 /regression/coverage_**

CMakeLists.txt

@@ -34,14 +34,15 @@ set(sat_impl "minisat2" CACHE STRING
     "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
 )
 
-add_subdirectory(src)
-add_subdirectory(jbmc)
-
 if(${enable_cbmc_tests})
     enable_testing()
 endif()
-add_subdirectory(unit)
+
+add_subdirectory(src)
 add_subdirectory(regression)
+add_subdirectory(unit)
+
+add_subdirectory(jbmc)
 
 set_target_properties(
     analyses

jbmc/regression/CMakeLists.txt

@@ -1,24 +1,4 @@
-set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
-
-macro(add_test_pl_profile name cmdline flag profile)
-    add_test(
-        NAME "${name}-${profile}"
-        COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
-        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-    )
-    set_tests_properties("${name}-${profile}" PROPERTIES
-        LABELS "${profile};CBMC"
-    )
-endmacro(add_test_pl_profile)
-
-macro(add_test_pl_tests cmdline)
-    get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
-    message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
-endmacro(add_test_pl_tests)
+set(test_pl_path "${CMAKE_SOURCE_DIR}/regression/test.pl")
 
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are

jbmc/regression/janalyzer-taint/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-analyzer>"
+    "$<TARGET_FILE:janalyzer>"
 )

jbmc/regression/jbmc-cover/CMakeLists.txt

@@ -1,10 +1,3 @@
 add_test_pl_tests(
     "$<TARGET_FILE:jbmc>"
 )
-
-add_test_pl_profile(
-    "cbmc-java-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
-    "-C;-X;symex-driven-lazy-loading-expected-failure"
-    "CORE"
-)

jbmc/regression/jbmc-strings/CMakeLists.txt

@@ -5,6 +5,6 @@ add_test_pl_tests(
 add_test_pl_profile(
     "jbmc-strings-symex-driven-lazy-loading"
     "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
-    "-C;-X;symex-driven-lazy-loading-expected-failure"
+    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
     "CORE"
 )

jbmc/regression/jbmc-strings/Makefile

@@ -4,19 +4,19 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
@@ -29,4 +29,3 @@ clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
 	$(RM) tests.log
-

jbmc/regression/jbmc/CMakeLists.txt

@@ -3,8 +3,8 @@ add_test_pl_tests(
 )
 
 add_test_pl_profile(
-    "cbmc-java-symex-driven-lazy-loading"
+    "jbmc-symex-driven-lazy-loading"
     "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
-    "-C;-X;symex-driven-lazy-loading-expected-failure"
+    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
     "CORE"
 )

jbmc/regression/jbmc/Makefile

@@ -4,11 +4,11 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \

jbmc/regression/jdiff/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-diff>"
+    "$<TARGET_FILE:jdiff>"
 )

jbmc/regression/strings-smoke-tests/CMakeLists.txt

@@ -5,6 +5,6 @@ add_test_pl_tests(
 add_test_pl_profile(
     "strings-smoke-tests-symex-driven-lazy-loading"
     "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
-    "-C;-X;symex-driven-lazy-loading-expected-failure"
+    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
     "CORE"
 )

jbmc/regression/strings-smoke-tests/Makefile

@@ -4,19 +4,19 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
-	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:
 	@for dir in *; do \
@@ -29,4 +29,3 @@ clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
 	$(RM) tests.log
-

regression/test.pl

@@ -66,8 +66,8 @@ ($)
   return @data;
 }
 
-sub test($$$$$$$$$) {
-  my ($name, $test, $t_level, $cmd, $ign, $dry_run, $defines, $include_tags, $exclude_tags) = @_;
+sub test($$$$$$$$$$) {
+  my ($name, $test, $t_level, $cmd, $ign, $dry_run, $defines, $include_tags, $exclude_tags, $output_suffix) = @_;
   my ($level_and_tags, $input, $options, $grep_options, @results) = load("$test");
   my @keys = keys %{$defines};
   foreach my $key (@keys) {
@@ -115,7 +115,12 @@ ($$$$$$$$$)
 
   my $descriptor = basename($test);
   my $output = $descriptor;
-  $output =~ s/\.[^.]*$/.out/;
+  $output =~ s/\.[^.]*$//;
+  if($output_suffix) {
+    $output .= "-";
+    $output .= $output_suffix;
+  }
+  $output .= ".out";
 
   if($output eq $input) {
     print("Error in test file -- $test\n");
@@ -269,7 +274,10 @@ ($$$$)
                  test descriptors
   -I <tag>   run only tests that have the given secondary tag. Can be repeated.
   -X <tag>   exclude tests that have the given secondary tag. Can be repeated.
-
+  -s <suffix>  append <suffix> to all output and log files. Enables concurrent
+             testing of the same desc file with different commands or options,
+             as runs with different suffixes will operate independently and keep
+             independent logs.
 
 test.pl expects a test.desc file in each subdirectory. The file test.desc
 follows the format specified below. Any line starting with // will be ignored.
@@ -304,9 +312,9 @@ ($$$$)
 use Getopt::Long qw(:config pass_through bundling);
 $main::VERSION = 0.1;
 $Getopt::Std::STANDARD_HELP_VERSION = 1;
-our ($opt_c, $opt_i, $opt_j, $opt_n, $opt_p, $opt_h, $opt_C, $opt_T, $opt_F, $opt_K, %defines, @include_tags, @exclude_tags); # the variables for getopt
+our ($opt_c, $opt_i, $opt_j, $opt_n, $opt_p, $opt_h, $opt_C, $opt_T, $opt_F, $opt_K, $opt_s, %defines, @include_tags, @exclude_tags); # the variables for getopt
 GetOptions("D=s" => \%defines, "X=s" => \@exclude_tags, "I=s" => \@include_tags);
-getopts('c:i:j:nphCTFK') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
+getopts('c:i:j:nphCTFKs:') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
 $opt_c or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
 $opt_j = $opt_j || $ENV{'TESTPL_JOBS'} || 0;
 if($opt_j && $opt_j != 1 && !$has_thread_pool) {
@@ -321,9 +329,16 @@ ($$$$)
 $t_level += 8 if($opt_K);
 $t_level += 1 if($opt_C || 0 == $t_level);
 my $dry_run = $opt_n;
+my $log_suffix = $opt_s;
 
+my $logfile_name = "tests";
+if($log_suffix) {
+  $logfile_name .= "-";
+  $logfile_name .= $log_suffix;
+}
+$logfile_name .= ".log";
 
-open LOG,">tests.log";
+open LOG, (">" . $logfile_name);
 
 print "Loading\n";
 my @tests = @ARGV != 0 ? @ARGV : dirs();
@@ -349,7 +364,7 @@ ($)
     defined($pool) or print "  Running $files[$_]";
     my $start_time = time();
     $failed_skipped = test(
-      $test, $files[$_], $t_level, $opt_c, $opt_i, $dry_run, \%defines, \@include_tags, \@exclude_tags);
+      $test, $files[$_], $t_level, $opt_c, $opt_i, $dry_run, \%defines, \@include_tags, \@exclude_tags, $log_suffix);
     my $runtime = time() - $start_time;
 
     lock($skips);