diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-21 15:53:05 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-21 15:53:05 +0000 |
| commit | 58c7f5045c9cf1b64311fd7a168ed3b496666bb0 (patch) | |
| tree | b71dc7537a473b26a2109339e6ee21dc69581655 /powerpc/Asmgenproof1.v | |
| parent | b39791601bb128c37db82eb66a8bc1991047818f (diff) | |
Recognition of rlwimi instruction (useful for bitfield assignment)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1676 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgenproof1.v')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index ee3aa38..55a74be 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1340,7 +1340,27 @@ Proof. apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. apply agree_set_commut. auto with ppcgen. apply agree_set_other. apply agree_set_mireg_twice; auto with ppcgen. - compute; auto. auto with ppcgen. + compute; auto. auto with ppcgen. + (* Oroli *) + destruct (mreg_eq m0 res). subst m0. + TranslOpSimpl. + econstructor; split. + eapply exec_straight_three. + simpl. reflexivity. + simpl. reflexivity. + simpl. reflexivity. + auto. auto. auto. + set (rs1 := nextinstr (rs # GPR0 <- (rs (ireg_of m0)))). + set (rs2 := nextinstr (rs1 # GPR0 <- + (Val.or (Val.and (rs1 GPR0) (Vint (Int.not i0))) + (Val.rolm (rs1 (ireg_of m1)) i i0)))). + apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg. + apply agree_undef_temps with rs. auto. + intros. unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + unfold rs1. repeat rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gss. rewrite Pregmap.gso; auto with ppcgen. decEq. auto with ppcgen. (* Ointoffloat *) econstructor; split. apply exec_straight_one. simpl; eauto. auto. |