src/HOL/Mutabelle/lib/Tools/mutabelle

isabelle_process is superseded by "isabelle process" tool;
tuned tool usage;
misc updates and tuning of "system" manual;

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


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

function usage() {
  [ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None"
  echo
  echo "Usage: isabelle $PRG [OPTIONS] THEORY"
  echo
  echo "  Options are:"
  echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
  echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
  echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
  echo "    -N NUMBER    number of lemmas to choose randomly, if not given all lemmas are chosen"
  echo "    -M NUMBER    number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)"
  echo "    -X NUMBER    number of mutations in a mutant  (default $MUTABELLE_NUMBER_OF_MUTATIONS)"
  echo
  echo "  THEORY is the name of the theory of which all theorems should be"
  echo "  mutated and tested."
  echo
  exit 1
}


## process command line

# options

MUTABELLE_IMPORTS=""

while getopts "L:T:O:N:M:X:" OPT
do
  case "$OPT" in
    L)
      MUTABELLE_LOGIC="$OPTARG"
      ;;
    T)
      MUTABELLE_IMPORTS="$MUTABELLE_IMPORTS \"$OPTARG\""
      ;;
    O)      
      MUTABELLE_OUTPUT_PATH="$OPTARG"
      ;;
    N)
      NUMBER_OF_LEMMAS="$OPTARG"
      ;;
    M)
      MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG"
      ;;
    X)
      MUTABELLE_NUMBER_OF_MUTATIONS="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))

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

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

MUTABELLE_TEST_THEORY="$1"

if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then
  MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$"
  PURGE_OUTPUT="true"
fi

export MUTABELLE_OUTPUT_PATH

if [ "$NUMBER_OF_LEMMAS" != "" ]; then
  MUTABELLE_FILTER="|> MutabelleExtra.take_random $NUMBER_OF_LEMMAS"
fi

## main

echo "Starting Mutabelle..."


# setup

mkdir -p "$MUTABELLE_OUTPUT_PATH"

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

declare [[quickcheck_timeout = 30]]

ML {*
val mtds = [
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
    #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
(*, MutabelleExtra.refute_mtd, *)
  , MutabelleExtra.nitpick_mtd

]
*}

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

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

end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy"


# execution

"$ISABELLE_TOOL" process -o auto_time_limit=10.0 \
  -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1


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


# make statistics

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

function mk_stat() {
  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"
}

mk_stat "quickcheck_random"
mk_stat "quickcheck_random_int"
mk_stat "quickcheck_exhaustive"
mk_stat "quickcheck_exhaustive_int"
mk_stat "quickcheck_narrowing"
mk_stat "quickcheck_narrowing_int"
mk_stat "quickcheck_narrowing_nat"
##mk_stat "refute"
mk_stat "nitpick"

## cleanup

if [ -n "$PURGE_OUTPUT" ]; then
  rm -rf "$MUTABELLE_OUTPUT_PATH"
fi