From: trevor_hansen Date: Sun, 25 Apr 2010 16:13:40 +0000 (+0000) Subject: * Reduce the number of scripts we use to run regression tests. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1a1a9b05fcbd77a9af36d8551c7e4794e4e8b49b;p=francis%2Fstp.git * Reduce the number of scripts we use to run regression tests. * Remove redundacy from the Makefile. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@707 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 05a2c4e..8eea52f 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -35,8 +35,11 @@ ifeq ($(SAT),minisat) 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 diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 6812494..940625a 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -108,144 +108,82 @@ configclean: 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 diff --git a/scripts/run_basic_cvctests.pl b/scripts/run_basic_cvctests.pl deleted file mode 100755 index c40e2f4..0000000 --- a/scripts/run_basic_cvctests.pl +++ /dev/null @@ -1,482 +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 -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 = ; - defined($str) && $lines > 0; - $lines--, $str = ) - { - 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=)) { - # 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); diff --git a/scripts/run_basic_smttests.pl b/scripts/run_basic_smttests.pl deleted file mode 100755 index 5e23e74..0000000 --- a/scripts/run_basic_smttests.pl +++ /dev/null @@ -1,482 +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 -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 = ; - defined($str) && $lines > 0; - $lines--, $str = ) - { - 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=)) { - # 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); diff --git a/scripts/run_cvc_tests.pl b/scripts/run_cvc_tests.pl deleted file mode 100755 index db797ee..0000000 --- a/scripts/run_cvc_tests.pl +++ /dev/null @@ -1,483 +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 -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 = ; - defined($str) && $lines > 0; - $lines--, $str = ) - { - 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=)) { - # 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); - diff --git a/scripts/run_synthesis_tests.pl b/scripts/run_synthesis_tests.pl deleted file mode 100755 index cf33837..0000000 --- a/scripts/run_synthesis_tests.pl +++ /dev/null @@ -1,483 +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 -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 = ; - defined($str) && $lines > 0; - $lines--, $str = ) - { - 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=)) { - # 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); - diff --git a/scripts/run_bigarray_tests.pl b/scripts/run_tests.pl similarity index 91% rename from scripts/run_bigarray_tests.pl rename to scripts/run_tests.pl index 9e81486..c2ad63b 100755 --- a/scripts/run_bigarray_tests.pl +++ b/scripts/run_tests.pl @@ -1,5 +1,9 @@ #!/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. @@ -26,6 +30,7 @@ # are not recognized are also ignored. use strict; +use Getopt::Long; my %optionsHelp = ("-h" => "Print this help and exit", @@ -39,11 +44,12 @@ my %optionsHelp = "-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 @@ -63,11 +69,12 @@ chomp $pwd ; # 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", @@ -81,11 +88,14 @@ my %optionsDefault = ("level" => 4, "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 @@ -144,6 +154,16 @@ my $level = getOpt('level'); 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 @@ -237,11 +257,18 @@ sub addProblem { } } -# 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 = (); @@ -309,13 +336,17 @@ foreach my $testcase (@testcases) { 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"; @@ -324,15 +355,12 @@ foreach my $testcase (@testcases) { 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++; @@ -365,6 +393,10 @@ foreach my $testcase (@testcases) { 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)/) { @@ -373,6 +405,10 @@ foreach my $testcase (@testcases) { 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") { @@ -381,13 +417,13 @@ foreach my $testcase (@testcases) { 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 "") { @@ -402,9 +438,11 @@ foreach my $testcase (@testcases) { 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"); } @@ -480,3 +518,4 @@ if($testsProblems > 0 && $verbose) { system("/bin/rm -rf $tmpdir"); #exit ($testsProblems > 0 ? 2 : 0); +