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