diff options
Diffstat (limited to 'ia32/CombineOpproof.v')
-rw-r--r-- | ia32/CombineOpproof.v | 48 |
1 files changed, 37 insertions, 11 deletions
diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v index 8f600054..f59e582b 100644 --- a/ia32/CombineOpproof.v +++ b/ia32/CombineOpproof.v @@ -2,7 +2,7 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -14,12 +14,8 @@ during the [CSE] phase. *) Require Import Coqlib. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Op. -Require Import RTL. -Require Import CSEdomain. +Require Import Integers Values Memory. +Require Import Op RTL CSEdomain. Require Import CombineOp. Section COMBINE. @@ -122,14 +118,36 @@ Proof. simpl; eapply combine_compimm_eq_1_sound; eauto. Qed. +Theorem combine_addr_32_sound: + forall addr args addr' args', + combine_addr_32 get addr args = Some(addr', args') -> + eval_addressing32 ge sp addr' (map valu args') = eval_addressing32 ge sp addr (map valu args). +Proof. + intros. functional inversion H; subst. + (* indexed - lea *) + UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. + eapply eval_offset_addressing_total_32; eauto. +Qed. + +Theorem combine_addr_64_sound: + forall addr args addr' args', + combine_addr_64 get addr args = Some(addr', args') -> + eval_addressing64 ge sp addr' (map valu args') = eval_addressing64 ge sp addr (map valu args). +Proof. + intros. functional inversion H; subst. + (* indexed - leal *) + UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. + eapply eval_offset_addressing_total_64; 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 - lea *) - UseGetSound. simpl. eapply eval_offset_addressing_total; eauto. + unfold combine_addr, eval_addressing; intros; destruct Archi.ptr64. + apply combine_addr_64_sound; auto. + apply combine_addr_32_sound; auto. Qed. Theorem combine_op_sound: @@ -139,13 +157,21 @@ Theorem combine_op_sound: Proof. intros. functional inversion H; subst. (* lea-lea *) - simpl. eapply combine_addr_sound; eauto. + simpl. eapply combine_addr_32_sound; eauto. +(* leal-leal *) + simpl. eapply combine_addr_64_sound; eauto. (* andimm - andimm *) UseGetSound; simpl. rewrite <- H0. rewrite Val.and_assoc. auto. (* orimm - orimm *) UseGetSound; simpl. rewrite <- H0. rewrite Val.or_assoc. auto. (* xorimm - xorimm *) UseGetSound; simpl. rewrite <- H0. rewrite Val.xor_assoc. auto. +(* andimm - andimm *) + UseGetSound; simpl. rewrite <- H0. rewrite Val.andl_assoc. auto. +(* orimm - orimm *) + UseGetSound; simpl. rewrite <- H0. rewrite Val.orl_assoc. auto. +(* xorimm - xorimm *) + UseGetSound; simpl. rewrite <- H0. rewrite Val.xorl_assoc. auto. (* cmp *) simpl. decEq; decEq. eapply combine_cond_sound; eauto. Qed. |