src/HOL/Mutabelle/lib/Tools/mutabelle
author wenzelm
Mon, 20 Dec 2010 15:24:25 +0100
changeset 41309 2e9bf718a7a1
parent 41191 4aa6465fec65
child 41949 f9a2e10c49cb
permissions -rwxr-xr-x
some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
#
41309
2e9bf718a7a1 some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
wenzelm
parents: 41191
diff changeset
     5
# DESCRIPTION: mutant-testing for counterexample generators and automated tools
40975
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
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    15
  echo "    -L LOGIC     parent logic to use (default $DEFAULT_MUTABELLE_LOGIC)"
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    16
  echo "    -T THEORY    parent theory to use (default $DEFAULT_MUTABELLE_IMPORT_THEORY)"
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    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
41309
2e9bf718a7a1 some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
wenzelm
parents: 41191
diff changeset
    19
  echo "  THEORY is the name of the theory of which all theorems should be"
2e9bf718a7a1 some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
wenzelm
parents: 41191
diff changeset
    20
  echo "  mutated and tested."
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    21
  echo
40975
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    22
  exit 1
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
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    26
## process command line
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
# options
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    29
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    30
MUTABELLE_LOGIC="$DEFAULT_MUTABELLE_LOGIC"
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    31
MUTABELLE_OUTPUT_PATH="$DEFAULT_MUTABELLE_OUTPUT_PATH"
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    32
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    33
MUTABELLE_IMPORT_THEORY=""
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    34
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    35
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
    36
do
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    37
  case "$OPT" in
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    38
    L)
41021
3efa0ec42ed4 adapting copied bash code in mutabelle script
bulwahn
parents: 40975
diff changeset
    39
      MUTABELLE_LOGIC="$OPTARG"
40975
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
    T)
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    42
      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
    43
      ;;
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    44
    O)      
41021
3efa0ec42ed4 adapting copied bash code in mutabelle script
bulwahn
parents: 40975
diff changeset
    45
      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
    46
      ;;
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
      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
  esac
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    51
done
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    52
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    53
shift $(($OPTIND - 1))
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    54
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    55
if [ "$MUTABELLE_IMPORT_THEORY" = "" ]
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    56
then
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    57
  MUTABELLE_IMPORT_THEORY="$DEFAULT_MUTABELLE_IMPORT_THEORY"
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    58
fi
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    59
40975
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    60
[ "$#" -ne 1 ] && usage
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    61
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    62
MUTABELLE_TEST_THEORY="$1"
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    63
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    64
export MUTABELLE_OUTPUT_PATH
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    65
40975
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    66
## main
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    67
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    68
echo "Starting Mutabelle..."
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    69
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    70
# setup
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    71
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
    72
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
    73
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    74
echo "theory Mutabelle_Test
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    75
imports $MUTABELLE_IMPORT_THEORY
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    76
uses     
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    77
  \"$MUTABELLE_HOME/mutabelle.ML\"
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    78
  \"$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
    79
begin
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
ML {*
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    82
val mtds = [
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 \"random\") \"random\",
41191
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
    84
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\",
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
    85
  MutabelleExtra.nitpick_mtd
40975
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
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    89
ML {*
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    90
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
    91
  (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
    92
  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
    93
  |> (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
    94
         @{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
    95
*}
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    96
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    97
ML {*
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
    98
  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
    99
*}
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
   100
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
   101
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
   102
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
   103
# execution
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
   104
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
   105
"$ISABELLE_PROCESS" -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q $MUTABELLE_LOGIC > /dev/null 2>&1
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
   106
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
   107
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
   108
[ $? -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
   109
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
   110
# make statistics
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
   111
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
   112
function count() {
41191
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
   113
  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l
41077
fd6f41d349ef improving the mutabelle script
bulwahn
parents: 41021
diff changeset
   114
}
40975
498f272b4bcb adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn
parents:
diff changeset
   115
41191
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
   116
echo "random      : C: $(count "quickcheck_random" "GenuineCex") N: $(count "quickcheck_random" "NoCex") \
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
   117
T: $(count "quickcheck_random" "Timeout") E: $(count "quickcheck_random" "Error")"
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
   118
echo "exhaustive  : C: $(count "quickcheck_exhaustive" "GenuineCex") N: $(count "quickcheck_exhaustive" "NoCex") \
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
   119
T: $(count "quickcheck_exhaustive" "Timeout") E: $(count "quickcheck_exhaustive" "Error")"
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
   120
echo "nitpick     : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \
4aa6465fec65 added nitpick to mutabelle script
bulwahn
parents: 41077
diff changeset
   121
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
   122