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.