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