src/HOL/Mutabelle/mutabelle_extra.ML
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 60638 16d80e5ef2dc
child 62519 a564458f94db
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Mutabelle/mutabelle_extra.ML
     2     Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
     3 
     4 Invokation of Counterexample generators.
     5 *)
     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 | Solved | Unsolved
    13 type timings = (string * int) list
    14 
    15 type mtd = string * (theory -> term -> outcome * timings)
    16 
    17 type mutant_subentry = term * (string * (outcome * timings)) 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 : (Proof.context -> Proof.context) -> string -> mtd
    25 
    26 val solve_direct_mtd : mtd
    27 val try0_mtd : mtd
    28 (*
    29 val sledgehammer_mtd : mtd
    30 *)
    31 val nitpick_mtd : mtd
    32 
    33 val refute_mtd : mtd
    34 
    35 val freezeT : term -> term
    36 val thms_of : bool -> theory -> thm list
    37 
    38 val string_for_report : report -> string
    39 val write_report : string -> report -> unit
    40 val mutate_theorems_and_write_report :
    41   theory -> int * int -> mtd list -> thm list -> string -> unit
    42 
    43 val init_random : real -> unit
    44 end;
    45 
    46 structure MutabelleExtra : MUTABELLE_EXTRA =
    47 struct
    48 
    49 (* Another Random engine *)
    50 
    51 exception RANDOM;
    52 
    53 fun rmod x y = x - y * Real.realFloor (x / y);
    54 
    55 local
    56   (* Own seed; can't rely on the Isabelle one to stay the same *)
    57   val random_seed = Synchronized.var "random_seed" 1.0;
    58 
    59   val a = 16807.0;
    60   val m = 2147483647.0;
    61 in
    62 
    63 fun init_random r = Synchronized.change random_seed (K r);
    64 
    65 fun random () =
    66   Synchronized.change_result random_seed
    67     (fn s =>
    68       let val r = rmod (a * s) m
    69       in (r, r) end);
    70 
    71 end;
    72 
    73 fun random_range l h =
    74   if h < l orelse l < 0 then raise RANDOM
    75   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    76 
    77 fun take_random 0 _ = []
    78   | take_random _ [] = []
    79   | take_random n xs =
    80     let val j = random_range 0 (length xs - 1) in
    81       Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
    82     end
    83   
    84 (* possible outcomes *)
    85 
    86 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
    87 
    88 fun string_of_outcome GenuineCex = "GenuineCex"
    89   | string_of_outcome PotentialCex = "PotentialCex"
    90   | string_of_outcome NoCex = "NoCex"
    91   | string_of_outcome Donno = "Donno"
    92   | string_of_outcome Timeout = "Timeout"
    93   | string_of_outcome Error = "Error"
    94   | string_of_outcome Solved = "Solved"
    95   | string_of_outcome Unsolved = "Unsolved"
    96 
    97 type timings = (string * int) list
    98 
    99 type mtd = string * (theory -> term -> outcome * timings)
   100 
   101 type mutant_subentry = term * (string * (outcome * timings)) list
   102 type detailed_entry = string * bool * term * mutant_subentry list
   103 
   104 type subentry = string * int * int * int * int * int * int
   105 type entry = string * bool * subentry list
   106 type report = entry list
   107 
   108 (* possible invocations *)
   109 
   110 (** quickcheck **)
   111 
   112 fun invoke_quickcheck change_options thy t =
   113   TimeLimit.timeLimit (seconds 30.0)
   114       (fn _ =>
   115           let
   116             val ctxt' = change_options (Proof_Context.init_global thy)
   117             val (result :: _) = case Quickcheck.active_testers ctxt' of
   118               [] => error "No active testers for quickcheck"
   119             | [tester] => tester ctxt' false [] [(t, [])]
   120             | _ => error "Multiple active testers for quickcheck"
   121           in
   122             case Quickcheck.counterexample_of result of 
   123               NONE => (NoCex, Quickcheck.timings_of result)
   124             | SOME _ => (GenuineCex, Quickcheck.timings_of result)
   125           end) ()
   126   handle TimeLimit.TimeOut =>
   127          (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
   128 
   129 fun quickcheck_mtd change_options quickcheck_generator =
   130   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
   131 
   132 (** solve direct **)
   133  
   134 fun invoke_solve_direct thy t =
   135   let
   136     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) 
   137   in
   138     case Solve_Direct.solve_direct state of
   139       (true, _) => (Solved, [])
   140     | (false, _) => (Unsolved, [])
   141   end
   142 
   143 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
   144 
   145 (** try0 **)
   146 
   147 fun invoke_try0 thy t =
   148   let
   149     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
   150   in
   151     case Try0.try0 (SOME (seconds 5.0)) ([], [], [], []) state of
   152       true => (Solved, [])
   153     | false => (Unsolved, [])
   154   end
   155 
   156 val try0_mtd = ("try0", invoke_try0)
   157 
   158 (** sledgehammer **)
   159 (*
   160 fun invoke_sledgehammer thy t =
   161   if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
   162       (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
   163     (Solved, ([], NONE))
   164   else
   165     (Unsolved, ([], NONE))
   166 
   167 val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
   168 *)
   169 
   170 fun invoke_refute thy t =
   171   let
   172     val params = []
   173     val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
   174     val _ = writeln ("Refute: " ^ res)
   175   in
   176     (rpair []) (case res of
   177       "genuine" => GenuineCex
   178     | "likely_genuine" => GenuineCex
   179     | "potential" => PotentialCex
   180     | "none" => NoCex
   181     | "unknown" => Donno
   182     | _ => Error)
   183   end
   184   handle Refute.REFUTE (loc, details) =>
   185          (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
   186                    "."))
   187 val refute_mtd = ("refute", invoke_refute)
   188 
   189 (** nitpick **)
   190 
   191 fun invoke_nitpick thy t =
   192   let
   193     val ctxt = Proof_Context.init_global thy
   194     val state = Proof.init ctxt
   195     val (res, _) = Nitpick.pick_nits_in_term state
   196       (Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
   197     val _ = writeln ("Nitpick: " ^ res)
   198   in
   199     (rpair []) (case res of
   200       "genuine" => GenuineCex
   201     | "likely_genuine" => GenuineCex
   202     | "potential" => PotentialCex
   203     | "none" => NoCex
   204     | "unknown" => Donno
   205     | _ => Error)
   206   end
   207 
   208 val nitpick_mtd = ("nitpick", invoke_nitpick)
   209 
   210 (* filtering forbidden theorems and mutants *)
   211 
   212 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
   213 
   214 val forbidden =
   215  [(* (@{const_name "power"}, "'a"), *)
   216   (*(@{const_name induct_equal}, "'a"),
   217   (@{const_name induct_implies}, "'a"),
   218   (@{const_name induct_conj}, "'a"),*)
   219   (@{const_name "undefined"}, "'a"),
   220   (@{const_name "default"}, "'a"),
   221   (@{const_name "Pure.dummy_pattern"}, "'a::{}"),
   222   (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
   223   (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
   224   (@{const_name "top_fun_inst.top_fun"}, "'a"),
   225   (@{const_name "Pure.term"}, "'a"),
   226   (@{const_name "top_class.top"}, "'a"),
   227   (@{const_name "Quotient.Quot_True"}, "'a")(*,
   228   (@{const_name "uminus"}, "'a"),
   229   (@{const_name "Nat.size"}, "'a"),
   230   (@{const_name "Groups.abs"}, "'a") *)]
   231 
   232 val forbidden_thms =
   233  ["finite_intvl_succ_class",
   234   "nibble"]
   235 
   236 val forbidden_consts = [@{const_name Pure.type}]
   237 
   238 fun is_forbidden_theorem (s, th) =
   239   let val consts = Term.add_const_names (Thm.prop_of th) [] in
   240     exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
   241     exists (member (op =) forbidden_consts) consts orelse
   242     length (Long_Name.explode s) <> 2 orelse
   243     String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
   244     String.isSuffix "_def" s orelse
   245     String.isSuffix "_raw" s orelse
   246     String.isPrefix "term_of" (List.last (Long_Name.explode s))
   247   end
   248 
   249 val forbidden_mutant_constnames =
   250 [@{const_name HOL.induct_equal},
   251  @{const_name HOL.induct_implies},
   252  @{const_name HOL.induct_conj},
   253  @{const_name HOL.induct_forall},
   254  @{const_name undefined},
   255  @{const_name default},
   256  @{const_name Pure.dummy_pattern},
   257  @{const_name "HOL.simp_implies"},
   258  @{const_name "bot_fun_inst.bot_fun"},
   259  @{const_name "top_fun_inst.top_fun"},
   260  @{const_name "Pure.term"},
   261  @{const_name "top_class.top"},
   262  (*@{const_name "HOL.equal"},*)
   263  @{const_name "Quotient.Quot_True"},
   264  @{const_name "equal_fun_inst.equal_fun"},
   265  @{const_name "equal_bool_inst.equal_bool"},
   266  @{const_name "ord_fun_inst.less_eq_fun"},
   267  @{const_name "ord_fun_inst.less_fun"},
   268  @{const_name Meson.skolem},
   269  @{const_name ATP.fequal},
   270  @{const_name ATP.fEx},
   271  @{const_name transfer_morphism},
   272  @{const_name enum_prod_inst.enum_all_prod},
   273  @{const_name enum_prod_inst.enum_ex_prod},
   274  @{const_name Quickcheck_Random.catch_match},
   275  @{const_name Quickcheck_Exhaustive.unknown},
   276  @{const_name Num.Bit0}, @{const_name Num.Bit1}
   277  (*@{const_name Pure.imp}, @{const_name Pure.eq}*)]
   278 
   279 val forbidden_mutant_consts =
   280   [
   281    (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
   282    (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
   283    (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
   284    (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
   285    (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
   286       (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
   287    (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
   288    (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
   289    (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
   290    (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
   291    (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
   292    (@{const_name Rings.divide}, @{typ "prop => prop => prop"}),
   293    (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
   294    (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
   295    (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
   296    (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
   297    (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"}),
   298    (@{const_name "equal_class.equal"},@{typ "bool => bool => bool"})]
   299 
   300 fun is_forbidden_mutant t =
   301   let
   302     val const_names = Term.add_const_names t []
   303     val consts = Term.add_consts t []
   304   in
   305     exists (String.isPrefix "Nitpick") const_names orelse
   306     exists (String.isSubstring "_sumC") const_names orelse
   307     exists (member (op =) forbidden_mutant_constnames) const_names orelse
   308     exists (member (op =) forbidden_mutant_consts) consts
   309   end
   310 
   311 (* executable via quickcheck *)
   312 
   313 fun is_executable_term thy t =
   314   let
   315     val ctxt = Proof_Context.init_global thy
   316   in
   317     can (TimeLimit.timeLimit (seconds 30.0)
   318       (Quickcheck.test_terms
   319         ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
   320           Config.put Quickcheck.finite_types true #>
   321           Config.put Quickcheck.finite_type_size 1 #>
   322           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
   323         (false, false) [])) (map (rpair [] o Object_Logic.atomize_term ctxt)
   324         (fst (Variable.import_terms true [t] ctxt)))
   325   end
   326 
   327 fun is_executable_thm thy th = is_executable_term thy (Thm.prop_of th)
   328 
   329 val freezeT =
   330   map_types (map_type_tvar (fn ((a, i), S) =>
   331     TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
   332 
   333 fun thms_of all thy =
   334   filter
   335     (fn th => (all orelse Thm.theory_name_of_thm th = Context.theory_name thy)
   336       (* andalso is_executable_thm thy th *))
   337     (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
   338 
   339 fun elapsed_time description e =
   340   let val ({elapsed, ...}, result) = Timing.timing e ()
   341   in (result, (description, Time.toMilliseconds elapsed)) end
   342 (*
   343 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   344   let
   345     val _ = writeln ("Invoking " ^ mtd_name)
   346     val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
   347       handle ERROR s => (tracing s; (Error, ([], NONE))))
   348     val _ = writeln (" Done")
   349   in (res, (time :: timing, reports)) end
   350 *)  
   351 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   352   let
   353     val _ = writeln ("Invoking " ^ mtd_name)
   354     val (res, timing) = elapsed_time "total time"
   355       (fn () => case try (invoke_mtd thy) t of
   356           SOME (res, _) => res
   357         | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
   358             Error))
   359     val _ = writeln (" Done")
   360   in (res, [timing]) end
   361 
   362 (* creating entries *)
   363 
   364 fun create_detailed_entry thy thm exec mutants mtds =
   365   let
   366     fun create_mutant_subentry mutant = (mutant,
   367       map (fn (mtd_name, invoke_mtd) =>
   368         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
   369   in
   370     (Thm.get_name_hint thm, exec, Thm.prop_of thm, map create_mutant_subentry mutants)
   371   end
   372 
   373 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
   374 fun mutate_theorem create_entry thy (num_mutations, max_mutants) mtds thm =
   375   let
   376     val exec = is_executable_thm thy thm
   377     val _ = tracing (if exec then "EXEC" else "NOEXEC")
   378     val mutants =
   379           (if num_mutations = 0 then
   380              [Thm.prop_of thm]
   381            else
   382              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
   383                                   num_mutations)
   384              |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
   385              |> filter_out is_forbidden_mutant
   386     val mutants =
   387       if exec then
   388         let
   389           val _ = writeln ("BEFORE PARTITION OF " ^
   390                             string_of_int (length mutants) ^ " MUTANTS")
   391           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
   392           val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
   393                            " vs " ^ string_of_int (length noexecs) ^ ")")
   394         in
   395           execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
   396         end
   397       else
   398         mutants
   399     val mutants = mutants
   400           |> map Mutabelle.freeze |> map freezeT
   401 (*          |> filter (not o is_forbidden_mutant) *)
   402           |> map_filter (try (Sign.cert_term thy))
   403           |> filter (is_some o try (Thm.global_cterm_of thy))
   404           |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
   405           |> take_random max_mutants
   406     val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   407   in
   408     create_entry thy thm exec mutants mtds
   409   end
   410 
   411 fun string_of_mutant_subentry' thy thm_name (t, results) =
   412   let
   413    (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
   414       satisfied_assms = s, positive_concl_tests = p}) =
   415       "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
   416     fun string_of_reports NONE = ""
   417       | string_of_reports (SOME reports) =
   418         cat_lines (map (fn (size, [report]) =>
   419           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
   420     fun string_of_mtd_result (mtd_name, (outcome, timing)) =
   421       mtd_name ^ ": " ^ string_of_outcome outcome
   422       ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
   423       (*^ "\n" ^ string_of_reports reports*)
   424   in
   425     "mutant of " ^ thm_name ^ ":\n" ^
   426       YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
   427       space_implode "; " (map string_of_mtd_result results)
   428   end
   429 
   430 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
   431    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
   432    Syntax.string_of_term_global thy t ^ "\n" ^                                    
   433    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
   434 
   435 (* subentry -> string *)
   436 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
   437                          timeout, error) =
   438   "    " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^
   439   string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^
   440   string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^
   441   string_of_int error ^ "!"
   442 
   443 (* entry -> string *)
   444 fun string_for_entry (thm_name, exec, subentries) =
   445   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
   446   cat_lines (map string_for_subentry subentries) ^ "\n"
   447 
   448 (* report -> string *)
   449 fun string_for_report report = cat_lines (map string_for_entry report)
   450 
   451 (* string -> report -> unit *)
   452 fun write_report file_name =
   453   File.write (Path.explode file_name) o string_for_report
   454 
   455 (* theory -> mtd list -> thm list -> string -> unit *)
   456 fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
   457   let
   458     val _ = writeln "Starting Mutabelle..."
   459     val ctxt = Proof_Context.init_global thy
   460     val path = Path.explode file_name
   461     (* for normal report: *)
   462     (*
   463     val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
   464     *)
   465     (* for detailled report: *)
   466     val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
   467     (* for theory creation: *)
   468     (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
   469   in
   470     File.write path (
   471     "Mutation options = "  ^
   472       "max_mutants: " ^ string_of_int max_mutants ^
   473       "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
   474     "QC options = " ^
   475       (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
   476       "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
   477       "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^
   478     "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n");
   479     map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy (num_mutations, max_mutants) mtds) thms;
   480     ()
   481   end
   482 
   483 end;