From a14b9578ee5297d954103e05d7b2d322816ddd8f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sat, 1 Oct 2016 17:38:24 +0200
Subject: Support for 64-bit architectures: x86 in 64-bit mode

This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.

To activate x86-64 bit support, configure with "x86_64-linux".

Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode

To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
  (currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.
---
 ia32/ConstpropOpproof.v | 499 +++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 410 insertions(+), 89 deletions(-)

(limited to 'ia32/ConstpropOpproof.v')

diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 3dfb8ccf..4175d2f9 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.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       *)
@@ -12,26 +12,11 @@
 
 (** Correctness proof for operator strength reduction. *)
 
-Require Import Coqlib.
-Require Import Compopts.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import ValueDomain.
+Require Import Coqlib Compopts.
+Require Import Integers Floats Values Memory Globalenvs Events.
+Require Import Op Registers RTL ValueDomain.
 Require Import ConstpropOp.
 
-(** We now show that strength reduction over operators and addressing
-  modes preserve semantics: the strength-reduced operations and
-  addressings evaluate to the same values as the original ones if the
-  actual arguments match the static approximations used for strength
-  reduction. *)
-
 Section STRENGTH_REDUCTION.
 
 Variable bc: block_classification.
@@ -73,6 +58,10 @@ Ltac SimplVM :=
       let E := fresh in
       assert (E: v = Vint n) by (inversion H; auto);
       rewrite E in *; clear H; SimplVM
+  | [ H: vmatch _ ?v (L ?n) |- _ ] =>
+      let E := fresh in
+      assert (E: v = Vlong n) by (inversion H; auto);
+      rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (F ?n) |- _ ] =>
       let E := fresh in
       assert (E: v = Vfloat n) by (inversion H; auto);
@@ -92,6 +81,43 @@ Ltac SimplVM :=
   | _ => idtac
   end.
 
+Lemma eval_Olea_ptr:
+  forall a el,
+  eval_operation ge (Vptr sp Ptrofs.zero) (Olea_ptr a) el m = eval_addressing ge (Vptr sp Ptrofs.zero) a el.
+Proof.
+  unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. 
+Qed.
+
+Lemma const_for_result_correct:
+  forall a op v,
+  const_for_result a = Some op ->
+  vmatch bc v a ->
+  exists v', eval_operation ge (Vptr sp Ptrofs.zero) op nil m = Some v' /\ Val.lessdef v v'.
+Proof.
+  unfold const_for_result; intros.
+  destruct a; inv H; SimplVM.
+- (* integer *)
+  exists (Vint n); auto.
+- (* long *)
+  destruct Archi.ptr64; inv H2. exists (Vlong n); auto.
+- (* float *)
+  destruct (Compopts.generate_float_constants tt); inv H2. exists (Vfloat f); auto.
+- (* single *)
+  destruct (Compopts.generate_float_constants tt); inv H2. exists (Vsingle f); auto.
+- (* pointer *)
+  destruct p; try discriminate; SimplVM.
+  + (* global *)
+    destruct (symbol_is_external id).
+  * revert H2; predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero; intros EQ; inv EQ.
+    exists (Genv.symbol_address ge id Ptrofs.zero); auto.
+  * inv H2. exists (Genv.symbol_address ge id ofs); split; auto.
+    rewrite eval_Olea_ptr. apply eval_addressing_Aglobal.  
+  + (* stack *)
+    inv H2. exists (Vptr sp ofs); split; auto.
+    rewrite eval_Olea_ptr. rewrite eval_addressing_Ainstack.  
+    simpl. rewrite Ptrofs.add_zero_l; auto.  
+Qed.
+
 Lemma cond_strength_reduction_correct:
   forall cond args vl,
   vl = map (fun r => AE.get r ae) args ->
@@ -104,64 +130,175 @@ Proof.
 - auto.
 - apply Val.swap_cmpu_bool.
 - auto.
+- apply Val.swap_cmpl_bool.
+- auto.
+- apply Val.swap_cmplu_bool.
+- auto.
 - auto.
 Qed.
 
-Lemma addr_strength_reduction_correct:
+Lemma addr_strength_reduction_32_generic_correct:
   forall addr args vl res,
   vl = map (fun r => AE.get r ae) args ->
-  eval_addressing ge (Vptr sp Int.zero) addr e##args = Some res ->
-  let (addr', args') := addr_strength_reduction addr args vl in
-  exists res', eval_addressing ge (Vptr sp Int.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
-Proof.
-  intros until res. unfold addr_strength_reduction.
-  destruct (addr_strength_reduction_match addr args vl); simpl;
-  intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- rewrite Genv.shift_symbol_address. econstructor; split. eauto. apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Int.add_zero_l.
-  change (Vptr sp (Int.add n ofs)) with (Val.add (Vptr sp n) (Vint ofs)). apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Int.add_assoc. rewrite Genv.shift_symbol_address.
-  rewrite Val.add_assoc. apply Val.add_lessdef; auto.
-- econstructor; split; eauto.
-  fold (Val.add (Vint n1) e#r2). rewrite (Val.add_commut (Vint n1)).
-  rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto.
-  rewrite Int.add_commut. rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Int.add_zero_l. rewrite Int.add_assoc.
-  change (Vptr sp (Int.add n1 (Int.add n2 ofs)))
-    with (Val.add (Vptr sp n1) (Vint (Int.add n2 ofs))).
-  rewrite Val.add_assoc. apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Int.add_zero_l.
-  fold (Val.add (Vint n1) e#r2). rewrite (Int.add_commut n1).
-  change (Vptr sp (Int.add (Int.add n2 n1) ofs))
-    with (Val.add (Val.add (Vint n1) (Vptr sp n2)) (Vint ofs)).
-  apply Val.add_lessdef; auto. apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Genv.shift_symbol_address.
+  eval_addressing32 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
+  let (addr', args') := addr_strength_reduction_32_generic addr args vl in
+  exists res', eval_addressing32 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
+Proof.
+Local Opaque Val.add.
+  assert (A: forall x y, Int.repr (Int.signed x + y) = Int.add x (Int.repr y)).
+  { intros; apply Int.eqm_samerepr; auto using Int.eqm_signed_unsigned with ints. }
+  assert (B: forall x y z, Int.repr (Int.signed x * y + z) = Int.add (Int.mul x (Int.repr y)) (Int.repr z)).
+  { intros; apply Int.eqm_samerepr; apply Int.eqm_add; auto with ints.
+    unfold Int.mul; auto using Int.eqm_signed_unsigned with ints. }
+  intros until res; intros VL EA. 
+  unfold addr_strength_reduction_32_generic; destruct (addr_strength_reduction_32_generic_match addr args vl); 
+  simpl in *; InvApproxRegs; SimplVM; try (inv EA).
+- econstructor; split; eauto. rewrite A, Val.add_assoc, Val.add_permut. auto.
+- econstructor; split; eauto. rewrite A, Val.add_assoc. auto.
+- Local Transparent Val.add.
+  econstructor; split; eauto. simpl. rewrite B. auto.
+- econstructor; split; eauto. rewrite A, Val.add_permut. auto.
+- exists res; auto.
+Qed.
+
+Lemma addr_strength_reduction_32_correct:
+  forall addr args vl res,
+  vl = map (fun r => AE.get r ae) args ->
+  eval_addressing32 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
+  let (addr', args') := addr_strength_reduction_32 addr args vl in
+  exists res', eval_addressing32 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
+Proof.
+  intros until res; intros VL EA. unfold addr_strength_reduction_32.
+  destruct Archi.ptr64 eqn:SF. apply addr_strength_reduction_32_generic_correct; auto.
+  assert (A: forall n, Ptrofs.of_int (Int.repr n) = Ptrofs.repr n) by auto with ptrofs.
+  assert (B: forall symb ofs n,
+             Genv.symbol_address ge symb (Ptrofs.add ofs (Ptrofs.repr n)) =
+             Val.add (Genv.symbol_address ge symb ofs) (Vint (Int.repr n))).
+  { intros. rewrite <- A. apply Genv.shift_symbol_address_32; auto. }
+Local Opaque Val.add.
+  destruct (addr_strength_reduction_32_match addr args vl); 
+  simpl in *; InvApproxRegs; SimplVM; try (inv EA); rewrite ? SF.
+- econstructor; split; eauto. rewrite B. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Ptrofs.add_zero_l.
+Local Transparent Val.add.
+  inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto.
+- econstructor; split; eauto. 
+  unfold Ptrofs.add at 2. rewrite B. 
+  fold (Ptrofs.add n1 (Ptrofs.of_int n2)).
+  rewrite Genv.shift_symbol_address_32 by auto.
   rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
-  rewrite Val.add_commut. apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Genv.shift_symbol_address.
-  rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc.
-  apply Val.add_lessdef; auto. rewrite Val.add_commut. apply Val.add_lessdef; auto.
-- fold (Val.add (Vint n1) e#r2). econstructor; split; eauto.
-  rewrite (Val.add_commut (Vint n1)). rewrite Val.add_assoc.
-  apply Val.add_lessdef; eauto.
-- econstructor; split; eauto.  rewrite ! Val.add_assoc.
-  apply Val.add_lessdef; eauto.
-- econstructor; split; eauto. rewrite Int.add_assoc.
-  rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto.
 - econstructor; split; eauto.
-  rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
-  rewrite Val.add_commut; auto.
+  unfold Ptrofs.add at 2. rewrite B. 
+  fold (Ptrofs.add n2 (Ptrofs.of_int n1)).
+  rewrite Genv.shift_symbol_address_32 by auto.
+  rewrite ! Val.add_assoc. rewrite Val.add_permut. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.add_assoc.
+  eapply Val.lessdef_trans. apply Val.add_lessdef; eauto.
+  simpl. rewrite SF. rewrite Ptrofs.add_assoc. apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
+- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.add_assoc, Val.add_permut.
+  eapply Val.lessdef_trans. apply Val.add_lessdef; eauto.
+  simpl. rewrite SF. rewrite <- (Ptrofs.add_commut n2). rewrite Ptrofs.add_assoc.
+  apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
+- econstructor; split; eauto. rewrite B. rewrite ! Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr ofs))).
+  apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite B. rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc. 
+  rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite B. rewrite Genv.shift_symbol_address_32 by auto.
+  rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite B. rewrite ! Val.add_assoc.
+  rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto.
+- rewrite SF in H1; inv H1. econstructor; split; eauto.
+  rewrite Genv.shift_symbol_address_32 by auto. auto.
+- rewrite SF in H1; inv H1. econstructor; split; eauto.
+  rewrite Genv.shift_symbol_address_32 by auto. auto.
+- apply addr_strength_reduction_32_generic_correct; auto.
+Qed.
+
+Lemma addr_strength_reduction_64_generic_correct:
+  forall addr args vl res,
+  vl = map (fun r => AE.get r ae) args ->
+  eval_addressing64 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
+  let (addr', args') := addr_strength_reduction_64_generic addr args vl in
+  exists res', eval_addressing64 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
+Proof.
+Local Opaque Val.addl.
+  assert (A: forall x y, Int64.repr (Int64.signed x + y) = Int64.add x (Int64.repr y)).
+  { intros; apply Int64.eqm_samerepr; auto using Int64.eqm_signed_unsigned with ints. }
+  assert (B: forall x y z, Int64.repr (Int64.signed x * y + z) = Int64.add (Int64.mul x (Int64.repr y)) (Int64.repr z)).
+  { intros; apply Int64.eqm_samerepr; apply Int64.eqm_add; auto with ints.
+    unfold Int64.mul; auto using Int64.eqm_signed_unsigned with ints. }
+  intros until res; intros VL EA. 
+  unfold addr_strength_reduction_64_generic; destruct (addr_strength_reduction_64_generic_match addr args vl); 
+  simpl in *; InvApproxRegs; SimplVM; try (inv EA).
+- econstructor; split; eauto. rewrite A, Val.addl_assoc, Val.addl_permut. auto.
+- econstructor; split; eauto. rewrite A, Val.addl_assoc. auto.
+- Local Transparent Val.addl.
+  econstructor; split; eauto. simpl. rewrite B. auto.
+- econstructor; split; eauto. rewrite A, Val.addl_permut. auto.
+- exists res; auto.
+Qed.
+
+Lemma addr_strength_reduction_64_correct:
+  forall addr args vl res,
+  vl = map (fun r => AE.get r ae) args ->
+  eval_addressing64 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
+  let (addr', args') := addr_strength_reduction_64 addr args vl in
+  exists res', eval_addressing64 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
+Proof.
+  intros until res; intros VL EA. unfold addr_strength_reduction_64.
+  destruct (negb Archi.ptr64) eqn:SF. apply addr_strength_reduction_64_generic_correct; auto.
+  rewrite negb_false_iff in SF.
+  assert (A: forall n, Ptrofs.of_int64 (Int64.repr n) = Ptrofs.repr n) by auto with ptrofs.
+  assert (B: forall symb ofs n,
+             Genv.symbol_address ge symb (Ptrofs.add ofs (Ptrofs.repr n)) =
+             Val.addl (Genv.symbol_address ge symb ofs) (Vlong (Int64.repr n))).
+  { intros. rewrite <- A. apply Genv.shift_symbol_address_64; auto. }
+Local Opaque Val.addl.
+  destruct (addr_strength_reduction_64_match addr args vl); 
+  simpl in *; InvApproxRegs; SimplVM; try (inv EA); rewrite ? SF.
+- econstructor; split; eauto. rewrite B. apply Val.addl_lessdef; auto.
+- econstructor; split; eauto. rewrite Ptrofs.add_zero_l.
+Local Transparent Val.addl.
+  inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto.
+- econstructor; split; eauto. 
+  unfold Ptrofs.add at 2. rewrite B. 
+  fold (Ptrofs.add n1 (Ptrofs.of_int64 n2)).
+  rewrite Genv.shift_symbol_address_64 by auto.
+  rewrite ! Val.addl_assoc. apply Val.addl_lessdef; auto.
 - econstructor; split; eauto.
-- econstructor; split; eauto. rewrite Genv.shift_symbol_address. auto.
-- econstructor; split; eauto. rewrite Genv.shift_symbol_address. rewrite Int.mul_commut; auto.
-- econstructor; eauto.
+  unfold Ptrofs.add at 2. rewrite B. 
+  fold (Ptrofs.add n2 (Ptrofs.of_int64 n1)).
+  rewrite Genv.shift_symbol_address_64 by auto.
+  rewrite ! Val.addl_assoc. rewrite Val.addl_permut. apply Val.addl_lessdef; auto.
+- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.addl_assoc.
+  eapply Val.lessdef_trans. apply Val.addl_lessdef; eauto.
+  simpl. rewrite SF. rewrite Ptrofs.add_assoc. apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
+- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.addl_assoc, Val.addl_permut.
+  eapply Val.lessdef_trans. apply Val.addl_lessdef; eauto.
+  simpl. rewrite SF. rewrite <- (Ptrofs.add_commut n2). rewrite Ptrofs.add_assoc.
+  apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
+- econstructor; split; eauto. rewrite B. rewrite Genv.shift_symbol_address_64 by auto.
+  rewrite ! Val.addl_assoc. apply Val.addl_lessdef; auto.
+- apply addr_strength_reduction_64_generic_correct; auto.
+Qed.
+
+Lemma addr_strength_reduction_correct:
+  forall addr args vl res,
+  vl = map (fun r => AE.get r ae) args ->
+  eval_addressing ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
+  let (addr', args') := addr_strength_reduction addr args vl in
+  exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
+Proof.
+  unfold eval_addressing, addr_strength_reduction. destruct Archi.ptr64.
+  apply addr_strength_reduction_64_correct.
+  apply addr_strength_reduction_32_correct.
 Qed.
 
 Lemma make_cmp_base_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp_base c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some v
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
 Proof.
   intros. unfold make_cmp_base.
@@ -174,7 +311,7 @@ Lemma make_cmp_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some v
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
 Proof.
   intros c args vl.
@@ -206,19 +343,20 @@ Qed.
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.add e#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.add e#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite Int.add_zero; auto.
-  exists (Val.add e#r (Vint n)); auto.
+  subst. exists (e#r); split; auto.
+  destruct (e#r); simpl; auto. rewrite Int.add_zero; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. 
+  exists (Val.add e#r (Vint n)); split; auto. simpl. rewrite Int.repr_signed; auto. 
 Qed.
 
 Lemma make_shlimm_correct:
   forall n r1 r2,
   e#r2 = Vint n ->
   let (op, args) := make_shlimm n r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shl e#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shl e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -232,7 +370,7 @@ Lemma make_shrimm_correct:
   forall n r1 r2,
   e#r2 = Vint n ->
   let (op, args) := make_shrimm n r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shr e#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shr e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -246,7 +384,7 @@ Lemma make_shruimm_correct:
   forall n r1 r2,
   e#r2 = Vint n ->
   let (op, args) := make_shruimm n r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shru e#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shru e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -259,7 +397,7 @@ Qed.
 Lemma make_mulimm_correct:
   forall n r1,
   let (op, args) := make_mulimm n r1 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mul e#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mul e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_mulimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -276,7 +414,7 @@ Lemma make_divimm_correct:
   Val.divs e#r1 e#r2 = Some v ->
   e#r2 = Vint n ->
   let (op, args) := make_divimm n r1 r2 in
-  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -291,7 +429,7 @@ Lemma make_divuimm_correct:
   Val.divu e#r1 e#r2 = Some v ->
   e#r2 = Vint n ->
   let (op, args) := make_divuimm n r1 r2 in
-  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -305,7 +443,7 @@ Lemma make_moduimm_correct:
   Val.modu e#r1 e#r2 = Some v ->
   e#r2 = Vint n ->
   let (op, args) := make_moduimm n r1 r2 in
-  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_moduimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -317,7 +455,7 @@ Lemma make_andimm_correct:
   forall n r x,
   vmatch bc e#r x ->
   let (op, args) := make_andimm n r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.and e#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.and e#r (Vint n)) v.
 Proof.
   intros; unfold make_andimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -342,7 +480,7 @@ Qed.
 Lemma make_orimm_correct:
   forall n r,
   let (op, args) := make_orimm n r in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.or e#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.or e#r (Vint n)) v.
 Proof.
   intros; unfold make_orimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -355,7 +493,7 @@ Qed.
 Lemma make_xorimm_correct:
   forall n r,
   let (op, args) := make_xorimm n r in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.xor e#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.xor e#r (Vint n)) v.
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -365,11 +503,157 @@ Proof.
   econstructor; split; eauto. auto.
 Qed.
 
+Lemma make_addlimm_correct:
+  forall n r,
+  let (op, args) := make_addlimm n r in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.addl e#r (Vlong n)) v.
+Proof.
+  intros. unfold make_addlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst. exists (e#r); split; auto.
+  destruct (e#r); simpl; auto. rewrite Int64.add_zero; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. 
+  exists (Val.addl e#r (Vlong n)); split; auto. simpl. rewrite Int64.repr_signed; auto. 
+Qed.
+
+Lemma make_shllimm_correct:
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shllimm n r1 r2 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shll e#r1 (Vint n)) v.
+Proof.
+  intros; unfold make_shllimm.
+  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
+  unfold Int64.shl'. rewrite Z.shiftl_0_r, Int64.repr_unsigned. auto.
+  destruct (Int.ltu n Int64.iwordsize').
+  econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
+Qed.
+
+Lemma make_shrlimm_correct:
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shrlimm n r1 r2 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shrl e#r1 (Vint n)) v.
+Proof.
+  intros; unfold make_shrlimm.
+  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
+  unfold Int64.shr'. rewrite Z.shiftr_0_r, Int64.repr_signed. auto.
+  destruct (Int.ltu n Int64.iwordsize').
+  econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
+Qed.
+
+Lemma make_shrluimm_correct:
+  forall n r1 r2,
+  e#r2 = Vint n ->
+  let (op, args) := make_shrluimm n r1 r2 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shrlu e#r1 (Vint n)) v.
+Proof.
+  intros; unfold make_shrluimm.
+  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
+  unfold Int64.shru'. rewrite Z.shiftr_0_r, Int64.repr_unsigned. auto.
+  destruct (Int.ltu n Int64.iwordsize').
+  econstructor; split. simpl. eauto. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
+Qed.
+
+Lemma make_mullimm_correct:
+  forall n r1,
+  let (op, args) := make_mullimm n r1 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mull e#r1 (Vlong n)) v.
+Proof.
+  intros; unfold make_mullimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst.
+  exists (Vlong Int64.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.one; intros. subst.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_one; auto.
+  destruct (Int64.is_power2' n) eqn:?; intros.
+  exists (Val.shll e#r1 (Vint i)); split; auto.
+  destruct (e#r1); simpl; auto.
+  erewrite Int64.is_power2'_range by eauto.
+  erewrite Int64.mul_pow2' by eauto. auto.
+  econstructor; split; eauto. auto.
+Qed.
+
+Lemma make_divluimm_correct:
+  forall n r1 r2 v,
+  Val.divlu e#r1 e#r2 = Some v ->
+  e#r2 = Vlong n ->
+  let (op, args) := make_divluimm n r1 r2 in
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
+Proof.
+  intros; unfold make_divluimm.
+  destruct (Int64.is_power2' n) eqn:?.
+  econstructor; split. simpl; eauto.
+  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2.
+  simpl.
+  erewrite Int64.is_power2'_range by eauto.    
+  erewrite Int64.divu_pow2' by eauto.  auto. 
+  exists v; auto.
+Qed.
+
+Lemma make_modluimm_correct:
+  forall n r1 r2 v,
+  Val.modlu e#r1 e#r2 = Some v ->
+  e#r2 = Vlong n ->
+  let (op, args) := make_modluimm n r1 r2 in
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
+Proof.
+  intros; unfold make_modluimm.
+  destruct (Int64.is_power2 n) eqn:?.
+  exists v; split; auto. simpl. decEq.
+  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. 
+  simpl. erewrite Int64.modu_and by eauto. auto.
+  exists v; auto.
+Qed.
+
+Lemma make_andlimm_correct:
+  forall n r x,
+  let (op, args) := make_andlimm n r x in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.andl e#r (Vlong n)) v.
+Proof.
+  intros; unfold make_andlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_mone; auto.
+  econstructor; split; eauto. auto.
+Qed.
+
+Lemma make_orlimm_correct:
+  forall n r,
+  let (op, args) := make_orlimm n r in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.orl e#r (Vlong n)) v.
+Proof.
+  intros; unfold make_orlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
+  subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_mone; auto.
+  econstructor; split; eauto. auto.
+Qed.
+
+Lemma make_xorlimm_correct:
+  forall n r,
+  let (op, args) := make_xorlimm n r in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.xorl e#r (Vlong n)) v.
+Proof.
+  intros; unfold make_xorlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.xor_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
+  subst n. exists (Val.notl e#r); split; auto.
+  econstructor; split; eauto. auto.
+Qed.
+
 Lemma make_mulfimm_correct:
   forall n r1 r2,
   e#r2 = Vfloat n ->
   let (op, args) := make_mulfimm n r1 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfimm.
   destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
@@ -382,7 +666,7 @@ Lemma make_mulfimm_correct_2:
   forall n r1 r2,
   e#r1 = Vfloat n ->
   let (op, args) := make_mulfimm n r2 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfimm.
   destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
@@ -396,7 +680,7 @@ Lemma make_mulfsimm_correct:
   forall n r1 r2,
   e#r2 = Vsingle n ->
   let (op, args) := make_mulfsimm n r1 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfsimm.
   destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
@@ -409,7 +693,7 @@ Lemma make_mulfsimm_correct_2:
   forall n r1 r2,
   e#r1 = Vsingle n ->
   let (op, args) := make_mulfsimm n r2 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfsimm.
   destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
@@ -423,7 +707,7 @@ Lemma make_cast8signed_correct:
   forall r x,
   vmatch bc e#r x ->
   let (op, args) := make_cast8signed r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 8 e#r) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 8 e#r) v.
 Proof.
   intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL.
   exists e#r; split; auto.
@@ -437,7 +721,7 @@ Lemma make_cast8unsigned_correct:
   forall r x,
   vmatch bc e#r x ->
   let (op, args) := make_cast8unsigned r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 8 e#r) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 8 e#r) v.
 Proof.
   intros; unfold make_cast8unsigned. destruct (vincl x (Uns Ptop 8)) eqn:INCL.
   exists e#r; split; auto.
@@ -451,7 +735,7 @@ Lemma make_cast16signed_correct:
   forall r x,
   vmatch bc e#r x ->
   let (op, args) := make_cast16signed r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 16 e#r) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 16 e#r) v.
 Proof.
   intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL.
   exists e#r; split; auto.
@@ -465,7 +749,7 @@ Lemma make_cast16unsigned_correct:
   forall r x,
   vmatch bc e#r x ->
   let (op, args) := make_cast16unsigned r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 16 e#r) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 16 e#r) v.
 Proof.
   intros; unfold make_cast16unsigned. destruct (vincl x (Uns Ptop 16)) eqn:INCL.
   exists e#r; split; auto.
@@ -478,9 +762,9 @@ Qed.
 Lemma op_strength_reduction_correct:
   forall op args vl v,
   vl = map (fun r => AE.get r ae) args ->
-  eval_operation ge (Vptr sp Int.zero) op e##args m = Some v ->
+  eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v ->
   let (op', args') := op_strength_reduction op args vl in
-  exists w, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some w /\ Val.lessdef v w.
 Proof.
   intros until v; unfold op_strength_reduction;
   case (op_strength_reduction_match op args vl); simpl; intros.
@@ -523,8 +807,45 @@ Proof.
 (* shru *)
   InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto.
 (* lea *)
-  exploit addr_strength_reduction_correct; eauto.
-  destruct (addr_strength_reduction addr args0 vl0) as [addr' args'].
+  exploit addr_strength_reduction_32_correct; eauto.
+  destruct (addr_strength_reduction_32 addr args0 vl0) as [addr' args'].
+  auto.
+(* subl *)
+  InvApproxRegs; SimplVM; inv H0.
+  replace (Val.subl e#r1 (Vlong n2)) with (Val.addl e#r1 (Vlong (Int64.neg n2))).
+  apply make_addlimm_correct; auto.
+  destruct (e#r1); simpl; auto.
+  rewrite Int64.sub_add_opp; auto.
+  destruct Archi.ptr64 eqn:SF; auto.
+  rewrite Ptrofs.sub_add_opp. do 2 f_equal. auto with ptrofs.
+(* mull *)
+  rewrite Val.mull_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto.
+(* divlu *)
+  assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
+  apply make_divluimm_correct; auto.
+(* modlu *)
+  assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
+  apply make_modluimm_correct; auto.
+(* andl *)
+  rewrite Val.andl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto.
+  inv H; inv H0. apply make_andlimm_correct; auto.
+(* orl *)
+  rewrite Val.orl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_orlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_orlimm_correct; auto.
+(* xorl *)
+  rewrite Val.xorl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_xorlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_xorlimm_correct; auto.
+(* shll *)
+  InvApproxRegs; SimplVM; inv H0. apply make_shllimm_correct; auto.
+(* shrl *)
+  InvApproxRegs; SimplVM; inv H0. apply make_shrlimm_correct; auto.
+(* shrlu *)
+  InvApproxRegs; SimplVM; inv H0. apply make_shrluimm_correct; auto.
+(* leal *)
+  exploit addr_strength_reduction_64_correct; eauto.
+  destruct (addr_strength_reduction_64 addr args0 vl0) as [addr' args'].
   auto.
 (* cond *)
   inv H0. apply make_cmp_correct; auto.
-- 
cgit