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