bench 3.57 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 --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 --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 116

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
117 118
# 1. Syntax
echo "=== Parsing good files  ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
119
goods bench/typing/bad --parse-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
120 121 122 123
echo ""

# 2. Typing
echo "=== Type-checking bad files ==="
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
124
bads bench/typing/bad --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
125 126 127
echo ""

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

131 132
echo "=== Type-checking theories ==="
goods theories --type-only
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
133 134
echo ""

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

153 154 155 156
echo "=== Checking drivers ==="
drivers drivers
echo ""

157 158 159 160
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
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)"
184

185 186 187 188 189 190
for file in bench/valid/*.why; do
    echo I test $file
    for prover in $good_provers; do
        test_prover $prover $file
    done
done