1structure ppc_encodeLib :> ppc_encodeLib =
2struct
3
4open HolKernel boolLib bossLib;
5open ppc_decoderTheory;
6
7val car = fst o dest_comb;
8val cdr = snd o dest_comb;
9
10val instructions = let
11  fun foo tm = let val (x,y) = dest_comb tm in
12    foo x @ [stringSyntax.fromHOLstring (cdr y)] end
13    handle _ => [(implode o tl o explode o fst o dest_const) tm]
14  fun d (x,y) = let
15    val xs = (foo o snd o dest_abs) y
16    val (i,t) = (hd xs, tl xs)
17    val f = String.tokens (fn x => (x = #" ")) (stringSyntax.fromHOLstring x)
18    val i = (implode o map (fn x => if x = #"_" then #"." else x) o explode) i
19    in (i,(t,f)) end
20  in (map d o map pairSyntax.dest_pair o fst o
21      listSyntax.dest_list o cdr o cdr o concl o SPEC_ALL) ppc_decode_def end;
22
23fun ppc_encode s = let
24  fun token_size name =
25    if mem name ["A","B","C","D","S","BO","BI","crbA","crbB","crbD","SH","MB","ME"] then 5
26    else if mem name ["BD"] then 14
27    else if mem name ["SIMM","UIMM","d"] then 16
28    else if mem name ["LI"] then 24
29    else if mem name ["AA","Rc","OE","y","z"] then 1
30    else fail();
31  fun fill n s = if size s < n then fill n ("0" ^ s) else s
32  fun to_binary n i = let
33    val m = Arbnum.pow(Arbnum.fromInt 2, Arbnum.fromInt n)
34    val m2 = Arbnum.pow(Arbnum.fromInt 2, Arbnum.fromInt (n - 1))
35    val j = Arbint.+(i,Arbint.fromNat m)
36    in if Arbint.<=(Arbint.zero,i) then fill n (Arbnum.toBinString(Arbint.toNat i))
37                                   else fill n (Arbnum.toBinString(Arbint.toNat j))
38    end
39  val xs = String.tokens (fn x => mem x [#",",#" ",#"(",#")",#"[",#"]"]) s
40  val (x,xs) = (hd xs, tl xs)
41  val (x,xs) = if x = "bne" then ("bc",["4","2"] @ xs) else
42               if x = "beq" then ("bc",["12","2"] @ xs) else
43               if x = "blt" then ("bc",["12","0"] @ xs) else
44               if x = "bge" then ("bc",["4","0"] @ xs) else
45               if x = "bgt" then ("bc",["4","1"] @ xs) else
46               if x = "ble" then ("bc",["12","1"] @ xs) else (x,xs)
47  val (_,(y,z)) = hd (filter (fn y => (fst y = x)) instructions)
48  val qs = zip y xs
49  val ts = map (fn (t,q) => (t,to_binary (token_size t) (Arbint.fromString q))) qs
50  fun find [] c = c
51    | find ((x,y)::xs) c = if x = c then y else find xs c
52  val res = map (find ts) z
53  val res = map (fn x => if mem x ["z","y"] then "0" else x) res
54  val result = Arbnum.toHexString(Arbnum.fromBinString (concat res))
55  in result end;
56
57fun ppc_supported_instructions () = let
58  fun all_distinct [] = []
59    | all_distinct (x::xs) = x::all_distinct (filter (fn y => not ((x:string) = y)) xs)
60  val i = map fst instructions @ ["bne","beq","blt","bgt","bge","ble"]
61  val i = filter (fn x => not (mem x ["bt","bf"])) i
62  in all_distinct (sort (fn x => fn y => x < y) i) end;
63
64end
65