author | bulwahn |
Mon, 06 Dec 2010 17:33:25 +0100 | |
changeset 41021 | 3efa0ec42ed4 |
parent 40975 | 498f272b4bcb |
child 41077 | fd6f41d349ef |
permissions | -rwxr-xr-x |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
2 |
# |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
3 |
# Author: Lukas Bulwahn |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
4 |
# |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
5 |
# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
6 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
7 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
8 |
PRG="$(basename "$0")" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
9 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
10 |
function usage() { |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
11 |
echo |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
12 |
echo "Usage: isabelle $PRG [OPTIONS] THEORY" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
13 |
echo |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
14 |
echo " Options are:" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
15 |
echo " -L LOGIC parent logic to use (default $MUTABELLE_LOGIC)" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
16 |
echo " -T THEORY parent theory to use (default $MUTABELLE_IMPORT_THEORY)" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
17 |
echo " -O DIR output directory for test data (default $MUTABELLE_OUTPUT_PATH)" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
18 |
echo |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
19 |
echo " THEORY is the name of the theory of which all theorems should be mutated and tested" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
20 |
exit 1 |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
21 |
} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
22 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
23 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
24 |
## process command line |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
25 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
26 |
# options |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
27 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
28 |
while getopts "L:T:O:t:q?" OPT |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
29 |
do |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
30 |
case "$OPT" in |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
31 |
L) |
41021 | 32 |
MUTABELLE_LOGIC="$OPTARG" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
33 |
;; |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
34 |
T) |
41021 | 35 |
MUTABELLE_IMPORT_THEORY="$OPTARG" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
36 |
;; |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
37 |
O) |
41021 | 38 |
MUTABELLE_OUTPUT_PATH="$OPTARG" |
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
39 |
;; |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
40 |
\?) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
41 |
usage |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
42 |
;; |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
43 |
esac |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
44 |
done |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
45 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
46 |
shift $(($OPTIND - 1)) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
47 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
48 |
[ "$#" -ne 1 ] && usage |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
49 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
50 |
MUTABELLE_TEST_THEORY="$1" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
51 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
52 |
## main |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
53 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
54 |
echo "Starting Mutabelle..." |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
55 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
56 |
# setup |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
57 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
58 |
mkdir -p "$MIRABELLE_OUTPUT_PATH" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
59 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
60 |
echo "theory Mutabelle_Test |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
61 |
imports $MUTABELLE_IMPORT_THEORY |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
62 |
uses |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
63 |
\"$MUTABELLE_HOME/mutabelle.ML\" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
64 |
\"$MUTABELLE_HOME/mutabelle_extra.ML\" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
65 |
begin |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
66 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
67 |
ML {* |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
68 |
val mtds = [ |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
69 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\", |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
70 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\" |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
71 |
] |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
72 |
*} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
73 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
74 |
ML {* |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
75 |
fun mutation_testing_of thy = |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
76 |
(MutabelleExtra.random_seed := 1.0; |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
77 |
MutabelleExtra.thms_of false thy |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
78 |
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
79 |
@{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\"))) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
80 |
*} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
81 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
82 |
ML {* |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
83 |
mutation_testing_of @{theory $MUTABELLE_TEST_THEORY} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
84 |
*} |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
85 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
86 |
end" > $MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
87 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
88 |
# execution |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
89 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
90 |
$ISABELLE_PROCESS -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q $MUTABELLE_LOGIC > /dev/null 2>&1 |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
91 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
92 |
# make statistics |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
93 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
94 |
GenuineCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: GenuineCex" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
95 |
NoCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: NoCex" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
96 |
Timeout_random=$(cat /$MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Timeout" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
97 |
Errors_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Error" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
98 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
99 |
GenuineCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: GenuineCex" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
100 |
NoCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: NoCex" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
101 |
Timeout_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Timeout" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
102 |
Errors_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Error" | wc -l) |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
103 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
104 |
|
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
105 |
echo "random :" C: $GenuineCex_random N: $NoCex_random T: $Timeout_random E: $Errors_random |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
106 |
echo "exhaustive :" C: $GenuineCex_exh N: $NoCex_exh T: $Timeout_exh E: $Errors_exh |
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset
|
107 |