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

2 files changed, 19 insertions, 23 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 649009f..7e6bde7 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 =>
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