1structure x64_codegenLib :> x64_codegenLib = 2struct 3 4open HolKernel boolLib bossLib Parse decompilerLib; 5open x64_codegen_inputLib helperLib; 6 7open x64_codegen_x64Lib; 8open prog_x64Lib; 9 10val assembler_tools = (x64_encode_instruction, x64_encode_branch, x64_branch_to_string) 11val conditional_tools = (x64_cond_code, x64_conditionalise, x64_remove_annotations) 12val generator_tools = (x64_assign2assembly, x64_guard2assembly) 13 14 15 16 17 18(* data-type used inside the code generator *) 19 20datatype asm_type = 21 ASM_ASSIGN of term * term (* lhs, rhs *) 22 | ASM_BRANCH of string option * string (* condition option, label name *) 23 | ASM_COMPARE of term (* e.g. ``r1 = r2`` *) 24 | ASM_INSERT of string * int * (string * string) option 25 (* name in !decompiler_memory, code length, option comparsion result code (true,false) *) 26 | ASM_INSTRUCTION of string * string * (string * string) option 27 (* concrete instruction, option comparsion result code (true,false) *) 28 | ASM_LABEL of string (* label name *); 29 30 31 32(* assembler *) 33 34fun list_append [] = [] | list_append (x::xs) = x @ list_append xs 35 36fun basic_assembler code3 = let 37 val (enc,branch,_) = assembler_tools 38 (* translate into machine code *) 39 fun extend (s,i) = if size s < 2 * i then extend ("0" ^ s, i) else s 40 fun split_at p [] ys = (implode (rev ys),"") 41 | split_at p (x::xs) ys = if p x then (implode (rev ys),implode (x::xs)) 42 else split_at p xs (x::ys) 43 fun better_encode x = let 44 val (x1,x2) = split_at (fn c => c = #"/") (explode x) [] 45 in extend (enc x1) ^ x2 end 46 fun translate (ASM_INSTRUCTION (x,z,y),q) = 47 if x = "" then (ASM_INSTRUCTION (x,z,y),q) 48 else (ASM_INSTRUCTION (better_encode x,z,y),q) 49 | translate x = x 50 val code4 = map translate code3 51 (* replace gotos, first with nothing, then regenerate iteratively until no change *) 52 fun dummy_jumps x = (x,"") 53 fun jump_length label (((ASM_INSERT (x,y,_),_) ,_)::xs) = y + jump_length label xs 54 | jump_length label (((ASM_INSTRUCTION (x,_,_),_) ,_)::xs) = (size(x) div 2) + jump_length label xs 55 | jump_length label (((ASM_BRANCH (_,_),_) ,x)::xs) = (size(x) div 2) + jump_length label xs 56 | jump_length label (((ASM_LABEL label2,_) ,_)::xs) = if label = label2 then 0 else jump_length label xs 57 | jump_length label _ = fail() 58 fun generate_jumps xs [] = rev xs 59 | generate_jumps xs (((ASM_BRANCH (c,label),s),_) :: ys) = let 60 val jump = branch false (jump_length label xs) c handle HOL_ERR _ => 61 branch true (jump_length label ys) c 62 in generate_jumps (((ASM_BRANCH (c,label),s), extend jump) :: xs) ys end 63 | generate_jumps xs (y::ys) = generate_jumps (y :: xs) ys 64 fun gencode_for_jumps code = generate_jumps [] code 65 fun find_fixpoint f x = let val y = f x in if x = y then x else find_fixpoint f y end 66 val code5 = find_fixpoint gencode_for_jumps (map dummy_jumps code4) 67 (* pull out the generated machine code *) 68 fun get_code ((ASM_INSTRUCTION (x,z,_),s),_) = [(x^z,s)] 69 | get_code ((ASM_INSERT (x,_,_),s),_) = [("insert:"^x,SOME "")] 70 | get_code ((ASM_BRANCH (_,_),s),x) = [(x,s)] 71 | get_code _ = [] 72 val code6 = list_append (map get_code code5) 73 fun ff (x,NONE) = (x,"") | ff (x,SOME y) = (x,y) 74 val code7 = map ff code6 75 val result = filter (fn x => not (x = "")) (map fst code6) 76 val len = jump_length "::" (code5 @ [((ASM_LABEL "::",NONE),"")]) 77 val result = list_append (map (String.tokens (fn x => x = #" ")) result) 78 in (result,len,code7) end 79 80fun quote_to_strings q = let (* turns a quote `...` into a list of strings *) 81 fun get_QUOTE (QUOTE t) = t | get_QUOTE _ = fail() 82 val xs = explode (get_QUOTE (hd q)) 83 fun strip_comments l [] = [] 84 | strip_comments l (x::xs) = 85 if x = #"(" then strip_comments (l+1) xs else 86 if x = #")" then strip_comments (l-1) xs else 87 if 0 < l then strip_comments l xs else x :: strip_comments l xs 88 fun strip_space [] = [] 89 | strip_space (x::xs) = 90 if mem x [#" ",#"\t",#"\n"] then strip_space xs else x::xs 91 fun lines [] [] = [] 92 | lines xs [] = [implode ((rev (strip_space xs)))] 93 | lines xs (y::ys) = 94 if mem y [#"\n",#"|"] 95 then implode ((rev (strip_space xs))) :: lines [] ys 96 else lines (y::xs) ys 97 fun delete_empty (""::xs) = delete_empty xs 98 | delete_empty xs = xs 99 val ys = (strip_comments 0) xs 100 in (rev o delete_empty o rev o delete_empty o lines []) ys end; 101 102fun assemble code = let 103 fun replace_char c str = 104 String.translate (fn x => if x = c then str else implode [x]); 105 fun f s = (String.fields (fn x => x = #":") s,s) 106 val ys = map f (quote_to_strings code) 107 fun space s = replace_char #" " "" s 108 fun process ([],s) = fail() 109 | process ([x],s) = 110 if (String.substring(space(x),0,6) = "insert" handle e => false) then let 111 val name = space(String.substring(space(x),6,size((space(x)))-6)) 112 val (_,code_length,_) = get_decompiled name 113 in [(ASM_INSERT(name,code_length,NONE),SOME s)] end 114 else [(ASM_INSTRUCTION (x,"",NONE),SOME s)] 115 | process ((y::x::xs),s) = (ASM_LABEL (space y),NONE) :: process ((x::xs),s) 116 val ys = map process ys 117 fun spaces [] = 0 | spaces (x::xs) = if x = #" " then 1 + spaces xs else 0 118 fun max [] = fail() 119 | max [x] = x 120 | max (x::y::xs) = let val m = max (y::xs) in if x < m then m else x end 121 fun get_spaces NONE = 0 | get_spaces (SOME x) = spaces (explode x) 122 val m = max (map (get_spaces o snd o last) ys) 123 fun repeatc n c = if n = 0 then [] else c :: repeatc (n-1) c 124 val str = implode (repeatc m #" ") 125 fun option_concat s NONE = NONE 126 | option_concat s (SOME t) = SOME (t ^ s) 127 val ys = list_append ys 128 val zs = map (fn (x,y) => (x, option_concat str y)) ys 129 fun labels (ASM_LABEL l) = [l] | labels _ = [] 130 val ls = list_append (map (labels o fst) zs) 131 fun create_branch x = let 132 val ts = String.tokens (fn x => mem x [#" ",#","]) x 133 val _ = if mem (last ts) ls then () else fail() 134 in ASM_BRANCH (SOME (hd ts),last ts) end 135 fun foo (ASM_INSTRUCTION (x,y,z),s) = ((create_branch x handle _ => ASM_INSTRUCTION (x,y,z)),s) 136 | foo qq = qq 137 val qs = map foo zs 138 fun h (SOME x) = [x] | h _ = [] 139 val n = max (map size (list_append (map (h o snd) qs))) 140 fun hh (x,NONE) = (x,NONE) | hh (x,SOME s) = (x, SOME ("(* " ^ s ^ implode (repeatc (n - size(s)) #" ") ^ " *)")) 141 val code3 = map hh qs 142 val (result,_,xs) = basic_assembler code3 143 val m = max (map (size o fst) xs) 144 val ys = map (fn (s,v) => " " ^ s ^ implode (repeatc (m - size(s)) #" ") ^ " " ^ v ^ "\n") xs 145 val _ = print "\n\n" 146 val _ = map print ys 147 val _ = print "\n\n" 148 in result end 149 150 151(* methods for loading in theorems for use in compilation *) 152 153val compiler_assignments = ref ([]: (term * term * int * string * string) list); 154val compiler_conditionals = ref ([]: (term * term * int * string * string) list); 155 156fun add_compiler_assignment tm1 tm2 name len model_name = 157 (compiler_assignments := (tm1,tm2,len,name,model_name) :: (!compiler_assignments)); 158 159fun print_compiler_grammar () = let 160 val xs = !compiler_assignments 161 fun f (x,y,_,_,m) = " " ^ m ^ ": let "^(term_to_string x)^" = "^(term_to_string y)^" in _\n" 162 val assign = map f xs 163 val xs = !compiler_conditionals 164 fun f (x,_,_,_,m) = " " ^ m ^ ": if "^(term_to_string (repeat dest_neg x))^" then _ else _\n" 165 val cond = map f xs 166 val sorter = sort (curry (fn (x:string,y:string) => x <= y)) 167 val _ = print "\nAssignments:\n\n" 168 val _ = map print (sorter assign) 169 val _ = print "\nConditionals:\n\n" 170 val _ = map print (sorter cond) 171 val _ = print "\n" 172 in () end; 173 174fun get_model_name th = let 175 val (m,_,_,_) = (dest_spec o concl o UNDISCH_ALL o SPEC_ALL) th 176 in fst (dest_const m) end; 177 178fun get_tools th = let 179 val s = get_model_name th 180 in if s = "X64_MODEL" then prog_x64Lib.x64_tools else fail() end 181 182fun add_assignment (tm1,tm2,th,len) = let 183 val (_,_,_,pc) = get_tools th 184 val pc_ty = (hd o snd o dest_type o type_of) pc 185 val th = RW [GSYM progTheory.SPEC_MOVE_COND] (DISCH_ALL th) 186 val thx = CONV_RULE (PRE_CONV (SIMP_CONV (std_ss++sep_cond_ss) [])) th 187 val thx = UNDISCH_ALL (RW [progTheory.SPEC_MOVE_COND] thx) 188 val (m,p,_,q) = (dest_spec o concl o SPEC_ALL) thx 189 val m = get_model_name thx 190 val name = ("AUTO_"^m^"_ASSIGN_"^(int_to_string (length (!compiler_assignments)))) 191 val _ = (compiler_assignments := (tm1,tm2,len,name,m) :: (!compiler_assignments)) 192 val dest_tuple = list_dest pairSyntax.dest_pair 193 val ys = zip (dest_tuple tm1) (dest_tuple tm2) handle e => [(tm1,tm2)] 194 val ys = filter (fn (x,y) => not (x = y)) ys 195 val post = cdr (find_term (can (match_term (mk_comb(pc,genvar(pc_ty))))) q) 196 val tm2 = subst [mk_var("p",pc_ty) |-> post] p 197 val tm2 = if can dest_sep_disj q then mk_sep_disj(tm2,snd(dest_sep_disj q)) else tm2 198 val vs = pairSyntax.list_mk_pair (map fst ys) 199 val ws = pairSyntax.list_mk_pair (map snd ys) 200 val tm3 = pairSyntax.mk_anylet([(vs,ws)],tm2) 201 val lemma = prove(mk_eq(q,tm3), 202 SIMP_TAC std_ss [LET_DEF] 203 THEN SPEC_TAC (ws,genvar(type_of ws)) 204 THEN SIMP_TAC (std_ss++star_ss) [pairTheory.FORALL_PROD,LET_DEF] 205 THEN (fn t => hd [])) handle Empty => (print ("\n\nUnable to store assignment:\n\n" ^ term_to_string(mk_eq(q,tm3)) ^ "\n\n"); TRUTH) 206 val th = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [lemma])) th 207 val _ = add_decompiled (name,th,len,SOME len) 208 in () end; 209 210fun add_conditional (tm1,tm2,th,len) = let 211 val th = RW [GSYM progTheory.SPEC_MOVE_COND] (DISCH_ALL th) 212 val m = get_model_name th 213 val name = ("AUTO_"^m^"_COND_"^(int_to_string (length (!compiler_conditionals)))) 214 val _ = (compiler_conditionals := (tm1,tm2,len,name,m) :: (!compiler_conditionals)) 215 val _ = add_decompiled (name,th,len,SOME len) 216 in () end; 217 218fun extract_ops th = let 219 val tools = (get_tools th) 220 val (_,_,th1,pc) = tools 221 val (x,y) = dest_eq (concl th1) 222 val xs = list_dest dest_star x @ list_dest dest_star y 223 val xs = map (fn x => dest_sep_hide x handle e => x) xs 224 val th = UNDISCH_ALL (SIMP_RULE (std_ss++sep_cond_ss) [progTheory.SPEC_MOVE_COND] th) 225 val (m,p,c,q) = dest_spec (concl th) 226 val (i,q) = pairSyntax.dest_anylet q handle HOL_ERR _ => ([],q) 227 fun fst_sep_disj tm = fst (dest_sep_disj tm) handle HOL_ERR _ => tm 228 val ps = list_dest dest_star p 229 val qs = list_dest dest_star (fst_sep_disj q) 230 (* length of instruction *) 231 val l = (numSyntax.int_of_term o cdr o cdr o cdr o hd) (filter (fn tm => car tm = pc) qs) 232 (* calculate update *) 233 fun sep_domain tm = dest_sep_hide tm handle _ => car tm 234 val ps' = filter (fn tm => not (mem (sep_domain tm) (pc::xs))) ps 235 val qs' = filter (fn tm => not (mem (sep_domain tm) (pc::xs))) qs 236 fun foo tm [] = fail() 237 | foo tm (x::xs) = if sep_domain x = tm then x else foo tm xs 238 val zs = map (fn tm => (cdr tm,cdr (foo (sep_domain tm) qs'))) ps' 239 val (tm1,tm2) = hd zs 240 fun goo (tm1,tm2) = let 241 val i = fst (match_term tm1 tm2) 242 val ys = list_dest pairSyntax.dest_pair tm1 243 in zip ys (map (subst i) ys) end 244 val ys = foldr (uncurry append) [] (map goo zs) handle e => [] 245 val ys = filter (fn (t1,t2) => not (t1 = t2)) ys 246 val tm1 = pairSyntax.list_mk_pair(map fst ys) handle HOL_ERR e => ``()`` 247 val tm2 = pairSyntax.list_mk_pair(map snd ys) handle HOL_ERR e => ``()`` 248 val ((tm1,tm2),ys) = if length i = 0 then ((tm1,tm2),ys) else (hd i,i) 249 val len = l 250 (* store thm *) 251 val _ = if length ys = 0 then () else add_assignment (tm1,tm2,th,l) 252 (* possible tests *) 253 fun foo tm = optionSyntax.dest_some tm handle e => tm 254 val qs = filter (fn tm => mem (car tm) xs) qs 255 val qs = map (fn tm => add_conditional(foo (cdr tm),car tm,th,l)) qs 256 handle HOL_ERR _ => [] 257 in () end; 258 259fun add_compiled thms = let val _ = map extract_ops thms in () end; 260 261(* code generator *) 262 263fun print_asm code = let 264 val (_,_,branch) = assembler_tools 265 fun print_cmp NONE = "" 266 | print_cmp (SOME (t,f)) = " ["^t^"|"^f^"]" 267 fun print_inst (ASM_ASSIGN (t1,t2)) = 268 term_to_string t1 ^ " := " ^ term_to_string t2 269 | print_inst (ASM_BRANCH (c,name)) = 270 branch c ^ " " ^ name 271 | print_inst (ASM_COMPARE tm) = 272 "compare " ^ term_to_string tm 273 | print_inst (ASM_INSERT (s,i,cmp)) = 274 "MACRO INSERT: " ^ s ^ " [length: " ^ int_to_string i ^ "]" ^ print_cmp cmp 275 | print_inst (ASM_INSTRUCTION (s,_,cmp)) = 276 s ^ print_cmp cmp 277 | print_inst (ASM_LABEL s) = 278 s ^ ":" 279 fun is_LABEL (ASM_LABEL s) = true | is_LABEL _ = false 280 fun all_labels [] = [] 281 | all_labels ((ASM_BRANCH (_,s))::xs) = s :: all_labels xs 282 | all_labels (x::xs) = all_labels xs 283 val ls = all_labels code 284 fun filter_labels [] = [] 285 | filter_labels ((ASM_LABEL s)::xs) = if mem s ls then ASM_LABEL s :: filter_labels xs else filter_labels xs 286 | filter_labels (x::xs) = x :: filter_labels xs 287 val code = filter_labels code 288 fun expand s = if size s < 5 then expand (s ^ " ") else s 289 fun code2string [] prev_was_label = "" 290 | code2string (c::cs) prev_was_label = 291 if is_LABEL c then 292 (if prev_was_label then "\n" else "") ^ expand (print_inst c) ^ code2string cs true 293 else 294 (if prev_was_label then "" else expand "") ^ print_inst c ^ "\n" ^ code2string cs false 295 val str = code2string code false 296 in print ("\n" ^ str ^ "\n") end 297 298val EXPAND_IF = prove( 299 ``!b c s1 (s2:'a). 300 ((if b \/ c then s1 else s2) = if b then s1 else if c then s1 else s2) /\ 301 ((if b /\ c then s1 else s2) = if b then if c then s1 else s2 else s2)``, 302 Cases THEN Cases THEN SIMP_TAC std_ss []); 303 304fun generate_code model_name print_assembly tm = let 305 val (assign2assembly, guard2assembly) = generator_tools 306 val (cond_code, conditionalise, remove_annotations) = conditional_tools 307 (* handle /\ and \/ in guards *) 308 val tm = (cdr o concl o REWRITE_CONV [EXPAND_IF]) tm handle e => tm 309 (* fold constants *) 310 val tm = (cdr o concl o EVAL_ANY_MATCH_CONV word_patterns) tm handle e => tm 311 (* generate abstract code *) 312 val l = ref 0; 313 fun label_name () = let val _ = l := !l + 1 in "L" ^ (int_to_string (!l)) end 314 val top_label = label_name() 315 fun shared_tail xs ys = let 316 fun aux [] ys zs = ([],rev ys,zs) 317 | aux xs [] zs = (rev xs,[],zs) 318 | aux (x::xs) (y::ys) zs = 319 if x = y then aux xs ys (x::zs) else (rev (x::xs), rev (y::ys), zs) 320 in aux (rev xs) (rev ys) [] end 321 fun compile (FUN_VAL tm) = 322 if not (pairSyntax.is_pair tm) andalso is_comb tm then [ASM_BRANCH (NONE,top_label)] else [] 323 | compile (FUN_COND _) = raise (mk_HOL_ERR "compilerLib" "compile" "Structure not supported.") 324 | compile (FUN_LET (tm1,tm2,t)) = 325 [ ASM_ASSIGN (tm1,tm2) ] @ compile t 326 | compile (FUN_IF (tm,t1,t2)) = 327 if is_neg tm then compile (FUN_IF (dest_neg tm,t2,t1)) else let 328 val rest1 = compile t1 329 val rest2 = compile t2 330 val label1 = label_name() 331 val (rest1,rest2,rest3) = shared_tail rest1 rest2 332 val (rest1,rest2,rest3) = 333 if rest3 = [ASM_BRANCH (NONE,top_label)] 334 then (rest1 @ rest3, rest2 @ rest3,[]) else (rest1, rest2, rest3) 335 in if rest1 = [] then 336 [ASM_COMPARE tm, ASM_BRANCH (SOME "true",label1)] @ rest2 @ [ASM_LABEL label1] @ rest3 337 else if rest2 = [] then 338 [ASM_COMPARE tm, ASM_BRANCH (SOME "false",label1)] @ rest1 @ [ASM_LABEL label1] @ rest3 339 else if rest1 = [ASM_BRANCH (NONE,top_label)] then 340 [ASM_COMPARE tm, ASM_BRANCH (SOME "true",top_label)] @ rest2 @ rest3 341 else if rest2 = [ASM_BRANCH (NONE,top_label)] then 342 [ASM_COMPARE tm, ASM_BRANCH (SOME "false",top_label)] @ rest1 @ rest3 343 else if last rest1 = ASM_BRANCH (NONE,top_label) then 344 [ASM_COMPARE tm, ASM_BRANCH (SOME "false",label1)] @ rest1 @ [ASM_LABEL label1] @ rest2 @ rest3 345 else if last rest2 = ASM_BRANCH (NONE,top_label) then 346 [ASM_COMPARE tm, ASM_BRANCH (SOME "true",label1)] @ rest2 @ [ASM_LABEL label1] @ rest1 @ rest3 347 else let val label2 = label_name() in 348 if length rest2 < length rest1 then 349 [ASM_COMPARE tm, ASM_BRANCH (SOME "true",label1)] @ rest2 @ [ASM_BRANCH (NONE,label2)] @ 350 [ASM_LABEL label1] @ rest1 @ [ASM_LABEL label2] @ rest3 351 else 352 [ASM_COMPARE tm, ASM_BRANCH (SOME "false",label1)] @ rest1 @ [ASM_BRANCH (NONE,label2)] @ 353 [ASM_LABEL label1] @ rest2 @ [ASM_LABEL label2] @ rest3 354 end end 355 val x = fst (dest_eq tm) 356 val t = tm2ftree (snd (dest_eq tm)) 357 (* remove dead code *) 358 fun rem (FUN_VAL tm) = FUN_VAL tm 359 | rem (FUN_COND x) = FUN_COND x 360 | rem (FUN_IF (tm,t1,t2)) = FUN_IF (tm,rem t1,rem t2) 361 | rem (FUN_LET (tm1,tm2,t)) = let 362 val t = rem t 363 val vs = free_vars tm1 364 val ws = free_vars (ftree2tm t) 365 in if filter (fn x => mem x ws) vs = [] then t else FUN_LET (tm1,tm2,t) end 366 val t = rem t 367 (* compile *) 368 val name = fst (dest_const (repeat car x)) handle e => fst (dest_var (repeat car x)) 369 val code1 = [ASM_LABEL top_label] @ compile t 370 (* do basic instruction reorderings here *) 371 (* ... *) 372 (* look up assembly instructions for assignments and comparisions *) 373 fun find_assignment (tm1,tm2) [] = fail() 374 | find_assignment (tm1,tm2) ((x,y,l,n,m)::xs) = 375 if (tm1 = x) andalso (tm2 = y) andalso (m = model_name) 376 then (n,l) else find_assignment (tm1,tm2) xs 377 fun find_compiled_assignment (tm1,tm2) = find_assignment (tm1,tm2) (!compiler_assignments) 378 fun find_conditional tm [] = fail() 379 | find_conditional tm ((x,y,l,n,m)::xs) = 380 if ((tm = x) orelse (mk_neg tm = x)) andalso (m = model_name) 381 then (x,y,l,n) else find_conditional tm xs 382 fun find_compiled_conditional tm = find_conditional tm (!compiler_conditionals) 383 fun compile_inst1 (ASM_ASSIGN (t1,t2)) = let 384 val (s,i) = find_compiled_assignment (t1,t2) 385 in [ASM_INSERT (s,i,NONE)] end 386 | compile_inst1 (ASM_COMPARE tm) = let 387 val (t1,t2,i,s) = find_compiled_conditional tm 388 val (t,f) = cond_code t2 389 val (t,f) = if is_neg t1 then (f,t) else (t,f) 390 in [ASM_INSERT (s,i,SOME (t,f))] end 391 | compile_inst1 x = fail() 392 fun func_name_annotations t1 t2 = let 393 val vs = free_vars t1 @ free_vars t2 394 val v = hd (filter (fn v => mem (type_of v) 395 [``:word64 -> word64``,``:word64 -> word32``,``:word64 -> word8``]) vs) 396 in "/" ^ fst (dest_var v) end handle _ => "" 397 fun unable_to_compile s = (print ("\n\n\n ERROR! Unable to generate x64 for:\n\n " ^ s ^ "\n\n\n") ; fail()) 398 fun compile_inst2 (ASM_ASSIGN (t1,t2)) = ((let 399 val code = assign2assembly (term2assign t1 t2) 400 val s = func_name_annotations t1 t2 401 in map (fn x => ASM_INSTRUCTION (x,s,NONE)) code end) 402 handle e => unable_to_compile ("let " ^ term_to_string (mk_eq(t1,t2)) ^ " in ...")) 403 | compile_inst2 (ASM_COMPARE tm) = ((let 404 val (code,y) = guard2assembly (term2guard tm) 405 val s = func_name_annotations tm T 406 in map (fn x => ASM_INSTRUCTION (x,s,SOME y)) code end) 407 handle e => unable_to_compile ("if " ^ term_to_string tm ^ " then ... else ...")) 408 | compile_inst2 x = [x] 409 fun append_list [] = [] | append_list (x::xs) = x @ append_list xs 410 val code2 = append_list (map (fn x => compile_inst1 x handle _ => compile_inst2 x) code1) 411 (* try to produce conditional execution *) 412 fun bool2str c = if c then "true" else "false" 413 fun conditionally_execute code u (t,f) label = let 414 fun find_label [] head = fail() 415 | find_label (x::xs) head = 416 if x = ASM_LABEL label then (head,xs) else find_label xs (head @ [x]) 417 val (code,rest) = find_label code [] 418 val condition = if u then f else t 419 fun force_condition (ASM_INSTRUCTION (c,x,h)) = ASM_INSTRUCTION (conditionalise c condition,x,h) 420 | force_condition (ASM_BRANCH (NONE, l2)) = ASM_BRANCH (SOME (bool2str (not u)), l2) 421 | force_condition _ = fail() 422 val _ = if length code < 5 then () else fail() 423 in map force_condition code @ rest end 424 fun conditionalise [] (t,f) = [] 425 | conditionalise ((ASM_BRANCH (SOME u,label))::xs) (t,f) = 426 (conditionalise (conditionally_execute xs (u = "true") (t,f) label) (t,f) handle e => 427 (ASM_BRANCH (SOME u,label)) :: conditionalise xs (t,f)) 428 | conditionalise ((ASM_INSTRUCTION (x,y,SOME cond))::xs) (t,f) = 429 (ASM_INSTRUCTION (x,y,SOME cond)) :: conditionalise xs cond 430 | conditionalise ((ASM_INSERT (x,y,SOME cond))::xs) (t,f) = 431 (ASM_INSERT (x,y,SOME cond)) :: conditionalise xs cond 432 | conditionalise (zzz::xs) (t,f) = zzz :: conditionalise xs (t,f) 433 val code3 = conditionalise code2 ("","") 434 (* assign proper branch conditions *) 435 fun update_branches [] (t,f) = [] 436 | update_branches ((ASM_BRANCH (SOME u,label))::xs) (t,f) = 437 (ASM_BRANCH (SOME (if u = "true" then t else (if u = "false" then f else u)),label)) :: update_branches xs (t,f) 438 | update_branches ((ASM_INSTRUCTION (x,y,SOME cond))::xs) (t,f) = 439 (ASM_INSTRUCTION (x,y,NONE)) :: update_branches xs cond 440 | update_branches ((ASM_INSERT (x,y,SOME cond))::xs) (t,f) = 441 (ASM_INSERT (x,y,NONE)) :: update_branches xs cond 442 | update_branches (zzz::xs) (t,f) = zzz :: update_branches xs (t,f) 443 val code3 = update_branches code3 ("","") 444 (* remove any annotations that were left in the assembly *) 445 fun remove_extra_annotations (ASM_INSTRUCTION (x,z,y)) = ASM_INSTRUCTION (remove_annotations x,z,y) 446 | remove_extra_annotations x = x 447 val code3 = map remove_extra_annotations code3 448 val _ = if print_assembly then print_asm code3 else () 449 (* assembler should start here *) 450 val code3 = (map (fn x => (x,(NONE:string option))) code3) 451 val (code6,len,_) = basic_assembler code3 452 in (code6,len) end 453 454 455end; 456