diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-14 15:41:26 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-14 15:41:26 +0000 |
commit | 5aea6849eed83009e300b04ef17786643ead9cbc (patch) | |
tree | eb9a329ce46a7ddc568a2fba7692b8eaea1e618f /ia32/Asmgenretaddr.v | |
parent | fd0f28867db2f183216b27d7030265ae9e887586 (diff) | |
download | compcert-5aea6849eed83009e300b04ef17786643ead9cbc.tar.gz compcert-5aea6849eed83009e300b04ef17786643ead9cbc.zip |
Locations.v: add Loc.diff_dec.
ia32: lift restriction that 1st arg of ops cannot be ECX
(could be useful for a future, better reloading strategy)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1711 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgenretaddr.v')
-rw-r--r-- | ia32/Asmgenretaddr.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v index e0787d72..e963c2e4 100644 --- a/ia32/Asmgenretaddr.v +++ b/ia32/Asmgenretaddr.v @@ -112,7 +112,7 @@ Ltac IsTail := match goal with | [ |- is_tail _ (_ :: _) ] => constructor; IsTail | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inversion H; subst; IsTail + | [ H: OK _ = OK _ |- _ ] => inv H; IsTail | [ H: bind _ _ = OK _ |- _ ] => monadInv H; IsTail | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; IsTail | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; IsTail @@ -131,16 +131,28 @@ Proof. unfold mk_shift; intros; IsTail. Qed. +Lemma mk_mov2_tail: + forall r1 r2 r3 r4 k, is_tail k (mk_mov2 r1 r2 r3 r4 k). +Proof. + unfold mk_mov2; intros. + destruct (ireg_eq r1 r2). IsTail. + destruct (ireg_eq r3 r4). IsTail. + destruct (ireg_eq r3 r2); IsTail. + destruct (ireg_eq r1 r4); IsTail. +Qed. + Lemma mk_div_tail: forall di r1 r2 k c, mk_div di r1 r2 k = OK c -> is_tail k c. Proof. unfold mk_div; intros; IsTail. + eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail. Qed. Lemma mk_mod_tail: forall di r1 r2 k c, mk_mod di r1 r2 k = OK c -> is_tail k c. Proof. unfold mk_mod; intros; IsTail. + eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail. Qed. Lemma mk_shrximm_tail: |