SOLVER_INCLUDE = $(TOP)/src/sat/core
endif
+# todo: These should be set by the config script of course..
+TEST_PREFIX=../stp-tests/
SHELL=/bin/bash
+
# You can compile using make STATIC=true to compile a statically
# linked executable Note that you should execute liblinks.sh first.
#STATIC=true
rm -rf scripts/config.info
.PHONY: regressall
-regressall:
- $(MAKE) regresscapi && $(MAKE) regresscvc && $(MAKE) regresssmt && $(MAKE) regressstp && $(MAKE) regressbigarray
-
+regressall:
+ $(MAKE) check
+ $(MAKE) regresscapi
+ $(MAKE) regresscvc
+ $(MAKE) regresssyn
+ $(MAKE) regresssmt
+ $(MAKE) regressbigarray
+ $(MAKE) regressstp
+
+# Runs the basic tests in tests/
.PHONY: check
check:
$(MAKE) regresscvcbasic && $(MAKE) regresssmtbasic
-# The higher the level, the more tests are run (3 = all)
-REGRESS_LEVEL=4
-REGRESS_TESTS=$(REGRESS_TESTS0)
-PROGNAME=bin/stp
-ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
-
-REGRESS_LOG = `date +%Y-%m-%d`"-regress-cvc.log"
-.PHONY: regresscvc
-regresscvc:
+#A generic test target called by the other tests.
+.PHONY: baseTest
+baseTest:
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
- scripts/run_cvc_tests.pl $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
+ $(TO_RUN) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
-# The higher the level, the more tests are run (3 = all)
-BIGARRAY_LOG = `date +%Y-%m-%d`"-regress-bigarray.log"
-PROGNAME=bin/stp
-ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME)
+
+.PHONY: regresscvc
+regresscvc: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)test/
+regresscvc: REGRESS_LOG=`date +%Y-%m-%d`"-regress-cvc.log"
+regresscvc: baseTest
+
+.PHONY: regresssyn
+regresssyn: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)synthesis-tests/
+regresssyn: REGRESS_LOG = `date +%Y-%m-%d`"-regress-syn.log"
+regresssyn: baseTest
.PHONY: regressbigarray
-regressbigarray:
- @echo "*********************************************************" \
- | tee -a $(BIGARRAY_LOG)
- @echo "Starting tests at" `date` | tee -a $(BIGARRAY_LOG)
- @echo "*********************************************************" \
- | tee -a $(BIGARRAY_LOG)
- scripts/run_bigarray_tests.pl $(ALL_OPTIONS) 2>&1 | tee -a $(BIGARRAY_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
- @echo "*********************************************************" \
- | tee -a $(BIGARRAY_LOG)
- @echo "Output is saved in $(BIGARRAY_LOG)" | tee -a $(BIGARRAY_LOG)
- @echo "*********************************************************" \
- | tee -a $(BIGARRAY_LOG)
+regressbigarray: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)bigarray-test/
+regressbigarray: REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log"
+regressbigarray: baseTest
-SMT_LOG = `date +%Y-%m-%d`"-regress-smt.log"
.PHONY: regresssmt
-regresssmt:
- @echo "*********************************************************" \
- | tee -a $(SMT_LOG)
- @echo "Starting tests at" `date` | tee -a $(SMT_LOG)
- @echo "*********************************************************" \
- | tee -a $(SMT_LOG)
- scripts/run_smt_tests.pl $(ALL_OPTIONS) 2>&1 | tee -a $(SMT_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
- @echo "*********************************************************" \
- | tee -a $(SMT_LOG)
- @echo "Output is saved in $(SMT_LOG)" | tee -a $(SMT_LOG)
- @echo "*********************************************************" \
- | tee -a $(SMT_LOG)
+regresssmt: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)smt-test/
+regresssmt: REGRESS_LOG = `date +%Y-%m-%d`"-regress-smt.log"
+regresssmt: baseTest
-CAPI_LOG = `date +%Y-%m-%d`"-regress-c-api.log"
.PHONY: regresscapi
-regresscapi:
- @echo "*********************************************************" \
- | tee -a $(CAPI_LOG)
- @echo "Starting tests at" `date` | tee -a $(CAPI_LOG)
- @echo "*********************************************************" \
- | tee -a $(CAPI_LOG)
- $(MAKE) -C tests/c-api-tests 2>&1 | tee -a $(CAPI_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
- @echo "*********************************************************" \
- | tee -a $(CAPI_LOG)
- @echo "Output is saved in $(CAPI_LOG)" | tee -a $(CAPI_LOG)
- @echo "*********************************************************" \
- | tee -a $(CAPI_LOG)
+regresscapi: TO_RUN=$(MAKE) -C tests/c-api-tests
+regresscapi: REGRESS_LOG = `date +%Y-%m-%d`"-regress-c-api.log"
+regresscapi: baseTest
-STP_LOG = `date +%Y-%m-%d`"-regress-stp.log"
.PHONY: regressstp
-regressstp:
- @echo "*********************************************************" \
- | tee -a $(STP_LOG)
- @echo "Starting tests at" `date` | tee -a $(STP_LOG)
- @echo "*********************************************************" \
- | tee -a $(STP_LOG)
- scripts/run_stp_tests.pl 2>&1 | tee -a $(STP_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
- @echo "*********************************************************" \
- | tee -a $(STP_LOG)
- @echo "Output is saved in $(STP_LOG)" | tee -a $(STP_LOG)
- @echo "*********************************************************" \
- | tee -a $(STP_LOG)
+regressstp: TO_RUN=scripts/run_stp_tests.pl 2>&1
+regressstp: STP_LOG = `date +%Y-%m-%d`"-regress-stp-api.log"
+regressstp: baseTest
-CVCBASIC_LOG = `date +%Y-%m-%d`"-regress-cvcbasic.log"
.PHONY: regresscvcbasic
-regresscvcbasic:
- @echo "*********************************************************" \
- | tee -a $(CVCBASIC_LOG)
- @echo "Starting tests at" `date` | tee -a $(CVCBASIC_LOG)
- @echo "*********************************************************" \
- | tee -a $(CVCBASIC_LOG)
- scripts/run_basic_cvctests.pl 2>&1 | tee -a $(CVCBASIC_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
- @echo "*********************************************************" \
- | tee -a $(CVCBASIC_LOG)
- @echo "Output is saved in $(CVCBASIC_LOG)" | tee -a $(CVCBASIC_LOG)
- @echo "*********************************************************" \
- | tee -a $(CVCBASIC_LOG)
+regresscvcbasic: TO_RUN=scripts/run_tests.pl --td=tests/sample-tests
+regresscvcbasic: REGRESS_LOG = `date +%Y-%m-%d`"-regress-regresscvcbasic.log"
+regresscvcbasic: baseTest
-SMTBASIC_LOG = `date +%Y-%m-%d`"-regress-smtbasic.log"
.PHONY: regresssmtbasic
-regresssmtbasic:
- @echo "*********************************************************" \
- | tee -a $(SMTBASIC_LOG)
- @echo "Starting tests at" `date` | tee -a $(SMTBASIC_LOG)
- @echo "*********************************************************" \
- | tee -a $(SMTBASIC_LOG)
- scripts/run_basic_smttests.pl 2>&1 | tee -a $(SMTBASIC_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
- @echo "*********************************************************" \
- | tee -a $(SMTBASIC_LOG)
- @echo "Output is saved in $(SMTBASIC_LOG)" | tee -a $(SMTBASIC_LOG)
- @echo "*********************************************************" \
- | tee -a $(SMTBASIC_LOG)
-
-SYNTHESIS_LOG = `date +%Y-%m-%d`"-regress-synthesis.log"
-.PHONY: regresssyn
-regresssyn:
- @echo "*********************************************************" \
- | tee -a $(SYNTHESIS_LOG)
- @echo "Starting tests at" `date` | tee -a $(SYNTHESIS_LOG)
- @echo "*********************************************************" \
- | tee -a $(SYNTHESIS_LOG)
- scripts/run_synthesis_tests.pl $(ALL_OPTIONS) 2>&1 | tee -a $(SYNTHESIS_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
- @echo "*********************************************************" \
- | tee -a $(SYNTHESIS_LOG)
- @echo "Output is saved in $(SYNTHESIS_LOG)" | tee -a $(SYNTHESIS_LOG)
- @echo "*********************************************************" \
- | tee -a $(SYNTHESIS_LOG)
+regresssmtbasic: TO_RUN=scripts/run_tests.pl --td=tests/sample-smt-tests
+regresssmtbasic: REGRESS_LOG = `date +%Y-%m-%d`"-regress-regresssmtbasic.log"
+regresssmtbasic: baseTest
+# The higher the level, the more tests are run (3 = all)
+REGRESS_LEVEL=4
+REGRESS_TESTS=$(REGRESS_TESTS0)
+PROGNAME=bin/stp
+ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
GRIND_LOG = `date +%Y-%m-%d`"-grind.log"
GRINDPROG = valgrind --leak-check=full --undef-value-errors=no
GRIND_TAR = $(BIN_DIR)/stp -d
+++ /dev/null
-#!/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 -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" => 30,
- # Additional command line options to stp
- "stpOptions" => "-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/sample-tests");
-# 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];
- }
-}
-
-# 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);
+++ /dev/null
-#!/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 -d -m", # 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" => 30,
- # Additional command line options to stp
- "stpOptions" => "-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/sample-smt-tests");
-# 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];
- }
-}
-
-# 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);
+++ /dev/null
-#!/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 -d -t", # 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" => 180,
- # Additional command line options to stp
- "stpOptions" => "-d -t ");
-
-# Database of command line options. Initially, they are undefined
-my %options = ();
-# The list of testcases to run
-#
-#my @testcases = "sample-tests";
-my @testcases = "../../stp-tests/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];
- }
-}
-
-# 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);
-
+++ /dev/null
-#!/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 -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" => 180,
- # Additional command line options to stp
- "stpOptions" => "-d");
-
-# Database of command line options. Initially, they are undefined
-my %options = ();
-# The list of testcases to run
-#
-#my @testcases = "sample-tests";
-my @testcases = "../../stp-tests/synthesis-tests/";
-# 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];
- }
-}
-
-# 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|stp)$/ && -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);
-
#!/usr/bin/perl -w
+# This is based on the CVC regression test program. Thanks.
+
+
+
# 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.
# are not recognized are also ignored.
use strict;
+use Getopt::Long;
my %optionsHelp =
("-h" => "Print this help and exit",
"-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)"
- );
+ "-pfc prog" => "Use \"prog\" to run a proof checker (default=true)",
+ "-td dir" => "Use \"dir\" as the test directory"
+ );
my $usageString =
- "run_tests [ options ] [ test1 test2 ... ] [ -- [ stp options ] ]
+ "run_tests --td=dir [options]
Run STP Lite regression tests. Concrete test files or directories
with test files should be specified by name with a full path or
# Database of default values for options
my %optionsDefault = ("level" => 4,
"verbose" => 1,
- "rt" => 1,
+ "td" => "../stp-tests/test",
+ "rt" => 1,
"proofs" => 0,
"lang" => "all",
"stppath" => "stp/bin",
- "vc" => $pwd . "/bin/stp -d", # Program names
+ "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",
"stpOptions" => "-d");
# Database of command line options. Initially, they are undefined
+
my %options = ();
-# The list of testcases to run
-#
-#my @testcases = "sample-tests";
-my @testcases = "../../stp-tests/bigarray-test";
+
+#td: test directory. Get the "td" parameter from the command line.
+my $td;
+GetOptions("td=s" => \$td);
+
+
# Temporary array for STP options
my @stpOptions = ();
# State is either "own" or "stp", meaning that we're reading either
my $lang = getOpt('lang');
my $rt = getOpt('rt');
+# The list of testcases to run
+my @testcases;
+if (defined($td))
+{
+ @testcases = $td;
+}
+else
+{ @testcases = getOpt('td');
+}
+
# Read the first 'maxInfoLines' of the testcase and fetch information
# from the comments
}
}
-# Total running time
-my $totalTime = time;
my $defaultDir = `pwd`;
$defaultDir =~ s/\n//;
+ 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;
+
foreach my $testcase (@testcases) {
chdir $defaultDir or die "Cannot chdir to $defaultDir: $?";
my @testcasesTmp = ();
mkdir $tmpdir or die "Cannot create directory $tmpdir: $?";
chdir $tmpdir or die "Cannot chdir to $tmpdir: $?";
- # Compute stp arguments
- my @stpArgs = ();
+ # If the filename contains ".smt", then tell stp to use the SMT-LIB parser.
+ my $stpArgs ="";
+ if($file =~ m/\.smt/)
+ {
+ $stpArgs = "-m";
+ }
+
# 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";
my $timing = ($verbose)? "time " : "";
if($verbose) {
print "***\n";
- #print "Running $stp $stpArgs < $file\n";
- print "Running $stp < $file\n";
+ print "Running $stp $stpArgs < $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");
+ # Now, run the sucker
+ my $exitVal = system("$limits; $timing $stp $stpArgs < $file $logging");
$time = time - $time;
# OK, let's see what happened
$testsTotal++;
if($result ne "valid" && $str =~ /^(Valid|In[Vv]alid|Unknown)./) {
$result=lc $1;
}
+ if($result ne "sat" && $str =~ /^(sat|unsat|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)/) {
if($str =~ /^(\*|\s)*((parse\s+)?[Ee]rror)/) {
$hasErrors=1;
}
+ # STP reports if the the SMT-LIB file format has a different actual and expected result.
+ if($str =~ /Expected/ && $str =~ /FOUND/) {
+ $hasErrors=1;
+ }
}
close IN;
if($exitVal ne "0") {
addProblem($name, $lang, 'fail');
}
# Checking for errors
- if($hasErrors) {
+ elsif($hasErrors) {
$hasProblem=1;
addProblem($name, $lang, 'error');
print "ERRORS in the test\n";
}
# Printing result diagnostics
- if(defined($expResult)) {
+ elsif(defined($expResult)) {
if($expResult ne $result) {
$hasProblem=1;
if($result eq "") {
print "Result is correct\n";
}
}
- # else {
-# print "Error: No result\n";
-# }
+ elsif ($result eq "" ) {
+ print "Error: No result\n";
+ addProblem($name, $lang, 'fail');
+ $hasProblem=1
+ }
$testsProblems += $hasProblem;
print("=============== End of testcase ===============\n");
}
system("/bin/rm -rf $tmpdir");
#exit ($testsProblems > 0 ? 2 : 0);
+
projects / francis / stp.git / commitdiff