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

6 files changed, 213 insertions, 83 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index d46afdc..e9613c9 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -27,6 +27,7 @@ Require Import Registers.
 Require Import RTL.
 Require Import RTLtyping.
 Require Import Kildall.
+Require Import CombineOp.
 
 (** * Value numbering *)
 
@@ -49,11 +50,13 @@ Require Import Kildall.
   Equations are of the form [valnum = rhs], where the right-hand sides
   [rhs] are either arithmetic operations or memory loads. *)
 
+(*
 Definition valnum := positive.
 
 Inductive rhs : Type :=
   | Op: operation -> list valnum -> rhs
   | Load: memory_chunk -> addressing -> list valnum -> rhs.
+*)
 
 Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq.
 
@@ -272,8 +275,8 @@ Definition add_store (n: numbering) (chunk: memory_chunk) (addr: addressing)
   | _ => n2
   end.
 
-(* [reg_valnum n vn] returns a register that is mapped to value number
-   [vn], or [None] if no such register exists. *)
+(** [reg_valnum n vn] returns a register that is mapped to value number
+    [vn], or [None] if no such register exists. *)
 
 Definition reg_valnum (n: numbering) (vn: valnum) : option reg :=
   match PMap.get vn n.(num_val) with
@@ -281,10 +284,19 @@ Definition reg_valnum (n: numbering) (vn: valnum) : option reg :=
   | r :: rs => Some r
   end.
 
-(* [find_rhs] and its specializations [find_op] and [find_load]
-   return a register that already holds the result of the given arithmetic
-   operation or memory load, according to the given numbering.
-   [None] is returned if no such register exists. *)
+Fixpoint regs_valnums (n: numbering) (vl: list valnum) : option (list reg) :=
+  match vl with
+  | nil => Some nil
+  | v1 :: vs =>
+      match reg_valnum n v1, regs_valnums n vs with
+      | Some r1, Some rs => Some (r1 :: rs)
+      | _, _ => None
+      end
+  end.
+
+(** [find_rhs] return a register that already holds the result of the given arithmetic
+    operation or memory load, according to the given numbering.
+    [None] is returned if no such register exists. *)
 
 Definition find_rhs (n: numbering) (rh: rhs) : option reg :=
   match find_valnum_rhs rh n.(num_eqs) with
@@ -292,15 +304,44 @@ Definition find_rhs (n: numbering) (rh: rhs) : option reg :=
   | Some vres => reg_valnum n vres
   end.
 
-Definition find_op
-    (n: numbering) (op: operation) (rs: list reg) : option reg :=
-  let (n1, vl) := valnum_regs n rs in
-  find_rhs n1 (Op op vl).
+(** Experimental: take advantage of known equations to select more efficient
+  forms of operations, addressing modes, and conditions. *)
+
+Section REDUCE.
+
+Variable A: Type.
+Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
+Variable n: numbering.
+
+Fixpoint reduce_rec (niter: nat) (op: A) (args: list valnum) : option(A * list reg) :=
+  match niter with
+  | O => None
+  | S niter' =>
+      match f (fun v => find_valnum_num v n.(num_eqs)) op args with
+      | None => None
+      | Some(op', args') =>
+          match reduce_rec niter' op' args' with
+          | None =>
+              match regs_valnums n args' with Some rl => Some(op', rl) | None => None end
+          | Some _ as res =>
+              res
+          end
+      end
+  end.
+
+Definition reduce (op: A) (rl: list reg) (vl: list valnum) : A * list reg :=
+  match reduce_rec 4%nat op vl with
+  | None     => (op, rl)
+  | Some res => res
+  end.
+
+End REDUCE.
 
-Definition find_load
-    (n: numbering) (chunk: memory_chunk) (addr: addressing) (rs: list reg) : option reg :=
-  let (n1, vl) := valnum_regs n rs in
-  find_rhs n1 (Load chunk addr vl).
+(*
+Parameter combine_cond: (valnum -> option rhs) -> condition -> list valnum -> option (condition * list valnum).
+Parameter combine_addr: (valnum -> option rhs) -> addressing -> list valnum -> option (addressing * list valnum).
+Parameter combine_op: (valnum -> option rhs) -> operation -> list valnum -> option (operation * list valnum).
+*)
 
 (** * The static analysis *)
 
@@ -442,15 +483,31 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
   match instr with
   | Iop op args res s =>
       if is_trivial_op op then instr else
-        match find_op n op args with
-        | None => instr
-        | Some r => Iop Omove (r :: nil) res s
+        let (n1, vl) := valnum_regs n args in
+        match find_rhs n1 (Op op vl) with
+        | Some r =>
+            Iop Omove (r :: nil) res s
+        | None =>
+            let (op', args') := reduce _ combine_op n1 op args vl in
+            Iop op' args' res s
         end
   | Iload chunk addr args dst s =>
-      match find_load n chunk addr args with
-      | None => instr
-      | Some r => Iop Omove (r :: nil) dst s
+      let (n1, vl) := valnum_regs n args in
+      match find_rhs n1 (Load chunk addr vl) with
+      | Some r =>
+          Iop Omove (r :: nil) dst s
+      | None =>
+          let (addr', args') := reduce _ combine_addr n1 addr args vl in
+          Iload chunk addr' args' dst s
       end
+  | Istore chunk addr args src s =>
+      let (n1, vl) := valnum_regs n args in
+      let (addr', args') := reduce _ combine_addr n1 addr args vl in
+      Istore chunk addr' args' src s
+  | Icond cond args s1 s2 =>
+      let (n1, vl) := valnum_regs n args in
+      let (cond', args') := reduce _ combine_cond n1 cond args vl in
+      Icond cond' args' s1 s2
   | _ =>
       instr
   end.
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index fa07716..49b213b 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -28,6 +28,8 @@ Require Import Registers.
 Require Import RTL.
 Require Import RTLtyping.
 Require Import Kildall.
+Require Import CombineOp.
+Require Import CombineOpproof.
 Require Import CSE.
 
 (** * Semantic properties of value numberings *)
@@ -708,7 +710,7 @@ Proof.
   eapply VAL. rewrite Heql. auto with coqlib.
 Qed.
 
-(** Correctness of [find_op] and [find_load]: if successful and in a
+(** Correctness of [find_rhs]: if successful and in a
   satisfiable numbering, the returned register does contain the 
   result value of the operation or memory load. *)
 
@@ -730,42 +732,73 @@ Proof.
   discriminate.
 Qed.
 
-Lemma find_op_correct:
-  forall rs m n op args r,
-  wf_numbering n ->
-  numbering_satisfiable ge sp rs m n ->
-  find_op n op args = Some r ->
-  eval_operation ge sp op rs##args m = Some rs#r.
+(** Correctness of operator reduction *)
+
+Section REDUCE.
+
+Variable A: Type.
+Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
+Variable V: Type.
+Variable rs: regset.
+Variable m: mem.
+Variable sem: A -> list val -> option V.
+Hypothesis f_sound:
+  forall eqs valu op args op' args',
+  (forall v rhs, eqs v = Some rhs -> equation_holds valu ge sp m v rhs) ->
+  f eqs op args = Some(op', args') ->
+  sem op' (map valu args') = sem op (map valu args).
+Variable n: numbering.
+Variable valu: valnum -> val.
+Hypothesis n_holds: numbering_holds valu ge sp rs m n.
+Hypothesis n_wf: wf_numbering n.
+
+Lemma regs_valnums_correct:
+  forall vl rl, regs_valnums n vl = Some rl -> rs##rl = map valu vl.
 Proof.
-  intros until r. intros WF [valu NH].
-  unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND.
-  assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto).
-  generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR).
-  intros [valu2 [NH2 [EQ AG]]].
-  rewrite <- EQ. 
-  change (rhs_evals_to valu2 (Op op vl) m rs#r).
-  eapply find_rhs_correct; eauto.
+  induction vl; simpl; intros.
+  inv H. auto.
+  destruct (reg_valnum n a) as [r1|]_eqn; try discriminate.
+  destruct (regs_valnums n vl) as [rx|]_eqn; try discriminate.
+  inv H. simpl; decEq; auto. 
+  eapply (proj2 n_holds); eauto. eapply reg_valnum_correct; eauto.
 Qed.
 
-Lemma find_load_correct:
-  forall rs m n chunk addr args r,
-  wf_numbering n ->
-  numbering_satisfiable ge sp rs m n ->
-  find_load n chunk addr args = Some r ->
-  exists a,
-  eval_addressing ge sp addr rs##args = Some a /\
-  Mem.loadv chunk m a = Some rs#r.
+Lemma reduce_rec_sound:
+  forall niter op args op' rl' res,
+  reduce_rec A f n niter op args = Some(op', rl') ->
+  sem op (map valu args) = Some res ->
+  sem op' (rs##rl') = Some res.
 Proof.
-  intros until r. intros WF [valu NH].
-  unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND.
-  assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto).
-  generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR).
-  intros [valu2 [NH2 [EQ AG]]].
-  rewrite <- EQ. 
-  change (rhs_evals_to valu2 (Load chunk addr vl) m rs#r).
-  eapply find_rhs_correct; eauto.
+  induction niter; simpl; intros.
+  discriminate.
+  destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args)
+           as [[op1 args1] | ]_eqn.
+  assert (sem op1 (map valu args1) = Some res).
+    rewrite <- H0. eapply f_sound; eauto.
+    simpl; intros. apply (proj1 n_holds). eapply find_valnum_num_correct; eauto. 
+  destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ]_eqn.
+  inv H. eapply IHniter; eauto.
+  destruct (regs_valnums n args1) as [rl|]_eqn.
+  inv H. erewrite regs_valnums_correct; eauto.
+  discriminate.
+  discriminate.
 Qed.
 
+Lemma reduce_sound:
+  forall op rl vl op' rl' res,
+  reduce A f n op rl vl = (op', rl') ->
+  map valu vl = rs##rl ->
+  sem op rs##rl = Some res ->
+  sem op' rs##rl' = Some res.
+Proof.
+  unfold reduce; intros. 
+  destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ]_eqn; inv H.
+  eapply reduce_rec_sound; eauto. congruence.
+  auto.
+Qed.
+
+End REDUCE.
+
 End SATISFIABILITY.
 
 (** The numberings associated to each instruction by the static analysis
@@ -942,17 +975,27 @@ Proof.
 
   (* Iop *)
   exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split.
-  assert (eval_operation tge sp op rs##args m = Some v).
-    rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
   destruct (is_trivial_op op) as []_eqn.
-  eapply exec_Iop'; eauto. 
-  destruct (find_op approx!!pc op args) as [r|]_eqn. 
-  eapply exec_Iop'; eauto. simpl. 
-  assert (eval_operation ge sp op rs##args m = Some rs#r).
-    eapply find_op_correct; eauto.
-    eapply wf_analyze; eauto.
-  congruence.
   eapply exec_Iop'; eauto.
+  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (find_rhs n1 (Op op vl)) as [r|]_eqn.
+  (* replaced by move *)
+  assert (EV: rhs_evals_to ge sp valu2 (Op op vl) m rs#r). eapply find_rhs_correct; eauto.
+  assert (RES: rs#r = v). red in EV. congruence.
+  eapply exec_Iop'; eauto. simpl. congruence. 
+  (* possibly simplified *)
+  destruct (reduce operation combine_op n1 op args vl) as [op' args']_eqn.
+  assert (RES: eval_operation ge sp op' rs##args' m = Some v).
+    eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. 
+    intros; eapply combine_op_sound; eauto.
+  eapply exec_Iop'; eauto.
+  rewrite <- RES. apply eval_operation_preserved. exact symbols_preserved.
+  (* state matching *)
   econstructor; eauto.
   apply wt_regset_assign; auto. 
   generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
@@ -966,17 +1009,25 @@ Proof.
 
   (* Iload *)
   exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split.
-  assert (eval_addressing tge sp addr rs##args = Some a).
-    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  destruct (find_load approx!!pc chunk addr args) as [r|]_eqn.
-  eapply exec_Iop'; eauto. simpl. 
-  assert (exists a, eval_addressing ge sp addr rs##args = Some a
-                 /\ Mem.loadv chunk m a = Some rs#r).
-    eapply find_load_correct; eauto.
-    eapply wf_analyze; eauto.
-  destruct H3 as [a' [A B]].
-  congruence.
-  eapply exec_Iload'; eauto.
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (find_rhs n1 (Load chunk addr vl)) as [r|]_eqn.
+  (* replaced by move *)
+  assert (EV: rhs_evals_to ge sp valu2 (Load chunk addr vl) m rs#r). eapply find_rhs_correct; eauto.
+  assert (RES: rs#r = v). red in EV. destruct EV as [a' [EQ1 EQ2]]. congruence.
+  eapply exec_Iop'; eauto. simpl. congruence. 
+  (* possibly simplified *)
+  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn.
+  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
+    eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
+    intros; eapply combine_addr_sound; eauto.
+  assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload; eauto.
+  (* state matching *)
   econstructor; eauto.
   generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI.
   apply wt_regset_assign. auto. rewrite H8. eapply type_of_chunk_correct; eauto.
@@ -986,8 +1037,17 @@ Proof.
 
   (* Istore *)
   exists (State s' (transf_function' f approx) sp pc' rs m'); split.
-  assert (eval_addressing tge sp addr rs##args = Some a).
-    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn.
+  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
+    eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. 
+    intros; eapply combine_addr_sound; eauto.
+  assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a).
+    rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Istore; eauto.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto. 
@@ -1035,6 +1095,15 @@ Proof.
   eapply kill_loads_satisfiable; eauto. 
 
   (* Icond *)
+  destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn.
+  assert (wf_numbering approx!!pc). eapply wf_analyze; eauto.
+  elim SAT; intros valu1 NH1.
+  exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. 
+  assert (wf_numbering n1). eapply wf_valnum_regs; eauto. 
+  destruct (reduce condition combine_cond n1 cond args vl) as [cond' args']_eqn.
+  assert (RES: eval_condition cond' rs##args' m = Some b).
+    eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. 
+    intros; eapply combine_cond_sound; eauto.
   econstructor; split.
   eapply exec_Icond; eauto. 
   econstructor; eauto.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index c62e173..f88ca81 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -868,9 +868,10 @@ Proof.
     eauto.
   fold (saddr ctx addr). intros [a' [P Q]].
   exploit Mem.loadv_inject; eauto. intros [v' [U V]].
+  assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a').
+  rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
   left; econstructor; split.
-  eapply plus_one. eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto.
-  exact symbols_preserved. 
+  eapply plus_one. eapply exec_Iload; eauto.
   econstructor; eauto. 
   apply match_stacks_inside_set_reg; auto.
   apply agree_set_reg; auto. 
@@ -885,9 +886,10 @@ Proof.
   fold saddr. intros [a' [P Q]].
   exploit Mem.storev_mapped_inject; eauto. eapply agree_val_reg; eauto. 
   intros [m1' [U V]].
+  assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a').
+    rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
   left; econstructor; split.
-  eapply plus_one. eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto.
-  exact symbols_preserved. 
+  eapply plus_one. eapply exec_Istore; eauto.
   destruct a; simpl in H1; try discriminate.
   destruct a'; simpl in U; try discriminate.
   econstructor; eauto.
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 50db0c6..b72268a 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -641,7 +641,7 @@ Proof.
   econstructor; split.
   eapply plus_left'.  
   eapply exec_Lcond_false; eauto.
-  change false with (negb true). apply eval_negate_condition; auto.
+  rewrite eval_negate_condition; rewrite H0; auto.
   eapply add_branch_correct; eauto.
   eapply is_tail_add_branch. eapply is_tail_cons_left. 
   eapply is_tail_find_label. eauto.
@@ -657,7 +657,7 @@ Proof.
   destruct (starts_with ifso c').
   econstructor; split.
   apply plus_one. eapply exec_Lcond_true; eauto.
-  change true with (negb false). apply eval_negate_condition; auto.
+  rewrite eval_negate_condition; rewrite H0; auto.
   econstructor; eauto.
   econstructor; split.
   eapply plus_left'. 
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index a1b32b8..5ec29e2 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -171,13 +171,15 @@ Proof.
   constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* load *)
   econstructor; split.
-  eapply exec_Iload; eauto.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. 
+  eapply exec_Iload; eauto.
   constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* store *)
   econstructor; split.
-  eapply exec_Istore; eauto.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. 
+  eapply exec_Istore; eauto.
   constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* call *)
   econstructor; split.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 4e67181..0aa2b6b 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -50,7 +50,7 @@ Proof.
   induction 1; simpl.
   constructor.
   constructor.
-  econstructor. eauto. apply eval_negate_condition. auto.
+  econstructor. eauto. rewrite eval_negate_condition. rewrite H0. auto.
   econstructor. eauto. destruct vb1; auto.
 Qed. 
 
@@ -124,7 +124,7 @@ Proof.
   intros. apply is_compare_neq_zero_correct with (negate_condition c).
   destruct c; simpl in H; simpl; try discriminate;
   destruct c; simpl; try discriminate; auto.
-  apply eval_negate_condition; auto.
+  rewrite eval_negate_condition. rewrite H0. auto.
 Qed.
 
 Lemma eval_condition_of_expr: