Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore utilisee dans le front-end C.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

19 files changed, 449 insertions, 10 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index df541a11..c1e3bd18 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -50,7 +50,8 @@ Inductive unary_operation : Set :=
   | Onegf: unary_operation                 (**r float opposite *)
   | Oabsf: unary_operation                 (**r float absolute value *)
   | Osingleoffloat: unary_operation        (**r float truncation *)
-  | Ointoffloat: unary_operation           (**r integer to float *)
+  | Ointoffloat: unary_operation           (**r signed integer to float *)
+  | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
   | Ofloatofint: unary_operation           (**r float to signed integer *)
   | Ofloatofintu: unary_operation.         (**r float to unsigned integer *)
 
@@ -239,6 +240,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Oabsf, Vfloat f1 => Some (Vfloat (Float.abs f1))
   | Osingleoffloat, _ => Some (Val.singleoffloat arg)
   | Ointoffloat, Vfloat f1 => Some (Vint (Float.intoffloat f1))
+  | Ointuoffloat, Vfloat f1 => Some (Vint (Float.intuoffloat f1))
   | Ofloatofint, Vint n1 => Some (Vfloat (Float.floatofint n1))
   | Ofloatofintu, Vint n1 => Some (Vfloat (Float.floatofintu n1))
   | _, _ => None
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 18fa589f..e7feb101 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -259,6 +259,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
   | Ointoffloat, F n1 :: nil => I(Float.intoffloat n1)
+  | Ointuoffloat, F n1 :: nil => I(Float.intuoffloat n1)
   | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
   | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1)
   | Ocmp c, vl =>
@@ -412,6 +413,9 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx),
   | eval_static_operation_case49:
       forall n1,
       eval_static_operation_cases (Ocast16unsigned) (I n1 :: nil)
+  | eval_static_operation_case50:
+      forall n1,
+      eval_static_operation_cases (Ointuoffloat) (F n1 :: nil)
   | eval_static_operation_default:
       forall (op: operation) (vl: list approx),
       eval_static_operation_cases op vl.
@@ -512,6 +516,8 @@ Definition eval_static_operation_match (op: operation) (vl: list approx) :=
       eval_static_operation_case48 n1
   | Ocast16unsigned, I n1 :: nil =>
       eval_static_operation_case49 n1
+  | Ointuoffloat, F n1 :: nil =>
+      eval_static_operation_case50 n1
   | op, vl =>
       eval_static_operation_default op vl
   end.
@@ -615,6 +621,8 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       I(Int.cast8unsigned n1)
   | eval_static_operation_case49 n1 =>
       I(Int.cast16unsigned n1)
+  | eval_static_operation_case50 n1 =>
+      I(Float.intuoffloat n1)
   | eval_static_operation_default op vl =>
       Unknown
   end.
diff --git a/backend/Op.v b/backend/Op.v
index 51b5e530..2094d597 100644
--- a/backend/Op.v
+++ b/backend/Op.v
@@ -94,7 +94,8 @@ Inductive operation : Set :=
   | Omulsubf: operation                 (**r [rd = r1 * r2 - r3] *)
   | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
 (*c Conversions between int and float: *)
-  | Ointoffloat: operation              (**r [rd = int_of_float(r1)] *)
+  | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
+  | Ointuoffloat: operation             (**r [rd = unsigned_int_of_float(r1)] *)
   | Ofloatofint: operation              (**r [rd = float_of_signed_int(r1)] *)
   | Ofloatofintu: operation             (**r [rd = float_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
@@ -229,6 +230,8 @@ Definition eval_operation
       Some (Val.singleoffloat v1)
   | Ointoffloat, Vfloat f1 :: nil => 
       Some (Vint (Float.intoffloat f1))
+  | Ointuoffloat, Vfloat f1 :: nil => 
+      Some (Vint (Float.intuoffloat f1))
   | Ofloatofint, Vint n1 :: nil => 
       Some (Vfloat (Float.floatofint n1))
   | Ofloatofintu, Vint n1 :: nil => 
@@ -506,6 +509,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Omulsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat)
   | Osingleoffloat => (Tfloat :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
+  | Ointuoffloat => (Tfloat :: nil, Tint)
   | Ofloatofint => (Tint :: nil, Tfloat)
   | Ofloatofintu => (Tint :: nil, Tfloat)
   | Ocmp c => (type_of_condition c, Tint)
@@ -666,6 +670,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
   | Omulsubf, v1::v2::v3::nil => Val.subf (Val.mulf v1 v2) v3
   | Osingleoffloat, v1::nil => Val.singleoffloat v1
   | Ointoffloat, v1::nil => Val.intoffloat v1
+  | Ointuoffloat, v1::nil => Val.intuoffloat v1
   | Ofloatofint, v1::nil => Val.floatofint v1
   | Ofloatofintu, v1::nil => Val.floatofintu v1
   | Ocmp c, _ => eval_condition_total c vl
diff --git a/backend/PPC.v b/backend/PPC.v
index 7a330639..cfd07405 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -125,7 +125,8 @@ Inductive instruction : Set :=
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
-  | Pfcti: ireg -> freg -> instruction                        (**r float-to-int conversion *)
+  | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion *)
+  | Pfctiu: ireg -> freg -> instruction                       (**r float-to-unsigned-int conversion *)
   | Pfdiv: freg -> freg -> freg -> instruction                (**r float division *)
   | Pfmadd: freg -> freg -> freg -> freg -> instruction       (**r float multiply-add *)
   | Pfmr: freg -> freg -> instruction                         (**r float move *)
@@ -199,7 +200,7 @@ lbl:    .double floatcst
 >>
   Initialized data in the constant data section are not modeled here,
   which is why we use a pseudo-instruction for this purpose.
-- [Pfcti]: convert a float to an integer.  This requires a transfer
+- [Pfcti]: convert a float to a signed integer.  This requires a transfer
   via memory of a 32-bit integer from a float register to an int register,
   which our memory model cannot express.  Expands to:
 <<
@@ -208,6 +209,30 @@ lbl:    .double floatcst
         lwz     rdst, 4(r1)
         addi    r1, r1, 8
 >>
+- [Pfctiu]: convert a float to an unsigned integer.  The PowerPC way
+  to do this is to compare the argument against the floating-point
+  constant [2^31], subtract [2^31] if bigger, then convert to a signed
+  integer as above, then add back [2^31] if needed.  Expands to:
+<<
+        addis   r2, 0, ha16(lbl1)
+        lfd     f13, lo16(lbl1)(r2)
+        fcmpu   cr7, rsrc, f13
+        cror    30, 29, 30
+        beq     cr7, lbl2
+        fctiwz  f13, rsrc
+        stfdu   f13, -8(r1)
+        lwz     rdst, 4(r1)
+        b       lbl3
+lbl2:   fsub    f13, rsrc, f13
+        fctiwz  f13, f13
+        stfdu   f13, -8(r1)
+        lwz     rdst, 4(r1)
+        addis   rdst, rdst, 0x8000
+lbl3:   addi    r1, r1, 8
+        .const_data
+lbl1:   .long   0x41e00000, 0x00000000    # 2^31 in double precision
+        .text
+>>
 - [Pictf]: convert a signed integer to a float.  This requires complicated
   bit-level manipulations of IEEE floats through mixed float and integer 
   arithmetic over a memory word, which our memory model and axiomatization
@@ -611,6 +636,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (compare_float rs rs#r1 rs#r2)) m
   | Pfcti rd r1 =>
       OK (nextinstr (rs#rd <- (Val.intoffloat rs#r1) #FPR13 <- Vundef)) m
+  | Pfctiu rd r1 =>
+      OK (nextinstr (rs#rd <- (Val.intuoffloat rs#r1) #FPR13 <- Vundef)) m
   | Pfdiv rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
   | Pfmadd rd r1 r2 r3 =>
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index 1789fb13..f6d1fec0 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -362,6 +362,8 @@ Definition transl_op
       Pfrsp (freg_of r) (freg_of a1) :: k
   | Ointoffloat, a1 :: nil =>
       Pfcti (ireg_of r) (freg_of a1) :: k
+  | Ointuoffloat, a1 :: nil =>
+      Pfctiu (ireg_of r) (freg_of a1) :: k
   | Ofloatofint, a1 :: nil =>
       Pictf (freg_of r) (ireg_of a1) :: k
   | Ofloatofintu, a1 :: nil =>
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index d3ecbdd8..215a9a7b 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -1386,6 +1386,11 @@ Proof.
   split. apply exec_straight_one. 
   repeat (rewrite (freg_val ms sp rs); auto).
   reflexivity. auto with ppcgen.
+  (* Ointuoffloat *)
+  exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)) #FPR13 <- Vundef)).
+  split. apply exec_straight_one. 
+  repeat (rewrite (freg_val ms sp rs); auto).
+  reflexivity. auto with ppcgen.
   (* Ofloatofint *)
   exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR2 <- Vundef #FPR13 <- Vundef)).
   split. apply exec_straight_one. 
diff --git a/backend/Selection.v b/backend/Selection.v
index 23d8d22f..a55b1918 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -1095,6 +1095,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Oabsf => Eop Oabsf (arg ::: Enil)
   | Cminor.Osingleoffloat => singleoffloat arg
   | Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil)
+  | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil)
   | Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil)
   | Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil)
   end.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 4674e1d9..07c3e7b9 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -1088,6 +1088,7 @@ Proof.
   EvalOp.
   EvalOp.
   EvalOp.
+  EvalOp.
 Qed.
 
 Lemma eval_sel_binop:
diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll
index ba67a699..9854117c 100644
--- a/caml/CMlexer.mll
+++ b/caml/CMlexer.mll
@@ -77,6 +77,7 @@ rule token = parse
   | "int8s"    { INT8S }
   | "int8u"    { INT8U }
   | "intoffloat"    { INTOFFLOAT }
+  | "intuoffloat"    { INTUOFFLOAT }
   | "{"    { LBRACE }
   | "{{"    { LBRACELBRACE }
   | "["    { LBRACKET }
diff --git a/caml/CMparser.mly b/caml/CMparser.mly
index e7c656d6..0b3eafd8 100644
--- a/caml/CMparser.mly
+++ b/caml/CMparser.mly
@@ -252,6 +252,7 @@ let mkmatch expr cases =
 %token INT8U
 %token <int32> INTLIT
 %token INTOFFLOAT
+%token INTUOFFLOAT
 %token LBRACE
 %token LBRACELBRACE
 %token LBRACKET
@@ -308,7 +309,7 @@ let mkmatch expr cases =
 %left LESSLESS GREATERGREATER GREATERGREATERU
 %left PLUS PLUSF MINUS MINUSF
 %left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU
-%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC
+%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC
 %left LPAREN
 
 /* Entry point */
@@ -459,6 +460,7 @@ expr:
   | MINUSF expr   %prec p_uminus                { Runop(Onegf, $2) }
   | ABSF expr                                   { Runop(Oabsf, $2) }
   | INTOFFLOAT expr                             { Runop(Ointoffloat, $2) }
+  | INTUOFFLOAT expr                            { Runop(Ointuoffloat, $2) }
   | FLOATOFINT expr                             { Runop(Ofloatofint, $2) }
   | FLOATOFINTU expr                            { Runop(Ofloatofintu, $2) }
   | TILDE expr                                  { Runop(Onotint, $2) }
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml
index 625c36fc..dccaadcf 100644
--- a/caml/CMtypecheck.ml
+++ b/caml/CMtypecheck.ml
@@ -99,6 +99,7 @@ let type_unary_operation = function
   | Oabsf -> tfloat, tfloat
   | Osingleoffloat -> tfloat, tfloat
   | Ointoffloat -> tfloat, tint
+  | Ointuoffloat -> tfloat, tint
   | Ofloatofint -> tint, tfloat
   | Ofloatofintu -> tint, tfloat
 
@@ -142,6 +143,7 @@ let name_of_unary_operation = function
   | Oabsf -> "absf"
   | Osingleoffloat -> "singleoffloat"
   | Ointoffloat -> "intoffloat"
+  | Ointuoffloat -> "intuoffloat"
   | Ofloatofint -> "floatofint"
   | Ofloatofintu -> "floatofintu"
 
diff --git a/caml/Floataux.ml b/caml/Floataux.ml
index 0226de27..6b3b825f 100644
--- a/caml/Floataux.ml
+++ b/caml/Floataux.ml
@@ -19,6 +19,9 @@ let singleoffloat f =
 let intoffloat f =
   coqint_of_camlint (Int32.of_float f)
 
+let intuoffloat f =
+  coqint_of_camlint (Int64.to_int32 (Int64.of_float f))
+
 let floatofint i =
   Int32.to_float (camlint_of_coqint i)
 
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index 1d2e32ca..030dcc67 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -185,6 +185,28 @@ let print_instruction oc labels = function
       fprintf oc "	fctiwz	f13, %a\n" freg r2;
       fprintf oc "	stfd	f13, -8(r1)\n";
       fprintf oc "	lwz	%a, -4(r1)\n" ireg r1
+  | Pfctiu(r1, r2) ->
+      let lbl1 = new_label() in
+      let lbl2 = new_label() in
+      let lbl3 = new_label() in
+      fprintf oc "	addis	r2, 0, ha16(L%d)\n" lbl1;
+      fprintf oc "	lfd	f13, lo16(L%d)(r2)\n" lbl1;
+      fprintf oc "	fcmpu	cr7, %a, f13\n" freg r2;
+      fprintf oc "	cror	30, 29, 30\n";
+      fprintf oc "	beq	cr7, L%d\n" lbl2;
+      fprintf oc "	fctiwz	f13, %a\n" freg r2;
+      fprintf oc "	stfdu	f13, -8(r1)\n";
+      fprintf oc "	lwz	%a, 4(r1)\n" ireg r1;
+      fprintf oc "	b	L%d\n" lbl3;
+      fprintf oc "L%d:	fsub	f13, %a, f13\n" lbl2 freg r2;
+      fprintf oc "	fctiwz	f13, f13\n";
+      fprintf oc "	stfdu	f13, -8(r1)\n";
+      fprintf oc "	lwz	%a, 4(r1)\n" ireg r1;
+      fprintf oc "	addis	%a, %a, 0x8000\n" ireg r1 ireg r1;
+      fprintf oc "L%d:	addi	r1, r1, 8\n" lbl3;
+      fprintf oc "	.const_data\n";
+      fprintf oc "L%d:	.long	0x41e00000, 0x00000000\n" lbl1;
+      fprintf oc "	.text\n"
   | Pfdiv(r1, r2, r3) ->
       fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfmadd(r1, r2, r3, r4) ->
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index a158b133..54f5ceb0 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -867,6 +867,7 @@ Proof.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
   inv H0; inv H; TrivialOp.
+  inv H0; inv H; TrivialOp.
 Qed.
 
 (** Compatibility of [eval_binop] with respect to [val_inject]. *)
diff --git a/common/Mem.v b/common/Mem.v
index 22a8e1f0..d369b808 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -2383,3 +2383,349 @@ Proof.
   replace (high_bound m b0) with (high_bound m' b0). auto.
   unfold high_bound; rewrite <- B; simpl; rewrite A. rewrite update_o; auto.
 Qed.
+
+(** ** Memory shifting *)
+
+(** A special case of memory injection where blocks are not coalesced:
+  each source block injects in a distinct target block. *)
+
+Definition memshift := block -> option Z.
+
+(*
+Inductive val_shift (mi: memshift): val -> val -> Prop :=
+  | val_shift_int:
+      forall i, val_shift mi (Vint i) (Vint i)
+  | val_shift_float:
+      forall f, val_shift mi (Vfloat f) (Vfloat f)
+  | val_shift_ptr:
+      forall b ofs1 ofs2 x,
+      mi b = Some x ->
+      ofs2 = Int.add ofs1 (Int.repr x) ->
+      val_shift mi (Vptr b ofs1) (Vptr b ofs2)
+  | val_shift_undef: 
+      val_shift mi Vundef Vundef.
+*)
+
+Definition meminj_of_shift (mi: memshift) : meminj :=
+  fun b => match mi b with None => None | Some x => Some (b, x) end.
+
+Definition val_shift (mi: memshift) (v1 v2: val): Prop :=
+  val_inject (meminj_of_shift mi) v1 v2.
+
+Record mem_shift (f: memshift) (m1 m2: mem) : Prop :=
+  mk_mem_shift {
+    ms_inj:
+      mem_inj val_inject (meminj_of_shift f) m1 m2;
+    ms_samedomain:
+      nextblock m1 = nextblock m2;
+    ms_domain:
+      forall b, match f b with Some _ => b < nextblock m1 | None => b >= nextblock m1 end;
+    ms_range_1:
+      forall b delta,
+      f b = Some delta ->
+      Int.min_signed <= delta <= Int.max_signed;
+    ms_range_2:
+      forall b delta,
+      f b = Some delta ->
+      Int.min_signed <= low_bound m2 b /\ high_bound m2 b <= Int.max_signed
+  }.
+
+(** The following lemmas establish the absence of machine integer overflow
+  during address computations. *)
+
+Lemma address_shift:
+  forall f m1 m2 chunk b ofs1 delta,
+  mem_shift f m1 m2 ->
+  valid_access m1 chunk b (Int.signed ofs1) ->
+  f b = Some delta ->
+  Int.signed (Int.add ofs1 (Int.repr delta)) = Int.signed ofs1 + delta.
+Proof.
+  intros. inversion H.
+  elim (ms_range_4 _ _ H1); intros.
+  rewrite Int.add_signed.
+  repeat rewrite Int.signed_repr. auto.
+  eauto.
+  assert (valid_access m2 chunk b (Int.signed ofs1 + delta)).
+    eapply valid_access_inj with (mi := meminj_of_shift f); eauto.
+    unfold meminj_of_shift. rewrite H1; auto. 
+  inv H4. generalize (size_chunk_pos chunk); omega.
+  eauto.
+Qed.
+
+Lemma valid_pointer_shift_no_overflow:
+  forall f m1 m2 b ofs x,
+  mem_shift f m1 m2 ->
+  valid_pointer m1 b (Int.signed ofs) = true ->
+  f b = Some x ->
+  Int.min_signed <= Int.signed ofs + Int.signed (Int.repr x) <= Int.max_signed.
+Proof.
+  intros. inv H. rewrite valid_pointer_valid_access in H0.
+  assert (valid_access m2 Mint8unsigned b (Int.signed ofs + x)).
+    eapply valid_access_inj with (mi := meminj_of_shift f); eauto.
+    unfold meminj_of_shift. rewrite H1; auto. 
+  inv H. change (size_chunk Mint8unsigned) with 1 in H4.
+  rewrite Int.signed_repr; eauto.
+  exploit ms_range_4; eauto. intros [A B]. omega.
+Qed.
+
+Lemma valid_pointer_shift:
+  forall f m1 m2 b ofs b' ofs',
+  mem_shift f m1 m2 ->
+  valid_pointer m1 b (Int.signed ofs) = true ->
+  val_shift f (Vptr b ofs) (Vptr b' ofs') ->
+  valid_pointer m2 b' (Int.signed ofs') = true.
+Proof.
+  intros. unfold val_shift in H1. inv H1.
+  assert (f b = Some x). 
+    unfold meminj_of_shift in H5. destruct (f b); congruence. 
+  exploit valid_pointer_shift_no_overflow; eauto. intro NOOV.
+  inv H. rewrite Int.add_signed. rewrite Int.signed_repr; auto.
+  rewrite Int.signed_repr; eauto.
+  eapply valid_pointer_inj; eauto.
+Qed.
+
+(** Relation between shifts and loads. *)
+
+Lemma load_shift:
+  forall f m1 m2 chunk b ofs delta v1,
+  mem_shift f m1 m2 ->
+  load chunk m1 b ofs = Some v1 ->
+  f b = Some delta ->
+  exists v2, load chunk m2 b (ofs + delta) = Some v2 /\ val_shift f v1 v2.
+Proof.
+  intros. inversion H.
+  unfold val_shift. eapply ms_inj0; eauto.
+  unfold meminj_of_shift; rewrite H1; auto.
+Qed.
+
+Lemma loadv_shift:
+  forall f m1 m2 chunk a1 a2 v1,
+  mem_shift f m1 m2 ->
+  loadv chunk m1 a1 = Some v1 ->
+  val_shift f a1 a2 ->
+  exists v2, loadv chunk m2 a2 = Some v2 /\ val_shift f v1 v2.
+Proof.
+  intros. unfold val_shift in H1. inv H1; simpl in H0; try discriminate.
+  generalize H2. unfold meminj_of_shift. caseEq (f b1); intros; inv H3.
+  exploit load_shift; eauto. intros [v2 [LOAD INJ]].
+  exists v2; split; auto. simpl.
+  replace (Int.signed (Int.add ofs1 (Int.repr x)))
+     with (Int.signed ofs1 + x).
+  auto. symmetry. eapply address_shift; eauto with mem.
+Qed.
+
+(** Relation between shifts and stores. *)
+
+Lemma store_within_shift:
+  forall f chunk m1 b ofs v1 n1 m2 delta v2,
+  mem_shift f m1 m2 ->
+  store chunk m1 b ofs v1 = Some n1 ->
+  f b = Some delta ->
+  val_shift f v1 v2 ->
+  exists n2,
+    store chunk m2 b (ofs + delta) v2 = Some n2
+    /\ mem_shift f n1 n2.
+Proof.
+  intros. inversion H. 
+  exploit store_mapped_inj; eauto.
+  intros; constructor.
+  red. intros until delta2. unfold meminj_of_shift. 
+  destruct (f b1). destruct (f b2). intros. inv H4. inv H5. auto. 
+  congruence. congruence. 
+  unfold meminj_of_shift. rewrite H1. auto.
+  intros. apply load_result_inject with chunk; eauto.
+  unfold val_shift in H2. eauto. 
+  intros [n2 [STORE MINJ]].
+  exists n2; split. auto. constructor.
+  (* inj *)
+  auto.
+  (* samedomain *)
+  rewrite (nextblock_store _ _ _ _ _ _ H0).
+  rewrite (nextblock_store _ _ _ _ _ _ STORE).
+  auto.
+  (* domain *)
+  rewrite (nextblock_store _ _ _ _ _ _ H0). auto.
+  (* range *)
+  auto.
+  intros. 
+  repeat rewrite (low_bound_store _ _ _ _ _ _ STORE).
+  repeat rewrite (high_bound_store _ _ _ _ _ _ STORE).
+  eapply ms_range_4; eauto.
+Qed.
+
+Lemma store_outside_shift:
+  forall f chunk m1 b ofs m2 v m2' delta,
+  mem_shift f m1 m2 ->
+  f b = Some delta ->
+  high_bound m1 b + delta <= ofs
+  \/ ofs + size_chunk chunk <= low_bound m1 b + delta ->
+  store chunk m2 b ofs v = Some m2' ->
+  mem_shift f m1 m2'.
+Proof.
+  intros. inversion H. constructor.
+  (* inj *)
+  eapply store_outside_inj; eauto. 
+  unfold meminj_of_shift. intros b' d'. caseEq (f b'); intros; inv H4.
+  congruence.
+  (* samedomain *)
+  rewrite (nextblock_store _ _ _ _ _ _ H2).
+  auto.
+  (* domain *)
+  auto.
+  (* range *)
+  auto.
+  intros. 
+  repeat rewrite (low_bound_store _ _ _ _ _ _ H2).
+  repeat rewrite (high_bound_store _ _ _ _ _ _ H2).
+  eapply ms_range_4; eauto.
+Qed.
+
+Lemma storev_shift:
+  forall f chunk m1 a1 v1 n1 m2 a2 v2,
+  mem_shift f m1 m2 ->
+  storev chunk m1 a1 v1 = Some n1 ->
+  val_shift f a1 a2 ->
+  val_shift f v1 v2 ->
+  exists n2,
+    storev chunk m2 a2 v2 = Some n2 /\ mem_shift f n1 n2.
+Proof.
+  intros. unfold val_shift in H1. inv H1; simpl in H0; try discriminate.
+  generalize H3. unfold meminj_of_shift. caseEq (f b1); intros; inv H4.
+  exploit store_within_shift; eauto. intros [n2 [A B]].
+  exists n2; split; auto.
+  unfold storev. 
+  replace (Int.signed (Int.add ofs1 (Int.repr x)))
+     with (Int.signed ofs1 + x).
+  auto. symmetry. eapply address_shift; eauto with mem.
+Qed.
+
+(** Relation between shifts and [free]. *)
+
+Lemma free_shift:
+  forall f m1 m2 b,
+  mem_shift f m1 m2 ->
+  mem_shift f (free m1 b) (free m2 b).
+Proof.
+  intros. inv H. constructor.
+  (* inj *)
+  apply free_right_inj. apply free_left_inj; auto.
+  intros until ofs. unfold meminj_of_shift. caseEq (f b1); intros; inv H0.
+  apply valid_access_free_2.
+  (* samedomain *)
+  simpl. auto.
+  (* domain *)
+  simpl. auto.
+  (* range *)
+  auto.
+  intros. destruct (eq_block b0 b). 
+  subst b0. rewrite low_bound_free_same. rewrite high_bound_free_same.
+  vm_compute; intuition congruence.
+  rewrite low_bound_free; auto. rewrite high_bound_free; auto. eauto.
+Qed.
+
+(** Relation between shifts and allocation. *)
+
+Definition shift_incr (f1 f2: memshift) : Prop :=
+  forall b, f1 b = f2 b \/ f1 b = None.
+
+Remark shift_incr_inject_incr:
+  forall f1 f2,
+  shift_incr f1 f2 -> inject_incr (meminj_of_shift f1) (meminj_of_shift f2).
+Proof.
+  intros. unfold meminj_of_shift. red. intros. 
+  elim (H b); intro. rewrite H0. auto. rewrite H0. auto.
+Qed.
+
+Lemma val_shift_incr:
+  forall f1 f2 v1 v2,
+  shift_incr f1 f2 -> val_shift f1 v1 v2 -> val_shift f2 v1 v2.
+Proof.
+  unfold val_shift; intros. 
+  apply val_inject_incr with (meminj_of_shift f1).
+  apply shift_incr_inject_incr. auto. auto.
+Qed.
+
+(***
+Remark mem_inj_incr:
+  forall f1 f2 m1 m2,
+  inject_incr f1 f2 -> mem_inj val_inject f1 m1 m2 -> mem_inj val_inject f2 m1 m2.
+Proof.
+  intros; red; intros. 
+  destruct (H b1). rewrite <- H3 in H1.
+  exploit H0; eauto. intros [v2 [A B]]. 
+  exists v2; split. auto. apply val_inject_incr with f1; auto.
+  congruence.
+***)
+
+Lemma alloc_shift:
+  forall f m1 m2 lo1 hi1 m1' b delta lo2 hi2,
+  mem_shift f m1 m2 ->
+  alloc m1 lo1 hi1 = (m1', b) ->
+  lo2 <= lo1 + delta -> hi1 + delta <= hi2 ->
+  Int.min_signed <= delta <= Int.max_signed ->
+  Int.min_signed <= lo2 -> hi2 <= Int.max_signed ->
+  exists f', exists m2',
+     alloc m2 lo2 hi2 = (m2', b)
+  /\ mem_shift f' m1' m2'
+  /\ shift_incr f f'
+  /\ f' b = Some delta.
+Proof.
+  intros. inv H. caseEq (alloc m2 lo2 hi2). intros m2' b' ALLOC2.
+  assert (b' = b).
+    rewrite (alloc_result _ _ _ _ _ H0).
+    rewrite (alloc_result _ _ _ _ _ ALLOC2).
+    auto.
+  subst b'.
+  assert (f b = None).
+    generalize (ms_domain0 b). 
+    rewrite (alloc_result _ _ _ _ _ H0).
+    destruct (f (nextblock m1)). 
+    intros. omegaContradiction.
+    auto.
+  set (f' := fun (b': block) => if zeq b' b then Some delta else f b').
+  assert (shift_incr f f').
+    red; unfold f'; intros.
+    destruct (zeq b0 b); auto.
+    subst b0. auto.
+  exists f'; exists m2'.
+  split. auto.
+  (* mem_shift *)
+  split. constructor.
+  (* inj *)
+  assert (mem_inj val_inject (meminj_of_shift f') m1 m2).
+    red; intros.
+    assert (meminj_of_shift f b1 = Some (b2, delta0)).
+      rewrite <- H7. unfold meminj_of_shift, f'.
+      destruct (zeq b1 b); auto.
+      subst b1.
+      assert (valid_block m1 b) by eauto with mem. 
+      assert (~valid_block m1 b) by eauto with mem.
+      contradiction.
+    exploit ms_inj0; eauto. intros [v2 [A B]].
+    exists v2; split; auto. 
+    apply val_inject_incr with (meminj_of_shift f).
+    apply shift_incr_inject_incr. auto. auto.
+  eapply alloc_parallel_inj; eauto.
+  unfold meminj_of_shift, f'. rewrite zeq_true. auto.
+  (* samedomain *)
+  rewrite (nextblock_alloc _ _ _ _ _ H0).
+  rewrite (nextblock_alloc _ _ _ _ _ ALLOC2).
+  congruence.
+  (* domain *)
+  intros. unfold f'. 
+  rewrite (nextblock_alloc _ _ _ _ _ H0).
+  rewrite (alloc_result _ _ _ _ _ H0).
+  destruct (zeq b0 (nextblock m1)). omega.
+  generalize (ms_domain0 b0). destruct (f b0); omega.
+  (* range *)
+  unfold f'; intros. destruct (zeq b0 b). congruence. eauto. 
+  unfold f'; intros.
+  rewrite (low_bound_alloc _ _ _ _ _ ALLOC2). 
+  rewrite (high_bound_alloc _ _ _ _ _ ALLOC2). 
+  destruct (zeq b0 b). auto. eauto.
+  (* shift_incr *)
+  split. auto.
+  (* f' b = delta *)
+  unfold f'. apply zeq_true. 
+Qed.
+
diff --git a/common/Values.v b/common/Values.v
index 80c5c93e..19772446 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -119,6 +119,12 @@ Definition intoffloat (v: val) : val :=
   | _ => Vundef
   end.
 
+Definition intuoffloat (v: val) : val :=
+  match v with
+  | Vfloat f => Vint (Float.intuoffloat f)
+  | _ => Vundef
+  end.
+
 Definition floatofint (v: val) : val :=
   match v with
   | Vint n => Vfloat (Float.floatofint n)
diff --git a/extraction/.depend b/extraction/.depend
index d26acb92..4f6abc22 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -59,9 +59,9 @@
 ../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \
     AST.cmx ../caml/PrintPPC.cmi 
 ../caml/RTLgenaux.cmo: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \
-    CList.cmi 
+    ../caml/Camlcoq.cmo CList.cmi 
 ../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \
-    CList.cmx 
+    ../caml/Camlcoq.cmx CList.cmx 
 ../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \
     ../caml/Camlcoq.cmo CList.cmi AST.cmi 
 ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \
@@ -191,7 +191,8 @@ Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Linear.cmi \
     Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
     CString.cmi CList.cmi Bounds.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
 Sumbool.cmi: Specif.cmi Datatypes.cmi 
-Switch.cmi: Integers.cmi EqNat.cmi Datatypes.cmi CList.cmi 
+Switch.cmi: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \
+    CList.cmi BinPos.cmi BinInt.cmi 
 Tunneling.cmi: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi 
 Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \
     BinPos.cmi BinInt.cmi AST.cmi 
@@ -490,8 +491,10 @@ Stacking.cmx: Specif.cmx Op.cmx Mach.cmx Locations.cmx Linear.cmx \
     Stacking.cmi 
 Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi 
 Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi 
-Switch.cmo: Integers.cmi EqNat.cmi Datatypes.cmi CList.cmi Switch.cmi 
-Switch.cmx: Integers.cmx EqNat.cmx Datatypes.cmx CList.cmx Switch.cmi 
+Switch.cmo: Specif.cmi Integers.cmi EqNat.cmi Datatypes.cmi Coqlib.cmi \
+    CList.cmi BinPos.cmi BinInt.cmi Switch.cmi 
+Switch.cmx: Specif.cmx Integers.cmx EqNat.cmx Datatypes.cmx Coqlib.cmx \
+    CList.cmx BinPos.cmx BinInt.cmx Switch.cmi 
 Tunneling.cmo: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi 
 Tunneling.cmx: Maps.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi 
 Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \
diff --git a/extraction/extraction.v b/extraction/extraction.v
index fc2920ef..abb792c0 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -30,6 +30,7 @@ Extract Constant Floats.Float.neg => "( ~-. )".
 Extract Constant Floats.Float.abs => "abs_float".
 Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat".
 Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat".
+Extract Constant Floats.Float.intuoffloat => "Floataux.intuoffloat".
 Extract Constant Floats.Float.floatofint => "Floataux.floatofint".
 Extract Constant Floats.Float.floatofintu => "Floataux.floatofintu".
 Extract Constant Floats.Float.add => "( +. )".
diff --git a/lib/Floats.v b/lib/Floats.v
index f11ead4a..6857236d 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -34,6 +34,7 @@ Parameter neg: float -> float.
 Parameter abs: float -> float.
 Parameter singleoffloat: float -> float.
 Parameter intoffloat: float -> int.
+Parameter intuoffloat: float -> int.
 Parameter floatofint: int -> float.
 Parameter floatofintu: int -> float.