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