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