Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).

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

powerpc/SelectOp.v

@@ -224,6 +224,8 @@ Definition add (e1: expr) (e2: expr) :=
   | Eop(Oaddimm n1) (t1:::Enil)), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | t1, Eop (Ointconst n2) Enil => addimm n2 t1
   | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | Eop (Oaddrsymbol s n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => Eop Oadd (Eop (Oaddrsymbol s (Int.add n1 n2)) Enil ::: t2 ::: Enil)
+  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => Eop Oadd (Eop (Oaddstack (Int.add n1 n2)) Enil ::: t2 ::: Enil)
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 *)
@@ -244,6 +246,12 @@ Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
   | add_case5:
       forall (t1: expr) (n2: int) (t2: expr),
       add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
+  | add_case6:
+      forall s n1 n2 t2,
+      add_cases (Eop (Oaddrsymbol s n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
+  | add_case7:
+      forall n1 n2 t2,
+      add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
   | add_default:
       forall (e1: expr) (e2: expr),
       add_cases e1 e2.
@@ -266,6 +274,10 @@ Definition add_match (e1: expr) (e2: expr) :=
       add_case2 n1 t1 n2 t2
   | Eop(Oaddimm n1) (t1:::Enil), t2 =>
       add_case3 n1 t1 t2
+  | Eop (Oaddrsymbol s n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => 
+      add_case6 s n1 n2 t2
+  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
+      add_case7 n1 n2 t2
   | e1, e2 =>
       add_match_aux e1 e2
   end.
@@ -282,6 +294,10 @@ Definition add (e1: expr) (e2: expr) :=
       addimm n2 t1
   | add_case5 t1 n2 t2 =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | add_case6 s n1 n2 t2 =>
+      Eop Oadd (Eop (Oaddrsymbol s (Int.add n1 n2)) Enil ::: t2 ::: Enil)
+  | add_case7 n1 n2 t2 =>
+      Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil)
   | add_default e1 e2 =>
       Eop Oadd (e1:::e2:::Enil)
   end.

powerpc/SelectOpproof.v

@@ -214,6 +214,8 @@ Proof.
   replace (Int.add x y) with (Int.add (Int.add x i) n2).
     apply eval_addimm. EvalOp.
     subst y. rewrite Int.add_assoc. auto.
+  destruct (Genv.find_symbol ge s); inv H0.
+  destruct sp; simpl in H0; inv H0.
   EvalOp.
 Qed.
 
@@ -235,6 +237,14 @@ Proof.
   replace (Int.add x y) with (Int.add (Int.add x i) n2).
     apply eval_addimm_ptr. EvalOp.
     subst y. rewrite Int.add_assoc. auto.
+  revert H0. case_eq (Genv.find_symbol ge s); intros; inv H1.
+  EvalOp. constructor. EvalOp. simpl. rewrite H0; eauto. 
+  constructor. eauto. constructor. 
+  simpl. decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  destruct sp; simpl in H0; inv H0. 
+  EvalOp. constructor. EvalOp. simpl. eauto. constructor. eauto. constructor.
+  simpl. decEq. decEq. repeat rewrite Int.add_assoc.
+  decEq. decEq. apply Int.add_commut. 
   EvalOp.
 Qed.
 
@@ -257,6 +267,8 @@ Proof.
   replace (Int.add y x) with (Int.add (Int.add i x) n2).
     apply eval_addimm_ptr. EvalOp. subst b0; reflexivity.
     subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  destruct (Genv.find_symbol ge s); inv H0.
+  destruct sp; simpl in H0; inv H0.
   EvalOp.
 Qed.