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