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