1#!/usr/bin/env bash 2# 3# Author: Lukas Bulwahn 4# 5# DESCRIPTION: mutant-testing for counterexample generators and automated tools 6 7 8PRG="$(basename "$0")" 9 10function usage() { 11 [ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None" 12 echo 13 echo "Usage: isabelle $PRG [OPTIONS] THEORY" 14 echo 15 echo " Options are:" 16 echo " -L LOGIC parent logic to use (default $MUTABELLE_LOGIC)" 17 echo " -T THEORY parent theory to use (default $MUTABELLE_IMPORT_THEORY)" 18 echo " -O DIR output directory for test data (default $MUTABELLE_OUTPUT_PATH)" 19 echo " -N NUMBER number of lemmas to choose randomly, if not given all lemmas are chosen" 20 echo " -M NUMBER number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)" 21 echo " -X NUMBER number of mutations in a mutant (default $MUTABELLE_NUMBER_OF_MUTATIONS)" 22 echo 23 echo " THEORY is the name of the theory of which all theorems should be" 24 echo " mutated and tested." 25 echo 26 exit 1 27} 28 29 30## process command line 31 32# options 33 34MUTABELLE_IMPORTS="" 35 36while getopts "L:T:O:N:M:X:" OPT 37do 38 case "$OPT" in 39 L) 40 MUTABELLE_LOGIC="$OPTARG" 41 ;; 42 T) 43 MUTABELLE_IMPORTS="$MUTABELLE_IMPORTS \"$OPTARG\"" 44 ;; 45 O) 46 MUTABELLE_OUTPUT_PATH="$OPTARG" 47 ;; 48 N) 49 NUMBER_OF_LEMMAS="$OPTARG" 50 ;; 51 M) 52 MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG" 53 ;; 54 X) 55 MUTABELLE_NUMBER_OF_MUTATIONS="$OPTARG" 56 ;; 57 \?) 58 usage 59 ;; 60 esac 61done 62 63shift $(($OPTIND - 1)) 64 65if [ "$MUTABELLE_IMPORTS" = "" ] 66then 67 MUTABELLE_IMPORTS="$MUTABELLE_IMPORT_THEORY" 68fi 69 70[ "$#" -ne 1 ] && usage 71 72MUTABELLE_TEST_THEORY="$1" 73 74if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then 75 MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$" 76 PURGE_OUTPUT="true" 77fi 78 79export MUTABELLE_OUTPUT_PATH 80 81if [ "$NUMBER_OF_LEMMAS" != "" ]; then 82 MUTABELLE_FILTER="|> MutabelleExtra.take_random $NUMBER_OF_LEMMAS" 83fi 84 85## main 86 87echo "Starting Mutabelle..." 88 89 90# setup 91 92mkdir -p "$MUTABELLE_OUTPUT_PATH" 93 94echo "theory Mutabelle_Test 95imports $MUTABELLE_IMPORTS 96uses 97 \"$MUTABELLE_HOME/mutabelle.ML\" 98 \"$MUTABELLE_HOME/mutabelle_extra.ML\" 99begin 100 101declare [[quickcheck_timeout = 30]] 102 103ML {* 104val mtds = [ 105 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\", 106 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\", 107 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\", 108 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\", 109 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\", 110 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\", 111 MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false 112 #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\" 113(*, MutabelleExtra.refute_mtd, *) 114 , MutabelleExtra.nitpick_mtd 115 116] 117*} 118 119ML {* 120fun mutation_testing_of thy = 121 (MutabelleExtra.random_seed := 1.0; 122 MutabelleExtra.thms_of false thy $MUTABELLE_FILTER 123 |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report 124 @{theory} ($MUTABELLE_NUMBER_OF_MUTATIONS, $MUTABELLE_NUMBER_OF_MUTANTS) mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\"))) 125*} 126 127ML {* 128 mutation_testing_of @{theory $MUTABELLE_TEST_THEORY} 129*} 130 131end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy" 132 133 134# execution 135 136isabelle process -o auto_time_limit=10.0 \ 137 -T "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test" -l "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1 138 139 140[ $? -ne 0 ] && echo "isabelle processing of mutabelle failed" 141 142 143# make statistics 144 145function count() { 146 cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l | sed "s/ //" 147} 148 149function mk_stat() { 150 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" 151} 152 153mk_stat "quickcheck_random" 154mk_stat "quickcheck_random_int" 155mk_stat "quickcheck_exhaustive" 156mk_stat "quickcheck_exhaustive_int" 157mk_stat "quickcheck_narrowing" 158mk_stat "quickcheck_narrowing_int" 159mk_stat "quickcheck_narrowing_nat" 160##mk_stat "refute" 161mk_stat "nitpick" 162 163## cleanup 164 165if [ -n "$PURGE_OUTPUT" ]; then 166 rm -rf "$MUTABELLE_OUTPUT_PATH" 167fi 168