Simplification des Cconst_symbol: seules les versions 'signed' sont conservees

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 59 insertions, 79 deletions

diff --git a/backend/PPC.v b/backend/PPC.v
index 5cd5e9f5..244c5951 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -50,10 +50,8 @@ Proof. decide equality. Defined.
 
 Inductive constant: Set :=
   | Cint: int -> constant
-  | Csymbol_low_signed: ident -> int -> constant
-  | Csymbol_high_signed: ident -> int -> constant
-  | Csymbol_low_unsigned: ident -> int -> constant
-  | Csymbol_high_unsigned: ident -> int -> constant.
+  | Csymbol_low: ident -> int -> constant
+  | Csymbol_high: ident -> int -> constant.
 
 (** A note on constants: while immediate operands to PowerPC
   instructions must be representable in 16 bits (with
@@ -350,37 +348,36 @@ Definition gpr_or_zero (rs: regset) (r: ireg) :=
 
 Variable ge: genv.
 
+Definition symbol_offset (id: ident) (ofs: int) : val :=
+  match Genv.find_symbol ge id with
+  | Some b => Vptr b ofs
+  | None => Vundef
+  end.
+
 (** The four functions below axiomatize how the linker processes
   symbolic references [symbol + offset] and splits their
-  actual values into two 16-bit halves, the lower half
-  being either signed or unsigned. *)
+  actual values into two 16-bit halves. *)
 
-Parameter low_half_signed: val -> val.
-Parameter high_half_signed: val -> val.
-Parameter low_half_unsigned: val -> val.
-Parameter high_half_unsigned: val -> val.
+Parameter low_half: val -> val.
+Parameter high_half: val -> val.
 
-(** The fundamental property of these operations is that their
-  results can be recombined by addition or logical ``or'',
-  and this recombination rebuilds the original value. *)
+(** The fundamental property of these operations is that, when applied
+  to the address of a symbol, their results can be recombined by
+  addition, rebuilding the original address. *)
 
-Axiom low_high_half_signed:
-  forall v, Val.add (low_half_signed v) (high_half_signed v) = v.
-Axiom low_high_half_unsigned:
-  forall v, Val.or (low_half_unsigned v) (high_half_unsigned v) = v.
+Axiom low_high_half:
+  forall id ofs,
+  Val.add (low_half (symbol_offset id ofs)) (high_half (symbol_offset id ofs))
+  = symbol_offset id ofs.
 
 (** The other axioms we take is that the results of
   the [low_half] and [high_half] functions are of type [Tint],
   i.e. either integers, pointers or undefined values. *)
 
-Axiom low_half_signed_type: 
-  forall v, Val.has_type (low_half_signed v) Tint.
-Axiom high_half_signed_type: 
-  forall v, Val.has_type (high_half_signed v) Tint.
-Axiom low_half_unsigned_type: 
-  forall v, Val.has_type (low_half_unsigned v) Tint.
-Axiom high_half_unsigned_type: 
-  forall v, Val.has_type (high_half_unsigned v) Tint.
+Axiom low_half_type: 
+  forall v, Val.has_type (low_half v) Tint.
+Axiom high_half_type: 
+  forall v, Val.has_type (high_half v) Tint.
  
 (** Armed with the [low_half] and [high_half] functions,
   we can define the evaluation of a symbolic constant.
@@ -390,28 +387,18 @@ Axiom high_half_unsigned_type:
   that the results of [high_half] are already shifted
   (their 16 low bits are equal to 0). *)
 
-Definition symbol_offset (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol ge id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
-
 Definition const_low (c: constant) :=
   match c with
   | Cint n => Vint n
-  | Csymbol_low_signed id ofs => low_half_signed (symbol_offset id ofs)
-  | Csymbol_high_signed id ofs => Vundef
-  | Csymbol_low_unsigned id ofs => low_half_unsigned (symbol_offset id ofs)
-  | Csymbol_high_unsigned id ofs => Vundef
+  | Csymbol_low id ofs => low_half (symbol_offset id ofs)
+  | Csymbol_high id ofs => Vundef
   end.
 
 Definition const_high (c: constant) :=
   match c with
   | Cint n => Vint (Int.shl n (Int.repr 16))
-  | Csymbol_low_signed id ofs => Vundef
-  | Csymbol_high_signed id ofs => high_half_signed (symbol_offset id ofs)
-  | Csymbol_low_unsigned id ofs => Vundef
-  | Csymbol_high_unsigned id ofs => high_half_unsigned (symbol_offset id ofs)
+  | Csymbol_low id ofs => Vundef
+  | Csymbol_high id ofs => high_half (symbol_offset id ofs)
   end.
 
 (** The semantics is purely small-step and defined as a function
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index d7a83b0b..171945de 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -265,8 +265,8 @@ Definition transl_op
   | Ofloatconst f, nil =>
       Plfi (freg_of r) f :: k
   | Oaddrsymbol s ofs, nil =>
-      Paddis (ireg_of r) GPR0 (Csymbol_high_unsigned s ofs) ::
-      Pori (ireg_of r) (ireg_of r) (Csymbol_low_unsigned s ofs) :: k
+      Paddis GPR2 GPR0 (Csymbol_high s ofs) ::
+      Paddi (ireg_of r) GPR2 (Csymbol_low s ofs) :: k
   | Oaddrstack n, nil =>
       addimm (ireg_of r) GPR1 n k
   | Ocast8signed, a1 :: nil =>
@@ -385,16 +385,16 @@ Definition transl_load_store
   | Aindexed2, a1 :: a2 :: nil =>
       mk2 (ireg_of a1) (ireg_of a2) :: k
   | Aglobal symb ofs, nil =>
-      Paddis GPR2 GPR0 (Csymbol_high_signed symb ofs) ::
-      mk1 (Csymbol_low_signed symb ofs) GPR2 :: k
+      Paddis GPR2 GPR0 (Csymbol_high symb ofs) ::
+      mk1 (Csymbol_low symb ofs) GPR2 :: k
   | Abased symb ofs, a1 :: nil =>
       if ireg_eq (ireg_of a1) GPR0 then
         Pmr GPR2 (ireg_of a1) ::
-        Paddis GPR2 GPR2 (Csymbol_high_signed symb ofs) ::
-        mk1 (Csymbol_low_signed symb ofs) GPR2 :: k
+        Paddis GPR2 GPR2 (Csymbol_high symb ofs) ::
+        mk1 (Csymbol_low symb ofs) GPR2 :: k
       else
-        Paddis GPR2 (ireg_of a1) (Csymbol_high_signed symb ofs) ::
-        mk1 (Csymbol_low_signed symb ofs) GPR2 :: k
+        Paddis GPR2 (ireg_of a1) (Csymbol_high symb ofs) ::
+        mk1 (Csymbol_low symb ofs) GPR2 :: k
   | Ainstack ofs, nil =>
       if Int.eq (high_s ofs) Int.zero then
         mk1 (Cint ofs) GPR1 :: k
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index 1b432c72..c0125fc2 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -19,23 +19,12 @@ Require Conventions.
 
 (** * Properties of low half/high half decomposition *)
 
-Lemma high_half_signed_zero:
-  forall v, Val.add (high_half_signed v) Vzero = high_half_signed v.
+Lemma high_half_zero:
+  forall v, Val.add (high_half v) Vzero = high_half v.
 Proof.
-  intros. generalize (high_half_signed_type v).
+  intros. generalize (high_half_type v).
   rewrite Val.add_commut. 
-  case (high_half_signed v); simpl; intros; try contradiction.
-  auto. 
-  rewrite Int.add_commut; rewrite Int.add_zero; auto. 
-  rewrite Int.add_zero; auto. 
-Qed.
-
-Lemma high_half_unsigned_zero:
-  forall v, Val.add (high_half_unsigned v) Vzero = high_half_unsigned v.
-Proof.
-  intros. generalize (high_half_unsigned_type v).
-  rewrite Val.add_commut. 
-  case (high_half_unsigned v); simpl; intros; try contradiction.
+  case (high_half v); simpl; intros; try contradiction.
   auto. 
   rewrite Int.add_commut; rewrite Int.add_zero; auto. 
   rewrite Int.add_zero; auto. 
@@ -1246,18 +1235,22 @@ Proof.
   split. apply exec_straight_one. reflexivity. reflexivity.
   auto with ppcgen.
   (* Oaddrsymbol *)
-  set (v := find_symbol_offset ge i i0).
-  pose (rs1 := nextinstr (rs#(ireg_of res) <- (high_half_unsigned v))).
+  change (find_symbol_offset ge i i0) with (symbol_offset ge i i0).
+  set (v := symbol_offset ge i i0).
+  pose (rs1 := nextinstr (rs#GPR2 <- (high_half v))).
   exists (nextinstr (rs1#(ireg_of res) <- v)).
   split. apply exec_straight_two with rs1 m.
   unfold exec_instr. rewrite gpr_or_zero_zero.
   unfold const_high. rewrite Val.add_commut. 
-  rewrite high_half_unsigned_zero. reflexivity. 
-  simpl. unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen.
-  rewrite Pregmap.gss.
-  fold v. rewrite Val.or_commut. rewrite low_high_half_unsigned.
+  rewrite high_half_zero. reflexivity. 
+  simpl. rewrite gpr_or_zero_not_zero. 2: congruence. 
+  unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen.
+  rewrite Pregmap.gss. 
+  fold v. rewrite Val.add_commut. unfold v. rewrite low_high_half.
   reflexivity. reflexivity. reflexivity. 
-  unfold rs1. auto with ppcgen.
+  unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto.
+  apply agree_set_mreg. apply agree_nextinstr.
+  apply agree_set_other. auto. simpl. tauto.
   (* Oaddrstack *)
   assert (GPR1 <> GPR2). discriminate.
   generalize (addimm_correct (ireg_of res) GPR1 i k rs m H2). 
@@ -1493,13 +1486,13 @@ Proof.
   apply H0. 
   simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto.
   (* Aglobal *)
-  set (rs1 := nextinstr (rs#GPR2 <- (const_high ge (Csymbol_high_signed i i0)))).
+  set (rs1 := nextinstr (rs#GPR2 <- (const_high ge (Csymbol_high i i0)))).
   assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil =
-                Val.add rs1#GPR2 (const_low ge (Csymbol_low_signed i i0))).
+                Val.add rs1#GPR2 (const_low ge (Csymbol_low i i0))).
     simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
     unfold const_high, const_low. 
     set (v := symbol_offset ge i i0).
-    symmetry. rewrite Val.add_commut. apply low_high_half_signed. 
+    symmetry. rewrite Val.add_commut. unfold v. apply low_high_half. 
     discriminate.
   assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
   assert (NOT0: GPR2 <> GPR0). discriminate.
@@ -1507,7 +1500,7 @@ Proof.
   exists rs'. split. apply exec_straight_step with rs1 m.
   unfold exec_instr. rewrite gpr_or_zero_zero. 
   rewrite Val.add_commut. unfold const_high. 
-  rewrite high_half_signed_zero.
+  rewrite high_half_zero.
   reflexivity. reflexivity.
   assumption. assumption.
   (* Abased *)
@@ -1518,19 +1511,19 @@ Proof.
     agree ms sp rs1 ->
     exists rs',
       exec_straight
-        (Paddis GPR2 r (Csymbol_high_signed i i0)
-         :: mk1 (Csymbol_low_signed i i0) GPR2 :: k) rs1 m k rs' m'
+        (Paddis GPR2 r (Csymbol_high i i0)
+         :: mk1 (Csymbol_low i i0) GPR2 :: k) rs1 m k rs' m'
       /\ agree ms' sp rs').
   intros. 
-  set (rs2 := nextinstr (rs1#GPR2 <- (Val.add (ms t) (const_high ge (Csymbol_high_signed i i0))))).
+  set (rs2 := nextinstr (rs1#GPR2 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))).
   assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) =
-                Val.add rs2#GPR2 (const_low ge (Csymbol_low_signed i i0))).
+                Val.add rs2#GPR2 (const_low ge (Csymbol_low i i0))).
     simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
     unfold const_high. 
     set (v := symbol_offset ge i i0).
     rewrite Val.add_assoc. 
-    rewrite (Val.add_commut (high_half_signed v)).
-    rewrite low_high_half_signed. apply Val.add_commut.
+    rewrite (Val.add_commut (high_half v)).
+    unfold v. rewrite low_high_half. apply Val.add_commut.
     discriminate.
   assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen.
   assert (NOT0: GPR2 <> GPR0). discriminate.