diff options
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Asm.v | 23 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 19 |
2 files changed, 19 insertions, 23 deletions
@@ -399,7 +399,9 @@ Inductive outcome: Type := | Stuck: outcome. (** Manipulations over the [PC] register: continuing with the next - instruction ([nextinstr]) or branching to a label ([goto_label]). *) + instruction ([nextinstr]) or branching to a label ([goto_label]). + [nextinstr_nf] is a variant of [nextinstr] that sets condition flags + to [Vundef] in addition to incrementing the [PC]. *) Definition nextinstr (rs: regset) := rs#PC <- (Val.add rs#PC Vone). @@ -438,11 +440,18 @@ Definition exec_store (chunk: memory_chunk) (m: mem) that correspond to actual IA32 instructions, the cases are straightforward transliterations of the informal descriptions given in the IA32 reference manuals. For pseudo-instructions, - refer to the informal descriptions given above. Note that - we set to [Vundef] the registers used as temporaries by the - expansions of the pseudo-instructions, so that the IA32 code - we generate cannot use those registers to hold values that - must survive the execution of the pseudo-instruction. + refer to the informal descriptions given above. + + Note that we set to [Vundef] the registers used as temporaries by + the expansions of the pseudo-instructions, so that the IA32 code + we generate cannot use those registers to hold values that must + survive the execution of the pseudo-instruction. + + Concerning condition flags, the comparison instructions set them + accurately; other instructions (moves, [lea]) preserve them; + and all other instruction set those flags to [Vundef], to reflect + the fact that the processor updates some or all of those flags, + but we do not need to model this precisely. *) Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := @@ -451,7 +460,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pmov_rr rd r1 => Next (nextinstr (rs#rd <- (rs r1))) m | Pmov_ri rd n => - Next (nextinstr (rs#rd <- (Vint n))) m + Next (nextinstr_nf (rs#rd <- (Vint n))) m | Pmov_rm rd a => exec_load Mint32 m a rs rd | Pmov_mr a r1 => diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 969b3b3..a7a5f1a 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -355,14 +355,12 @@ let print_annotation oc txt args res = (* Printing of instructions *) -module Labelset = Set.Make(struct type t = label let compare = compare end) - let float_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] (* Reminder on AT&T syntax: op source, dest *) -let print_instruction oc labels = function +let print_instruction oc = function (* Moves *) | Pmov_rr(rd, r1) -> fprintf oc " movl %a, %a\n" ireg r1 ireg rd @@ -568,8 +566,7 @@ let print_instruction oc labels = function fprintf oc " ret\n" (** Pseudo-instructions *) | Plabel(l) -> - if Labelset.mem l labels then - fprintf oc "%a:\n" label (transl_label l) + fprintf oc "%a:\n" label (transl_label l) | Pallocframe(sz, ofs_ra, ofs_link) -> let sz = sp_adjustment sz in let ofs_link = camlint_of_coqint ofs_link in @@ -594,16 +591,6 @@ let print_jumptable oc (lbl, tbl) = (fun l -> fprintf oc " .long %a\n" label (transl_label l)) tbl -let rec labels_of_code accu = function - | [] -> - accu - | (Pjmp_l lbl | Pjcc(_, lbl)) :: c -> - labels_of_code (Labelset.add lbl accu) c - | Pjmptbl(_, tbl) :: c -> - labels_of_code (List.fold_right Labelset.add tbl accu) c - | _ :: c -> - labels_of_code accu c - let print_function oc name code = Hashtbl.clear current_function_labels; float_literals := []; @@ -614,7 +601,7 @@ let print_function oc name code = if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; - List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code; + List.iter (print_instruction oc) code; if target = ELF then begin fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name |