1structure export_codeLib :> export_codeLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5
6open wordsTheory wordsLib helperLib;
7
8fun write_code_to_file filename th = let
9  val _ = print ("Extracting machine code to file \"" ^ filename ^ "\", ")
10  fun int_to_hexstring n = "0x" ^ (Arbnum.toHexString o Arbnum.fromInt) n
11  val (m,pre,c,post) = (dest_spec o concl) th
12  val model_name = fst (dest_const m)
13  val cs = (list_dest pred_setSyntax.dest_insert c)
14  val _ = pred_setSyntax.is_empty (last cs) orelse (print ("\n\nCode does not end in empty set. Found:\n\n"^ (term_to_string (last cs)) ^"\n\n"); fail())
15  val cs = butlast cs
16  val vs = map (pairSyntax.dest_pair) cs
17  val vs = map (fn (x,y) => (x,fst (pairSyntax.dest_pair y) handle e => y)) vs
18  val vs = map (fn (x,y) => (if is_var x then ``0:num`` else
19                             if wordsSyntax.is_word_add x then cdr (cdr x) else
20                               (print ("\n\nBad address: "^(term_to_string x)^"\n\n"); fail()),y)) vs
21  val vs = map (fn (x,y) => (Arbnum.toInt (numSyntax.dest_numeral x),y)) vs
22  val vs = sort (fn (x,_) => fn (y:int,_) => x <= y) vs
23  fun del_repetations (x::y::xs) =
24        if pair_eq equal aconv x y then del_repetations (x::xs)
25        else x :: del_repetations (y::xs)
26    | del_repetations zs = zs
27  val vs = del_repetations vs
28  fun no_duplicates (x::y::xs) =
29      if fst x = fst y then
30        (print ("\n\nDuplication at " ^ (int_to_hexstring (fst x)) ^ ": " ^
31                (term_to_string (snd x)) ^ " and " ^ (term_to_string (snd y)) ^
32                "\n\n"); fail())
33      else no_duplicates (y::xs)
34    | no_duplicates _ = true
35  val _ = no_duplicates vs
36  fun term_byte_size tm =
37    if type_of tm = ``:word8`` then 1 else
38    if type_of tm = ``:word32`` then 4 else
39      foldr (fn (x,y) => x + y) 0 (map term_byte_size (fst (listSyntax.dest_list tm)))
40  fun no_holes i [] = true
41    | no_holes i ((j,c)::xs) =
42       if i = j then no_holes (i + (term_byte_size c)) xs
43       else (print ("\n\nNo code at location: "^(int_to_hexstring i)^
44                    " (next instruction: "^(int_to_hexstring j)^")\n\n");fail())
45  val _ = no_holes 0 vs
46  val byte_count = ref 0;
47  val big_endian_format = ``[(w2w ((w:word32) >>> 24)):word8;
48                             (w2w ((w:word32) >>> 16)):word8;
49                             (w2w ((w:word32) >>> 8)):word8;
50                             (w2w ((w:word32) >>> 0)):word8]``
51  val little_endian_format = ``[(w2w ((w:word32) >>> 0)):word8;
52                                (w2w ((w:word32) >>> 8)):word8;
53                                (w2w ((w:word32) >>> 16)):word8;
54                                (w2w ((w:word32) >>> 24)):word8]``
55  val format_tm = if model_name = "PPC_MODEL" then big_endian_format else little_endian_format
56  val vs = map (fn (x,y) => (x,(cdr o concl o EVAL o subst [``w:word32``|->y]) format_tm handle e => y)) vs
57  fun fill c d n s = if size s < n then fill c d n (c ^ s ^ d) else s
58  fun word2hex tm = let
59    val _ = (byte_count := !byte_count + (if type_of tm = ``:word8`` then 1 else 4))
60    val s = Arbnum.toHexString (numSyntax.dest_numeral (cdr tm))
61    in "0x" ^ fill "0" "" (if type_of tm = ``:word8`` then 2 else
62                           if type_of tm = ``:word32`` then 8 else fail()) s end
63  fun word2string tm = let
64    val (tms,ty) = if listSyntax.is_list tm
65                   then listSyntax.dest_list tm
66                   else ([tm],type_of tm)
67    val str = if ty = ``:word8`` then "\t.byte\t" else
68              if ty = ``:word32`` then "\t.word\t" else fail()
69    fun foo [] = fail()
70      | foo [x] = word2hex x ^ "\n"
71      | foo (x::y::ys) = word2hex x ^ ", " ^ foo (y::ys)
72    in str ^ foo tms end
73  val rs = map (word2string o snd) vs
74  val instr_count = length rs
75  val size_count = (!byte_count)
76  val l1 = "Machine code automatically extracted from a HOL4 theorem."
77  val l2 = "The code consists of " ^ int_to_string instr_count ^ " instructions (" ^ int_to_string size_count ^ " bytes)."
78  val l3 = "End of automatically extracted machine code."
79  val o1 = "\t/*  " ^ l1 ^ "  */\n"
80  val o2 = "\t/*  " ^ fill "" " " (size l1) l2 ^ "  */\n"
81  val o3 = "\t/*  " ^ fill "" " " (size l1) l3 ^ "  */\n"
82  val output = ["\n","\n",o1,o2,"\n"] @ rs @ ["\n",o3,"\n"]
83  (* val _ = map print output *)
84  (* write to text file *)
85  val t = TextIO.openOut(filename)
86  val _ = map (fn s => TextIO.output(t,s)) output
87  val _ = TextIO.closeOut(t)
88  val _ = print "done.\n"
89  in () end;
90
91end
92