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

# auto bench for why

5
(* Useless in this script ?
MARCHE Claude's avatar
MARCHE Claude committed
6 7
export WHY3LIB=lib
export WHY3DATA=.
8 9
*)
export WHY3LOADPATH=theories
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10 11

pgm=$1
12
pgml=$2
13
pgml_options=
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
14 15 16 17 18 19 20 21

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"
22 23 24
            echo "env: WHY3DATA='$WHY3DATA'"
            echo "invocation: $pgm $2 $f"
            echo "result:"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
	    $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
45 46 47 48
drivers () {
    for f in $1/*.drv; do
	echo -n "  "$f"... "
	# running Why
49
	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
50
	    echo "why FAILED"
51
            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
52 53 54 55 56 57
	    exit 1
	fi
	echo "why ok... "
    done
}

58 59 60
programs () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
61 62 63
	if ! $pgml $pgml_options $f > /dev/null 2>&1; then 
	    echo 
	    echo "$pgml $pgml_options $f"
64
	    $pgml $pgml_options $f
65 66 67 68 69 70 71 72
	    echo "FAILED!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

73 74 75 76 77 78 79 80 81 82 83 84 85 86
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
}

87 88 89 90 91
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!"
92 93
	    echo "$pgml -P alt-ergo $f"
	    $pgml -P alt-ergo $f
94 95 96 97 98 99 100
	    exit 1
       else 
	    echo "ok"
	fi
    done
}

101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121

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
122 123 124 125 126 127 128
echo "=== Checking drivers ==="
drivers drivers
echo ""

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
131
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
132 133 134
echo ""

echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
135
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
136 137 138
echo ""

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

142 143
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
144 145
echo ""

146 147 148
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
149
programs bench/programs/good
150 151 152 153 154 155 156 157 158 159
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
160
programs bench/programs/good
161 162 163
programs examples/programs
echo ""

MARCHE Claude's avatar
MARCHE Claude committed
164 165 166 167
echo "=== VC generation on good programs ==="
pgml_options=
programs bench/programs/good
programs examples/programs
168 169
echo ""

170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
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)"
193

194 195 196 197 198 199
for file in bench/valid/*.why; do
    echo I test $file
    for prover in $good_provers; do
        test_prover $prover $file
    done
done