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

1 files changed, 16 insertions, 7 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 649009ff..7e6bde74 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -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 =>