1structure exportLib :> exportLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5open helperLib graph_specsLib backgroundLib writerLib;
6open GraphLangTheory;
7
8
9(* exporter state *)
10
11val failed_ty_translations = ref ([]:hol_type list);
12val failed_tm_translations = ref ([]:term list);
13
14
15(* recording errors *)
16
17local
18  fun head_of t = fst (strip_comb t)
19  fun print_ty_fail ty = let
20    val _ = print "FAILED to translate type: "
21    val _ = print_type ty
22    val _ = print "\n"
23    in () end;
24  fun print_tm_fail tm = let
25    val _ = print "FAILED to translate term: "
26    val _ = print_term tm
27    val _ = (print "\n\nwith head: "; print_term (head_of tm))
28    val _ = (print "\nwith type: "; print_type (type_of tm); print "\n\n")
29    in () end;
30in
31  fun add_ty_fail ty = let
32    val _ = (failed_ty_translations := ty::(!failed_ty_translations))
33    in print_ty_fail ty end
34  fun add_tm_fail tm = let
35    val _ = (failed_tm_translations := tm::(!failed_tm_translations))
36    in print_tm_fail tm end
37end
38
39
40(* syntax functions *)
41
42fun dest_graph tm =
43  if can (match_term ``graph (xs:('a # 'b) list)``) tm then let
44    val (x,y) = dest_comb tm
45    fun f (x,y) = (numSyntax.int_of_term x, y)
46    in listSyntax.dest_list y |> fst |> map (f o pairSyntax.dest_pair) end
47    handle HOL_ERR _ => failwith "dest_graph"
48  else failwith "dest_graph"
49
50fun dest_str_graph tm =
51  if can (match_term ``graph (xs:('a # 'b) list)``) tm then let
52    val (x,y) = dest_comb tm
53    fun f (x,y) = (stringSyntax.fromHOLstring x, y)
54    in listSyntax.dest_list y |> fst |> map (f o pairSyntax.dest_pair) end
55    handle HOL_ERR _ => failwith "dest_graph"
56  else failwith "dest_graph"
57
58fun dest_string_list tm = let
59  val (xs,ty) = listSyntax.dest_list tm
60  val _ = (ty = ``:string``) orelse fail()
61  val ys = map stringSyntax.fromHOLstring xs
62  in ys end handle HOL_ERR _ => failwith "dest_string_list"
63
64local
65  val pat = ``GraphFunction inps outps gg ep``
66in
67  fun dest_GraphFunction tm = let
68    val _ = can (match_term pat) tm orelse fail()
69    val ep = tm |> rand |> numSyntax.int_of_term
70    val gs = tm |> rator |> rand |> dest_graph
71    val ys = tm |> rator |> rator |> rand |> dest_string_list
72    val xs = tm |> rator |> rator |> rator |> rand |> dest_string_list
73    in (xs,ys,gs,ep) end
74end
75
76local
77  val pat = ``Basic n xs``
78in
79  fun dest_Basic tm = let
80    val _ = can (match_term pat) tm orelse fail()
81    val next = tm |> rator |> rand
82    val (xs,ty) = tm |> rand |> listSyntax.dest_list
83    val _ = (ty = ``:string # (state -> variable)``) orelse fail()
84    val ys = xs |> map pairSyntax.dest_pair
85                |> map (fn (x,y) => (stringSyntax.fromHOLstring x,y))
86    in (next,ys) end
87end
88
89local
90  val pat = ``Cond n1 n2 p``
91in
92  fun dest_Cond tm = let
93    val _ = can (match_term pat) tm orelse fail()
94    val next1 = tm |> rator |> rator |> rand
95    val next2 = tm |> rator |> rand
96    val tm = tm |> rand
97    in (next1,next2,tm) end
98end
99
100local
101  val pat = ``Call next name args strs``
102in
103  fun dest_Call tm = let
104    val _ = can (match_term pat) tm orelse fail()
105    val next = tm |> rator  |> rator  |> rator |> rand
106    val (strs,ty) = tm |> rand |> listSyntax.dest_list
107    val _ = (ty = ``:string``) orelse fail()
108    val strs = strs |> map stringSyntax.fromHOLstring
109    val name = tm |> rator |> rator |> rand |> stringSyntax.fromHOLstring
110    val (args,ty) = tm |> rator |> rand |> listSyntax.dest_list
111    val _ = (ty = ``:state -> variable``) orelse fail()
112    in (next,name,args,strs) end
113end
114
115local
116  val pat = ``NextNode n``
117in
118  fun dest_NextNode tm = let
119    val _ = can (match_term pat) tm orelse fail()
120    val next = tm |> rand |> numSyntax.int_of_term
121    in next end
122end
123
124local
125  val pat = ``var_acc str``
126in
127  fun dest_var_acc tm = let
128    val _ = can (match_term pat) tm orelse fail()
129    in tm |> rand |> stringSyntax.fromHOLstring end
130end
131
132local
133  val pat = ``SKIP_TAG str``
134in
135  fun dest_SKIP_TAG tm = let
136    val _ = can (match_term pat) tm orelse fail()
137    in tm |> rand |> stringSyntax.fromHOLstring end
138end
139
140local
141  fun any_var_acc pat = fn tm => let
142    val _ = can (match_term pat) tm orelse fail()
143    val x1 = tm |> rator |> rand |> stringSyntax.fromHOLstring
144    val x2 = tm |> rand
145    in (x1,x2) end
146in
147  val dest_var_word32 = any_var_acc ``var_word32 str s``
148  val dest_var_word8 = any_var_acc ``var_word8 str s``
149  val dest_var_nat = any_var_acc ``var_nat str s``
150  val dest_var_bool = any_var_acc ``var_bool str s``
151  val dest_var_mem = any_var_acc ``var_mem str s``
152  val dest_var_dom = any_var_acc ``var_dom str s``
153end;
154
155
156(* export to Graph's graph format *)
157
158val patterns =
159     [(``MemAcc8 m a``,"MemAcc"),
160      (``MemAcc32 m a``,"MemAcc"),
161      (``MemUpdate8 m a w``,"MemUpdate"),
162      (``MemUpdate32 m a w``,"MemUpdate"),
163      (``x = (y:'a)``,"Equals"),
164      (``T``,"True"),
165      (``F``,"False"),
166      (``~(b:bool)``,"Not"),
167      (``word_1comp (x:'a word)``,"BWNot"),
168      (``word_add (x:'a word) y``,"Plus"),
169      (``word_sub (x:'a word) y``,"Minus"),
170      (``word_mul (x:'a word) y``,"Times"),
171      (``word_and (x:'a word) y``,"BWAnd"),
172      (``word_or (x:'a word) y``,"BWOr"),
173      (``word_xor (x:'a word) y``,"BWXOR"),
174      (``ShiftLeft (x:'a word) y``,"ShiftLeft"),
175      (``ShiftRight (x:'a word) y``,"ShiftRight"),
176      (``SignedShiftRight (x:'a word) y``,"SignedShiftRight"),
177      (``x ==> y:bool``,"Implies"),
178      (``x /\ y:bool``,"And"),
179      (``x \/ y:bool``,"Or"),
180      (``(x:'a word) < y``,"SignedLess"),
181      (``(x:'a word) <+ y``,"Less"),
182      (``(x:'a word) <= y``,"SignedLessEquals"),
183      (``(x:'a word) <=+ y``,"LessEquals"),
184      (``(x:'a word) IN y``,"MemDom"),
185      (``(w2w (x:'a word)):'b word``,"WordCast"),
186      (``(sw2sw (x:'a word)):'b word``,"WordCastSigned"),
187      (``(n:num) + m``,"Plus"),
188      (``if b then x else y : 'a``,"IfThenElse"),
189      (``word_reverse (x:'a word)``,"WordReverse"),
190      (``count_leading_zero_bits (w:'a word)``,"CountLeadingZeroes")];
191
192val last_fail_node_tm = ref T;
193
194fun export_graph name rhs = let
195  fun int_to_hex i =
196    "0x" ^ Arbnumcore.toHexString (Arbnum.fromInt i)
197  fun get_var_type "mem" = "Mem"
198    | get_var_type "dom" = "Dom"
199    | get_var_type "stack" = "Mem"
200    | get_var_type "dom_stack" = "Dom"
201    | get_var_type "n" = "Bool"
202    | get_var_type "z" = "Bool"
203    | get_var_type "c" = "Bool"
204    | get_var_type "v" = "Bool"
205    | get_var_type "clock" = "Word 64"
206    | get_var_type _ = "Word 32"
207  fun arg s = "" ^ s ^ " " ^ get_var_type s
208  fun commas [] = ""
209    | commas [x] = x
210    | commas (x::xs) = x ^ " " ^ commas xs
211  fun export_list xs = int_to_string (length xs) ^ " " ^ commas xs
212  fun export_type ty = case total dest_type ty of
213    SOME ("cart", [_, idx]) => "Word "
214        ^ Arbnum.toString (fcpLib.index_to_num idx)
215  | _ => if ty = ``:word32->word8`` then "Mem" else
216    if ty = ``:word32->bool`` then "Dom" else
217    if ty = ``:bool`` then "Bool" else
218    if ty = ``:num`` then "Word 64" else failwith("type")
219  fun is_var_acc tm =
220    can dest_var_word32 tm orelse
221    can dest_var_word8 tm orelse
222    can dest_var_nat tm orelse
223    can dest_var_bool tm orelse
224    can dest_var_mem tm orelse
225    can dest_var_dom tm
226  fun match_pattern tm [] = fail()
227    | match_pattern tm ((pat,name)::xs) =
228        if not (can (match_term pat) tm) then match_pattern tm xs else let
229          val (s1,s2) = match_term pat tm
230          val cs = filter is_var (list_dest dest_comb pat)
231          in (name,map (subst s1 o inst s2) cs) end
232  fun term tm =
233    (* Num *)
234    (if numSyntax.is_numeral tm then
235      "Num " ^ int_to_string (tm |> numSyntax.int_of_term) ^ " Nat"
236    else if wordsSyntax.is_n2w tm then
237      let val i = tm |> rand |> numSyntax.int_of_term
238      in "Num " ^ int_to_string i ^ " " ^ export_type (type_of tm) end
239    (* Var *)
240    else if is_var_acc tm then
241      let val name = tm |> rator |> rand |> stringSyntax.fromHOLstring
242      in "Var " ^ name ^ " " ^ export_type (type_of tm) end
243    (* Op *)
244    else let
245      val (n,xs) = match_pattern tm patterns
246      val ty = export_type (type_of tm)
247      in "Op " ^ n ^ " " ^ ty ^ " " ^ export_list (map term xs) end
248    ) handle HOL_ERR err => (print (exn_to_string (HOL_ERR err));
249            add_tm_fail tm; fail())
250  val types = [``VarNat``,``VarWord8``,``VarWord32``,
251               ``VarMem``,``VarDom``,``VarBool``]
252  val s_var = mk_var("s",``:state``)
253  fun bool_exp tm =
254    if can dest_var_acc tm then let
255      val n = dest_var_acc tm
256      in "Var " ^ n ^ " " ^ get_var_type n end
257    else let
258      val (s,e) = dest_abs tm
259      val _ = type_of s = ``:state`` orelse failwith("bad exp")
260      val _ = type_of e = ``:bool`` orelse failwith("bad exp")
261      in term e end
262  fun exp tm =
263    if can dest_var_acc tm then let
264      val n = dest_var_acc tm
265      in "Var " ^ n ^ " " ^ get_var_type n end
266    else let
267      val (s,e) = dest_abs tm
268      val _ = type_of s = ``:state`` orelse failwith("bad exp")
269      val (t,tm) = dest_comb e
270      val _ = mem t types
271      in term tm end
272  fun dest_abs_skip_tag test = let
273    val (v,x) = dest_abs test
274    val n = dest_SKIP_TAG x
275    in n end
276  fun assign_var (n,tm) =
277    "" ^ n ^ " " ^ get_var_type n ^ " " ^ exp tm
278  val ret_node = ``Ret``
279  val err_node = ``Err``
280  fun export_nextnode tm =
281    if tm = ret_node then "Ret" else
282    if tm = err_node then "Err" else let
283      val i = dest_NextNode tm
284      in int_to_hex i end
285  fun export_node (n,tm) = let
286    val (next,assign) = dest_Basic tm
287    in commas [int_to_hex n,"Basic",export_nextnode next,
288               export_list (map assign_var assign)] ^ "\n" end
289    handle HOL_ERR _ => let
290    val (next1,next2,test) = dest_Cond tm
291    in if can dest_abs_skip_tag test then
292         "# " ^ int_to_hex n ^ " node is " ^
293         dest_abs_skip_tag test ^ "\n" ^
294         commas [int_to_hex n,"Cond",
295                 export_nextnode next1,
296                 export_nextnode next2,
297                 "Op UnspecifiedPrecond Bool 0"] ^ "\n"
298       else
299         commas [int_to_hex n,"Cond",
300                 export_nextnode next1,
301                 export_nextnode next2,
302                 bool_exp test] ^ "\n" end
303    handle HOL_ERR _ => let
304    val (next,func_name,input,output) = dest_Call tm
305    in commas [int_to_hex n,"Call",
306               export_nextnode next,
307               func_name,
308               export_list (map exp input),
309               export_list (map arg output)] ^ "\n" end
310  val rhs = rhs |> QCONV (REWRITE_CONV [graph_format_preprocessing])
311                |> concl |> rand
312  val (input,output,nodes,entry) = dest_GraphFunction rhs
313  val decl = "Function " ^ name ^ " " ^
314                export_list (map arg input) ^ " " ^
315                export_list (map arg output) ^ "\n"
316  val _ = write_graph decl
317  fun my_map f [] = []
318    | my_map f (x::xs) =
319    (let val y = f x in y end
320     handle HOL_ERR e =>
321     let val _ = print "\n\nFailed to translate node: \n\n"
322         val _ = print_term (snd x)
323         val _ = print "\n\n"
324         val _ = (last_fail_node_tm := snd x)
325     in raise (HOL_ERR e) end) :: my_map f xs
326  val _ = my_map (write_graph o export_node) nodes
327  val last_line = "EntryPoint " ^ int_to_hex entry ^ "\n"
328  val _ = if List.null nodes then () else write_graph last_line
329  in () end
330
331
332(* export constant definition *)
333
334fun export_func lemma = let
335  val (lhs,rhs) = lemma |> concl |> dest_eq
336  val name = lhs |> dest_const |> fst |> clean_name
337  val _ = export_graph name rhs
338  in "define_" ^ name end
339
340
341(* print export report *)
342
343fun print_export_report () = let
344  val l = length (!failed_ty_translations) + length (!failed_tm_translations)
345  in if l = 0 then write_line "No export failures." else let
346       val xs = map (fn ty => "Failed to translate type: " ^ type_to_string ty)
347                       (all_distinct (!failed_ty_translations)) @
348                map (fn tm => "Failed to translate term: " ^ term_to_string tm)
349                       (all_distinct (!failed_tm_translations))
350       in (map write_line xs; ()) end end
351
352
353(* conv used by func_decompiler *)
354
355val prepare_for_export_conv = let
356  fun unbeta_conv pat tm =
357    if is_comb tm andalso can (match_term pat) (rand tm) then let
358      val ty = rand tm |> type_of |> dest_type |> snd |> hd
359      in (RAND_CONV (REWR_CONV (GSYM ETA_AX))) tm end else NO_CONV tm
360  val foldback = (unbeta_conv ``var_bool str``) ORELSEC
361                 (unbeta_conv ``var_word32 str``) ORELSEC
362                 (unbeta_conv ``var_word8 str``) ORELSEC
363                 (unbeta_conv ``var_nat str``) ORELSEC
364                 (unbeta_conv ``var_mem str``) ORELSEC
365                 (unbeta_conv ``var_dom str``)
366  val c = PURE_REWRITE_CONV [decomp_simp1,all_names_def,
367            ret_and_all_names_def,
368            all_names_ignore_def, all_names_with_input_def] THENC
369          PURE_REWRITE_CONV [decomp_simp2] THENC
370          PURE_REWRITE_CONV [decomp_simp3] THENC
371          PURE_REWRITE_CONV [GSYM wordsTheory.WORD_NOT_LOWER] THENC
372          DEPTH_CONV foldback
373  in QCONV c end;
374
375end
376