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