#!/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 ML_process -o auto_time_limit=10.0 \
-e "Thy_Info.use_thy_legacy \"$MUTABELLE_OUTPUT_PATH/Mutabelle_Test\"" -l "$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
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
