src/HOL/Mutabelle/lib/Tools/mutabelle

improving the mutabelle script

#!/usr/bin/env bash
#
# Author: Lukas Bulwahn
#
# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools


PRG="$(basename "$0")"

function usage() {
  echo
  echo "Usage: isabelle $PRG [OPTIONS] THEORY"
  echo
  echo "  Options are:"
  echo "    -L LOGIC     parent logic to use (default $DEFAULT_MUTABELLE_LOGIC)"
  echo "    -T THEORY    parent theory to use (default $DEFAULT_MUTABELLE_IMPORT_THEORY)"
  echo "    -O DIR       output directory for test data (default $DEFAULT_MUTABELLE_OUTPUT_PATH)"
  echo
  echo "  THEORY is the name of the theory of which all theorems should be mutated and tested"
  echo
  exit 1
}


## process command line

# options

MUTABELLE_LOGIC="$DEFAULT_MUTABELLE_LOGIC"
MUTABELLE_OUTPUT_PATH="$DEFAULT_MUTABELLE_OUTPUT_PATH"

MUTABELLE_IMPORT_THEORY=""

while getopts "L:T:O:" OPT
do
  case "$OPT" in
    L)
      MUTABELLE_LOGIC="$OPTARG"
      ;;
    T)
      MUTABELLE_IMPORT_THEORY="$MUTABELLE_IMPORT_THEORY \"$OPTARG\""
      ;;
    O)      
      MUTABELLE_OUTPUT_PATH="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))

if [ "$MUTABELLE_IMPORT_THEORY" = "" ]
then
  MUTABELLE_IMPORT_THEORY="$DEFAULT_MUTABELLE_IMPORT_THEORY"
fi

[ "$#" -ne 1 ] && usage

MUTABELLE_TEST_THEORY="$1"

export MUTABELLE_OUTPUT_PATH

## main

echo "Starting Mutabelle..."

# setup

mkdir -p "$MUTABELLE_OUTPUT_PATH"

echo "theory Mutabelle_Test
imports $MUTABELLE_IMPORT_THEORY
uses     
  \"$MUTABELLE_HOME/mutabelle.ML\"
  \"$MUTABELLE_HOME/mutabelle_extra.ML\"
begin

ML {*
val mtds = [
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\"
]
*}

ML {*
fun mutation_testing_of thy =
  (MutabelleExtra.random_seed := 1.0;
  MutabelleExtra.thms_of false thy
  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
         @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
*}

ML {*
  mutation_testing_of @{theory $MUTABELLE_TEST_THEORY}
*}

end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy"

# execution

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


[ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"

# make statistics

function count() {
  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "quickcheck_$1: $2" | wc -l
}

echo "random      : C: $(count "random" "GenuineCex") N: $(count "random" "NoCex") \
T: $(count "random" "Timeout") E: $(count "random" "Error")"
echo "exhaustive  : C: $(count "exhaustive" "GenuineCex") N: $(count "exhaustive" "NoCex") \
T: $(count "exhaustive" "Timeout") E: $(count "exhaustive" "Error")"