1structure x64_compilerLib :> x64_compilerLib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open decompilerLib; 6open x64_codegenLib; 7open x64_codegen_x64Lib; 8 9open prog_x64Lib; 10open prog_x64_extraTheory; 11open wordsTheory wordsLib addressTheory; 12open helperLib; 13open tailrecLib; 14 15 16fun AUTO_ALPHA_CONV () = let 17 val counter = ref (Arbnum.zero) 18 fun inc () = let val v = !counter in (counter := Arbnum.+(v,Arbnum.one); v) end 19 fun counter_genvar ty = mk_var("auto_"^ Arbnum.toString (inc()),ty) 20 fun doit tm = 21 if is_abs tm then 22 (ALPHA_CONV (counter_genvar (type_of (fst (dest_abs tm)))) THENC 23 ABS_CONV doit) tm 24 else if is_comb tm then 25 (RATOR_CONV doit THENC RAND_CONV doit) tm 26 else ALL_CONV tm 27 in doit end 28 29val COMPILER_TAC_LEMMA = prove( 30 ``!a b:bool. (a /\ a /\ b <=> a /\ b) /\ (a \/ a \/ b <=> a \/ b)``, 31 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss []); 32 33val COMPILER_TAC = 34 SIMP_TAC bool_ss [LET_DEF,word_div_def,word_mod_def,w2w_CLAUSES] 35 THEN SIMP_TAC std_ss [WORD_OR_CLAUSES,GUARD_def] 36 THEN REWRITE_TAC [WORD_CMP_NORMALISE] 37 THEN REWRITE_TAC [WORD_HIGHER,WORD_GREATER,WORD_HIGHER_EQ, 38 WORD_GREATER_EQ,GSYM WORD_NOT_LOWER,GSYM WORD_NOT_LESS] 39 THEN SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w,NOT_IF, 40 WORD_OR_CLAUSES] 41 THEN CONV_TAC (EVAL_ANY_MATCH_CONV word_patterns) 42 THEN SIMP_TAC std_ss [WORD_SUB_RZERO, WORD_ADD_0, IF_IF, 43 AC WORD_ADD_COMM WORD_ADD_ASSOC, 44 AC WORD_MULT_COMM WORD_MULT_ASSOC, 45 AC WORD_AND_COMM WORD_AND_ASSOC, 46 AC WORD_OR_COMM WORD_OR_ASSOC, 47 AC WORD_XOR_COMM WORD_XOR_ASSOC, 48 AC CONJ_COMM CONJ_ASSOC, 49 AC DISJ_COMM DISJ_ASSOC, 50 IMP_DISJ_THM, WORD_MULT_CLAUSES] 51 THEN REPEAT STRIP_TAC 52 THEN CONV_TAC (RAND_CONV (AUTO_ALPHA_CONV ())) 53 THEN CONV_TAC ((RATOR_CONV o RAND_CONV) (AUTO_ALPHA_CONV ())) 54 THEN SIMP_TAC std_ss [AC CONJ_ASSOC CONJ_COMM, AC DISJ_COMM DISJ_ASSOC, 55 COMPILER_TAC_LEMMA] 56 THEN SIMP_TAC std_ss [WORD_SUB_RZERO, WORD_ADD_0, IF_IF, 57 AC WORD_ADD_COMM WORD_ADD_ASSOC, 58 AC WORD_MULT_COMM WORD_MULT_ASSOC, 59 AC WORD_AND_COMM WORD_AND_ASSOC, 60 AC WORD_OR_COMM WORD_OR_ASSOC, 61 AC WORD_XOR_COMM WORD_XOR_ASSOC, 62 AC CONJ_COMM CONJ_ASSOC, 63 AC DISJ_COMM DISJ_ASSOC, 64 IMP_DISJ_THM, WORD_MULT_CLAUSES] 65 THEN EQ_TAC 66 THEN ONCE_REWRITE_TAC [GSYM DUMMY_EQ_def] 67 THEN REWRITE_TAC [FLATTEN_IF] 68 THEN REPEAT STRIP_TAC 69 THEN ASM_SIMP_TAC std_ss []; 70 71fun x64_basic_compile tm = let 72 val target = "x64" 73 val (tools,target,model_name,s) = (x64_tools_64,"x64","X64_MODEL",[]) 74 val x = fst (dest_eq tm) 75 val name = fst (dest_const (repeat car x)) handle e => fst (dest_var (repeat car x)) 76 val _ = echo 1 ("\nCompiling " ^ name ^ " into "^ target ^ "...\n") 77 val (code,len) = generate_code model_name true tm 78 fun append' [] = "" | append' (x::xs) = x ^ "\n" ^ append' xs 79 val qcode = [QUOTE (append' code)] : term quotation 80 val in_tm = cdr x 81 fun ends (FUN_IF (_,c1,c2)) = ends c1 @ ends c2 82 | ends (FUN_LET (_,_,c)) = ends c 83 | ends (FUN_COND (_,c)) = ends c 84 | ends (FUN_VAL t) = if is_var t orelse pairSyntax.is_pair t then [t] else [] 85 val out_tm2 = hd (ends (tm2ftree (cdr tm))) 86 val (in_tm,out_tm) = (subst s in_tm, subst s out_tm2) 87 val function_in_out = SOME (in_tm,out_tm) 88 val qcode = ([QUOTE (append' code)]) : term Lib.frag list 89 val (th1,th2) = basic_decompile tools name function_in_out qcode 90 val _ = print "Proving equivalence, " 91 val const = (repeat car o fst o dest_eq o concl o hd o CONJUNCTS) th2 92 val tm = subst [ repeat car x |-> const ] tm 93 val pre = if is_conj (concl th2) then (last o CONJUNCTS) th2 else TRUTH 94 val pre = RW [IF_IF,WORD_TIMES2] pre 95 val th3 = auto_prove "compile" (tm, 96 REPEAT STRIP_TAC 97 THEN CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [th2])) 98 THEN COMPILER_TAC) 99 handle HOL_ERR e => let 100 val _ = (show_types := true) 101 val _ = print ("\n\nval tm = ``"^ term_to_string tm ^"``;\n\n") 102 val _ = (show_types := false) 103 in raise HOL_ERR e end; 104 val _ = add_compiler_assignment out_tm2 (fst (dest_eq tm)) name len model_name 105 val _ = print "done.\n" 106 in (th1,th3,pre) end; 107 108fun x64_compile t = let 109 val tm = Parse.Term t 110 val _ = set_abbreviate_code true 111 fun compile_each [] = [] 112 | compile_each (tm::tms) = let 113 val (th,def,pre) = x64_basic_compile tm 114 in (th,def,pre) :: compile_each tms end 115 val tms = list_dest dest_conj tm 116 val xs = compile_each tms 117 val defs = map (fn (x,y,z) => y) xs 118 val pres = map (fn (x,y,z) => z) xs 119 val def = RW [] (foldr (uncurry CONJ) TRUTH defs) 120 val pre = RW [] (foldr (uncurry CONJ) TRUTH pres) 121 val (th,_,_) = last xs 122 val _ = set_abbreviate_code false 123 val th = UNABBREV_CODE_RULE th 124 in (th,def,pre) end; 125 126val _ = add_compiled (map (SIMP_RULE std_ss [LET_DEF] o Q.INST [`rip`|->`p`]) 127 [x64_push_r0, x64_push_r1, x64_push_r2, x64_push_r3, x64_push_r6, 128 x64_push_r7, x64_push_r8, x64_push_r9, x64_push_r10, 129 x64_push_r11, x64_push_r12, x64_push_r13, x64_push_r14, 130 x64_push_r15, x64_pop_r0, x64_pop_r1, x64_pop_r2, x64_pop_r3, 131 x64_pop_r6, x64_pop_r7, x64_pop_r8, x64_pop_r9, x64_pop_r10, 132 x64_pop_r11, x64_pop_r12, x64_pop_r13, x64_pop_r14, x64_pop_r15]); 133 134end; 135