From a9490d9d8736a4214d11a00a2a0f09a34de4f666 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 24 Jun 2010 14:03:37 +0000
Subject: [PATCH] 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
---
 scripts/Makefile.in      |   7 +-
 scripts/run_stp_tests.pl | 489 ---------------------------------------
 2 files changed, 5 insertions(+), 491 deletions(-)
 delete mode 100755 scripts/run_stp_tests.pl

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);
-- 
2.47.3