bench 3.68 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3 4
#!/bin/sh

# auto bench for why

MARCHE Claude's avatar
MARCHE Claude committed
5 6
export WHY3LIB=lib
export WHY3DATA=.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7 8

pgm=$1
9
pgml=$2
10
pgml_options=
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38

goods () {
    for f in $1/*.why; do
	echo -n "  "$f"... "
	base=$1/`basename $f .why`
	# running Why
	if ! $pgm $2 $f > /dev/null 2>&1; then
	    echo "why FAILED"
	    $pgm $2 $f
	    exit 1
	fi
	echo "why ok... "
    done
}

bads () {
    for f in $1/*.why; do
	echo -n "  "$f"... "
	if $pgm $2 $f > /dev/null 2>&1; then 
	    echo "$pgm $2 $f"
	    echo "FAILED!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
39 40 41 42
drivers () {
    for f in $1/*.drv; do
	echo -n "  "$f"... "
	# running Why
43
	if ! echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f - > /dev/null 2>&1; then
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
44
	    echo "why FAILED"
45
            echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f -
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
46 47 48 49 50 51
	    exit 1
	fi
	echo "why ok... "
    done
}

52 53 54
programs () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
55 56 57
	if ! $pgml $pgml_options $f > /dev/null 2>&1; then 
	    echo 
	    echo "$pgml $pgml_options $f"
58
	    $pgml $pgml_options $f
59 60 61 62 63 64 65 66
	    echo "FAILED!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

67 68 69 70 71 72 73 74 75 76 77 78 79 80
bad_programs () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	if $pgml $pgml_options $f > /dev/null 2>&1; then 
	    echo 
	    echo "$pgml $pgml_options $f"
	    echo "SHOULD FAIL!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

81 82 83 84 85
valid_goals () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	if $pgml -P alt-ergo $f | grep -q -v Valid; then
	    echo "valid test $f failed!"
86 87
	    echo "$pgml -P alt-ergo $f"
	    $pgml -P alt-ergo $f
88 89 90 91 92 93 94
	    exit 1
       else 
	    echo "ok"
	fi
    done
}

95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115

test_provers () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	if $pgml -P alt-ergo $f | grep -q -v Valid; then
	    echo "valid test $f failed!"
	    exit 1
       else 
	    echo "ok"
	fi
    done
}

test_prover () {
    if $pgm -t 1 -P $1 $2 | grep -q -v Valid; then
	echo "  $1 fails!"
    else
        true
    fi
}

MARCHE Claude's avatar
MARCHE Claude committed
116 117 118 119 120 121 122
echo "=== Checking drivers ==="
drivers drivers
echo ""

echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
123

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
124
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
125
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
126 127 128
echo ""

echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
129
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130 131 132
echo ""

echo "=== Type-checking good files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
133
goods bench/typing/good --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134 135
echo ""

136 137
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
138 139
echo ""

140 141 142
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
143
programs bench/programs/good
144 145 146 147 148 149 150 151 152 153
programs examples/programs
echo ""

echo "=== Type-checking bad programs ==="
pgml_options=--type-only
bad_programs bench/programs/bad-typing
echo ""

echo "=== Type-checking good programs ==="
pgml_options=--type-only
154
programs bench/programs/good
155 156 157
programs examples/programs
echo ""

MARCHE Claude's avatar
MARCHE Claude committed
158 159 160 161
echo "=== VC generation on good programs ==="
pgml_options=
programs bench/programs/good
programs examples/programs
162 163
echo ""

164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
echo "=== Checking provers ==="
echo -n "Test provers on true..."
provers=$($pgm --list-provers | cut -d " " -f 3 |grep -v "^$")
good_provers=""
bad_provers=""
for prover in $(echo $provers); do 
    if bin/why.opt -P $prover bench/true_goal.why | grep -q -v Valid; then
        #echo "$i : Fail"
        bad_provers="$bad_provers $prover"
    else
        #echo "$i : Ok"
        good_provers="$good_provers $prover"
    fi
done
echo "done"
echo ""
echo "On your installation the following provers can't prove \"true\":"
echo "  $bad_provers"
echo ""
echo "So I will only test the following provers:"
echo $good_provers
echo ""
echo "nb : If a prover can't prove a goal it's perhaps normal (ex: TPTP int)"
187

188 189 190 191 192 193
for file in bench/valid/*.why; do
    echo I test $file
    for prover in $good_provers; do
        test_prover $prover $file
    done
done