src/HOL/Mutabelle/mutabelle_extra.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05)
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36743 ce2297415b54
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
     1 (*
     2     Title:      HOL/Mutabelle/mutabelle_extra.ML
     3     Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
     4 
     5     Invokation of Counterexample generators
     6 *)
     7 signature MUTABELLE_EXTRA =
     8 sig
     9 
    10 val take_random : int -> 'a list -> 'a list
    11 
    12 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
    13 type timing = (string * int) list
    14 
    15 type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
    16 
    17 type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
    18 type detailed_entry = string * bool * term * mutant_subentry list
    19 
    20 type subentry = string * int * int * int * int * int * int
    21 type entry = string * bool * subentry list
    22 type report = entry list
    23 
    24 val quickcheck_mtd : string -> mtd
    25 (*
    26 val refute_mtd : mtd
    27 val nitpick_mtd : mtd
    28 *)
    29 
    30 val freezeT : term -> term
    31 val thms_of : bool -> theory -> thm list
    32 
    33 val string_for_report : report -> string
    34 val write_report : string -> report -> unit
    35 val mutate_theorems_and_write_report :
    36   theory -> mtd list -> thm list -> string -> unit
    37 
    38 val random_seed : real Unsynchronized.ref
    39 end;
    40 
    41 structure MutabelleExtra : MUTABELLE_EXTRA =
    42 struct
    43 
    44 (* Own seed; can't rely on the Isabelle one to stay the same *)
    45 val random_seed = Unsynchronized.ref 1.0;
    46 
    47 
    48 (* mutation options *)
    49 val max_mutants = 4
    50 val num_mutations = 1
    51 (* soundness check: *)
    52 (*val max_mutants = 1
    53 val num_mutations = 0*)
    54 
    55 (* quickcheck options *)
    56 (*val quickcheck_generator = "SML"*)
    57 val iterations = 10
    58 val size = 5
    59 
    60 exception RANDOM;
    61 
    62 fun rmod x y = x - y * Real.realFloor (x / y);
    63 
    64 local
    65   val a = 16807.0;
    66   val m = 2147483647.0;
    67 in
    68 
    69 fun random () = CRITICAL (fn () =>
    70   let val r = rmod (a * ! random_seed) m
    71   in (random_seed := r; r) end);
    72 
    73 end;
    74 
    75 fun random_range l h =
    76   if h < l orelse l < 0 then raise RANDOM
    77   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    78 
    79 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
    80 type timing = (string * int) list
    81 
    82 type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
    83 
    84 type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
    85 type detailed_entry = string * bool * term * mutant_subentry list
    86 
    87 type subentry = string * int * int * int * int * int * int
    88 type entry = string * bool * subentry list
    89 type report = entry list
    90 
    91 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
    92   | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
    93 
    94 fun preprocess thy insts t = Object_Logic.atomize_term thy
    95  (map_types (inst_type insts) (Mutabelle.freeze t));
    96 
    97 fun invoke_quickcheck quickcheck_generator thy t =
    98   TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
    99       (fn _ =>
   100           case Quickcheck.gen_test_term (ProofContext.init_global thy) true true (SOME quickcheck_generator)
   101                                     size iterations (preprocess thy [] t) of
   102             (NONE, (time_report, report)) => (NoCex, (time_report, report))
   103           | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
   104   handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Counterexample.time_limit)], NONE))
   105 
   106 fun quickcheck_mtd quickcheck_generator =
   107   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
   108 
   109   (*
   110 fun invoke_refute thy t =
   111   let
   112     val res = MyRefute.refute_term thy [] t
   113     val _ = priority ("Refute: " ^ res)
   114   in
   115     case res of
   116       "genuine" => GenuineCex
   117     | "likely_genuine" => GenuineCex
   118     | "potential" => PotentialCex
   119     | "none" => NoCex
   120     | "unknown" => Donno
   121     | _ => Error
   122   end
   123   handle MyRefute.REFUTE (loc, details) =>
   124          (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
   125                    "."))
   126 val refute_mtd = ("refute", invoke_refute)
   127 *)
   128 
   129 (*
   130 open Nitpick_Util
   131 open Nitpick_Rep
   132 open Nitpick_Nut
   133 
   134 fun invoke_nitpick thy t =
   135   let
   136     val ctxt = ProofContext.init_global thy
   137     val state = Proof.init ctxt
   138   in
   139     let
   140       val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Isar.default_params thy []) false [] t
   141       val _ = priority ("Nitpick: " ^ res)
   142     in
   143       case res of
   144         "genuine" => GenuineCex
   145       | "likely_genuine" => GenuineCex
   146       | "potential" => PotentialCex
   147       | "none" => NoCex
   148       | "unknown" => Donno
   149       | _ => Error
   150     end
   151     handle ARG (loc, details) =>
   152            (error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ "."))
   153          | BAD (loc, details) =>
   154            (error ("Internal error (" ^ quote loc ^ "): " ^ details ^ "."))
   155          | LIMIT (_, details) =>
   156            (warning ("Limit reached: " ^ details ^ "."); Donno)
   157          | NOT_SUPPORTED details =>
   158            (warning ("Unsupported case: " ^ details ^ "."); Donno)
   159          | NUT (loc, us) =>
   160            (error ("Invalid nut" ^ plural_s_for_list us ^
   161                    " (" ^ quote loc ^ "): " ^
   162                   commas (map (string_for_nut ctxt) us) ^ "."))
   163          | REP (loc, Rs) =>
   164            (error ("Invalid representation" ^ plural_s_for_list Rs ^
   165                    " (" ^ quote loc ^ "): " ^
   166                    commas (map string_for_rep Rs) ^ "."))
   167          | TERM (loc, ts) =>
   168            (error ("Invalid term" ^ plural_s_for_list ts ^
   169                    " (" ^ quote loc ^ "): " ^
   170                    commas (map (Syntax.string_of_term ctxt) ts) ^ "."))
   171          | TYPE (loc, Ts, ts) =>
   172            (error ("Invalid type" ^ plural_s_for_list Ts ^
   173                    (if null ts then
   174                       ""
   175                     else
   176                       " for term" ^ plural_s_for_list ts ^ " " ^
   177                       commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
   178                    " (" ^ quote loc ^ "): " ^
   179                    commas (map (Syntax.string_of_typ ctxt) Ts) ^ "."))
   180          | Kodkod.SYNTAX (_, details) =>
   181            (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); Error)
   182          | Refute.REFUTE (loc, details) =>
   183            (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
   184                    "."))
   185          | Exn.Interrupt => raise Exn.Interrupt
   186          | _ => (priority ("Unknown error in Nitpick"); Error)
   187   end
   188 val nitpick_mtd = ("nitpick", invoke_nitpick)
   189 *)
   190 
   191 val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]
   192 
   193 val forbidden =
   194  [(* (@{const_name "power"}, "'a"), *)
   195   (*(@{const_name induct_equal}, "'a"),
   196   (@{const_name induct_implies}, "'a"),
   197   (@{const_name induct_conj}, "'a"),*)
   198   (@{const_name "undefined"}, "'a"),
   199   (@{const_name "default"}, "'a"),
   200   (@{const_name "dummy_pattern"}, "'a::{}"),
   201   (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
   202   (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
   203   (@{const_name "top_fun_inst.top_fun"}, "'a"),
   204   (@{const_name "Pure.term"}, "'a"),
   205   (@{const_name "top_class.top"}, "'a"),
   206   (@{const_name "eq_class.eq"}, "'a"),
   207   (@{const_name "Quotient.Quot_True"}, "'a")(*,
   208   (@{const_name "uminus"}, "'a"),
   209   (@{const_name "Nat.size"}, "'a"),
   210   (@{const_name "Groups.abs"}, "'a") *)]
   211 
   212 val forbidden_thms =
   213  ["finite_intvl_succ_class",
   214   "nibble"]
   215 
   216 val forbidden_consts =
   217  [@{const_name nibble_pair_of_char}]
   218 
   219 fun is_forbidden_theorem (s, th) =
   220   let val consts = Term.add_const_names (prop_of th) [] in
   221     exists (member (op =) (space_explode "." s)) forbidden_thms orelse
   222     exists (member (op =) forbidden_consts) consts orelse
   223     length (space_explode "." s) <> 2 orelse
   224     String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
   225     String.isSuffix "_def" s orelse
   226     String.isSuffix "_raw" s
   227   end
   228 
   229 val forbidden_mutant_constnames =
   230  ["HOL.induct_equal",
   231   "HOL.induct_implies",
   232   "HOL.induct_conj",
   233  @{const_name undefined},
   234  @{const_name default},
   235  @{const_name dummy_pattern},
   236  @{const_name "HOL.simp_implies"},
   237  @{const_name "bot_fun_inst.bot_fun"},
   238  @{const_name "top_fun_inst.top_fun"},
   239  @{const_name "Pure.term"},
   240  @{const_name "top_class.top"},
   241  @{const_name "eq_class.eq"},
   242  @{const_name "Quotient.Quot_True"}]
   243 
   244 fun is_forbidden_mutant t =
   245   let
   246     val consts = Term.add_const_names t []
   247   in
   248     exists (String.isPrefix "Nitpick") consts orelse
   249     exists (String.isSubstring "_sumC") consts orelse
   250     exists (member (op =) forbidden_mutant_constnames) consts
   251   end
   252 
   253 fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
   254  (ProofContext.init_global thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
   255 fun is_executable_thm thy th = is_executable_term thy (prop_of th)
   256 
   257 val freezeT =
   258   map_types (map_type_tvar (fn ((a, i), S) =>
   259     TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
   260 
   261 fun thms_of all thy =
   262   filter
   263     (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
   264       (* andalso is_executable_thm thy th *))
   265     (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
   266 
   267 val count = length oo filter o equal
   268 
   269 fun take_random 0 _ = []
   270   | take_random _ [] = []
   271   | take_random n xs =
   272     let val j = random_range 0 (length xs - 1) in
   273       Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
   274     end
   275 
   276 fun cpu_time description f =
   277   let
   278     val start = start_timing ()
   279     val result = Exn.capture f ()
   280     val time = Time.toMilliseconds (#cpu (end_timing start))
   281   in (Exn.release result, (description, time)) end
   282 
   283 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   284   let
   285     val _ = priority ("Invoking " ^ mtd_name)
   286     val ((res, (timing, reports)), time) = cpu_time "total time"
   287       (fn () => case try (invoke_mtd thy) t of
   288           SOME (res, (timing, reports)) => (res, (timing, reports))
   289         | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
   290            (Error , ([], NONE))))
   291     val _ = priority (" Done")
   292   in (res, (time :: timing, reports)) end
   293 
   294 (* theory -> term list -> mtd -> subentry *)
   295 (*
   296 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
   297   let
   298      val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
   299   in
   300     (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
   301      count Donno res, count Timeout res, count Error res)
   302   end
   303 
   304 fun create_entry thy thm exec mutants mtds =
   305   (Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
   306 *)
   307 fun create_detailed_entry thy thm exec mutants mtds =
   308   let
   309     fun create_mutant_subentry mutant = (mutant,
   310       map (fn (mtd_name, invoke_mtd) =>
   311         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
   312   in
   313     (Thm.get_name thm, exec, prop_of thm, map create_mutant_subentry mutants)
   314   end
   315 
   316 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
   317 fun mutate_theorem create_entry thy mtds thm =
   318   let
   319     val pp = Syntax.pp_global thy
   320     val exec = is_executable_thm thy thm
   321     val _ = priority (if exec then "EXEC" else "NOEXEC")
   322     val mutants =
   323           (if num_mutations = 0 then
   324              [Thm.prop_of thm]
   325            else
   326              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
   327                                   num_mutations)
   328              |> filter_out is_forbidden_mutant
   329     val mutants =
   330       if exec then
   331         let
   332           val _ = priority ("BEFORE PARTITION OF " ^
   333                             Int.toString (length mutants) ^ " MUTANTS")
   334           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
   335           val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^
   336                            " vs " ^ Int.toString (length noexecs) ^ ")")
   337         in
   338           execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
   339         end
   340       else
   341         mutants
   342     val mutants = mutants
   343           |> take_random max_mutants
   344           |> map Mutabelle.freeze |> map freezeT
   345 (*          |> filter (not o is_forbidden_mutant) *)
   346           |> List.mapPartial (try (Sign.cert_term thy))
   347     val _ = map (fn t => priority ("MUTANT: " ^ Pretty.string_of (Pretty.term pp t))) mutants
   348   in
   349     create_entry thy thm exec mutants mtds
   350   end
   351 
   352 (* theory -> mtd list -> thm list -> report *)
   353 val mutate_theorems = map ooo mutate_theorem
   354 
   355 fun string_of_outcome GenuineCex = "GenuineCex"
   356   | string_of_outcome PotentialCex = "PotentialCex"
   357   | string_of_outcome NoCex = "NoCex"
   358   | string_of_outcome Donno = "Donno"
   359   | string_of_outcome Timeout = "Timeout"
   360   | string_of_outcome Error = "Error"
   361 
   362 fun string_of_mutant_subentry thy thm_name (t, results) =
   363   "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
   364   space_implode "; "
   365     (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
   366   "\n"
   367 
   368 (* XML.tree -> string *)
   369 fun plain_string_from_xml_tree t =
   370   Buffer.empty |> XML.add_content t |> Buffer.content
   371 (* string -> string *)
   372 val unyxml = plain_string_from_xml_tree o YXML.parse
   373 
   374 fun string_of_mutant_subentry' thy thm_name (t, results) =
   375   let
   376     fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
   377       satisfied_assms = s, positive_concl_tests = p}) =
   378       "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
   379     fun string_of_reports NONE = ""
   380       | string_of_reports (SOME reports) =
   381         cat_lines (map (fn (size, [report]) =>
   382           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
   383     fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
   384       mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
   385       space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
   386       (*^ "\n" ^ string_of_reports reports*)
   387   in
   388     "mutant of " ^ thm_name ^ ":\n"
   389     ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ cat_lines (map string_of_mtd_result results)
   390   end
   391 
   392 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
   393    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
   394    Syntax.string_of_term_global thy t ^ "\n" ^                                    
   395    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
   396 
   397 fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
   398   "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
   399   "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
   400   "\" \nquickcheck[generator = SML]\nquickcheck[generator = predicate_compile_wo_ff]\n" ^
   401   "quickcheck[generator = predicate_compile_ff_nofs]\noops\n"
   402 
   403 fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
   404   "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
   405   cat_lines (map_index
   406     (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
   407 
   408 (* subentry -> string *)
   409 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
   410                          timeout, error) =
   411   "    " ^ mtd_name ^ ": " ^ Int.toString genuine_cex ^ "+ " ^
   412   Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
   413   Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
   414   Int.toString error ^ "!"
   415 (* entry -> string *)
   416 fun string_for_entry (thm_name, exec, subentries) =
   417   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
   418   cat_lines (map string_for_subentry subentries) ^ "\n"
   419 (* report -> string *)
   420 fun string_for_report report = cat_lines (map string_for_entry report)
   421 
   422 (* string -> report -> unit *)
   423 fun write_report file_name =
   424   File.write (Path.explode file_name) o string_for_report
   425 
   426 (* theory -> mtd list -> thm list -> string -> unit *)
   427 fun mutate_theorems_and_write_report thy mtds thms file_name =
   428   let
   429     val _ = priority "Starting Mutabelle..."
   430     val path = Path.explode file_name
   431     (* for normal report: *)
   432     (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
   433     (*for detailled report: *)
   434     val (gen_create_entry, gen_string_for_entry) =
   435       (create_detailed_entry, string_of_detailed_entry thy)
   436     val (gen_create_entry, gen_string_for_entry) =
   437       (create_detailed_entry, theoryfile_string_of_detailed_entry thy)
   438   in
   439     File.write path (
   440     "Mutation options = "  ^
   441       "max_mutants: " ^ string_of_int max_mutants ^
   442       "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
   443     "QC options = " ^
   444       (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
   445       "size: " ^ string_of_int size ^
   446       "; iterations: " ^ string_of_int iterations ^ "\n");
   447     map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
   448     ()
   449   end
   450 
   451 end;