1structure x86_encodeLib :> x86_encodeLib =
2struct
3
4open HolKernel boolLib bossLib;
5open x86_decoderTheory;
6
7val car = fst o dest_comb;
8val cdr = snd o dest_comb;
9
10val instructions = let
11  fun div_at [] ys = (ys,[])
12    | div_at (x::xs) ys = if x = "|" then (rev ys,xs) else
13      div_at xs (x::ys)
14  fun d xs = div_at xs []
15  val t = String.tokens (fn x => mem x [#" ",#","])
16  in (map (d o t) o map stringSyntax.fromHOLstring o fst o
17     listSyntax.dest_list o cdr o cdr o concl o SPEC_ALL) x86_decode_aux_def end;
18
19fun parse_address s = let
20  val xs = explode s
21  val _ = if hd xs = #"[" then () else fail()
22  val _ = if last xs = #"]" then () else fail()
23  fun f c = String.tokens (fn x => x = c)
24  val ts = f #"+" (implode (butlast (tl xs)))
25  fun append_lists [] = []
26    | append_lists (x::xs) = x @ append_lists xs
27  fun minus [x] = [("+",x)]
28    | minus ["",x] = [("-",x)]
29    | minus [x,y] = [("+",x),("-",y)]
30    | minus (x::xs) = minus [x] @ minus xs
31    | minus _ = fail()
32  val zs = append_lists (map (minus o f #"-") ts)
33  fun prod [x] = (1,x)
34    | prod [x,y] = if can string_to_int x then (string_to_int x, y)
35                                          else (string_to_int y, x)
36    | prod _ = fail()
37  val qs = map (fn (s,n) => (s,prod (f #"*" n))) zs
38  fun g (c,(3,x)) = [(c,(1,x)),(c,(2,x))]
39    | g (c,(5,x)) = [(c,(1,x)),(c,(4,x))]
40    | g (c,(9,x)) = [(c,(1,x)),(c,(8,x))]
41    | g y = [y]
42  val us = append_lists (map g qs)
43  fun extract_int ("-",(1,x)) = Arbint.-(Arbint.zero,Arbint.fromString x)
44    | extract_int ("+",(1,x)) = Arbint.fromString x
45    | extract_int _ = fail()
46  fun sum [] = Arbint.zero | sum (i::is) = Arbint.+(i,sum is)
47  val imm = sum (map extract_int (filter (can extract_int) us))
48  val vs = filter (not o can extract_int) us
49  val _ = if filter (fn (x,y) => not (x = "+")) vs = [] then () else fail()
50  val ks = map snd vs
51  val base = SOME ((snd o hd o filter (fn (x,y) => x = 1)) ks) handle e => NONE
52  fun delete_base NONE xs = xs
53    | delete_base (SOME b) [] = []
54    | delete_base (SOME b) ((n,x)::xs) = if (1,b) = (n,x) then xs else (n,x) :: delete_base (SOME b) xs
55  val index = delete_base base ks
56  val index = SOME (hd index) handle e => NONE
57  in (index,base,imm) end;
58
59fun fill n s = if size s < n then fill n ("0" ^ s) else s
60
61fun unsigned_hex n s = let
62  val i = fill n (Arbnum.toHexString (Arbnum.fromString s))
63  val i = (substring(i,6,2) ^ substring(i,4,2) ^ substring(i,2,2) ^
64           substring(i,0,2)) handle e => i
65  in if size i = n then i else fail() end
66
67fun signed_hex n i = let
68  val m = Arbnum.pow(Arbnum.fromInt 2, Arbnum.fromInt (4 * n))
69  val m2 = Arbnum.pow(Arbnum.fromInt 2, Arbnum.fromInt (4 * n - 1))
70  val j = Arbint.+(i,Arbint.fromNat m)
71  val i = if not (Arbint.<(i,Arbint.fromNat m2)) then fail() else
72          if not (Arbint.<=(Arbint.fromNat m2, j)) then fail() else
73          if Arbint.<=(Arbint.zero,i) then fill n (Arbnum.toHexString(Arbint.toNat i))
74                                      else fill n (Arbnum.toHexString(Arbint.toNat j))
75  val i = (substring(i,6,2) ^ substring(i,4,2) ^ substring(i,2,2) ^
76           substring(i,0,2)) handle e => i
77  in i end
78
79fun x86_reg2int r = let
80  fun find x [] = fail()
81    | find x ((y,z)::ys) = if x = y then z else find x ys
82  val regs = ["EAX","ECX","EDX","EBX","ESP","EBP","ESI","EDI"]
83  val indx = [0,1,2,3,4,5,6,7]
84  val r = String.translate (fn x => implode [Char.toUpper x]) r
85  in find r (zip regs indx) end
86
87fun x86_address_encode s = let
88  val (index,base,imm) = parse_address s
89  val rr = int_to_string o x86_reg2int
90  fun the (SOME x) = x | the NONE = fail()
91  fun get_scale (SOME (1,i)) = [("Scale","0"),("Index",rr i)]
92    | get_scale (SOME (2,i)) = [("Scale","1"),("Index",rr i)]
93    | get_scale (SOME (4,i)) = [("Scale","2"),("Index",rr i)]
94    | get_scale (SOME (8,i)) = [("Scale","3"),("Index",rr i)]
95    | get_scale _ = fail()
96  fun f (index,base,disp) =
97    if index = NONE then
98      if base = NONE then
99        [("R/M","5"),("Mod","0"),("disp",signed_hex 8 disp)]
100      else if base = SOME "ESP" then
101        [("R/M",rr "ESP"),("Base","4"),("Index","4"),("Scale","0")] @
102        (if disp = Arbint.fromInt 0 then [("Mod","0")]
103         else if can (signed_hex 2) disp
104         then [("Mod","1"),("disp",signed_hex 2 disp)]
105         else [("Mod","2"),("disp",signed_hex 8 disp)])
106      else if (disp = Arbint.fromInt 0) andalso not (base = SOME "EBP") then
107        [("R/M",rr (the base)),("Mod","0")]
108      else if can (signed_hex 2) disp then
109        [("R/M",rr (the base)),("Mod","1"),("disp",signed_hex 2 disp)]
110      else
111        [("R/M",rr (the base)),("Mod","2"),("disp",signed_hex 8 disp)]
112    else
113      if base = NONE then
114        [("R/M",rr "ESP"),("Mod","2"),("Base","5"),("disp",signed_hex 8 disp)]
115        @ get_scale index
116      else if (disp = Arbint.fromInt 0) andalso not (base = SOME "EBP") then
117        [("R/M",rr "ESP"),("Mod","0"),("Base",rr (the base))] @ get_scale index
118      else if can (signed_hex 2) disp then
119        [("R/M",rr "ESP"),("Mod","1"),("Base",rr (the base))] @ get_scale index
120        @ [("disp",signed_hex 2 disp)]
121      else
122        [("R/M",rr "ESP"),("Mod","2"),("Base",rr (the base))] @ get_scale index
123        @ [("disp",signed_hex 8 disp)]
124  in f (index,base,imm) end
125
126fun x86_encode s = let
127  fun rem [] b ys = rev ys
128    | rem (x::xs) b ys =
129         if x = #"[" then rem xs true (x::ys) else
130         if x = #"]" then rem xs false (x::ys) else
131         if x = #" " then if b then rem xs b ys else rem xs b (x::ys) else
132           rem xs b (x::ys)
133  val s = implode (rem (explode s) false [])
134  val s = String.translate (fn x => implode [Char.toUpper x]) s
135  val xs = String.tokens (fn x => mem x [#" ",#","]) s
136  val ys = filter (fn (x,y) => ((hd y = hd xs) handle _ => false)) instructions
137  fun translate "r8" = "r32"
138    | translate "r/m8" = "r/m32"
139    | translate s = s
140  val (xs,ys) = if not (mem "BYTE" xs) then (xs,ys) else
141                  (filter (fn x => not (x = "BYTE")) xs,
142                   map (fn (x,y) => (x, map translate y))
143                   (filter (fn (x,y) => mem "r/m8" y) ys))
144  fun pos x [] = fail()
145    | pos x (y::ys) = if x = y then 0 else 1 + pos x ys
146  fun find x [] = fail()
147    | find x ((y,z)::ys) = if x = y then z else find x ys
148  val regs = ["EAX","ECX","EDX","EBX","ESP","EBP","ESI","EDI"]
149  fun try_all f [] = []
150    | try_all f (x::xs) = f x :: try_all f xs handle e => try_all f xs
151(*
152  val (zs,ys) = (hd) ys
153*)
154  fun use_encoding (zs,ys) = let
155    val l = filter (fn (x,y) => not (x = y)) (zip xs ys)
156    fun foo (y,x) =
157      if x = "imm32" then
158        [("id",unsigned_hex 8 y)]
159      else if x = "imm16" then
160        [("iw",signed_hex 4 (Arbint.fromString y))]
161      else if x = "imm8" then
162        [("ib",signed_hex 2 (Arbint.fromString y))]
163      else if x = "rel8" then
164        [("cb",signed_hex 2 (Arbint.fromString y))]
165      else if x = "rel32" then
166        [("cd",signed_hex 8 (Arbint.fromString y))]
167      else if x = "r32" then
168        [("Reg/Opcode",int_to_string (pos y regs))]
169      else if (x = "r/m32") andalso (mem y regs) then
170        [("R/M",int_to_string (pos y regs)),("Mod","3")]
171      else if ((x = "r/m32") orelse (x = "m")) andalso can x86_address_encode y then
172        x86_address_encode y
173      else fail()
174    fun list_append [] = [] | list_append (x::xs) = x @ list_append xs
175    val ts = list_append (map foo l)
176    fun create_SIB xs =
177      (fill 2 o Arbnum.toHexString o Arbnum.fromInt)
178      (string_to_int (find "Base" xs) +
179       string_to_int (find "Index" xs) * 8 +
180       string_to_int (find "Scale" xs) * 8 * 8) handle _ => ""
181    fun create_ModRM xs =
182      (fill 2 o Arbnum.toHexString o Arbnum.fromInt)
183      (string_to_int (find "R/M" xs) +
184       string_to_int (find "Reg/Opcode" xs) * 8 +
185       string_to_int (find "Mod" xs) * 8 * 8) ^
186      create_SIB xs ^ (find "disp" ts handle e => "")
187    fun is_plus x = (implode (tl (tl (explode x))) = "+rd") handle _ => false
188    fun do_replace x =
189      if mem x ["id","iw","ib","cb","cw","cd"] then find x ts else
190      if is_plus x then let
191        val reg = Arbnum.fromString(find "Reg/Opcode" ts)
192        val s = implode [hd (explode x), hd (tl (explode x))]
193        in Arbnum.toHexString(Arbnum.+(Arbnum.fromHexString s, reg)) end else
194      if can Arbnum.fromHexString x then x else
195      if x = "/r" then create_ModRM ts else
196      if hd (explode x) = #"/" then
197        create_ModRM (("Reg/Opcode",(implode o tl o explode) x)::ts)
198      else fail()
199    val e = concat (map do_replace zs)
200    in e end;
201  val all = try_all use_encoding ys
202  val e = hd (sort (fn x => fn y => size x <= size y) all)
203  in e end
204
205fun x86_supported_instructions () = let
206  fun all_distinct [] = []
207    | all_distinct (x::xs) = x::all_distinct (filter (fn y => not ((x:string) = y)) xs)
208  in all_distinct (map (fn (x,y) => hd y) instructions) end;
209
210
211end
212