1#!/bin/bash 2 3# 4# This file is part of the Yices SMT Solver. 5# Copyright (C) 2017 SRI International. 6# 7# Yices is free software: you can redistribute it and/or modify 8# it under the terms of the GNU General Public License as published by 9# the Free Software Foundation, either version 3 of the License, or 10# (at your option) any later version. 11# 12# Yices is distributed in the hope that it will be useful, 13# but WITHOUT ANY WARRANTY; without even the implied warranty of 14# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 15# GNU General Public License for more details. 16# 17# You should have received a copy of the GNU General Public License 18# along with Yices. If not, see <http://www.gnu.org/licenses/>. 19# 20 21# 22# Run regression tests 23# 24# Usage: check.sh <test-dir> <bin-dir> 25# 26# tests-dir contains test files in the SMT1, SMT2, or Yices input language 27# bin-dir contains the Yices binaries for each of these languages 28# 29# For each test file, the expected results are stored in file.gold 30# and command-line options are stored in file.options. 31# 32# This scripts calls the appropriate binary on each test file, passing it 33# the command-line options if any, then check whether the output matches 34# what's expected. 35# 36 37if test $# != 2 ; then 38 echo "Usage: $0 <test-directory> <bin-directory>" 39 exit 40fi 41 42regress_dir=$1 43bin_dir=$2 44 45# Make sure fatal errors go to stderr 46export LIBC_FATAL_STDERR_=1 47 48# 49# System-dependent configuration 50# 51os_name=`uname 2>/dev/null` || os_name=unknown 52 53case "$os_name" in 54 *Darwin* ) 55 mktemp_cmd="/usr/bin/mktemp -t out" 56 ;; 57 58 * ) 59 mktemp_cmd=mktemp 60 ;; 61 62esac 63 64# 65# We try bash's builtin time command 66# 67TIMEFORMAT="%U" 68 69 70# 71# Output colors 72# 73red= 74green= 75black= 76if test -t 1 ; then 77 red=`tput setaf 1` 78 green=`tput setaf 2` 79 black=`tput sgr0` 80fi 81 82# 83# The temp file for output 84# 85outfile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; } 86timefile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; } 87 88fail=0 89pass=0 90 91failed_tests=() 92 93if [[ -z "$REGRESS_FILTER" ]]; 94then 95 REGRESS_FILTER="." 96fi 97 98if [[ -z "$TIME_LIMIT" ]]; 99then 100 TIME_LIMIT=60 101fi 102 103 104# 105# Check if MCSAT is supported 106# 107./$bin_dir/yices_smt2 --mcsat >& /dev/null < /dev/null 108if [ $? -ne 0 ] 109then 110 MCSAT_FILTER="-v mcsat" 111else 112 MCSAT_FILTER="." 113fi 114 115all_tests=$( 116 find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' | 117 grep $REGRESS_FILTER | grep $MCSAT_FILTER | 118 sort 119) 120 121for file in $all_tests; do 122 123 echo -n $file 124 125 # Get the binary based on the filename 126 filename=`basename "$file"` 127 128 case $filename in 129 *.smt2) 130 binary=yices_smt2 131 ;; 132 *.smt) 133 binary=yices_smtcomp 134 ;; 135 *.ys) 136 binary=yices 137 ;; 138 *) 139 echo FAIL: unknown extension for $filename 140 fail=`expr $fail + 1` 141 continue 142 esac 143 144 # Get the options 145 if [ -e "$file.options" ] 146 then 147 options=`cat $file.options` 148 echo " [ $options ]" 149 test_string="$file [ $options ]" 150 else 151 options= 152 test_string="$file" 153 echo 154 fi 155 156 # Get the expected result 157 if [ -e "$file.gold" ] 158 then 159 gold=$file.gold 160 else 161 echo -n $red 162 echo FAIL: missing file: $file.gold 163 echo -n $black 164 fail=`expr $fail + 1` 165 failed_tests+=("$test_string") 166 continue 167 fi 168 169 # Run the binary 170 ( 171 ulimit -S -t $TIME_LIMIT &> /dev/null 172 ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null 173 (time ./$bin_dir/$binary $options ./$file >& $outfile ) >& $timefile 174 ) 175 thetime=`cat $timefile` 176 177 # Do the diff 178 DIFF=`diff -w $outfile $gold` 179 180 if [ $? -eq 0 ] 181 then 182 echo -n $green 183 echo PASS [${thetime} s] 184 echo -n $black 185 pass=`expr $pass + 1` 186 else 187 echo -n $red 188 echo FAIL 189 echo -n $black 190 fail=`expr $fail + 1` 191 failed_tests+=("$test_string"$'\n'"$DIFF") 192 fi 193 194done 195 196rm $outfile 197rm $timefile 198 199if [ $fail -eq 0 ] 200then 201 echo -n $green 202 echo Pass: $pass 203 echo Fail: $fail 204 echo -n $black 205else 206 echo -n $red 207 echo Pass: $pass 208 echo Fail: $fail 209 echo -n $black 210fi 211 212if [ $fail -eq 0 ] 213then 214 exit 0 215else 216 for i in "${!failed_tests[@]}"; do echo "$((i+1)). ${failed_tests[$i]}"; done 217 exit 1 218fi 219 220echo -n $black 221