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