author  bulwahn 
Wed, 08 Dec 2010 14:25:07 +0100  
changeset 41077  fd6f41d349ef 
parent 41021  3efa0ec42ed4 
child 41191  4aa6465fec65 
permissions  rwxrxrx 
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: mutanttesting 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:" 
41077  15 
echo " L LOGIC parent logic to use (default $DEFAULT_MUTABELLE_LOGIC)" 
16 
echo " T THEORY parent theory to use (default $DEFAULT_MUTABELLE_IMPORT_THEORY)" 

17 
echo " O DIR output directory for test data (default $DEFAULT_MUTABELLE_OUTPUT_PATH)" 

40975
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" 
41077  20 
echo 
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

21 
exit 1 
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 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

25 
## process command line 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

26 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

27 
# options 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

28 

41077  29 
MUTABELLE_LOGIC="$DEFAULT_MUTABELLE_LOGIC" 
30 
MUTABELLE_OUTPUT_PATH="$DEFAULT_MUTABELLE_OUTPUT_PATH" 

31 

32 
MUTABELLE_IMPORT_THEORY="" 

33 

34 
while getopts "L:T:O:" OPT 

40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

35 
do 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

36 
case "$OPT" in 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

37 
L) 
41021  38 
MUTABELLE_LOGIC="$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 
T) 
41077  41 
MUTABELLE_IMPORT_THEORY="$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

42 
;; 
41077  43 
O) 
41021  44 
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

45 
;; 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

46 
\?) 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

47 
usage 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

48 
;; 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

49 
esac 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

50 
done 
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 
shift $(($OPTIND  1)) 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

53 

41077  54 
if [ "$MUTABELLE_IMPORT_THEORY" = "" ] 
55 
then 

56 
MUTABELLE_IMPORT_THEORY="$DEFAULT_MUTABELLE_IMPORT_THEORY" 

57 
fi 

58 

40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

59 
[ "$#" ne 1 ] && usage 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

60 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

61 
MUTABELLE_TEST_THEORY="$1" 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

62 

41077  63 
export MUTABELLE_OUTPUT_PATH 
64 

40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

65 
## main 
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 
echo "Starting Mutabelle..." 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

68 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

69 
# setup 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

70 

41077  71 
mkdir p "$MUTABELLE_OUTPUT_PATH" 
40975
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 
echo "theory Mutabelle_Test 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

74 
imports $MUTABELLE_IMPORT_THEORY 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

75 
uses 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

76 
\"$MUTABELLE_HOME/mutabelle.ML\" 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

77 
\"$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

78 
begin 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

79 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

80 
ML {* 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

81 
val mtds = [ 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

82 
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

83 
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

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 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

87 
ML {* 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

88 
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

89 
(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

90 
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

91 
> (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

92 
@{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

93 
*} 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

94 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

95 
ML {* 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

96 
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

97 
*} 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

98 

41077  99 
end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy" 
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

100 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

101 
# execution 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

102 

41077  103 
"$ISABELLE_PROCESS" e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' q $MUTABELLE_LOGIC > /dev/null 2>&1 
104 

105 

106 
[ $? ne 0 ] && echo "isabelle processing of mutabelle failed" 

40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

107 

498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

108 
# make statistics 
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

109 

41077  110 
function count() { 
111 
cat "$MUTABELLE_OUTPUT_PATH/log"  grep "quickcheck_$1: $2"  wc l 

112 
} 

40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

113 

41077  114 
echo "random : C: $(count "random" "GenuineCex") N: $(count "random" "NoCex") \ 
115 
T: $(count "random" "Timeout") E: $(count "random" "Error")" 

116 
echo "exhaustive : C: $(count "exhaustive" "GenuineCex") N: $(count "exhaustive" "NoCex") \ 

117 
T: $(count "exhaustive" "Timeout") E: $(count "exhaustive" "Error")" 

40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

118 