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