powerpc/: new unary operation "addsymbol"

Support far-data addressing in sections.
(Currently ignored in checklink.)


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

1 files changed, 13 insertions, 3 deletions

diff --git a/powerpc/Op.v b/powerpc/Op.v
index 085a098..dbc474e 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -61,6 +61,7 @@ Inductive operation : Type :=
   | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
   | Oadd: operation                     (**r [rd = r1 + r2] *)
   | Oaddimm: int -> operation           (**r [rd = r1 + n] *)
+  | Oaddsymbol: ident -> int -> operation (**r [rd = addr(id + ofs) + r1] *)
   | Osub: operation                     (**r [rd = r1 - r2] *)
   | Osubimm: int -> operation           (**r [rd = n - r1] *)
   | Omul: operation                     (**r [rd = r1 * r2] *)
@@ -183,6 +184,7 @@ Definition eval_operation
   | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1::v2::nil => Some (Val.add v1 v2)
   | Oaddimm n, v1::nil => Some (Val.add v1 (Vint n))
+  | Oaddsymbol s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1)
   | Osub, v1::v2::nil => Some (Val.sub v1 v2)
   | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1)
   | Omul, v1::v2::nil => Some (Val.mul v1 v2)
@@ -276,6 +278,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocast16signed => (Tint :: nil, Tint)
   | Oadd => (Tint :: Tint :: nil, Tint)
   | Oaddimm _ => (Tint :: nil, Tint)
+  | Oaddsymbol _ _ => (Tint :: nil, Tint)
   | Osub => (Tint :: Tint :: nil, Tint)
   | Osubimm _ => (Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
@@ -353,6 +356,7 @@ Proof with (try exact I).
   destruct v0...
   destruct v0; destruct v1...
   destruct v0...
+  unfold symbol_address. destruct (Genv.find_symbol genv i)... destruct v0...
   destruct v0; destruct v1... simpl. destruct (eq_block b b0)...
   destruct v0...
   destruct v0; destruct v1...
@@ -650,19 +654,24 @@ Variable ge2: Genv.t F2 V2.
 Hypothesis agree_on_symbols:
   forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
 
+Remark symbol_address_preserved:
+  forall s ofs, symbol_address ge2 s ofs = symbol_address ge1 s ofs.
+Proof.
+  unfold symbol_address; intros. rewrite agree_on_symbols; auto.
+Qed.
+ 
 Lemma eval_operation_preserved:
   forall sp op vl m,
   eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
 Proof.
-  intros. destruct op; simpl; auto. 
-  destruct vl; auto. decEq. unfold symbol_address. rewrite agree_on_symbols. auto.
+  intros. destruct op; simpl; auto; rewrite symbol_address_preserved; auto.
 Qed.
 
 Lemma eval_addressing_preserved:
   forall sp addr vl,
   eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl.
 Proof.
-  intros. destruct addr; simpl; auto; unfold symbol_address; rewrite agree_on_symbols; auto.
+  intros. destruct addr; simpl; auto; rewrite symbol_address_preserved; auto.
 Qed.
 
 End GENV_TRANSF.
@@ -760,6 +769,7 @@ Proof.
   inv H4; simpl; auto.
   apply Values.val_add_inject; auto.
   apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto.
   inv H4; inv H2; simpl; auto. econstructor; eauto. 
     rewrite Int.sub_add_l. auto.
     destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true.