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

4 files changed, 245 insertions, 20 deletions

diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
new file mode 100644
index 0000000..61f26e7
--- /dev/null
+++ b/ia32/CombineOp.v
@@ -0,0 +1,101 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 (Olea a) ys) => Some(SelectOp.offset_addressing a n, ys)
+      | _ => None
+      end
+  | _, _ => None
+  end.
+
+Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
+  match op, args with
+  | Oandimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm m) ys) => Some(Oandimm (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
+  | Olea addr, _ =>
+      match combine_addr addr args with
+      | Some(addr', args') => Some(Olea addr', args')
+      | None => 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/ia32/CombineOpproof.v b/ia32/CombineOpproof.v
new file mode 100644
index 0000000..c6d2509
--- /dev/null
+++ b/ia32/CombineOpproof.v
@@ -0,0 +1,130 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.
+  exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ.
+  assert (forall vl,
+         eval_addressing ge sp (SelectOp.offset_addressing a n) vl =
+         option_map (fun v => Val.add v (Vint n)) (eval_addressing ge sp a vl)).
+    intros. destruct a; simpl; repeat (destruct vl; auto); simpl. 
+    rewrite Val.add_assoc. auto. 
+    repeat rewrite Val.add_assoc. auto.
+    rewrite Val.add_assoc. auto.
+    repeat rewrite Val.add_assoc. auto.
+    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto. 
+    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto.
+      repeat rewrite <- (Val.add_commut v). rewrite Val.add_assoc. auto. 
+    unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i0); auto.
+      repeat rewrite <- (Val.add_commut (Val.mul v (Vint i))). rewrite Val.add_assoc. auto.
+    rewrite Val.add_assoc; auto.
+  rewrite H0. rewrite EQ. 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.
+(* andimm *)
+  exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv.
+  rewrite <- H1. rewrite Val.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.
+(* lea *)
+  simpl. eapply combine_addr_sound; eauto. 
+(* cmp *)
+  simpl. decEq; decEq. eapply combine_cond_sound; eauto.
+Qed.
+
+End COMBINE.
diff --git a/ia32/Op.v b/ia32/Op.v
index 896badf..0b32b88 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -446,20 +446,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/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 658a755..9b1cd89 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -176,13 +176,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.