1structure x64_codegen_x64Lib :> x64_codegen_x64Lib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open helperLib x64_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 QWORD" 82 | mov_name ACCESS_BYTE = "mov BYTE" 83 fun mem_rhs ACCESS_WORD (ASSIGN_X_REG t) = r t 84 | mem_rhs ACCESS_BYTE (ASSIGN_X_REG t) = r t ^ "b" 85 | mem_rhs ACCESS_WORD (ASSIGN_X_CONST i) = Arbnum.toString i 86 | mem_rhs ACCESS_BYTE (ASSIGN_X_CONST i) = let 87 val imm8 = Arbnum.toInt i 88 val imm8 = if 128 <= imm8 then "-" ^ int_to_string (0 - (imm8 - 256)) else int_to_string imm8 89 in imm8 end 90 fun f (ASSIGN_EXP (d, ASSIGN_EXP_REG s)) = ["cmov? " ^ r d ^ ", " ^ r s] 91 | f (ASSIGN_EXP (d, ASSIGN_EXP_CONST i)) = ["mov " ^ r d ^ ", " ^ Arbnum.toString i] 92 | f (ASSIGN_EXP (d, ASSIGN_EXP_STACK i)) = ["mov " ^ r d ^ ", " ^ s i] 93 | f (ASSIGN_EXP (d, ASSIGN_EXP_BINOP (i,b,j))) = code_for_binop d b i j false 94 | f (ASSIGN_EXP (d, ASSIGN_EXP_MONOP (m,j))) = code_for_monop d m j 95 | f (ASSIGN_EXP (d, ASSIGN_EXP_MEMORY (ACCESS_WORD,a))) = ["MOV " ^ r d ^ ", " ^ address a] 96 | f (ASSIGN_EXP (d, ASSIGN_EXP_MEMORY (ACCESS_BYTE,a))) = ["MOVZX " ^ r d ^ ", BYTE " ^ address a] 97 | f (ASSIGN_EXP (d, ASSIGN_EXP_SHIFT_LEFT (j,n))) = code_for_shift d j n "shl" 98 | f (ASSIGN_EXP (d, ASSIGN_EXP_SHIFT_RIGHT (j,n))) = code_for_shift d j n "shr" 99 | f (ASSIGN_EXP (d, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (j,n))) = code_for_shift d j n "sar" 100 | f (ASSIGN_STACK (i,d)) = ["mov " ^ s i ^ ", " ^ mem_rhs ACCESS_WORD d] 101 | f (ASSIGN_MEMORY (b,a,d)) = [mov_name b ^ " " ^ address a ^ ", " ^ mem_rhs b d] 102 | f (ASSIGN_OTHER (t1,t2)) = fail() 103 in f end 104 105fun x64_guard2assembly (GUARD_NOT t) = let 106 val (code,(x,y)) = x64_guard2assembly t in (code,(y,x)) end 107 | x64_guard2assembly (GUARD_COMPARE (i,cmp,j)) = let 108 val rd = x64_reg i 109 fun f (ASSIGN_X_REG r) = x64_reg r 110 | f (ASSIGN_X_CONST c) = Arbnum.toString c 111 val code = ["cmp " ^ rd ^ ", " ^ f j] 112 fun g (GUARD_COMPARE_LESS false) = ("b","nb") 113 | g (GUARD_COMPARE_LESS true) = ("lt","ge") 114 | g (GUARD_COMPARE_LESS_EQUAL false) = ("na","a") 115 | g (GUARD_COMPARE_LESS_EQUAL true) = ("le","gt") 116 | g (GUARD_COMPARE_EQUAL) = ("e","ne") 117 in (code, g cmp) end 118 | x64_guard2assembly (GUARD_TEST (i,j)) = let 119 val rd = x64_reg i 120 fun f (ASSIGN_X_REG r) = x64_reg r 121 | f (ASSIGN_X_CONST c) = Arbnum.toString c 122 val code = ["test " ^ rd ^ ", " ^ f j] 123 in (code, ("e","ne")) end 124 | x64_guard2assembly (GUARD_EQUAL_BYTE (a,i)) = let 125 fun r i = x64_reg i 126 fun address (ASSIGN_ADDRESS_REG i) = "[" ^ r i ^ "]" 127 | address (ASSIGN_ADDRESS_OFFSET_ADD (d,i)) = "[" ^ r d ^ " + " ^ Arbnum.toString i ^ "]" 128 | address (ASSIGN_ADDRESS_OFFSET_SUB (d,i)) = "[" ^ r d ^ " - " ^ Arbnum.toString i ^ "]" 129 in (["cmp BYTE " ^ address a ^ ", " ^ Arbnum.toString i], ("e","ne")) end 130 | x64_guard2assembly (GUARD_OTHER tm) = let 131 val (t1,t2) = dest_eq tm 132 val code = hd (x64_assign2assembly (term2assign t1 t2)) 133 val code = "cmp" ^ (implode o tl o tl o tl o tl o tl o explode) code 134 in ([code], ("e","ne")) end; 135 136 137 138fun x64_conditionalise c condition = let 139 val c' = String.translate (fn x => if x = #"?" then condition else implode [x]) c 140 in if c = c' then fail() else c' end 141 142fun x64_remove_annotations c = 143 if String.substring(c,0,5) = "cmov?" then 144 "mov" ^ String.substring(c,5,size(c) - 5) 145 else c handle _ => c 146 147fun x64_cond_code tm = 148 (* zero *) if tm = ``zS1 Z_ZF`` then ("e","ne") else 149 (* sign *) if tm = ``zS1 Z_SF`` then ("s","ns") else 150 (* below *) if tm = ``zS1 Z_CF`` then ("b","nb") else fail() 151 152 153fun x64_encode_instruction s = 154 let val s = x64_encode s in (s, (size s) div 2) end 155 156fun x64_encode_branch_aux forward l cond = let 157 fun asm NONE = "jmp" 158 | asm (SOME c) = if mem c ["loop","loope","loopne"] then c else 159 if hd (explode c) = #"j" then c else "j" ^ c 160 val s = asm cond 161 fun address l = s ^ (if forward then " " else " -") ^ int_to_string l 162 fun find_encoding f l s = let 163 val v = f (l + size s div 2) 164 in if s = v then v else find_encoding f l v end 165 val i = (if forward then x64_encode (address l) 166 else find_encoding (x64_encode o address) l "") 167 in (i, (size i) div 2) end 168 169fun x64_flip_cond c = 170 if mem c ["ne","jne"] then "e" else 171 if mem c ["e","je"] then "ne" else 172 if mem c ["ns","jns"] then "s" else 173 if mem c ["s","js"] then "ns" else 174 if mem c ["na","jna"] then "a" else 175 if mem c ["a","ja"] then "na" else 176 if mem c ["nb","jnb"] then "b" else 177 if mem c ["b","jb"] then "nb" else fail() 178 179fun x64_encode_branch forward l cond = 180 x64_encode_branch_aux forward l cond handle HOL_ERR _ => 181 let (* The implementation of long conditional jumps assume 182 that short conditional jumps are 2 bytes in length, 183 and that long unconditional branches are 5 bytes. *) 184 fun the NONE = fail() | the (SOME x) = x 185 val c = x64_flip_cond (the cond) 186 val (xs,i) = x64_encode_branch_aux true 5 (SOME c) 187 val _ = if i = 2 then () else fail() 188 val l = if forward then l else l+2 189 val (ys,j) = x64_encode_branch_aux forward l NONE 190 in (xs ^ " " ^ ys, i + j) end 191 192fun x64_branch_to_string NONE = "jmp" 193 | x64_branch_to_string (SOME c) = "j" ^ c 194 195end; 196