From 5235938f0c00344cf1d6710eea1c638ad8f70bc8 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 23 May 2018 12:04:45 +0100 Subject: [PATCH 1/2] Restore testing of jbmc --- CMakeLists.txt | 9 ++++---- jbmc/regression/CMakeLists.txt | 22 +------------------ .../regression/janalyzer-taint/CMakeLists.txt | 2 +- jbmc/regression/jbmc/CMakeLists.txt | 2 +- jbmc/regression/jdiff/CMakeLists.txt | 2 +- 5 files changed, 9 insertions(+), 28 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index ed5a46d85a0..d8de16b0011 100644 --- a/CMakeLists.txt +++ b/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 diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt index 86e68b6c590..86037a4ff70 100644 --- a/jbmc/regression/CMakeLists.txt +++ b/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 diff --git a/jbmc/regression/janalyzer-taint/CMakeLists.txt b/jbmc/regression/janalyzer-taint/CMakeLists.txt index 73af8689568..d8ebffaf7de 100644 --- a/jbmc/regression/janalyzer-taint/CMakeLists.txt +++ b/jbmc/regression/janalyzer-taint/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$" ) diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt index 2742f7ba078..05e47a56dfe 100644 --- a/jbmc/regression/jbmc/CMakeLists.txt +++ b/jbmc/regression/jbmc/CMakeLists.txt @@ -3,7 +3,7 @@ add_test_pl_tests( ) add_test_pl_profile( - "cbmc-java-symex-driven-lazy-loading" + "jbmc-symex-driven-lazy-loading" "$ --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure" "CORE" diff --git a/jbmc/regression/jdiff/CMakeLists.txt b/jbmc/regression/jdiff/CMakeLists.txt index e55a44d8003..a92e079fcc9 100644 --- a/jbmc/regression/jdiff/CMakeLists.txt +++ b/jbmc/regression/jdiff/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$" ) From 42a78afad81b40fdedac23161f7bfa402d3f957e Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 23 May 2018 14:56:01 +0100 Subject: [PATCH 2/2] JBMC tests: suffix logfiles when using symex-driven loading The three test directories jbmc, jbmc-strings and strings-smoke-tests all have a second test profile that uses --symex-driven-lazy-loading, but this meant after the test completed the logfiles from the first profile would have been overwritten, and if very unlucky the two profiles could run concurrently and fight over the same logfile. Therefore we now allow test.pl to be given a log-file suffix, both for its main log and test output logs, use that facility for these tests. --- .gitignore | 1 + jbmc/regression/jbmc-cover/CMakeLists.txt | 7 ----- jbmc/regression/jbmc-strings/CMakeLists.txt | 2 +- jbmc/regression/jbmc-strings/Makefile | 9 +++--- jbmc/regression/jbmc/CMakeLists.txt | 2 +- jbmc/regression/jbmc/Makefile | 4 +-- .../strings-smoke-tests/CMakeLists.txt | 2 +- jbmc/regression/strings-smoke-tests/Makefile | 9 +++--- regression/test.pl | 31 ++++++++++++++----- 9 files changed, 37 insertions(+), 30 deletions(-) diff --git a/.gitignore b/.gitignore index 12ec184191b..87b3c4c28c4 100644 --- a/.gitignore +++ b/.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_** diff --git a/jbmc/regression/jbmc-cover/CMakeLists.txt b/jbmc/regression/jbmc-cover/CMakeLists.txt index 2742f7ba078..afe0ea5761a 100644 --- a/jbmc/regression/jbmc-cover/CMakeLists.txt +++ b/jbmc/regression/jbmc-cover/CMakeLists.txt @@ -1,10 +1,3 @@ add_test_pl_tests( "$" ) - -add_test_pl_profile( - "cbmc-java-symex-driven-lazy-loading" - "$ --symex-driven-lazy-loading" - "-C;-X;symex-driven-lazy-loading-expected-failure" - "CORE" -) diff --git a/jbmc/regression/jbmc-strings/CMakeLists.txt b/jbmc/regression/jbmc-strings/CMakeLists.txt index 9b4832e9833..1b698f38161 100644 --- a/jbmc/regression/jbmc-strings/CMakeLists.txt +++ b/jbmc/regression/jbmc-strings/CMakeLists.txt @@ -5,6 +5,6 @@ add_test_pl_tests( add_test_pl_profile( "jbmc-strings-symex-driven-lazy-loading" "$ --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" ) diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile index 9c4a5076c4f..4ff4e5ba834 100644 --- a/jbmc/regression/jbmc-strings/Makefile +++ b/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 - diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt index 05e47a56dfe..fa345944621 100644 --- a/jbmc/regression/jbmc/CMakeLists.txt +++ b/jbmc/regression/jbmc/CMakeLists.txt @@ -5,6 +5,6 @@ add_test_pl_tests( add_test_pl_profile( "jbmc-symex-driven-lazy-loading" "$ --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" ) diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile index 04d5932c7b7..81024778e07 100644 --- a/jbmc/regression/jbmc/Makefile +++ b/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 \ diff --git a/jbmc/regression/strings-smoke-tests/CMakeLists.txt b/jbmc/regression/strings-smoke-tests/CMakeLists.txt index 8c8577192c0..0b63a67939c 100644 --- a/jbmc/regression/strings-smoke-tests/CMakeLists.txt +++ b/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" "$ --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" ) diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile index 9c4a5076c4f..4ff4e5ba834 100644 --- a/jbmc/regression/strings-smoke-tests/Makefile +++ b/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 - diff --git a/regression/test.pl b/regression/test.pl index d137e2dbb84..ab89c030185 100755 --- a/regression/test.pl +++ b/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 run only tests that have the given secondary tag. Can be repeated. -X exclude tests that have the given secondary tag. Can be repeated. - + -s append 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);