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