1structure codegen_x86Lib :> codegen_x86Lib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open helperLib x86_encodeLib codegen_inputLib; 6 7 8val x86_regs = ref [(0,"eax"), (1,"ecx"), (2,"edx"), (3,"ebx"), 9 (4,"edi"), (5,"esi"), (6,"ebp")]; 10 11fun set_x86_regs regs = (x86_regs := regs); 12fun get_x86_regs () = (!x86_regs); 13 14fun x86_reg n = (snd o hd o filter (fn (x,y) => x = n)) (get_x86_regs ()) 15 16fun to_x86_regs () = let 17 fun foo (i,s) = mk_var("r" ^ int_to_string i,``:word32``) |-> mk_var(s, ``:word32``) 18 in map foo (get_x86_regs ()) end 19 20val x86_assign2assembly = let 21 fun r i = x86_reg i 22 fun s i = "[ebp - " ^ int_to_string (4 * i) ^ "]" 23 fun address (ASSIGN_ADDRESS_REG i) = "[" ^ r i ^ "]" 24 | address (ASSIGN_ADDRESS_OFFSET_ADD (d,i)) = "[" ^ r d ^ " + " ^ Arbnum.toString i ^ "]" 25 | address (ASSIGN_ADDRESS_OFFSET_SUB (d,i)) = "[" ^ r d ^ " - " ^ Arbnum.toString i ^ "]" 26 fun binop_to_name ASSIGN_BINOP_ADD = "add" 27 | binop_to_name ASSIGN_BINOP_AND = "and" 28 | binop_to_name ASSIGN_BINOP_SUB = "sub" 29 | binop_to_name ASSIGN_BINOP_XOR = "xor" 30 | binop_to_name ASSIGN_BINOP_OR = "or" 31 | binop_to_name _ = fail() 32 fun exp (ASSIGN_X_REG j) = x86_reg j 33 | exp (ASSIGN_X_CONST i) = Arbnum.toString i 34 fun code_for_binop k ASSIGN_BINOP_MUL 35 (ASSIGN_X_REG i) (ASSIGN_X_REG j) reversed = let 36 val k_reg = x86_reg k 37 val i_reg = x86_reg i 38 val j_reg = x86_reg j 39 val (i_reg,j_reg) = if i_reg = "eax" then (i_reg,j_reg) else (j_reg,i_reg) 40 in if (i_reg = "eax") andalso (k_reg = "eax") then ["mul " ^ x86_reg j] 41 else (print ("\n\nUnable to create x86 code for: " ^ k_reg ^ " := " ^ i_reg ^ 42 " * " ^ j_reg ^ "\n\n"); fail()) end 43 | code_for_binop k ASSIGN_BINOP_DIV 44 (ASSIGN_X_REG i) (ASSIGN_X_REG j) reversed = let 45 val k_reg = x86_reg k 46 val i_reg = x86_reg i 47 val j_reg = x86_reg j 48 val (i_reg,j_reg) = if i_reg = "eax" then (i_reg,j_reg) else (j_reg,i_reg) 49 in if (i_reg = "eax") andalso (k_reg = "eax") then ["xor edx, edx", "div " ^ x86_reg j] 50 else (print ("\n\nUnable to create x86 code for: " ^ k_reg ^ " := " ^ i_reg ^ 51 " DIV " ^ j_reg ^ "\n\n"); fail()) end 52 | code_for_binop k ASSIGN_BINOP_MOD 53 (ASSIGN_X_REG i) (ASSIGN_X_REG j) reversed = let 54 val k_reg = x86_reg k 55 val i_reg = x86_reg i 56 val j_reg = x86_reg j 57 val (i_reg,j_reg) = if i_reg = "eax" then (i_reg,j_reg) else (j_reg,i_reg) 58 in if (i_reg = "eax") andalso (k_reg = "edx") then ["xor edx, edx", "mod " ^ x86_reg j] 59 else (print ("\n\nUnable to create x86 code for: " ^ k_reg ^ " := " ^ i_reg ^ 60 " MOD " ^ j_reg ^ "\n\n"); fail()) end 61 | code_for_binop d b (ASSIGN_X_CONST i) (ASSIGN_X_REG j) reversed = 62 code_for_binop d b (ASSIGN_X_REG j) (ASSIGN_X_CONST i) (not reversed) 63 | code_for_binop d b (ASSIGN_X_CONST i) (ASSIGN_X_CONST j) reversed = fail() 64 | code_for_binop d b (ASSIGN_X_REG i) j reversed = 65 if (b = ASSIGN_BINOP_SUB) andalso reversed then 66 (if j = ASSIGN_X_REG d then [] else ["mov " ^ x86_reg d ^ ", " ^ exp j]) @ 67 ["neg " ^ x86_reg d] @ ["add " ^ x86_reg d ^ ", " ^ x86_reg i] 68 else 69 if (j = ASSIGN_X_REG d) andalso not (i = d) then 70 code_for_binop d b (ASSIGN_X_REG d) (ASSIGN_X_REG i) (not reversed) 71 else if (i = d) andalso (j = ASSIGN_X_CONST (Arbnum.fromInt 1)) andalso (b = ASSIGN_BINOP_ADD) then 72 ["inc " ^ x86_reg d] 73 else if (i = d) andalso (j = ASSIGN_X_CONST (Arbnum.fromInt 1)) andalso (b = ASSIGN_BINOP_SUB) then 74 ["dec " ^ x86_reg d] 75 else if (b = ASSIGN_BINOP_ADD) andalso not (i = d) then 76 ["lea " ^ x86_reg d ^ ", [" ^ x86_reg i ^ "+" ^ exp j ^ "]"] 77 else 78 (if d = i then [] else ["mov " ^ x86_reg d ^ ", " ^ x86_reg i]) @ 79 [binop_to_name b ^ " " ^ x86_reg d ^ ", " ^ exp j] 80 fun monop_to_name ASSIGN_MONOP_NEG = "neg" 81 | monop_to_name ASSIGN_MONOP_NOT = "not" 82 fun code_for_monop d m j = 83 (if j = ASSIGN_X_REG d then [] else ["mov " ^ x86_reg d ^ ", " ^ exp j]) @ 84 [monop_to_name m ^ " " ^ x86_reg d] 85 fun code_for_shift d j n name = 86 (if j = ASSIGN_X_REG d then [] else ["mov " ^ x86_reg d ^ ", " ^ exp j]) @ 87 [name ^ " " ^ x86_reg d ^ ", " ^ int_to_string n] 88 fun mov_name ACCESS_WORD = "mov" 89 | mov_name ACCESS_BYTE = "mov BYTE" 90 fun mem_rhs _ (ASSIGN_X_REG t) = r t 91 | mem_rhs ACCESS_WORD (ASSIGN_X_CONST i) = Arbnum.toString i 92 | mem_rhs ACCESS_BYTE (ASSIGN_X_CONST i) = let 93 val imm8 = Arbnum.toInt i 94 val imm8 = if 128 <= imm8 then "-" ^ int_to_string (0 - (imm8 - 256)) else int_to_string imm8 95 in imm8 end 96 fun f (ASSIGN_EXP (d, ASSIGN_EXP_REG s)) = ["cmov? " ^ r d ^ ", " ^ r s] 97 | f (ASSIGN_EXP (d, ASSIGN_EXP_CONST i)) = ["mov " ^ r d ^ ", " ^ Arbnum.toString i] 98 | f (ASSIGN_EXP (d, ASSIGN_EXP_STACK i)) = ["mov " ^ r d ^ ", " ^ s i] 99 | f (ASSIGN_EXP (d, ASSIGN_EXP_BINOP (i,b,j))) = code_for_binop d b i j false 100 | f (ASSIGN_EXP (d, ASSIGN_EXP_MONOP (m,j))) = code_for_monop d m j 101 | f (ASSIGN_EXP (d, ASSIGN_EXP_MEMORY (ACCESS_WORD,a))) = ["MOV " ^ r d ^ ", " ^ address a] 102 | f (ASSIGN_EXP (d, ASSIGN_EXP_MEMORY (ACCESS_BYTE,a))) = ["MOVZX " ^ r d ^ ", BYTE " ^ address a] 103 | f (ASSIGN_EXP (d, ASSIGN_EXP_SHIFT_LEFT (j,n))) = code_for_shift d j n "shl" 104 | f (ASSIGN_EXP (d, ASSIGN_EXP_SHIFT_RIGHT (j,n))) = code_for_shift d j n "shr" 105 | f (ASSIGN_EXP (d, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (j,n))) = code_for_shift d j n "sar" 106 | f (ASSIGN_STACK (i,d)) = ["mov " ^ s i ^ ", " ^ mem_rhs ACCESS_WORD d] 107 | f (ASSIGN_MEMORY (b,a,d)) = [mov_name b ^ " " ^ address a ^ ", " ^ mem_rhs b d] 108 | f (ASSIGN_OTHER (t1,t2)) = fail() 109 in f end 110 111fun x86_guard2assembly (GUARD_NOT t) = let 112 val (code,(x,y)) = x86_guard2assembly t in (code,(y,x)) end 113 | x86_guard2assembly (GUARD_COMPARE (i,cmp,j)) = let 114 val rd = x86_reg i 115 fun f (ASSIGN_X_REG r) = x86_reg r 116 | f (ASSIGN_X_CONST c) = Arbnum.toString c 117 val code = ["cmp " ^ rd ^ ", " ^ f j] 118 fun g (GUARD_COMPARE_LESS false) = ("b","nb") 119 | g (GUARD_COMPARE_LESS true) = ("lt","ge") 120 | g (GUARD_COMPARE_LESS_EQUAL false) = ("na","a") 121 | g (GUARD_COMPARE_LESS_EQUAL true) = ("le","gt") 122 | g (GUARD_COMPARE_EQUAL) = ("e","ne") 123 in (code, g cmp) end 124 | x86_guard2assembly (GUARD_TEST (i,j)) = let 125 val rd = x86_reg i 126 fun f (ASSIGN_X_REG r) = x86_reg r 127 | f (ASSIGN_X_CONST c) = Arbnum.toString c 128 val code = ["test " ^ rd ^ ", " ^ f j] 129 in (code, ("e","ne")) end 130 | x86_guard2assembly (GUARD_EQUAL_BYTE (a,i)) = let 131 fun r i = x86_reg i 132 fun address (ASSIGN_ADDRESS_REG i) = "[" ^ r i ^ "]" 133 | address (ASSIGN_ADDRESS_OFFSET_ADD (d,i)) = "[" ^ r d ^ " + " ^ Arbnum.toString i ^ "]" 134 | address (ASSIGN_ADDRESS_OFFSET_SUB (d,i)) = "[" ^ r d ^ " - " ^ Arbnum.toString i ^ "]" 135 in (["cmp BYTE " ^ address a ^ ", " ^ Arbnum.toString i], ("e","ne")) end 136 | x86_guard2assembly (GUARD_OTHER tm) = let 137 val (t1,t2) = dest_eq tm 138 val code = hd (x86_assign2assembly (term2assign t1 t2)) 139 val code = "cmp" ^ (implode o tl o tl o tl o tl o tl o explode) code 140 in ([code], ("e","ne")) end; 141 142 143 144fun x86_conditionalise c condition = let 145 val c' = String.translate (fn x => if x = #"?" then condition else implode [x]) c 146 in if c = c' then fail() else c' end 147 148fun x86_remove_annotations c = 149 if String.substring(c,0,5) = "cmov?" then 150 "mov" ^ String.substring(c,5,size(c) - 5) 151 else c handle _ => c 152 153fun x86_cond_code tm = 154 (* zero *) if tm ~~ ``xS1 X_ZF`` then ("e","ne") else 155 (* sign *) if tm ~~ ``xS1 X_SF`` then ("s","ns") else 156 (* below *) if tm ~~ ``xS1 X_CF`` then ("b","nb") else fail() 157 158 159fun x86_encode_instruction s = 160 let val s = x86_encode s in (s, (size s) div 2) end 161 162fun x86_encode_branch_aux forward l cond = let 163 fun asm NONE = "jmp" 164 | asm (SOME c) = if mem c ["loop","loope","loopne"] then c else 165 if hd (explode c) = #"j" then c else "j" ^ c 166 val s = asm cond 167 fun address l = s ^ (if forward then " " else " -") ^ int_to_string l 168 fun find_encoding f l s = let 169 val v = f (l + size s div 2) 170 in if s = v then v else find_encoding f l v end 171 val i = (if forward then x86_encode (address l) 172 else find_encoding (x86_encode o address) l "") 173 in (i, (size i) div 2) end 174 175fun x86_flip_cond c = 176 if mem c ["ne","jne"] then "e" else 177 if mem c ["e","je"] then "ne" else 178 if mem c ["ns","jns"] then "s" else 179 if mem c ["s","js"] then "ns" else 180 if mem c ["na","jna"] then "a" else 181 if mem c ["a","ja"] then "na" else 182 if mem c ["nb","jnb"] then "b" else 183 if mem c ["b","jb"] then "nb" else fail() 184 185fun x86_encode_branch forward l cond = 186 x86_encode_branch_aux forward l cond handle HOL_ERR _ => 187 let (* The implementation of long conditional jumps assume 188 that short conditional jumps are 2 bytes in length, 189 and that long unconditional branches are 5 bytes. *) 190 fun the NONE = fail() | the (SOME x) = x 191 val c = x86_flip_cond (the cond) 192 val (xs,i) = x86_encode_branch_aux true 5 (SOME c) 193 val _ = if i = 2 then () else fail() 194 val l = if forward then l else l+2 195 val (ys,j) = x86_encode_branch_aux forward l NONE 196 in (xs ^ " " ^ ys, i + j) end 197 198fun x86_branch_to_string NONE = "jmp" 199 | x86_branch_to_string (SOME c) = "j" ^ c 200 201end; 202