src/HOL/Mutabelle/mutabelle_extra.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35537 59dd6be5834c
child 36255 f8b3381e1437
permissions -rw-r--r--
modernized structure Object_Logic;
     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 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 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 "uminus"}, "'a"),
   202   (@{const_name "Nat.size"}, "'a"),
   203   (@{const_name "Groups.abs"}, "'a") *)]
   204 
   205 val forbidden_thms =
   206  ["finite_intvl_succ_class",
   207   "nibble"]
   208 
   209 val forbidden_consts =
   210  [@{const_name nibble_pair_of_char}]
   211 
   212 fun is_forbidden_theorem (s, th) =
   213   let val consts = Term.add_const_names (prop_of th) [] in
   214     exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
   215     exists (fn s' => s' mem forbidden_consts) consts orelse
   216     length (space_explode "." s) <> 2 orelse
   217     String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
   218     String.isSuffix "_def" s orelse
   219     String.isSuffix "_raw" s
   220   end
   221 
   222 fun is_forbidden_mutant t =
   223   let val consts = Term.add_const_names t [] in
   224     exists (String.isPrefix "Nitpick") consts orelse
   225     exists (String.isSubstring "_sumC") consts (* internal function *)
   226   end
   227 
   228 fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
   229  (ProofContext.init thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
   230 fun is_executable_thm thy th = is_executable_term thy (prop_of th)
   231 
   232 val freezeT =
   233   map_types (map_type_tvar (fn ((a, i), S) =>
   234     TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
   235 
   236 fun thms_of all thy =
   237   filter
   238     (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
   239       (* andalso is_executable_thm thy th *))
   240     (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
   241 
   242 val count = length oo filter o equal
   243 
   244 fun take_random 0 _ = []
   245   | take_random _ [] = []
   246   | take_random n xs =
   247     let val j = random_range 0 (length xs - 1) in
   248       Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
   249     end
   250 
   251 fun cpu_time description f =
   252   let
   253     val start = start_timing ()
   254     val result = Exn.capture f ()
   255     val time = Time.toMilliseconds (#cpu (end_timing start))
   256   in (Exn.release result, (description, time)) end
   257 
   258 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   259   let
   260     val _ = priority ("Invoking " ^ mtd_name)
   261     val ((res, (timing, reports)), time) = cpu_time "total time"
   262       (fn () => case try (invoke_mtd thy) t of
   263           SOME (res, (timing, reports)) => (res, (timing, reports))
   264         | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
   265            (Error , ([], NONE))))
   266     val _ = priority (" Done")
   267   in (res, (time :: timing, reports)) end
   268 
   269 (* theory -> term list -> mtd -> subentry *)
   270 (*
   271 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
   272   let
   273      val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
   274   in
   275     (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
   276      count Donno res, count Timeout res, count Error res)
   277   end
   278 
   279 fun create_entry thy thm exec mutants mtds =
   280   (Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
   281 *)
   282 fun create_detailed_entry thy thm exec mutants mtds =
   283   let
   284     fun create_mutant_subentry mutant = (mutant,
   285       map (fn (mtd_name, invoke_mtd) =>
   286         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
   287   in
   288     (Thm.get_name thm, exec, prop_of thm, map create_mutant_subentry mutants)
   289   end
   290 
   291 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
   292 fun mutate_theorem create_entry thy mtds thm =
   293   let
   294     val pp = Syntax.pp_global thy
   295     val exec = is_executable_thm thy thm
   296     val _ = priority (if exec then "EXEC" else "NOEXEC")
   297     val mutants =
   298           (if num_mutations = 0 then
   299              [Thm.prop_of thm]
   300            else
   301              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
   302                                   num_mutations)
   303              |> filter_out is_forbidden_mutant
   304     val mutants =
   305       if exec then
   306         let
   307           val _ = priority ("BEFORE PARTITION OF " ^
   308                             Int.toString (length mutants) ^ " MUTANTS")
   309           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
   310           val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^
   311                            " vs " ^ Int.toString (length noexecs) ^ ")")
   312         in
   313           execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
   314         end
   315       else
   316         mutants
   317     val mutants = mutants
   318           |> take_random max_mutants
   319           |> map Mutabelle.freeze |> map freezeT
   320 (*          |> filter (not o is_forbidden_mutant) *)
   321           |> List.mapPartial (try (Sign.cert_term thy))
   322     val _ = map (fn t => priority ("MUTANT: " ^ Pretty.string_of (Pretty.term pp t))) mutants
   323   in
   324     create_entry thy thm exec mutants mtds
   325   end
   326 
   327 (* theory -> mtd list -> thm list -> report *)
   328 val mutate_theorems = map ooo mutate_theorem
   329 
   330 fun string_of_outcome GenuineCex = "GenuineCex"
   331   | string_of_outcome PotentialCex = "PotentialCex"
   332   | string_of_outcome NoCex = "NoCex"
   333   | string_of_outcome Donno = "Donno"
   334   | string_of_outcome Timeout = "Timeout"
   335   | string_of_outcome Error = "Error"
   336 
   337 fun string_of_mutant_subentry thy thm_name (t, results) =
   338   "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
   339   space_implode "; "
   340     (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
   341   "\n"
   342 
   343 fun string_of_mutant_subentry' thy thm_name (t, results) =
   344   let
   345     fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
   346       satisfied_assms = s, positive_concl_tests = p}) =
   347       "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
   348     fun string_of_reports NONE = ""
   349       | string_of_reports (SOME reports) =
   350         cat_lines (map (fn (size, [report]) =>
   351           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
   352     fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
   353       mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
   354       space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
   355       ^ "\n" ^ string_of_reports reports
   356   in
   357     "mutant of " ^ thm_name ^ ":\n" ^ cat_lines (map string_of_mtd_result results)
   358   end
   359 
   360 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
   361    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
   362    Syntax.string_of_term_global thy t ^ "\n" ^
   363    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
   364 
   365 (* subentry -> string *)
   366 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
   367                          timeout, error) =
   368   "    " ^ mtd_name ^ ": " ^ Int.toString genuine_cex ^ "+ " ^
   369   Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
   370   Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
   371   Int.toString error ^ "!"
   372 (* entry -> string *)
   373 fun string_for_entry (thm_name, exec, subentries) =
   374   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
   375   cat_lines (map string_for_subentry subentries) ^ "\n"
   376 (* report -> string *)
   377 fun string_for_report report = cat_lines (map string_for_entry report)
   378 
   379 (* string -> report -> unit *)
   380 fun write_report file_name =
   381   File.write (Path.explode file_name) o string_for_report
   382 
   383 (* theory -> mtd list -> thm list -> string -> unit *)
   384 fun mutate_theorems_and_write_report thy mtds thms file_name =
   385   let
   386     val _ = priority "Starting Mutabelle..."
   387     val path = Path.explode file_name
   388     (* for normal report: *)
   389     (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
   390     (*for detailled report: *)
   391     val (gen_create_entry, gen_string_for_entry) =
   392       (create_detailed_entry, string_of_detailed_entry thy)
   393   in
   394     File.write path (
   395     "Mutation options = "  ^
   396       "max_mutants: " ^ string_of_int max_mutants ^
   397       "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
   398     "QC options = " ^
   399       (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
   400       "size: " ^ string_of_int size ^
   401       "; iterations: " ^ string_of_int iterations ^ "\n");
   402     map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
   403     ()
   404   end
   405 
   406 end;