1#!@PERL@ -w
2
3# Run regression tests of a given level (default: 0, meaning
4# minimum amount of tests).  The higher the regression level, the more
5# tests to run, and the harder they get.
6
7# Each test may contain information about its regression level,
8# expected outcome, expected runtime, whether it produces a proof,
9# etc. in the format given below.  This script will scan the first 100
10# lines of each test and try to collect this information.
11
12# If some info is not found, defaults are assumed.  Default regression
13# level is 0, expected runtime is unbounded, outcome is undefined
14# (whatever it returns is OK), proof should be produced if outcome is
15# Valid, and if it is produced, it'll be verified.
16
17# Test info is given in the comments; here are examples
18#
19# %%% Regression level = 2
20# %%% Result = Valid  %% or Invalid, or Unknown
21# %%% Runtime = 10   %% in seconds
22# %%% Proof = yes    %% or 'no', if it doesn't produce a proof
23# %%% Language = presentation %% or 'internal'
24
25# The number of '%' and following spaces can vary, case is not
26# important.  Any text after the value is ignored.  Any comments that
27# are not recognized are also ignored.
28
29use strict;
30
31my %optionsHelp =
32    ("-h" => "Print this help and exit",
33     "-v" => "Be verbose (default, opposite of -q)",
34     "-q" => "Quiet mode (opposite of -v)",
35     "-l n" => "Set regression level (default 0, the easiest level)",
36     "+rt" => "Check that each test finishes within the specified runtime",
37     "-rt" => "Do not check whether test finishes within the specified runtime (default)",
38#      "+proofs" => "Produce and verify proofs",
39#      "-proofs" => "Do not produce / verify proofs (default)",
40     "-lang name" => "Use the named input language only (default=all)",
41     "-t secs" => "Run each executable for at most 'secs' seconds [0 = no limit]",
42     "-vc prog" => "Use \"prog\" to run tests (default=cvc3)",
43     "-pfc prog" => "Use \"prog\" to run a proof checker (default=true)"
44     );
45
46my $usageString =
47    "run_tests [ options ] [ test1 test2 ... ] [ -- [ command line options ] ]
48
49Run regression tests.  Concrete test files or directories
50with test files should be specified by name with a full path or
51relative path to the current directory.  If none specified, all
52subdirectories are searched for test files.
53
54Default running mode is overriden by test specs;
55test specs are overriden by command line options.
56
57Options:
58  " . join("\n  ",
59	   map { sprintf("%-9s %s", $_, $optionsHelp{$_}) } keys(%optionsHelp));
60
61
62# Database of default values for options
63my %optionsDefault = ("level" => 0,
64		      "verbose" => 1,
65                      "rt" => 0,
66		      "proofs" => 0,
67		      "lang" => "all",
68		      "runpath" => "@TOP@/bin/",
69		      "vc" => "cvc3", # Program names
70		      "pfc" => "true",
71		      "testpath" => "@TOP@/testcases",
72		      "tempdir" => "/tmp",
73		      # max. number of lines to read from the testcase file
74		      # when looking for info comments
75		      "maxInfoLines" => 100,
76		      # Runtime limit; 0 = no limit
77		      "time" => 0,
78		      # Additional command line options
79		      "clOptions" => "");
80
81# Database of command line options.  Initially, they are undefined
82my %options = ();
83# The list of testcases to run
84my @testcases = ();
85# Temporary array for options
86my @clOptions = ();
87# State is either "own" or "prog", meaning that we're reading either
88# our own or prog's options.
89my $argState = "own";
90for(my $i=0; $i <= $#ARGV; $i++) {
91    if($argState eq "own") {
92	if($ARGV[$i] eq "--") { $argState = "prog"; }
93	elsif($ARGV[$i] eq "-h") { print($usageString, "\n"); exit 0; }
94	elsif($ARGV[$i] eq "+rt") { $options{'rt'} = 1; }
95	elsif($ARGV[$i] eq "-rt") { $options{'rt'} = 0; }
96	elsif($ARGV[$i] eq "+proofs") { $options{'proofs'} = 1; }
97	elsif($ARGV[$i] eq "-proofs") { $options{'proofs'} = 0; }
98	elsif($ARGV[$i] eq "-v") { $options{'verbose'} = 1; }
99	elsif($ARGV[$i] eq "-q") { $options{'verbose'} = 0; }
100	elsif($ARGV[$i] eq "-lang") {
101	    if(++$i>$#ARGV) {
102		print STDERR "Option -lang requires an argument.\n";
103		print STDERR "Run run_tests -h for help\n";
104		exit 1;
105	    }
106	    $options{'lang'} = $ARGV[$i];
107	} elsif($ARGV[$i] eq "-l") {
108	    if(++$i>$#ARGV) {
109		print STDERR "Option -l requires an argument.\n";
110		print STDERR "Run run_tests -h for help\n";
111		exit 1;
112	    }
113	    $options{'level'} = $ARGV[$i];
114	} elsif($ARGV[$i] eq "-t") {
115	    if(++$i>$#ARGV) {
116		print STDERR "Option -t requires an argument.\n";
117		print STDERR "Run run_tests -h for help\n";
118		exit 1;
119	    }
120	    $options{'time'} = $ARGV[$i];
121	} elsif($ARGV[$i] eq "-vc") {
122	    if(++$i>$#ARGV) {
123		print STDERR "Option -vc requires an argument.\n";
124		print STDERR "Run run_tests -h for help\n";
125		exit 1;
126	    }
127	    $options{'vc'} = $ARGV[$i];
128	} elsif($ARGV[$i] eq "-pfc") {
129	    if(++$i>$#ARGV) {
130		print STDERR "Option -pfc requires an argument.\n";
131		print STDERR "Run run_tests -h for help\n";
132		exit 1;
133	    }
134	    $options{'pfc'} = $ARGV[$i];
135	} else {
136	    # This must be a testcase name
137	    push @testcases, $ARGV[$i];
138	}
139    } elsif($argState eq "prog") {
140	push @clOptions, $ARGV[$i];
141    } else {
142	die "BUG: Bad argState: $argState";
143    }
144}
145
146if($#clOptions >= 0) {
147    $options{'clOptions'} = join(" ", map { "\"" . $_ . "\"" } @clOptions);
148}
149
150# Compute the value of the option: first check the command line
151# option, then the supplied database (by ref. as the second arg), then
152# default values database.  If it cannot find definition, it is a bug,
153# and the script is stopped.
154
155sub getOpt {
156    my ($name, $dbRef) = @_;
157
158    return $options{$name} if(defined($options{$name}));
159    return $dbRef->{$name} if(defined($dbRef) && defined($dbRef->{$name}));
160    return $optionsDefault{$name} if(defined($optionsDefault{$name}));
161
162    # Option value is not found
163    die "getOpt($name): option is undefined";
164}
165
166my $verbose = getOpt('verbose');
167
168# Set the path
169my $systemPath = ".";
170if(defined($ENV{'PATH'})) {
171    $systemPath = $ENV{'PATH'};
172}
173$ENV{'PATH'} = getOpt('runpath') . ":" . $systemPath;
174
175if($verbose) {
176    print "*********\n";
177    print("Regression level: ", getOpt('level'), "\n");
178    print("Language: ", getOpt('lang'), "\n");
179    print("Whether to produce / check proofs: ",
180	  (defined($options{'proofs'}))?
181	  (($options{'proofs'})? "yes" : "no") : "depends on testcase",
182	  "\n");
183    if(getOpt('time') > 0) {
184	print("Time limit per test: ", getOpt('time'), " sec\n");
185    }
186    print("PATH = ", $ENV{'PATH'}, "\n");
187    print "*********\n";
188}
189
190my $tmpdir = getOpt('tempdir') . "/run_tests_tmp-$$";
191my $currdir = `pwd`;
192my $prog = getOpt('vc');
193my $pfc = getOpt('pfc');
194my $level = getOpt('level');
195my $lang = getOpt('lang');
196my $rt = getOpt('rt');
197
198# Read the first 'maxInfoLines' of the testcase and fetch information
199# from the comments
200
201sub getTestOpt {
202    my ($name) = @_;
203    # This is what we return
204    my %db = ();
205
206    open IN, $name or die "Cannot open $name: $?";
207    for(my $lines = getOpt('maxInfoLines'), my $str = <IN>;
208	defined($str) && $lines > 0;
209	$lines--, $str = <IN>)
210    {
211	if($str =~ /^(;|\s|%|\#)*Regression level\s*=\s*(\d+)/i) {
212	    $db{'level'} = $2;
213	}
214	if($str =~ /^(;|\s|%|\#)*Result\s*=\s*(Valid|Invalid|Satisfiable|Unsatisfiable|Unknown)/i) {
215	    $db{'result'} = lc $2;
216	}
217	if($str =~ /^( |\t)*:status\s*(unsat|sat|unknown)/i) {
218	    $db{'result'} = lc $2;
219	}
220	if($str =~ /^(;|\s|%|\#)*Runtime\s*=\s*(\d+)/i) {
221	    $db{'runtime'} = $2;
222	}
223	if($str =~ /^(;|\s|%|\#)*Proof\s*=\s*(yes|no)/i) {
224	    if($2 eq "yes") { $db{'proofs'} = 1; }
225	    else { $db{'proofs'} = 0; }
226	}
227	if($str =~ /^(;|\s|%|\#)*SAT mode\s*=\s*(on|off)/i) {
228	    if($2 eq "on") { $db{'sat'} = 1; }
229	    else { $db{'sat'} = 0; }
230	}
231	if($str =~ /^(;|\s|%|\#)*Language\s*=\s*(.*)$/i) {
232	    $db{'lang'} = lc $2;
233	}
234	if($str =~ /^(;|\s|%|\#)*Program Options\s*=\s*(.*)$/i) {
235	    $db{'clOptions'} = $2;
236	}
237    }
238    close IN;
239
240    # If regression level is not set, make it 3. So, if a lower level
241    # is requested, only explicitly marked tests will be run.
242    if(!defined($db{'level'})) { $db{'level'}=3; }
243    # If the input language is not defined, guess it by extension
244    if(!defined($db{'lang'})) {
245	if($name =~ /\.(cvc|svc)$/) {
246	    $db{'lang'} = "presentation";
247	} elsif($name =~ /\.(li?sp)$/) {
248	    $db{'lang'} = "internal";
249	} elsif($name =~ /\.(smt)$/) {
250	    $db{'lang'} = "smtlib";
251	}
252    }
253
254    return %db;
255}
256
257# Total number of tests run
258my $testsTotal=0;
259# Total number of proofs checked by pfc
260my $proofsChecked=0;
261# Total number of tests with problems (each test is counted at most once)
262my $testsProblems=0;
263### Database of results
264# It is a hash mapping problem keys to arrays of testcase names.
265# Only problematic testcase are inserted here.
266# Keys are: fail, result, proof, noproof (no proof generated when should),
267# time, timeTooMuch, lang (wrong language),
268# error (program reported errors, but didn't die)
269my %testsDB=();
270
271# Search for a string element in the array ref, and return 1 if found, 0 if not
272sub findStringElement {
273    my ($el, $aRef) = @_;
274    foreach my $v (@{$aRef}) {
275	if($v eq $el) { return 1; }
276    }
277    return 0;
278}
279
280# Add a testcase to the set of problematic runs.
281# Args:
282#   test is the full or relative path to the test file
283#   lang is the input language (not used currently)
284#   problem is the name of the problem the testcase exhibits
285sub addProblem {
286    my ($test, $lang, $problem) = @_;
287    my $aRef = $testsDB{$problem};
288    if(!defined($aRef)) { $aRef=[ ]; }
289    if(!findStringElement($test, $aRef)) {
290	$testsDB{$problem} = [@{$aRef}, $test];
291    }
292}
293
294# Total running time
295my $totalTime = time;
296my $totalRunningTime = 0;
297my $defaultDir = `pwd`;
298$defaultDir =~ s/\n//;
299
300foreach my $testcase (@testcases) {
301    chdir $defaultDir or die "Cannot chdir to $defaultDir: $?";
302    my @testcasesTmp = ();
303    if(-f $testcase) { push @testcasesTmp, $testcase; }
304    elsif(-d $testcase) {
305	# Compute the list of files for testcases
306	opendir(TESTS, $testcase)
307	    or die "Cannot open directory $testcase: $?";
308	@testcasesTmp = grep {
309	    /[.]([sc]vcl?|li?sp|smt)$/ && -f "$testcase/$_" } readdir(TESTS);
310	closedir TESTS;
311	@testcasesTmp = map { "$testcase/$_" } @testcasesTmp;
312    } else {
313	print("*** WARNING: cannot find testcase $testcase: ",
314	      "no such file or directory\n");
315    }
316
317    for(my $i=0; $i<=$#testcasesTmp; $i++) {
318	my $name = $testcasesTmp[$i];
319	my $file = "$defaultDir/$name";
320	my $hasProblem=0;
321	if(!(-f $file)) {
322	    print "WARNING: no such file: $file\n";
323	    next;
324	}
325	my %opt = getTestOpt($file);
326	# Check regression level
327	if(defined($opt{'level'}) && $level < $opt{'level'}) {
328	    # Regression level of this test is too high; skip it
329	    next;
330	}
331	# Print the testcase name
332	print("===============================================\n",
333	      $testcasesTmp[$i], ":\n");
334	# Check the input language
335	if (!defined($opt{'lang'})) {
336	    print "Unknown language, skipping $testcasesTmp[$i]\n";
337	    $hasProblem=1;
338	    addProblem($name, $lang, 'lang');
339	    next;
340	}
341	if($lang ne "all" && $lang ne $opt{'lang'}) {
342	    print "Wrong input language, skipping $testcasesTmp[$i]\n";
343	    $hasProblem=1;
344	    addProblem($name, $lang, 'lang');
345	    next;
346	}
347	my $checkProofs = getOpt('proofs', \%opt);
348	my $expRuntime = $opt{'runtime'};
349	my $expResult = $opt{'result'};
350	my $clOptions = getOpt('clOptions', \%opt);
351	my $language = $opt{'lang'};
352	# Print some testcase specific info
353	if($verbose) {
354	    print("Language: $language\n");
355	    print("Checking proofs: ", ($checkProofs)? "yes" : "no",
356		  "\n");
357	    if($rt && defined($expRuntime)) {
358		print("Expected runtime: ", $expRuntime, " sec\n");
359	    }
360	    if(defined($expResult)) {
361		print("Expected result: ", $expResult, "\n");
362	    }
363	    if($clOptions =~ /\S/) {
364		print("Program options: ", $clOptions, "\n");
365	    }
366	}
367	# Create a temporary dir, but first delete it; there may be
368	# junk there
369	system("/bin/rm -rf $tmpdir");
370	mkdir $tmpdir or print "Cannot create directory $tmpdir\n";
371	chdir $tmpdir or die "Cannot chdir to $tmpdir: $?";
372
373	# Compute arguments
374	my @progArgs = ();
375	push @progArgs, ($checkProofs)? "+proofs" : "-proofs";
376	if($language ne "presentation") { push @progArgs, "-lang $language"; }
377	push @progArgs, $clOptions;
378	my $progArgs = join(" ",  @progArgs);
379	# Now, run the sucker
380	my $timeMax = getOpt('time');
381	my $timeLimit = ($timeMax > 0)? "-t $timeMax" : "";
382	my $limits = "ulimit -c 0 -d 1000000 -m 1000000 ".
383	    "-s 50000 -v 1000000 $timeLimit";
384	# Windows ulimit dies if you pass -m
385	$limits = "ulimit -c 0 -d 1000000 -s 50000 -v 1000000 $timeLimit" if `uname -o` eq 'Cygwin';
386	my $logging = ($verbose)? " 2>&1 | tee output" : "> output 2>&1";
387	my $timing = "'@TIME@' -f \"User+Sys Time: %U+%S\" ";
388	if($verbose) {
389	    print "***\n";
390	    print "Running '$prog' $progArgs < '$file'\n";
391	    print "***\n";
392	}
393	my $time = time;
394	my $exitVal = system("$limits; $timing '$prog' $progArgs "
395			     . "< '$file' $logging");
396	$time = time - $time;
397	# OK, let's see what happened
398	$testsTotal++;
399	# Printing runtime
400	print "Elapsed Runtime: $time sec\n";
401	# Parsing the output
402	open IN, "output" or die "Cannot open `pwd`/output: $?";
403	my $str;
404	my $result="";
405	while(defined($str=<IN>)) {
406	    # Find at least one valid result
407	    if($result ne "valid" && $str =~ /^(Valid|In[Vv]alid|Satisfiable|Unsatisfiable|Unknown|unsat|sat|unknown)/) {
408		$result=lc $1;
409	    }
410	    # Exit value may be masked by the shell pipe.  Fish it
411	    # out from the output
412	    if($str =~ /^(Interrupted|Segmentation|Bus error|.*exception|.*Fatal error|.*std::bad_alloc)/) {
413		$exitVal = $1;
414	    }
415	    if($str =~ /^User\+Sys Time: (\d+\.\d\d)\+(\d+\.\d\d)/) {
416		$time = $1+$2;
417		print "Program Runtime: $time";
418		$totalRunningTime = $totalRunningTime + $time;
419	    }
420	}
421	close IN;
422	if($rt && defined($expRuntime)) {
423	    if($time > $expRuntime) {
424		if($time > 10*$expRuntime) {
425		    print " MUCH";
426		    addProblem($name, $lang, 'timeTooMuch');
427		}
428		print " LONGER than expected: $expRuntime sec";
429		$hasProblem=1;
430		addProblem($name, $lang, 'time');
431	    }
432	    elsif(($expRuntime >= 4 && $expRuntime <= 15 && $time <= $expRuntime-2) ||
433	          ($expRuntime > 15 && $time <= (17*$expRuntime)/20)) {
434		if($time <= $expRuntime/2) {
435		    print " MUCH";
436		    addProblem($name, $lang, 'timeTooFast');
437		}
438                print " FASTER than expected: $expRuntime sec";
439                addProblem($name, $lang, 'timeFast');
440                $hasProblem=1;
441            }
442	}
443	print "\n";
444	if($exitVal ne "0") {
445	    print "*** FAILED with exit code $exitVal\n";
446	    $hasProblem=1;
447	    addProblem($name, $lang, 'fail');
448	}
449	# Checking for errors
450#	if($hasErrors) {
451#	    $hasProblem=1;
452#	    addProblem($name, $lang, 'error');
453#	    print "ERRORS in the test\n";
454#	}
455	# Printing result diagnostics
456	if(defined($expResult)) {
457	    if($expResult ne $result) {
458		$hasProblem=1;
459		if($result eq "") {
460		    addProblem($name, $lang, 'fail');
461		    print("FAILED (no result, expected $expResult)\n");
462		} else {
463		    addProblem($name, $lang, 'result');
464		    print("WRONG RESULT (", $result,
465			  " instead of $expResult)\n");
466		}
467	    } else {
468		print "Result is correct\n";
469	    }
470	}
471	$testsProblems += $hasProblem;
472	print("=============== End of testcase ===============\n");
473    }
474}
475
476$totalTime = time - $totalTime;
477
478print "\nStatistics:\n";
479print "Total tests run: $testsTotal\n";
480print "Total running time: $totalRunningTime sec\n";
481print "Total elapsed time: $totalTime sec\n";
482print "Total number of proofs checked: $proofsChecked\n";
483print "Problematic cases: $testsProblems\n";
484if($testsProblems > 0 && $verbose) {
485    my $aref;
486    print "\nDetailed Statistics:\n";
487    $aref=$testsDB{'fail'};
488    if(defined($aref)) {
489	my @a = @{$aref};
490	printf("Failed tests [%d]:\n", $#a+1);
491	foreach my $n (@a) { print "  $n\n"; }
492    }
493#    $aref=$testsDB{'error'};
494#    if(defined($aref)) {
495#	my @a = @{$aref};
496#	printf("Tests with errors [%d]:\n", $#a+1);
497#	foreach my $n (@a) { print "  $n\n"; }
498#    }
499    $aref=$testsDB{'result'};
500    if(defined($aref)) {
501	my @a = @{$aref};
502	printf("Tests with wrong results [%d]:\n", $#a+1);
503	foreach my $n (@a) { print "  $n\n"; }
504    }
505    $aref=$testsDB{'proof'};
506    if(defined($aref)) {
507	my @a = @{$aref};
508	printf("Tests with failed proofs [%d]:\n", $#a+1);
509	foreach my $n (@a) { print "  $n\n"; }
510    }
511    $aref=$testsDB{'noproof'};
512    if(defined($aref)) {
513	my @a = @{$aref};
514	printf("Tests that should have proofs but don't [%d]:\n", $#a+1);
515	foreach my $n (@a) { print "  $n\n"; }
516    }
517    $aref=$testsDB{'timeFast'};
518    if(defined($aref)) {
519	my @a = @{$aref};
520	printf("Tests running faster than expected [%d]:\n", $#a+1);
521	foreach my $n (@a) { print "  $n\n"; }
522    }
523    $aref=$testsDB{'timeTooFast'};
524    if(defined($aref)) {
525	my @a = @{$aref};
526	printf("...including tests running at least twice as fast as expected [%d]:\n", $#a+1);
527	foreach my $n (@a) { print "  $n\n"; }
528    }
529    $aref=$testsDB{'time'};
530    if(defined($aref)) {
531	my @a = @{$aref};
532	printf("Tests running longer [%d]:\n", $#a+1);
533	foreach my $n (@a) { print "  $n\n"; }
534    }
535    $aref=$testsDB{'timeTooMuch'};
536    if(defined($aref)) {
537	my @a = @{$aref};
538	printf("...including tests running WAY too long [%d]:\n", $#a+1);
539	foreach my $n (@a) { print "  $n\n"; }
540    }
541    $aref=$testsDB{'lang'};
542    if(defined($aref)) {
543	my @a = @{$aref};
544	printf("Tests with wrong input language [%d]:\n", $#a+1);
545	foreach my $n (@a) { print "  $n\n"; }
546    }
547}
548
549# Delete temporary dir if there is one
550system("/bin/rm -rf $tmpdir");
551
552exit ($testsProblems > 0 ? 2 : 0);
553