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