author  bulwahn 
Thu, 16 Dec 2010 11:31:07 +0100  
changeset 41191  4aa6465fec65 
parent 41077  fd6f41d349ef 
child 41309  2e9bf718a7a1 
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\", 
41191  83 
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\", 
84 
MutabelleExtra.nitpick_mtd 

40975
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 

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

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

89 
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

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

91 
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

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

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

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

95 

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

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

97 
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

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

99 

41077  100 
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

101 

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

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

103 

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

106 

107 
[ $? 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

108 

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

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

110 

41077  111 
function count() { 
41191  112 
cat "$MUTABELLE_OUTPUT_PATH/log"  grep "$1: $2"  wc l 
41077  113 
} 
40975
498f272b4bcb
adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff
changeset

114 

41191  115 
echo "random : C: $(count "quickcheck_random" "GenuineCex") N: $(count "quickcheck_random" "NoCex") \ 
116 
T: $(count "quickcheck_random" "Timeout") E: $(count "quickcheck_random" "Error")" 

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

118 
T: $(count "quickcheck_exhaustive" "Timeout") E: $(count "quickcheck_exhaustive" "Error")" 

119 
echo "nitpick : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \ 

120 
T: $(count "nitpick" "Timeout") E: $(count "nitpick" "Error")" 

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

121 