diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
commit | c45fc2431ea70e0cb5a80e65d0ac99f91e94693e (patch) | |
tree | dfc11f4507c6ddaab96074382d8406dbc4031f60 /ia32/Asm.v | |
parent | 67e74f6f1a24247bfcd3d6c165a2d6cd45c83b06 (diff) | |
download | compcert-c45fc2431ea70e0cb5a80e65d0ac99f91e94693e.tar.gz compcert-c45fc2431ea70e0cb5a80e65d0ac99f91e94693e.zip |
Added pass CleanupLabels to remove unreferenced labels in a proved way.
ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed.
ia32/Asm.v: Pmov_ri can undef flags (if translated to xor)
cparser/Ceval.ml: treat ~ in constant exprs
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asm.v')
-rw-r--r-- | ia32/Asm.v | 23 |
1 files changed, 16 insertions, 7 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 => |