1(* Title: HOL/Mutabelle/mutabelle_extra.ML 2 Author: Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen 3 4Invokation of Counterexample generators. 5*) 6 7signature MUTABELLE_EXTRA = 8sig 9 10val take_random : int -> 'a list -> 'a list 11 12datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved 13type timings = (string * int) list 14 15type mtd = string * (theory -> term -> outcome * timings) 16 17type mutant_subentry = term * (string * (outcome * timings)) list 18type detailed_entry = string * bool * term * mutant_subentry list 19 20type subentry = string * int * int * int * int * int * int 21type entry = string * bool * subentry list 22type report = entry list 23 24val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd 25 26val solve_direct_mtd : mtd 27val try0_mtd : mtd 28(* 29val sledgehammer_mtd : mtd 30*) 31val nitpick_mtd : mtd 32 33val refute_mtd : mtd 34 35val freezeT : term -> term 36val thms_of : bool -> theory -> thm list 37 38val string_for_report : report -> string 39val write_report : string -> report -> unit 40val mutate_theorems_and_write_report : 41 theory -> int * int -> mtd list -> thm list -> string -> unit 42 43val init_random : real -> unit 44end; 45 46structure MutabelleExtra : MUTABELLE_EXTRA = 47struct 48 49(* Another Random engine *) 50 51exception RANDOM; 52 53fun rmod x y = x - y * Real.realFloor (x / y); 54 55local 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; 61in 62 63fun init_random r = Synchronized.change random_seed (K r); 64 65fun random () = 66 Synchronized.change_result random_seed 67 (fn s => 68 let val r = rmod (a * s) m 69 in (r, r) end); 70 71end; 72 73fun 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 77fun 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 86datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved 87 88fun 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 97type timings = (string * int) list 98 99type mtd = string * (theory -> term -> outcome * timings) 100 101type mutant_subentry = term * (string * (outcome * timings)) list 102type detailed_entry = string * bool * term * mutant_subentry list 103 104type subentry = string * int * int * int * int * int * int 105type entry = string * bool * subentry list 106type report = entry list 107 108(* possible invocations *) 109 110(** quickcheck **) 111 112fun invoke_quickcheck change_options thy t = 113 Timeout.apply (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 Timeout.TIMEOUT _ => 127 (Timeout, [("timelimit", Real.floor (Options.default_real \<^system_option>\<open>auto_time_limit\<close>))]) 128 129fun quickcheck_mtd change_options quickcheck_generator = 130 ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options) 131 132(** solve direct **) 133 134fun 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 143val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 144 145(** try0 **) 146 147fun 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 156val try0_mtd = ("try0", invoke_try0) 157 158(** sledgehammer **) 159(* 160fun 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 167val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer) 168*) 169 170fun 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 ".")) 187val refute_mtd = ("refute", invoke_refute) 188 189(** nitpick **) 190 191fun 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 208val nitpick_mtd = ("nitpick", invoke_nitpick) 209 210(* filtering forbidden theorems and mutants *) 211 212val comms = [\<^const_name>\<open>HOL.eq\<close>, \<^const_name>\<open>HOL.disj\<close>, \<^const_name>\<open>HOL.conj\<close>] 213 214val 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>\<open>undefined\<close>, "'a"), 220 (\<^const_name>\<open>default\<close>, "'a"), 221 (\<^const_name>\<open>Pure.dummy_pattern\<close>, "'a::{}"), 222 (\<^const_name>\<open>HOL.simp_implies\<close>, "prop => prop => prop"), 223 (\<^const_name>\<open>bot_fun_inst.bot_fun\<close>, "'a"), 224 (\<^const_name>\<open>top_fun_inst.top_fun\<close>, "'a"), 225 (\<^const_name>\<open>Pure.term\<close>, "'a"), 226 (\<^const_name>\<open>top_class.top\<close>, "'a"), 227 (\<^const_name>\<open>Quotient.Quot_True\<close>, "'a")(*, 228 (@{const_name "uminus"}, "'a"), 229 (@{const_name "Nat.size"}, "'a"), 230 (@{const_name "Groups.abs"}, "'a") *)] 231 232val forbidden_thms = 233 ["finite_intvl_succ_class", 234 "nibble"] 235 236val forbidden_consts = [\<^const_name>\<open>Pure.type\<close>] 237 238fun 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 249val forbidden_mutant_constnames = 250[\<^const_name>\<open>HOL.induct_equal\<close>, 251 \<^const_name>\<open>HOL.induct_implies\<close>, 252 \<^const_name>\<open>HOL.induct_conj\<close>, 253 \<^const_name>\<open>HOL.induct_forall\<close>, 254 \<^const_name>\<open>undefined\<close>, 255 \<^const_name>\<open>default\<close>, 256 \<^const_name>\<open>Pure.dummy_pattern\<close>, 257 \<^const_name>\<open>HOL.simp_implies\<close>, 258 \<^const_name>\<open>bot_fun_inst.bot_fun\<close>, 259 \<^const_name>\<open>top_fun_inst.top_fun\<close>, 260 \<^const_name>\<open>Pure.term\<close>, 261 \<^const_name>\<open>top_class.top\<close>, 262 (*@{const_name "HOL.equal"},*) 263 \<^const_name>\<open>Quotient.Quot_True\<close>, 264 \<^const_name>\<open>equal_fun_inst.equal_fun\<close>, 265 \<^const_name>\<open>equal_bool_inst.equal_bool\<close>, 266 \<^const_name>\<open>ord_fun_inst.less_eq_fun\<close>, 267 \<^const_name>\<open>ord_fun_inst.less_fun\<close>, 268 \<^const_name>\<open>Meson.skolem\<close>, 269 \<^const_name>\<open>ATP.fequal\<close>, 270 \<^const_name>\<open>ATP.fEx\<close>, 271 \<^const_name>\<open>enum_prod_inst.enum_all_prod\<close>, 272 \<^const_name>\<open>enum_prod_inst.enum_ex_prod\<close>, 273 \<^const_name>\<open>Quickcheck_Random.catch_match\<close>, 274 \<^const_name>\<open>Quickcheck_Exhaustive.unknown\<close>, 275 \<^const_name>\<open>Num.Bit0\<close>, \<^const_name>\<open>Num.Bit1\<close> 276 (*@{const_name Pure.imp}, @{const_name Pure.eq}*)] 277 278val forbidden_mutant_consts = 279 [ 280 (\<^const_name>\<open>Groups.zero_class.zero\<close>, \<^typ>\<open>prop => prop => prop\<close>), 281 (\<^const_name>\<open>Groups.one_class.one\<close>, \<^typ>\<open>prop => prop => prop\<close>), 282 (\<^const_name>\<open>Groups.plus_class.plus\<close>, \<^typ>\<open>prop => prop => prop\<close>), 283 (\<^const_name>\<open>Groups.minus_class.minus\<close>, \<^typ>\<open>prop => prop => prop\<close>), 284 (\<^const_name>\<open>Groups.times_class.times\<close>, \<^typ>\<open>prop => prop => prop\<close>), 285 (\<^const_name>\<open>Lattices.inf_class.inf\<close>, \<^typ>\<open>prop => prop => prop\<close>), 286 (\<^const_name>\<open>Lattices.sup_class.sup\<close>, \<^typ>\<open>prop => prop => prop\<close>), 287 (\<^const_name>\<open>Orderings.bot_class.bot\<close>, \<^typ>\<open>prop => prop => prop\<close>), 288 (\<^const_name>\<open>Orderings.ord_class.min\<close>, \<^typ>\<open>prop => prop => prop\<close>), 289 (\<^const_name>\<open>Orderings.ord_class.max\<close>, \<^typ>\<open>prop => prop => prop\<close>), 290 (\<^const_name>\<open>Rings.modulo\<close>, \<^typ>\<open>prop => prop => prop\<close>), 291 (\<^const_name>\<open>Rings.divide\<close>, \<^typ>\<open>prop => prop => prop\<close>), 292 (\<^const_name>\<open>GCD.gcd_class.gcd\<close>, \<^typ>\<open>prop => prop => prop\<close>), 293 (\<^const_name>\<open>GCD.gcd_class.lcm\<close>, \<^typ>\<open>prop => prop => prop\<close>), 294 (\<^const_name>\<open>Orderings.bot_class.bot\<close>, \<^typ>\<open>bool => prop\<close>), 295 (\<^const_name>\<open>Groups.one_class.one\<close>, \<^typ>\<open>bool => prop\<close>), 296 (\<^const_name>\<open>Groups.zero_class.zero\<close>,\<^typ>\<open>bool => prop\<close>), 297 (\<^const_name>\<open>equal_class.equal\<close>,\<^typ>\<open>bool => bool => bool\<close>)] 298 299fun is_forbidden_mutant t = 300 let 301 val const_names = Term.add_const_names t [] 302 val consts = Term.add_consts t [] 303 in 304 exists (String.isPrefix "Nitpick") const_names orelse 305 exists (String.isSubstring "_sumC") const_names orelse 306 exists (member (op =) forbidden_mutant_constnames) const_names orelse 307 exists (member (op =) forbidden_mutant_consts) consts 308 end 309 310(* executable via quickcheck *) 311 312fun is_executable_term thy t = 313 let 314 val ctxt = Proof_Context.init_global thy 315 in 316 can (Timeout.apply (seconds 30.0) 317 (Quickcheck.test_terms 318 ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #> 319 Config.put Quickcheck.finite_types true #> 320 Config.put Quickcheck.finite_type_size 1 #> 321 Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt) 322 (false, false) [])) (map (rpair [] o Object_Logic.atomize_term ctxt) 323 (fst (Variable.import_terms true [t] ctxt))) 324 end 325 326fun is_executable_thm thy th = is_executable_term thy (Thm.prop_of th) 327 328val freezeT = 329 map_types (map_type_tvar (fn ((a, i), S) => 330 TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S))) 331 332fun thms_of all thy = 333 filter 334 (fn th => (all orelse Thm.theory_name th = Context.theory_name thy) 335 (* andalso is_executable_thm thy th *)) 336 (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false))) 337 338fun elapsed_time description e = 339 let val ({elapsed, ...}, result) = Timing.timing e () 340 in (result, (description, Time.toMilliseconds elapsed)) end 341(* 342fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t = 343 let 344 val _ = writeln ("Invoking " ^ mtd_name) 345 val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t 346 handle ERROR s => (tracing s; (Error, ([], NONE)))) 347 val _ = writeln (" Done") 348 in (res, (time :: timing, reports)) end 349*) 350fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t = 351 let 352 val _ = writeln ("Invoking " ^ mtd_name) 353 val (res, timing) = elapsed_time "total time" 354 (fn () => case try (invoke_mtd thy) t of 355 SOME (res, _) => res 356 | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t); 357 Error)) 358 val _ = writeln (" Done") 359 in (res, [timing]) end 360 361(* creating entries *) 362 363fun create_detailed_entry thy thm exec mutants mtds = 364 let 365 fun create_mutant_subentry mutant = (mutant, 366 map (fn (mtd_name, invoke_mtd) => 367 (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds) 368 in 369 (Thm.get_name_hint thm, exec, Thm.prop_of thm, map create_mutant_subentry mutants) 370 end 371 372(* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *) 373fun mutate_theorem create_entry thy (num_mutations, max_mutants) mtds thm = 374 let 375 val exec = is_executable_thm thy thm 376 val _ = tracing (if exec then "EXEC" else "NOEXEC") 377 val mutants = 378 (if num_mutations = 0 then 379 [Thm.prop_of thm] 380 else 381 Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden 382 num_mutations) 383 |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts))) 384 |> filter_out is_forbidden_mutant 385 val mutants = 386 if exec then 387 let 388 val _ = writeln ("BEFORE PARTITION OF " ^ 389 string_of_int (length mutants) ^ " MUTANTS") 390 val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants) 391 val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^ 392 " vs " ^ string_of_int (length noexecs) ^ ")") 393 in 394 execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs 395 end 396 else 397 mutants 398 val mutants = mutants 399 |> map Mutabelle.freeze |> map freezeT 400(* |> filter (not o is_forbidden_mutant) *) 401 |> map_filter (try (Sign.cert_term thy)) 402 |> filter (is_some o try (Thm.global_cterm_of thy)) 403 |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy))) 404 |> take_random max_mutants 405 val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants 406 in 407 create_entry thy thm exec mutants mtds 408 end 409 410fun string_of_mutant_subentry' thy thm_name (t, results) = 411 let 412 (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e, 413 satisfied_assms = s, positive_concl_tests = p}) = 414 "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p 415 fun string_of_reports NONE = "" 416 | string_of_reports (SOME reports) = 417 cat_lines (map (fn (size, [report]) => 418 "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*) 419 fun string_of_mtd_result (mtd_name, (outcome, timing)) = 420 mtd_name ^ ": " ^ string_of_outcome outcome 421 ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")" 422 (*^ "\n" ^ string_of_reports reports*) 423 in 424 "mutant of " ^ thm_name ^ ":\n" ^ 425 YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^ 426 space_implode "; " (map string_of_mtd_result results) 427 end 428 429fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 430 thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^ 431 Syntax.string_of_term_global thy t ^ "\n" ^ 432 cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n" 433 434(* subentry -> string *) 435fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno, 436 timeout, error) = 437 " " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^ 438 string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^ 439 string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^ 440 string_of_int error ^ "!" 441 442(* entry -> string *) 443fun string_for_entry (thm_name, exec, subentries) = 444 thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^ 445 cat_lines (map string_for_subentry subentries) ^ "\n" 446 447(* report -> string *) 448fun string_for_report report = cat_lines (map string_for_entry report) 449 450(* string -> report -> unit *) 451fun write_report file_name = 452 File.write (Path.explode file_name) o string_for_report 453 454(* theory -> mtd list -> thm list -> string -> unit *) 455fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name = 456 let 457 val _ = writeln "Starting Mutabelle..." 458 val ctxt = Proof_Context.init_global thy 459 val path = Path.explode file_name 460 (* for normal report: *) 461 (* 462 val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry) 463 *) 464 (* for detailled report: *) 465 val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy) 466 (* for theory creation: *) 467 (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*) 468 in 469 File.write path ( 470 "Mutation options = " ^ 471 "max_mutants: " ^ string_of_int max_mutants ^ 472 "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^ 473 "QC options = " ^ 474 (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*) 475 "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^ 476 "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^ 477 "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n"); 478 map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy (num_mutations, max_mutants) mtds) thms; 479 () 480 end 481 482end; 483