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

# auto bench for why

export WHYLIB=../lib

pgm=$1
8
pgml=$2
9
pgml_options=
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10 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

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

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

65 66 67 68 69 70 71 72 73 74 75 76 77 78
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
}

79 80 81 82 83 84 85 86 87 88 89 90
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!"
	    exit 1
       else 
	    echo "ok"
	fi
    done
}

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112

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
}


Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113 114
# 1. Syntax
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
115
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116 117 118 119
echo ""

# 2. Typing
echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
120
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121 122 123
echo ""

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

127 128
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
129 130
echo ""

131 132 133
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
134
programs bench/programs/good
135 136 137 138 139 140 141 142 143 144
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
145
programs bench/programs/good
146 147 148
programs examples/programs
echo ""

149 150 151 152
echo "=== Checking drivers ==="
drivers drivers
echo ""

153 154 155 156
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
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)"
180

181 182 183 184 185 186
for file in bench/valid/*.why; do
    echo I test $file
    for prover in $good_provers; do
        test_prover $prover $file
    done
done