From 636e45004c6fc3530f47ae237802bec732c32b30 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 31 Oct 2007 17:08:31 +0000
Subject: [PATCH] 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
---
backend/PPC.v | 65 +++++++++++++++++-------------------------
backend/PPCgen.v | 16 +++++------
backend/PPCgenproof1.v | 57 ++++++++++++++++--------------------
3 files changed, 59 insertions(+), 79 deletions(-)
diff --git a/backend/PPC.v b/backend/PPC.v
index 5cd5e9f58..244c59516 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 d7a83b0b5..171945dea 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 1b432c72c..c0125fc24 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.
--
GitLab