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