1structure core_decompilerLib :> core_decompilerLib = 2struct 3 4open HolKernel Parse boolLib bossLib 5open helperLib tripleTheory tripleSyntax 6 7val ERR = Feedback.mk_HOL_ERR "core_decompilerLib" 8 9(* ========================================================================== * 10 11 The decompiler as three phases: 12 1. derive specs for each instruction 13 2. calcuate CFG and split into separate 'decompilation rounds' 14 3. for each round: compose specs together to produce function 15 16 * ========================================================================== *) 17 18(* Hooks for ISA specific tools. *) 19 20val get_triple = 21 ref (fn _: string => 22 (raise ERR "get_triple" "uninitialised"): helperLib.instruction) 23val initialise = ref (Lib.I: unit -> unit) 24val pc = ref boolSyntax.F 25val pc_size = ref 0 26val at_pc_conv = ref (Lib.I: conv -> conv) 27val swap_primes = ref (Lib.I: term -> term) 28val code_parser = ref (NONE: (string quotation -> string list) option) 29 30fun add_prime v = Term.mk_var (fst (Term.dest_var v) ^ "'", Term.type_of v) 31 32fun configure 33 {triple_fn = f, 34 init_fn = i, 35 pc_tm = p, 36 pc_conv = c, 37 component_vars = vs 38 } = 39 ( get_triple := f 40 ; initialise := i 41 ; pc := p 42 ; at_pc_conv := c 43 ; pc_size := Arbnum.toInt (wordsSyntax.size_of p) 44 ; swap_primes := 45 Term.subst 46 (List.concat 47 (List.map 48 (fn v => 49 let val pv = add_prime v in [v |-> pv, pv |-> v] end) vs)) 50 ) 51 52val code_abbrevs = ref ([]:thm list); 53fun add_code_abbrev th = (code_abbrevs := th::(!code_abbrevs)); 54 55val decomp_mem = ref ([]:(string * thm * int) list); 56fun add_decomp name th len = (decomp_mem := ((name,th,len)::(!decomp_mem))); 57 58(* PHASE 1 -- evaluate model *) 59 60fun add_to_pc n = 61 [!pc |-> wordsSyntax.mk_word_add (!pc, wordsSyntax.mk_wordii (n, !pc_size))] 62 63local 64 (* vt100 escape string *) 65 val ESC = String.str (Char.chr 0x1B) 66in 67 val inPlaceEcho = 68 if !Globals.interactive 69 then fn s => helperLib.echo 1 ("\n" ^ s) 70 else fn s => helperLib.echo 1 (ESC ^ "[1K" ^ "\n" ^ ESC ^ "[A" ^ s) 71end 72 73local 74 val POST_ASSERT = RAND_CONV o RAND_CONV 75 val PRE_ASSERT = RATOR_CONV o RATOR_CONV o POST_ASSERT 76 val ARITH_SUB_CONV = wordsLib.WORD_ARITH_CONV THENC wordsLib.WORD_SUB_CONV 77 fun is_reducible tm = 78 case Lib.total wordsSyntax.dest_word_add tm of 79 SOME (v, _) => not (Term.is_var v) 80 | _ => not (boolSyntax.is_cond tm) 81 fun PC_CONV tm = 82 if is_reducible tm then (!at_pc_conv) ARITH_SUB_CONV tm else ALL_CONV tm 83 val PC_RULE = Conv.CONV_RULE (PRE_ASSERT PC_CONV THENC POST_ASSERT PC_CONV) 84 fun set_pc n (th, l, j) = 85 (PC_RULE (Thm.INST (add_to_pc n) th), l, Option.map (fn i => n + i) j) 86 fun derive1 hex n = 87 if String.isPrefix "insert:" hex 88 then let 89 val name = 90 helperLib.remove_whitespace 91 (String.extract (hex, size ("insert:"), NONE)) 92 val (_, th, l) = first (fn (n, _, _) => n = name) (!decomp_mem) 93 in 94 (n + l, (set_pc n (UNDISCH_ALL th, l, SOME l), NONE)) 95 end 96 else let 97 val (x as (_, l, _), y) = (!get_triple) hex 98 in 99 (n + l, (set_pc n x, Option.map (set_pc n) y)) 100 end 101 fun derive n [] aux l = rev aux 102 | derive n (x::xs) aux l = 103 let 104 val () = inPlaceEcho (" " ^ Int.toString l) 105 val (n', (x, y)) = derive1 x n 106 in 107 derive n' xs ((n, (x, y)) :: aux) (l - 1) 108 end 109in 110 fun derive_specs name code = 111 let 112 val l = length code 113 val s = if l = 1 then "" else "s" 114 in 115 echo 1 ("\nDeriving instruction spec" ^ s ^ " for " ^ 116 Lib.quote name ^ "...\n\n") 117 ; derive 0 code [] l before 118 inPlaceEcho 119 (" Finished " ^ Int.toString l ^ " instruction" ^ s ^ ".\n\n") 120 end 121end 122 123local 124 val tac = 125 SIMP_TAC (srw_ss()) [pred_setTheory.SUBSET_DEF, pred_setTheory.UNION_DEF] 126 val IN_DEFN = Q.prove(`(c = b) ==> a IN b ==> a IN c`, tac) 127 val SUBSET_DEFN = Q.prove(`(c = b) ==> a SUBSET b ==> a SUBSET c`, tac) 128 val IN_LEFT_DEFN = Q.prove(`(c = b UNION d) ==> a IN b ==> a IN c`, tac) 129 val IN_RIGHT_DEFN = 130 Q.prove(`(c = b UNION d) ==> a SUBSET d ==> a SUBSET c`, tac) 131 val SUBSET_REST = Q.prove(`a SUBSET b ==> a SUBSET (b UNION d)`, tac) 132 val SUBSET_UNION2 = Thm.CONJUNCT2 pred_setTheory.SUBSET_UNION 133 fun subset_conv rwts = 134 Conv.LAND_CONV 135 (PURE_REWRITE_CONV ([boolTheory.AND_CLAUSES, 136 pred_setTheory.EMPTY_SUBSET, 137 pred_setTheory.INSERT_SUBSET, 138 pred_setTheory.UNION_SUBSET] @ rwts)) 139 THENC PURE_REWRITE_CONV [boolTheory.IMP_CLAUSES] 140 val list_mk_union = 141 HolKernel.list_mk_lbinop (Lib.curry pred_setSyntax.mk_union) 142 val strip_union = HolKernel.strip_binop pred_setSyntax.dest_union 143 val get_model_name = 144 helperLib.to_lower o fst o Term.dest_const o tripleSyntax.dest_model o 145 Thm.concl 146 fun extract_code (_, ((th, _, _), _)) = tripleSyntax.dest_code (Thm.concl th) 147 val get_code = 148 (((Lib.op_mk_set aconv o List.concat o List.map pred_setSyntax.strip_set) 149 ## 150 Lib.op_mk_set aconv) o 151 List.partition pred_setSyntax.is_insert o 152 List.concat o List.map (strip_union o extract_code)): 153 (int * helperLib.instruction) list -> term list * term list 154 val (CONJ1_CONV, CONJ2_CONV) = 155 case Drule.CONJUNCTS (Drule.SPEC_ALL boolTheory.OR_CLAUSES) of 156 c1 :: c2 :: _ => (Conv.REWR_CONV c1, Conv.REWR_CONV c2) 157 | _ => fail() 158in 159 fun abbreviate_code _ [] = raise ERR "abbreviate_code" "no code" 160 | abbreviate_code name (thms as (_: int, ((th, _, _), _)) :: _) = 161 let 162 val (newcode, acode) = get_code thms 163 val (cs, l, r) = 164 if List.null acode 165 then let 166 val l = pred_setSyntax.mk_set newcode 167 in 168 (l, l, boolSyntax.F) 169 end 170 else if List.null newcode 171 then let 172 val r = list_mk_union acode 173 in 174 (r, boolSyntax.F, r) 175 end 176 else let 177 val l = pred_setSyntax.mk_set newcode 178 val r = list_mk_union acode 179 in 180 (pred_setSyntax.mk_union (l, r), l, r) 181 end 182 val def_name = name ^ "_" ^ get_model_name th 183 val x = pairSyntax.list_mk_pair (Term.free_vars cs) 184 val v = 185 Term.mk_var (def_name, Term.type_of (pairSyntax.mk_pabs (x, cs))) 186 val code_def = 187 Definition.new_definition 188 (def_name ^ "_def", boolSyntax.mk_eq (Term.mk_comb (v, x), cs)) 189 val () = add_code_abbrev code_def 190 val spec_code_def = Drule.SPEC_ALL code_def 191 val tm = boolSyntax.lhs (Thm.concl spec_code_def) 192 val sty = Term.type_of cs 193 val ty = pred_setSyntax.dest_set_type sty 194 val inst_ty = Thm.INST_TYPE [Type.alpha |-> ty] 195 fun f thm = MATCH_MP thm spec_code_def 196 val (in_left, in_right) = 197 if List.null newcode 198 then (TRUTH, f SUBSET_DEFN) 199 else if List.null acode 200 then (f IN_DEFN, TRUTH) 201 else (f IN_LEFT_DEFN, f IN_RIGHT_DEFN) 202 val rwts1 = 203 if List.null newcode 204 then [] 205 else let 206 val a = Term.mk_var ("a", ty) 207 val refl_cnv = 208 Conv.REWR_CONV (inst_ty boolTheory.REFL_CLAUSE) 209 val in_cnv = 210 Conv.REWR_CONV (inst_ty pred_setTheory.IN_INSERT) 211 fun expand_in n tm = 212 if n <= 0 213 then (in_cnv 214 THENC Conv.LAND_CONV refl_cnv 215 THENC CONJ1_CONV) tm 216 else (in_cnv 217 THENC Conv.RAND_CONV (expand_in (n - 1)) 218 THENC CONJ2_CONV) tm 219 fun cnv i = EQT_ELIM o expand_in i 220 in 221 Lib.mapi 222 (fn i => fn c => 223 MP (Thm.INST [a |-> c] in_left) 224 (cnv i (pred_setSyntax.mk_in (c, l)))) newcode 225 end 226 val rwts2 = 227 if List.null acode 228 then [] 229 else let 230 val a = Term.mk_var ("a", sty) 231 val n = List.length acode - 1 232 val tac1 = MATCH_MP_TAC (inst_ty SUBSET_REST) 233 val tac2 = 234 REWRITE_TAC 235 [inst_ty SUBSET_UNION2, pred_setTheory.SUBSET_REFL] 236 in 237 Lib.mapi 238 (fn i => fn c => 239 MP (Thm.INST [a |-> c] in_right) 240 (Tactical.prove 241 (pred_setSyntax.mk_subset (c, r), 242 NTAC (n - i) tac1 THEN tac2))) acode 243 end 244 val rule = CONV_RULE (subset_conv (rwts1 @ rwts2)) o 245 Thm.SPEC tm o MATCH_MP TRIPLE_EXTEND 246 in 247 List.map (fn (i, x) => (i, helperLib.instruction_apply rule x)) thms 248 end 249end 250 251fun stage_1 name qcode = 252 let 253 val p = Option.getOpt (!code_parser, helperLib.quote_to_strings) 254 in 255 (!initialise) () 256 ; abbreviate_code name (derive_specs name (p qcode)) 257 end 258 259(* Testing 260val name = "test" 261val qcode = `e59f322c 00012f94 262 e59f222c 00012f80 263 edd37a00` 264val (_, ((th, _, _), _)) = hd thms 265*) 266 267 268(* PHASE 2 -- compute CFG *) 269 270val extract_graph = 271 List.concat o 272 List.map (fn (i, ((_, _, j), NONE): helperLib.instruction) => [(i: int, j)] 273 | (i, ((_, _, j), SOME (_, _, k))) => [(i, j), (i, k)]) 274 275val jumps2edges = 276 List.concat o 277 List.map (fn (i, NONE) => []: (int * int) list 278 | (i, SOME j) => [(i, j)]) 279 280val all_distinct = Lib.mk_set 281 282fun drop_until P [] = [] 283 | drop_until P (x :: xs) = if P x then x :: xs else drop_until P xs 284 285fun subset [] ys = true 286 | subset (x :: xs) ys = mem x ys andalso subset xs ys 287 288local 289 fun all_paths_from edges i prefix = 290 let 291 fun f [] = [] 292 | f ((k, j) :: xs) = if i = k then j :: f xs else f xs 293 val next = all_distinct (f edges) 294 val prefix = prefix @ [i] 295 val xs = map (fn x => if mem x prefix 296 then [prefix @ [x]] 297 else all_paths_from edges x prefix) next 298 val xs = if xs = [] then [[prefix]] else xs 299 in 300 Lib.flatten xs 301 end 302 303 fun is_loop xs = Lib.mem (List.last xs) (Lib.butlast xs) 304 305 (* clean loop tails *) 306 fun clean_tails (i, xs, tails) = 307 (i, xs, 308 List.mapPartial 309 (fn t => let 310 val l = drop_until (fn x => not (mem x xs)) t 311 in 312 if List.null l then NONE else SOME l 313 end) tails) 314 315 fun cross [] ys = [] 316 | cross (x :: xs) ys = map (fn y => (x, y)) ys @ cross xs ys 317 318 fun sat_goal ((i, j), path) = hd path = i andalso mem j (tl path) 319 320 fun find_and_merge zs = 321 let 322 val ls = Lib.flatten (map (fn (x, y, z) => x) zs) 323 val qs = map (fn (x, y, z) => (x, y, map hd z)) zs 324 fun f ys = filter (fn x => mem x ls andalso (not (mem x ys))) 325 val qs = map (fn (x, y, z) => (x, all_distinct (f x y @ f x z))) qs 326 val edges = Lib.flatten (map (fn (x,y) => cross x y) qs) 327 val paths = map (fn i => all_paths_from edges i []) ls 328 val goals = map (fn (x,y) => (y,x)) edges 329 val (i, j) = 330 fst (hd (filter sat_goal (cross goals (Lib.flatten paths)))) 331 val (p1, q1, x1) = hd (filter (fn (x,y,z) => mem i x) zs) 332 val (p2, q2, x2) = hd (filter (fn (x,y,z) => mem j x) zs) 333 val (p, q, x) = (p1 @ p2, all_distinct (q1 @ q2), x1 @ x2) 334 val zs = 335 (p,q,x) :: 336 filter (fn (x, y, z) => not (mem i x) andalso not (mem j x)) zs 337 val zs = map clean_tails zs 338 in 339 zs 340 end 341 342 fun mem_all x = List.all (Lib.mem x) 343 344 fun find_exit_points (x, y, z) = 345 let 346 val q = hd (filter (fn x => mem_all x (tl z)) (hd z)) 347 in 348 (x, [q]) 349 end 350 handle Empty => (x, all_distinct (map hd z)) 351 352 fun list_before x y [] = true 353 | list_before x y (z :: zs) = 354 z <> y andalso (z = x orelse list_before x y zs) 355 356 val int_sort = Lib.sort (Lib.curry (op Int.<=)) 357in 358 fun extract_loops jumps = 359 let 360 (* find all possible paths *) 361 val edges = jumps2edges jumps 362 val paths = all_paths_from edges 0 [] 363 (* get looping points *) 364 val loops = all_distinct (map last (filter is_loop paths)) 365 (* find loop bodies and tails *) 366 fun loop_body_tail i = 367 let 368 val bodies = filter (fn xs => last xs = i) paths 369 val bodies = filter is_loop bodies 370 val bodies = map (drop_until (fn x => x = i) o butlast) bodies 371 val bodies = all_distinct (Lib.flatten bodies) 372 val tails = 373 filter (fn xs => mem i xs andalso not (last xs = i)) paths 374 val tails = map (drop_until (fn x => x = i)) tails 375 in 376 (fn (x, y, z) => ([x], y, z)) (clean_tails (i, bodies, tails)) 377 end 378 val zs = map loop_body_tail loops 379 (* merge combined loops *) 380 val zs = repeat find_and_merge zs 381 (* attempt to find common exit point *) 382 val zs = map find_exit_points zs 383 (* finalise *) 384 val exit = (all_distinct o map last o filter (not o is_loop)) paths 385 val zero = ([0], exit) 386 val zs = 387 if List.null 388 (filter (fn (x, y) => mem 0 x andalso subset exit y) zs) 389 then zs @ [zero] 390 else zs 391 fun compare (xs, _) (ys, _) = 392 let 393 val x = hd xs 394 val y = hd ys 395 val p = hd (filter (fn xs => mem x xs andalso mem y xs) paths) 396 in 397 not (list_before x y p) 398 end 399 handle Empty => false 400 val loops = sort compare zs 401 (* sort internal *) 402 val loops = map (int_sort ## int_sort) loops 403 in 404 loops 405 end 406end 407 408local 409 fun forks_acc a = 410 fn [] => List.rev a 411 | (x1, _) :: xs => 412 if List.exists (fn (x2, _) => x2 = x1) xs 413 then forks_acc (x1 :: a) (filter (fn (x2, _) => x2 <> x1) xs) 414 else forks_acc a xs 415in 416 val forks = forks_acc [] 417end 418 419fun stage_12 name qcode = 420 let 421 val thms = stage_1 name qcode 422 val jumps = extract_graph thms 423 val loops = extract_loops jumps 424 val loops = 425 case loops of 426 [([0], [n])] => 427 let 428 val fs = Lib.sort (Lib.curry (op >=)) (forks jumps) 429 in 430 map (fn f => ([f], [n])) fs @ [([0], [n])] 431 end 432 | other => other 433 in 434 (thms, loops) 435 end 436 437 438(* PHASE 3 -- compose and extract *) 439 440datatype compose_tree = 441 End of int 442 | Repeat of int 443 | Cons of thm * compose_tree 444 | Merge of term * compose_tree * compose_tree 445 | ConsMerge of term * thm * thm * compose_tree 446 447fun is_rec (Repeat _) = true 448 | is_rec (End _) = false 449 | is_rec (Cons (_, t)) = is_rec t 450 | is_rec (Merge (_, t1, t2)) = is_rec t1 orelse is_rec t2 451 | is_rec (ConsMerge (_, _, _, t)) = is_rec t 452 453local 454 val (_, _, _, is_abbrev) = HolKernel.syntax_fns1 "marker" "Abbrev" 455 fun get_Abbrev th = 456 case Thm.hyp th of 457 [h] => Lib.with_exn (Term.rand o HolKernel.find_term is_abbrev) h 458 (ERR "get_Abbrev" "Abbrev not found") 459 | _ => raise ERR "get_Abbrev" "not a single hyp" 460in 461 fun build_compose_tree (b, e) thms = 462 let 463 fun find_next i = first (fn (n, _:helperLib.instruction) => n = i) thms 464 fun sub init NONE = 465 raise ERR "build_compose_tree" "cannot handle bad exists" 466 | sub init (SOME i) = 467 if mem i e 468 then End i 469 else if not init andalso mem i b 470 then Repeat i 471 else case find_next i of 472 (_, ((th1, l1, x1), NONE)) => Cons (th1, sub false x1) 473 | (_, ((th1, l1, x1), SOME (th2, l2, x2))) => 474 if x1 = x2 475 then ConsMerge (get_Abbrev th1, th1, th2, sub false x1) 476 else let 477 val t1 = Cons (th1, sub false x1) 478 val t2 = Cons (th2, sub false x2) 479 in 480 Merge (get_Abbrev th1, t1, t2) 481 end 482 in 483 sub true (SOME (hd b)) 484 end 485end 486 487val l1 = ref TRUTH 488val l2 = ref TRUTH 489val l3 = ref T; 490 491local 492 fun VALUE_RULE c = CONV_RULE (RAND_CONV (RAND_CONV c)) 493 val PAIR_RULE = 494 CONV_RULE ((RATOR_CONV o RAND_CONV) (PURE_REWRITE_CONV [pairTheory.PAIR])) 495 fun ii lhs rhs = 496 let 497 val (x, y) = pairSyntax.dest_pair rhs 498 val x1 = pairSyntax.mk_fst lhs 499 val y1 = pairSyntax.mk_snd lhs 500 in 501 (x |-> x1) :: ii y1 y 502 end 503 handle HOL_ERR _ => [rhs |-> lhs] 504in 505 fun compose th1 th2 = 506 let 507 val th3 = MATCH_MP (MATCH_MP TRIPLE_COMPOSE_ALT th2) th1 508 in 509 case Thm.hyp th3 of 510 [] => th3 511 | tm :: _ => 512 let 513 val lemma = SYM (ASSUME tm) 514 val (lhs, rhs) = dest_eq tm 515 val th4 = VALUE_RULE 516 (PairRules.UNPBETA_CONV rhs 517 THENC REWR_CONV (SYM (SPEC_ALL LET_THM)) 518 THENC RAND_CONV (fn _ => lemma)) th3 519 in 520 MP (PAIR_RULE (INST (ii lhs rhs) (DISCH_ALL th4))) (REFL lhs) 521 end 522 end 523 handle HOL_ERR e => (l1 := th1; l2 := th2; raise HOL_ERR e) 524end 525 526(* 527val th1 = !l1 528val th2 = !l2 529val tm = !l3 530*) 531 532local 533 val rule1 = 534 REWRITE_RULE [markerTheory.Abbrev_def, addressTheory.CONTAINER_def] 535 val rule2 = CONV_RULE ((RAND_CONV o RAND_CONV) (SIMP_CONV bool_ss [])) 536in 537 fun merge tm th1 th2 = 538 let 539 val th1 = DISCH tm (rule1 th1) 540 val th2 = DISCH (mk_neg tm) (rule1 th2) 541 in 542 rule2 (MATCH_MP COND_MERGE (CONJ th1 th2)) 543 end 544 handle HOL_ERR e => (l1 := th1; l2 := th2; l3 := tm; raise HOL_ERR e) 545end 546 547(* 548 fun fan (End i) = 1 549 | fan (Repeat i) = 1 550 | fan (Cons (th,t)) = fan t 551 | fan (Merge (tm,t1,t2)) = fan t1 + fan t2 552 | fan (ConsMerge (tm,th1,th2,t)) = fan t + fan t 553 554 fan t 555*) 556 557val case_sum_conv = 558 SIMP_CONV (std_ss++simpLib.rewrites [tripleTheory.case_sum_def]) [] 559val case_sum_rule = Conv.CONV_RULE (Conv.RATOR_CONV case_sum_conv) 560val beta_fst_rule = 561 CONV_RULE ((RATOR_CONV o RAND_CONV) 562 (DEPTH_CONV PairedLambda.GEN_BETA_CONV 563 THENC REWRITE_CONV [pairTheory.FST]) 564 THENC REWRITE_CONV [boolTheory.IMP_CLAUSES]) 565val forall_prod_ss = pure_ss++simpLib.rewrites [pairTheory.FORALL_PROD] 566 567fun round (input, get_assert, triple_refl) = 568 fn name => fn (b, e) => fn thms => 569 let 570 val () = inPlaceEcho (name ^ ": ") 571 val () = echo 1 "." 572 val t = build_compose_tree (b, e) thms 573 val loop = is_rec t 574 val pre = get_assert (hd b) 575 val post = get_assert (hd e) 576 val (enter_th, exit_th) = 577 if loop 578 then let 579 fun refl_sum f = 580 triple_refl 581 (tripleSyntax.mk_case_sum 582 (pre, post, f (input, Term.type_of input))) 583 in 584 (refl_sum sumSyntax.mk_inl, refl_sum sumSyntax.mk_inr) 585 end 586 else (boolTheory.TRUTH, triple_refl (Term.mk_comb (post, input))) 587 (* perform composition *) 588 val () = echo 1 "." 589 fun comp (End i) = exit_th 590 | comp (Repeat i) = enter_th 591 | comp (Cons (th, t)) = compose th (comp t) 592 | comp (Merge (tm, t1, t2)) = merge tm (comp t1) (comp t2) 593 | comp (ConsMerge (tm, th1, th2, t)) = 594 let 595 val res = comp t 596 in 597 merge tm (compose th1 res) (compose th2 res) 598 end 599 val th = 600 CONV_RULE ((RAND_CONV o RAND_CONV) (PairRules.UNPBETA_CONV input)) 601 (comp t) 602 val th = 603 if loop 604 then let 605 val () = echo 1 "." 606 (* apply loop rule *) 607 val lemma = case_sum_conv (mk_comb (pre, input)) 608 val th = CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) 609 (fn _ => GSYM lemma)) th 610 val x = Term.mk_var ("x", Term.type_of input) 611 val tm = mk_forall (x, subst [input |-> x] (Thm.concl th)) 612 val lemma = 613 prove 614 (tm, 615 FULL_SIMP_TAC forall_prod_ss [] 616 THEN REPEAT STRIP_TAC 617 THEN MATCH_MP_TAC (DISCH T th) 618 THEN FULL_SIMP_TAC std_ss []) 619 val th = 620 MATCH_MP SHORT_TERM_TAILREC lemma 621 |> beta_fst_rule 622 |> SPEC input 623 |> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) 624 PairRules.PBETA_CONV) 625 in 626 th 627 end 628 else th 629 val () = echo 1 "." 630 val ff = th |> concl |> rand |> rand |> rator 631 val def = 632 new_definition (name ^ "_def", mk_eq (mk_var (name, type_of ff), ff)) 633 val th = th |> CONV_RULE 634 ((RAND_CONV o RAND_CONV o RATOR_CONV) (fn _ => GSYM def)) 635 (* clean up result *) 636 val lemma = mk_eq(mk_comb (boolSyntax.lhs (concl def), input), 637 (!swap_primes) input) 638 |> ASSUME 639 val result = 640 th |> CONV_RULE ((RAND_CONV o RAND_CONV) (fn _ => lemma) 641 THENC RAND_CONV PairRules.PBETA_CONV) 642 |> DISCH_ALL 643 val () = echo 1 "." 644 in 645 (def, result) 646 end 647 648fun core_decompile name qcode = 649 let 650 val (thms, loops) = time (stage_12 name) qcode 651 val (_, ((th, _, _), _)) = Lib.first (fn (x, _) => x = 0) thms 652 val (model, pre, code, _) = tripleSyntax.dest_triple (Thm.concl th) 653 val (cnd, asrt) = pairSyntax.dest_pair pre 654 val affected_vars = asrt |> Term.free_vars |> filter (fn v => v !~ !pc) 655 val inp = pairSyntax.list_mk_pair (cnd :: affected_vars) 656 fun get_assert i = pairSyntax.mk_pabs (inp, Term.subst (add_to_pc i) pre) 657 val refl = Thm.SPEC code (Drule.ISPEC model tripleTheory.TRIPLE_REFL) 658 fun triple_refl t = case_sum_rule (Thm.SPEC t refl) 659 val round = round (inp, get_assert, triple_refl) 660 fun rounds loops thms defs = 661 let 662 val (b, e) = hd loops 663 val loops = tl loops 664 val n = length loops 665 val part_name = if n = 0 then name 666 else name ^ "_part" ^ (int_to_string n) 667 val (def, result) = round part_name (b, e) thms 668 val thms = 669 (hd b, ((UNDISCH_ALL result, 0, SOME (hd e)), NONE)) :: thms 670 in 671 if n = 0 672 then (result, rev (def :: defs)) 673 else rounds loops thms (def :: defs) 674 end 675 val () = echo 1 "\nProcessing...\n\n" 676 val (res, defs) = 677 time (fn () => rounds loops thms [] before inPlaceEcho "Finished.\n\n") 678 () 679 val () = add_decomp name res (loops |> last |> snd |> hd) 680 in 681 (res, LIST_CONJ defs) 682 end 683 684end 685