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