From 636e45004c6fc3530f47ae237802bec732c32b30 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 31 Oct 2007 17:08:31 +0000 Subject: 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 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. -- cgit