CSE: add recognition of some combined operators, conditions, and addressing modes (cf. CombineOp.v)

Memory model: cleaning up Memdata
Inlining and new Constprop: updated for ARM.


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

5 files changed, 278 insertions, 23 deletions

diff --git a/powerpc/CombineOp.v b/powerpc/CombineOp.v
new file mode 100644
index 0000000..243da4e
--- /dev/null
+++ b/powerpc/CombineOp.v
@@ -0,0 +1,119 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Op.
+Require SelectOp.
+
+Definition valnum := positive.
+
+Inductive rhs : Type :=
+  | Op: operation -> list valnum -> rhs
+  | Load: memory_chunk -> addressing -> list valnum -> rhs.
+
+Section COMBINE.
+
+Variable get: valnum -> option rhs.
+
+Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys)
+  | _ => None
+  end.
+
+Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys)
+  | _ => None
+  end.
+
+Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) :=
+  match cond, args with
+  | Ccompimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | Ccompuimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None
+  | Ccompuimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None
+  | _, _ => None
+  end.
+
+Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+  match addr, args with
+  | Aindexed n, x::nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys)
+      | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None
+      | _ => None
+      end
+  | _, _ => None
+  end.
+
+Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
+  match op, args with
+  | Oaddimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Oaddimm (Int.add m n), ys)
+      | Some(Op (Osubimm m) ys) => Some(Osubimm (Int.add m n), ys)
+      | _ => None
+      end
+  | Osubimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Osubimm (Int.sub n m), ys)
+      | _ => None
+      end
+  | Oandimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
+      | Some(Op (Orolm amount m) ys) => Some(Orolm amount (Int.and m n), ys)
+      | _ => None
+      end
+  | Oorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
+      | _ => None
+      end
+  | Oxorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
+      | _ => None
+      end
+  | Orolm amount2 mask2, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm mask1) ys) =>
+           Some(Orolm (Int.modu amount2 Int.iwordsize)
+                     (Int.and (Int.rol mask1 amount2) mask2), ys)
+      | Some(Op (Orolm amount1 mask1) ys) =>
+           Some(Orolm (Int.modu (Int.add amount1 amount2) Int.iwordsize)
+                     (Int.and (Int.rol mask1 amount2) mask2), ys)
+      | _ => None
+      end
+  | Ocmp cond, _ =>
+      match combine_cond cond args with
+      | Some(cond', args') => Some(Ocmp cond', args')
+      | None => None
+      end
+  | _, _ => None
+  end.
+
+End COMBINE.
+
+
diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v
new file mode 100644
index 0000000..f493c16
--- /dev/null
+++ b/powerpc/CombineOpproof.v
@@ -0,0 +1,142 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions 
+  during the [CSE] phase. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import CombineOp.
+Require Import CSE.
+
+Section COMBINE.
+
+Variable ge: genv.
+Variable sp: val.
+Variable m: mem.
+Variable get: valnum -> option rhs.
+Variable valu: valnum -> val.
+Hypothesis get_sound: forall v rhs, get v = Some rhs -> equation_holds valu ge sp m v rhs.
+
+Lemma combine_compimm_ne_0_sound:
+  forall x cond args,
+  combine_compimm_ne_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero).
+Proof.
+  intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ.
+  (* of cmp *)
+  exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. 
+  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+  (* of and *)
+  exploit get_sound; eauto. unfold equation_holds; simpl. 
+  destruct args; try discriminate. destruct args; try discriminate. simpl. 
+  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+Qed.
+
+Lemma combine_compimm_eq_0_sound:
+  forall x cond args,
+  combine_compimm_eq_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero).
+Proof.
+  intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ.
+  (* of cmp *)
+  exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. 
+  rewrite eval_negate_condition. 
+  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+  (* of and *)
+  exploit get_sound; eauto. unfold equation_holds; simpl. 
+  destruct args; try discriminate. destruct args; try discriminate. simpl. 
+  intros EQ; inv EQ. destruct (valu v); simpl; auto. 
+Qed.
+
+Theorem combine_cond_sound:
+  forall cond args cond' args',
+  combine_cond get cond args = Some(cond', args') ->
+  eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+  (* compimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+  (* compuimm ne zero *)
+  simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compuimm eq zero *)
+  simpl; eapply combine_compimm_eq_0_sound; eauto.
+Qed.
+
+Theorem combine_addr_sound:
+  forall addr args addr' args',
+  combine_addr get addr args = Some(addr', args') ->
+  eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
+Proof.
+  intros. functional inversion H; subst.
+  (* indexed - addimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
+  rewrite <- H0. rewrite Val.add_assoc. auto. 
+  (* indexed 0 - add *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv.
+  rewrite <- H0. destruct v; destruct v0; simpl; auto; rewrite Int.add_zero; auto.
+Qed.
+
+Theorem combine_op_sound:
+  forall op args op' args',
+  combine_op get op args = Some(op', args') ->
+  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+(* addimm - addimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.add_assoc. auto.
+(* addimm - subimm *)
+Opaque Val.sub.
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)).
+  rewrite Val.sub_add_l. auto.
+(* subimm - addimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1.
+Transparent Val.sub.
+  destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc.
+  rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut.
+(* andimm - andimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.and_assoc. auto.
+(* andimm - rolm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. destruct v; simpl; auto. unfold Int.rolm. rewrite Int.and_assoc. auto.
+(* orimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.or_assoc. auto.
+(* xorimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.xor_assoc. auto.
+(* rolm - andimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm. 
+  rewrite (Int.add_commut Int.zero). rewrite Int.add_zero. auto.
+(* rolm - rolm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.rolm_rolm. auto. 
+(* cmp *)
+  simpl. decEq; decEq. eapply combine_cond_sound; eauto.
+Qed.
+
+End COMBINE.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 76c426b..986ea8c 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -420,20 +420,18 @@ Definition negate_condition (cond: condition): condition :=
   end.
 
 Lemma eval_negate_condition:
-  forall cond vl m b,
-  eval_condition cond vl m = Some b ->
-  eval_condition (negate_condition cond) vl m = Some (negb b).
+  forall cond vl m,
+  eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m).
 Proof.
-  intros. 
-  destruct cond; simpl in H; FuncInv; simpl.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite Val.negate_cmp_bool; rewrite H; auto.
-  rewrite Val.negate_cmpu_bool; rewrite H; auto.
-  rewrite H; auto.
-  destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. 
-  rewrite H0; auto.
-  rewrite <- H0. rewrite negb_elim; auto.
+  intros. destruct cond; simpl.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
+  destruct vl; auto. destruct v; auto. destruct vl; auto. 
+  destruct vl; auto. destruct v; auto. destruct vl; auto. simpl. rewrite negb_involutive. auto.
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index c54beed..6c83ab7 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -119,6 +119,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 =>
       addimm n1 t2
+  | t1, Eop (Ointconst n2) Enil =>
+      addimm n2 t1
   | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
   | Eop (Oaddimm n1) (t1:::Enil), t2 =>
@@ -127,8 +129,6 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       Eop Oadd (Eop (Oaddrsymbol s (Int.add n1 n2)) Enil ::: t2 ::: Enil)
   | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
       Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil)
-  | t1, Eop (Ointconst n2) Enil =>
-      addimm n2 t1
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
   | _, _ =>
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index b42503f..e4f981d 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -192,13 +192,9 @@ Proof.
 (* intconst *)
   destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
 (* cmp *)
-  inv H. simpl in H5.
-  destruct (eval_condition c vl m) as []_eqn. 
-  TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto.
-  inv H5. simpl. 
-  destruct (eval_condition (negate_condition c) vl m) as []_eqn.
-  destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto.
-  exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto.
+  inv H. simpl in H5. inv H5. 
+  TrivialExists. simpl. rewrite eval_negate_condition.
+  destruct (eval_condition c vl m); auto. destruct b; auto.
 (* condition *)
   inv H. destruct v1.
   exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
@@ -224,6 +220,7 @@ Proof.
   red; intros until y.
   unfold add; case (add_match a b); intros; InvEval.
   rewrite Val.add_commut. apply eval_addimm; auto.
+  apply eval_addimm; auto.
   subst. 
   replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
      with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
@@ -242,7 +239,6 @@ Proof.
     econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. 
     simpl. repeat rewrite Val.add_assoc. decEq; decEq.
     rewrite Val.add_commut. rewrite Val.add_permut. auto.
-  apply eval_addimm; auto.
   subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
   TrivialExists. 
 Qed.