1#!/usr/bin/env bash
2#
3# Author: Lukas Bulwahn
4#
5# DESCRIPTION: mutant-testing for counterexample generators and automated tools
6
7
8PRG="$(basename "$0")"
9
10function usage() {
11  [ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None"
12  echo
13  echo "Usage: isabelle $PRG [OPTIONS] THEORY"
14  echo
15  echo "  Options are:"
16  echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
17  echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
18  echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
19  echo "    -N NUMBER    number of lemmas to choose randomly, if not given all lemmas are chosen"
20  echo "    -M NUMBER    number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)"
21  echo "    -X NUMBER    number of mutations in a mutant  (default $MUTABELLE_NUMBER_OF_MUTATIONS)"
22  echo
23  echo "  THEORY is the name of the theory of which all theorems should be"
24  echo "  mutated and tested."
25  echo
26  exit 1
27}
28
29
30## process command line
31
32# options
33
34MUTABELLE_IMPORTS=""
35
36while getopts "L:T:O:N:M:X:" OPT
37do
38  case "$OPT" in
39    L)
40      MUTABELLE_LOGIC="$OPTARG"
41      ;;
42    T)
43      MUTABELLE_IMPORTS="$MUTABELLE_IMPORTS \"$OPTARG\""
44      ;;
45    O)      
46      MUTABELLE_OUTPUT_PATH="$OPTARG"
47      ;;
48    N)
49      NUMBER_OF_LEMMAS="$OPTARG"
50      ;;
51    M)
52      MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG"
53      ;;
54    X)
55      MUTABELLE_NUMBER_OF_MUTATIONS="$OPTARG"
56      ;;
57    \?)
58      usage
59      ;;
60  esac
61done
62
63shift $(($OPTIND - 1))
64
65if [ "$MUTABELLE_IMPORTS" = "" ]
66then
67  MUTABELLE_IMPORTS="$MUTABELLE_IMPORT_THEORY"
68fi
69
70[ "$#" -ne 1 ] && usage
71
72MUTABELLE_TEST_THEORY="$1"
73
74if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then
75  MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$"
76  PURGE_OUTPUT="true"
77fi
78
79export MUTABELLE_OUTPUT_PATH
80
81if [ "$NUMBER_OF_LEMMAS" != "" ]; then
82  MUTABELLE_FILTER="|> MutabelleExtra.take_random $NUMBER_OF_LEMMAS"
83fi
84
85## main
86
87echo "Starting Mutabelle..."
88
89
90# setup
91
92mkdir -p "$MUTABELLE_OUTPUT_PATH"
93
94echo "theory Mutabelle_Test
95imports $MUTABELLE_IMPORTS
96uses     
97  \"$MUTABELLE_HOME/mutabelle.ML\"
98  \"$MUTABELLE_HOME/mutabelle_extra.ML\"
99begin
100
101declare [[quickcheck_timeout = 30]]
102
103ML {*
104val mtds = [
105  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
106  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\",
107  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
108  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\",
109  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
110  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\",
111  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
112    #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
113(*, MutabelleExtra.refute_mtd, *)
114  , MutabelleExtra.nitpick_mtd
115
116]
117*}
118
119ML {*
120fun mutation_testing_of thy =
121  (MutabelleExtra.random_seed := 1.0;
122  MutabelleExtra.thms_of false thy $MUTABELLE_FILTER 
123  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
124         @{theory} ($MUTABELLE_NUMBER_OF_MUTATIONS, $MUTABELLE_NUMBER_OF_MUTANTS) mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
125*}
126
127ML {*
128  mutation_testing_of @{theory $MUTABELLE_TEST_THEORY}
129*}
130
131end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy"
132
133
134# execution
135
136isabelle process -o auto_time_limit=10.0 \
137  -T "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test" -l "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
138
139
140[ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
141
142
143# make statistics
144
145function count() {
146  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l | sed "s/     //"
147}
148
149function mk_stat() {
150  printf "%-40s C:$(count $1 "GenuineCex")  P:$(count $1 "PotentialCex")  N:$(count $1 "NoCex")  T:$(count $1 "Timeout")  D:$(count $1 "Donno")  E: $(count $1 "Error")\n" "$1"
151}
152
153mk_stat "quickcheck_random"
154mk_stat "quickcheck_random_int"
155mk_stat "quickcheck_exhaustive"
156mk_stat "quickcheck_exhaustive_int"
157mk_stat "quickcheck_narrowing"
158mk_stat "quickcheck_narrowing_int"
159mk_stat "quickcheck_narrowing_nat"
160##mk_stat "refute"
161mk_stat "nitpick"
162
163## cleanup
164
165if [ -n "$PURGE_OUTPUT" ]; then
166  rm -rf "$MUTABELLE_OUTPUT_PATH"
167fi
168