From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 24 Jun 2010 14:03:37 +0000 (+0000)
Subject: Bugfix. The script that was called by regressstp didn't record errors when some test... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a9490d9d8736a4214d11a00a2a0f09a34de4f666;p=francis%2Fstp.git

Bugfix. The script that was called by regressstp didn't record errors when some test cases failed. So I've removed it, and use the generic test runner instead. There are two differences: multiples log files are now created, and the timeout is 180 sec.



git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@874 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 71241b1..8149ed8 100644
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -196,8 +196,11 @@ regresscapi: REGRESS_LOG = `date +%Y-%m-%d`"-regress-c-api.log"
 regresscapi: baseTest
 
 .PHONY: regressstp
-regressstp: TO_RUN=scripts/run_stp_tests.pl
-regressstp: REGRESS_LOG = `date +%Y-%m-%d`"-regress-stp.log"
+regressstp: TO_RUN=scripts/run_tests.pl --td=tests/bio-tests
+regressstp: REGRESS_LOG = `date +%Y-%m-%d`"-regress-stp-bio.log"
+regressstp: baseTest
+regressstp: TO_RUN=scripts/run_tests.pl --td=tests/big-test
+regressstp: REGRESS_LOG = `date +%Y-%m-%d`"-regress-stp-big-test.log"
 regressstp: baseTest
 
 .PHONY: regresscvcbasic
diff --git a/scripts/run_stp_tests.pl b/scripts/run_stp_tests.pl
deleted file mode 100755
index b1b316c..0000000
--- a/scripts/run_stp_tests.pl
+++ /dev/null
@@ -1,489 +0,0 @@
-#!/usr/bin/perl -w
-
-# Run STP regression tests of a given level (default: 0, meaning
-# minimum amount of tests).  The higher the regression level, the more
-# tests to run, and the harder they get.
-# Each test may contain information about its regression level,
-# expected outcome, expected runtime, whether it produces a proof,
-# etc. in the format given below.  This script will scan the first 100
-# lines of each test and try to collect this information.
-
-# If some info is not found, defaults are assumed.  Default regression
-# level is 0, expected runtime is unbounded, outcome is undefined
-# (whatever it returns is OK), proof should be produced if outcome is
-# Valid, and if it is produced, it'll be verified.
-
-# Test info is given in the comments; here are examples
-# 
-# %%% Regression level = 2
-# %%% Result = Valid  %% or Invalid, or Unknown
-# %%% Runtime = 10   %% in seconds
-# %%% Proof = yes    %% or 'no', if it doesn't produce a proof
-# %%% Language = presentation %% or 'internal'
-
-# The number of '%' and following spaces can vary, case is not
-# important.  Any text after the value is ignored.  Any comments that
-# are not recognized are also ignored.
-
-use strict;
-
-my %optionsHelp =
-    ("-h" => "Print this help and exit",
-     "-v" => "Be verbose (default, opposite of -q)",
-     "-q" => "Quiet mode (opposite of -v)",
-     "-l n" => "Set regression level (default 0, the easiest level)",
-     "+rt" => "Check that each test finishes within the specified runtime",
-     "-rt" => "Do not check whether test finishes within the specified runtime (default)",
-#      "+proofs" => "Produce and verify proofs",
-#      "-proofs" => "Do not produce / verify proofs (default)",
-     "-lang name" => "Use the named input language only (default=all)",
-     "-t secs" => "Run each executable for at most 'secs' seconds [0 = no limit]",
-     "-vc prog" => "Use \"prog\" to run STP (default=bin/stp)",
-     "-pfc prog" => "Use \"prog\" to run a proof checker (default=true)"
-     );
-
-my $usageString =
-    "run_tests [ options ] [ test1 test2 ... ] [ -- [ stp options ] ]
-
-Run STP Lite regression tests.  Concrete test files or directories
-with test files should be specified by name with a full path or
-relative path to the current directory.  If none specified, all
-subdirectories are searched for test files.
-
-Default running mode is overriden by test specs;
-test specs are overriden by command line options.
-
-Options:
-  " . join("\n  ",
-	   map { sprintf("%-9s %s", $_, $optionsHelp{$_}) } keys(%optionsHelp));
-
-my $pwd = `pwd` ;
-chomp $pwd ;
-
-# Database of default values for options
-my %optionsDefault = ("level" => 4,
-		      "verbose" => 1,
-                      "rt" => 1,
-		      "proofs" => 0,
-		      "lang" => "all",
-		      "stppath" => "stp/bin",
-		      "vc" => $pwd . "/bin/stp -t -d", # Program names
-		      #"vc" => "valgrind --leak-check=full /home/vganesh/stp/bin/stp", # Program names
-		      "pfc" => "true",
-		      "stptestpath" => "stp/test",
-		      "stptemp" => "/tmp",
-		      # max. number of lines to read from the testcase file
-		      # when looking for info comments
-		      "maxInfoLines" => 4,
-		      # Runtime limit; 0 = no limit
-		      "time" => 60,
-		      # Additional command line options to stp
-		      "stpOptions" => "-t -d");
-
-# Database of command line options.  Initially, they are undefined
-my %options = ();
-# The list of testcases to run
-#
-#my @testcases = "sample-tests";
-my @testcases = ("tests/bio-tests", "tests/histar-big-tests", "tests/sample-tests", "tests/big-test");
-# Temporary array for STP options
-my @stpOptions = ();
-# State is either "own" or "stp", meaning that we're reading either
-# our own or stp's options.
-my $argState = "own";
-
-if($#stpOptions >= 0) {
-    $options{'stpOptions'} = join(" ", map { "\"" . $_ . "\"" } @stpOptions);
-}
-
-# Compute the value of the option: first check the command line
-# option, then the supplied database (by ref. as the second arg), then
-# default values database.  If it cannot find definition, it is a bug,
-# and the script is stopped.
-
-sub getOpt {
-    my ($name, $dbRef) = @_;
-    
-    return $options{$name} if(defined($options{$name}));
-    return $dbRef->{$name} if(defined($dbRef) && defined($dbRef->{$name}));
-    return $optionsDefault{$name} if(defined($optionsDefault{$name}));
-    
-    # Option value is not found
-    die "getOpt($name): option is undefined";
-}
-
-my $verbose = getOpt('verbose');
-
-# Set the path
-my $systemPath = ".";
-if(defined($ENV{'PATH'})) {
-    $systemPath = $ENV{'PATH'};
-}
-$ENV{'PATH'} = getOpt('stppath') . ":" . $systemPath;
-
-if($verbose) {
-    print "*********\n";
-    print("Regression level: ", getOpt('level'), "\n");
-    print("Language: ", getOpt('lang'), "\n");
-    print("Whether to produce / check proofs: ",
-	  (defined($options{'proofs'}))?
-	  (($options{'proofs'})? "yes" : "no") : "depends on testcase",
-	  "\n");
-    if(getOpt('time') > 0) {
-	print("Time limit per test: ", getOpt('time'), " sec\n");
-    }
-    print("PATH = ", $ENV{'PATH'}, "\n");
-    print "*********\n";
-}
-
-my $tmpdir = getOpt('stptemp') . "/stptmp-$$";
-my $currdir = `pwd`;
-my $stp = getOpt('vc');
-my $pfc = getOpt('pfc');
-my $level = getOpt('level');
-my $lang = getOpt('lang');
-my $rt = getOpt('rt');
-
-# Read the first 'maxInfoLines' of the testcase and fetch information
-# from the comments
-
-sub getTestOpt {
-    my ($name) = @_;
-    # This is what we return
-    my %db = ();
-
-    open IN, $name or die "Cannot open $name: $?";
-    for(my $lines = getOpt('maxInfoLines'), my $str = <IN>;
-	defined($str) && $lines > 0;
-	$lines--, $str = <IN>)
-    {
-	if($str =~ /^(\s|%|\#)*Regression level\s*=\s*(\d+)/i) {
-	    $db{'level'} = $2;
-	}
-	if($str =~ /^(\s|%|\#)*Result\s*=\s*(Valid|Invalid|Unknown)/i) {
-	    $db{'result'} = lc $2;
-	}
-	if($str =~ /^(\s|%|\#)*Runtime\s*=\s*(\d+)/i) {
-	    $db{'runtime'} = $2;
-	}
-	if($str =~ /^(\s|%|\#)*Proof\s*=\s*(yes|no)/i) {
-	    if($2 eq "yes") { $db{'proofs'} = 1; }
-	    else { $db{'proofs'} = 0; }
-	}
-	if($str =~ /^(\s|%|\#)*SAT mode\s*=\s*(on|off)/i) {
-	    if($2 eq "on") { $db{'sat'} = 1; }
-	    else { $db{'sat'} = 0; }
-	}
-	if($str =~ /^(\s|%|\#)*Language\s*=\s*((\w|\d|\_)+)/i) {
-	    $db{'lang'} = lc $2;
-	}
-	if($str =~ /^(\s|%|\#)*STP Options\s*=\s*(.*)$/i) {
-	    $db{'stpOptions'} = $2;
-	}
-    }
-    close IN;
-
-    # If regression level is not set, make it 3. So, if a lower level
-    # is requested, only explicitly marked tests will be run.
-    if(!defined($db{'level'})) { $db{'level'}=3; }
-    # If the input language is not defined, guess it by extension
-    if(!defined($db{'lang'})) {
-	if($name =~ /\.(stp|svc)$/) {
-	    $db{'lang'} = "presentation";
-	} elsif($name =~ /\.(li?sp)$/) {
-	    $db{'lang'} = "internal";
-	} elsif($name =~ /\.(smt)$/) {
-	    $db{'lang'} = "smt-lib";
-	}
-    }
-
-    return %db;
-}
-
-# Total number of tests run
-my $testsTotal=0;
-# Total number of proofs checked by pfc
-my $proofsChecked=0;
-# Total number of tests with problems (each test is counted at most once)
-my $testsProblems=0;
-### Database of results
-# It is a hash mapping problem keys to arrays of testcase names.
-# Only problematic testcase are inserted here.
-# Keys are: fail, result, proof, noproof (no proof generated when should),
-# time, timeTooMuch, lang (wrong language),
-# error (stp reported errors, but didn't die)
-my %testsDB=();
-
-# Search for a string element in the array ref, and return 1 if found, 0 if not
-sub findStringElement {
-    my ($el, $aRef) = @_;
-    foreach my $v (@{$aRef}) {
-	if($v eq $el) { return 1; }
-    }
-    return 0;
-}
-
-# Add a testcase to the set of problematic runs.
-# Args: 
-#   test is the full or relative path to the test file
-#   lang is the input language (not used currently)
-#   problem is the name of the problem the testcase exhibits
-sub addProblem {
-    my ($test, $lang, $problem) = @_;
-    my $aRef = $testsDB{$problem};
-    if(!defined($aRef)) { $aRef=[ ]; }
-    if(!findStringElement($test, $aRef)) {
-	$testsDB{$problem} = [@{$aRef}, $test];
-    }
-}
-
- system("echo Copying to /dev/null to fill the disk cache");
-
- foreach my $testcase (@testcases) {
-  system ("cat " . $testcase . "/*.* > /dev/null");
-}
-
-
-# Total running time
-my $totalTime = time;
-my $defaultDir = `pwd`;
-$defaultDir =~ s/\n//;
-
-foreach my $testcase (@testcases) {
-    chdir $defaultDir or die "Cannot chdir to $defaultDir: $?";
-    my @testcasesTmp = ();
-    if(-f $testcase) { push @testcasesTmp, $testcase; }
-    elsif(-d $testcase) {
-	# Compute the list of files for testcases
-	opendir(TESTS, $testcase)
-	    or die "Cannot open directory $testcase: $?";
-	@testcasesTmp = grep {
-	    /[.]([sc]vcl?|li?sp|smt)$/ && -f "$testcase/$_" } readdir(TESTS);
-	closedir TESTS;
-	@testcasesTmp = map { "$testcase/$_" } @testcasesTmp;
-    } else {
-	print("*** Error: WARNING: cannot find testcase $testcase: ",
-	      "no such file or directory\n");
-    }
-
-    for(my $i=0; $i<=$#testcasesTmp; $i++) {
-	my $name = $testcasesTmp[$i];
-	my $file = "$defaultDir/$name";
-	my $hasProblem=0;
-	if(!(-f $file)) {
-	    print "Error: WARNING: no such file: $file\n";
-	    next;
-	}
-	my %opt = getTestOpt($file);
-	# Check regression level
-	if(defined($opt{'level'}) && $level < $opt{'level'}) {
-	    # Regression level of this test is too high; skip it
-	    next;
-	}
-	# Print the testcase name
-	print("===============================================\n",
-	      $testcasesTmp[$i], ":\n");
-	# Check the input language
-	if($lang ne "all" && defined($opt{'lang'}) && $lang ne $opt{'lang'}) {
-	    print "Error: Wrong input language, skipping $testcasesTmp[$i]\n";
-	    $hasProblem=1;
-	    addProblem($name, $lang, 'lang');
-	    next;
-	}
-	my $checkProofs = getOpt('proofs', \%opt);
-	my $expRuntime = $opt{'runtime'};
-	my $expResult = $opt{'result'};
-	my $stpOptions = getOpt('stpOptions', \%opt);
-	# Print some testcase specific info
-	if($verbose) {
-	    print("Language: $lang\n");
-	    print("Checking proofs: ", ($checkProofs)? "yes" : "no",
-		  "\n");
-	    #if($rt && defined($expRuntime)) {
-	    if(defined($expRuntime)) {
-		print("Expected runtime: ", $expRuntime, " sec\n");
-	    }
-	    if(defined($expResult)) {
-		print("Expected result: ", $expResult, "\n");
-	    }
-	    if($stpOptions =~ /\S/) {
-		print("STP options: ", $stpOptions, "\n");
-	    }
-	}
-	# Create a temporary dir, but first delete it; there may be
-	# junk there
-	system("/bin/rm -rf $tmpdir");
-	mkdir $tmpdir or die "Cannot create directory $tmpdir: $?";
-	chdir $tmpdir or die "Cannot chdir to $tmpdir: $?";
-
-	# Compute stp arguments
-	my @stpArgs = ();
-	# push @stpArgs, ($checkProofs)? "+proofs" : "-proofs";
-	# if($lang ne "all") { push @stpArgs, "-lang $lang"; }
-	# push @stpArgs, $stpOptions;
-	# my $stpArgs = join(" ",  @stpArgs);
-	# Now, run the sucker
-	my $timeMax = getOpt('time');
-	my $timeLimit = ($timeMax > 0)? "-t $timeMax" : "";
-	my $limits = "ulimit -c 0; ulimit -d 2000000; ulimit -m 2000000; ulimit -v 2000000; ulimit $timeLimit";
-	#   "-s 10240 -v 2000000 $timeLimit";	
-	my $logging = ($verbose)? " 2>&1 | tee output" : "> output 2>&1";
-	my $timing = ($verbose)? "time " : "";
-	if($verbose) {
-	    print "***\n";
-	    #print "Running $stp $stpArgs < $file\n";
-	    print "Running $stp < $file\n";
-	    print "***\n";
-	}
-	my $time = time;
-	# my $exitVal = system("$limits; $timing $stp $stpArgs "
-	my $exitVal = system("$limits; $timing $stp "
-	#my $exitVal = system("$timing $stp "
-			     . "< $file $logging");
-	$time = time - $time;
-	# OK, let's see what happened
-	$testsTotal++;
-	# Printing runtime
-	print "Runtime: $time sec";
-	if($rt && defined($expRuntime)) {
-	    if($time > $expRuntime) {
-		if($time > 10*$expRuntime) {
-		    print " MUCH";
-		    addProblem($name, $lang, 'timeTooMuch');
-		}
-		print " : LONGER than expected: $expRuntime sec";
-		$hasProblem=1;
-		addProblem($name, $lang, 'time');
-	    }
-	    elsif($expRuntime >= 5 && $time < $expRuntime/2) {
-                print " : much FASTER than expected: $expRuntime sec";
-                addProblem($name, $lang, 'timeFast');
-                $hasProblem=1;
-            }
-	}
-	print "\n";
-	# Parsing the output
-	open IN, "output" or die "Cannot open `pwd`/output: $?";
-	my $str;
-	my $result="";
-	my $hasErrors=0;
-	while(defined($str=<IN>)) {
-	    # Find at least one valid result
-	    if($result ne "valid" && $str =~ /^(Valid|In[Vv]alid|Unknown)./) {
-		$result=lc $1;
-	    }
-	    # STP exit value may be masked by the shell pipe.  Fish it
-	    # out from the output
-	    if($str =~ /^(Interrupted|Segmentation|Bus error|Floating point exception|.*exception)/) {
-		$exitVal = $1;
-	    }
-	    if($str =~ /^(\*|\s)*((parse\s+)?[Ee]rror)/) {
-		$hasErrors=1;
-	    }
-	}
-	close IN;
-	if($exitVal ne "0") {
-	    print "*** Error: STP FAILED with exit code $exitVal\n";
-	    $hasProblem=1;
-	    addProblem($name, $lang, 'fail');
-	}
-	# Checking for errors
-	if($hasErrors) {
-	    $hasProblem=1;
-	    addProblem($name, $lang, 'error');
-	    print "ERRORS in the test\n";
-	}
-	# Printing result diagnostics
-	if(defined($expResult)) {
-	    if($expResult ne $result) {
-		$hasProblem=1;
-		if($result eq "") {
-		    addProblem($name, $lang, 'fail');
-		    print("Error: FAILED (no result, expected $expResult)\n");
-		} else {
-		    addProblem($name, $lang, 'result');
-		    print("Error: WRONG RESULT (", $result,
-			  " instead of $expResult)\n");
-		}
-	    } else {
-		print "Result is correct\n";
-	    }
-	}
-	# else {
-# 	    print "Error: No result\n";
-# 	}
-	$testsProblems += $hasProblem;
-	print("=============== End of testcase ===============\n");
-    }
-}
-
-$totalTime = time - $totalTime;
-
-print "\nStatistics:\n";
-print "Total tests run: $testsTotal\n";
-print "Total running time: $totalTime sec\n";
-print "Total number of proofs checked: $proofsChecked\n";
-print "Problematic cases: $testsProblems\n";
-if($testsProblems > 0 && $verbose) {
-    my $aref;
-    print "\nDetailed Statistics:\n";
-    $aref=$testsDB{'fail'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Failed tests [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'error'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Tests with errors [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'result'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Tests with wrong results [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'proof'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Tests with failed proofs [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'noproof'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Tests that should have proofs but don't [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'timeFast'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Tests running at least twice as fast as expected [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'time'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Tests running longer [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'timeTooMuch'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("...including tests running WAY too long [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-    $aref=$testsDB{'lang'};
-    if(defined($aref)) {
-	my @a = @{$aref};
-	printf("Tests with wrong input language [%d]:\n", $#a+1);
-	foreach my $n (@a) { print "  $n\n"; }
-    }
-}
-
-# Delete temporary dir if there is one
-system("/bin/rm -rf $tmpdir");
-
-#exit ($testsProblems > 0 ? 2 : 0);