Skip to content

Commit 42a78af

Browse files
committed
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.
1 parent 5235938 commit 42a78af

File tree

9 files changed

+37
-30
lines changed

9 files changed

+37
-30
lines changed

.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ regression/**/tests.log
5757
regression/**/*.gb
5858
regression/**/*.smt2
5959
jbmc/regression/**/tests.log
60+
jbmc/regression/**/tests-symex-driven-loading.log
6061

6162
# regression/coverage file
6263
/regression/coverage_**
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
11
add_test_pl_tests(
22
"$<TARGET_FILE:jbmc>"
33
)
4-
5-
add_test_pl_profile(
6-
"cbmc-java-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
9-
"CORE"
10-
)

jbmc/regression/jbmc-strings/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ add_test_pl_tests(
55
add_test_pl_profile(
66
"jbmc-strings-symex-driven-lazy-loading"
77
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
8+
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

jbmc/regression/jbmc-strings/Makefile

+4-5
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,19 @@ include ../../src/config.inc
44

55
test:
66
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
7+
@../$(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
88

99
testfuture:
1010
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF
11+
@../$(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
1212

1313
testall:
1414
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK
15+
@../$(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
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
1818
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
19+
@../$(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
2020

2121
show:
2222
@for dir in *; do \
@@ -29,4 +29,3 @@ clean:
2929
find -name '*.out' -execdir $(RM) '{}' \;
3030
find -name '*.gb' -execdir $(RM) '{}' \;
3131
$(RM) tests.log
32-

jbmc/regression/jbmc/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ add_test_pl_tests(
55
add_test_pl_profile(
66
"jbmc-symex-driven-lazy-loading"
77
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
8+
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

jbmc/regression/jbmc/Makefile

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@ include ../../src/config.inc
44

55
test:
66
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
7+
@../$(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
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
1010
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
11+
@../$(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
1212

1313
show:
1414
@for dir in *; do \

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ add_test_pl_tests(
55
add_test_pl_profile(
66
"strings-smoke-tests-symex-driven-lazy-loading"
77
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
8+
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

jbmc/regression/strings-smoke-tests/Makefile

+4-5
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,19 @@ include ../../src/config.inc
44

55
test:
66
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
7+
@../$(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
88

99
testfuture:
1010
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF
11+
@../$(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
1212

1313
testall:
1414
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK
15+
@../$(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
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
1818
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
19+
@../$(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
2020

2121
show:
2222
@for dir in *; do \
@@ -29,4 +29,3 @@ clean:
2929
find -name '*.out' -execdir $(RM) '{}' \;
3030
find -name '*.gb' -execdir $(RM) '{}' \;
3131
$(RM) tests.log
32-

regression/test.pl

+23-8
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,8 @@ ($)
6666
return @data;
6767
}
6868

69-
sub test($$$$$$$$$) {
70-
my ($name, $test, $t_level, $cmd, $ign, $dry_run, $defines, $include_tags, $exclude_tags) = @_;
69+
sub test($$$$$$$$$$) {
70+
my ($name, $test, $t_level, $cmd, $ign, $dry_run, $defines, $include_tags, $exclude_tags, $output_suffix) = @_;
7171
my ($level_and_tags, $input, $options, $grep_options, @results) = load("$test");
7272
my @keys = keys %{$defines};
7373
foreach my $key (@keys) {
@@ -115,7 +115,12 @@ ($$$$$$$$$)
115115

116116
my $descriptor = basename($test);
117117
my $output = $descriptor;
118-
$output =~ s/\.[^.]*$/.out/;
118+
$output =~ s/\.[^.]*$//;
119+
if($output_suffix) {
120+
$output .= "-";
121+
$output .= $output_suffix;
122+
}
123+
$output .= ".out";
119124

120125
if($output eq $input) {
121126
print("Error in test file -- $test\n");
@@ -269,7 +274,10 @@ ($$$$)
269274
test descriptors
270275
-I <tag> run only tests that have the given secondary tag. Can be repeated.
271276
-X <tag> exclude tests that have the given secondary tag. Can be repeated.
272-
277+
-s <suffix> append <suffix> to all output and log files. Enables concurrent
278+
testing of the same desc file with different commands or options,
279+
as runs with different suffixes will operate independently and keep
280+
independent logs.
273281
274282
test.pl expects a test.desc file in each subdirectory. The file test.desc
275283
follows the format specified below. Any line starting with // will be ignored.
@@ -304,9 +312,9 @@ ($$$$)
304312
use Getopt::Long qw(:config pass_through bundling);
305313
$main::VERSION = 0.1;
306314
$Getopt::Std::STANDARD_HELP_VERSION = 1;
307-
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
315+
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
308316
GetOptions("D=s" => \%defines, "X=s" => \@exclude_tags, "I=s" => \@include_tags);
309-
getopts('c:i:j:nphCTFK') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
317+
getopts('c:i:j:nphCTFKs:') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
310318
$opt_c or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
311319
$opt_j = $opt_j || $ENV{'TESTPL_JOBS'} || 0;
312320
if($opt_j && $opt_j != 1 && !$has_thread_pool) {
@@ -321,9 +329,16 @@ ($$$$)
321329
$t_level += 8 if($opt_K);
322330
$t_level += 1 if($opt_C || 0 == $t_level);
323331
my $dry_run = $opt_n;
332+
my $log_suffix = $opt_s;
324333

334+
my $logfile_name = "tests";
335+
if($log_suffix) {
336+
$logfile_name .= "-";
337+
$logfile_name .= $log_suffix;
338+
}
339+
$logfile_name .= ".log";
325340

326-
open LOG,">tests.log";
341+
open LOG, (">" . $logfile_name);
327342

328343
print "Loading\n";
329344
my @tests = @ARGV != 0 ? @ARGV : dirs();
@@ -349,7 +364,7 @@ ($)
349364
defined($pool) or print " Running $files[$_]";
350365
my $start_time = time();
351366
$failed_skipped = test(
352-
$test, $files[$_], $t_level, $opt_c, $opt_i, $dry_run, \%defines, \@include_tags, \@exclude_tags);
367+
$test, $files[$_], $t_level, $opt_c, $opt_i, $dry_run, \%defines, \@include_tags, \@exclude_tags, $log_suffix);
353368
my $runtime = time() - $start_time;
354369

355370
lock($skips);

0 commit comments

Comments
 (0)