From f4b41226d60ca57c5981b0a46e0a495152b5301f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 30 May 2008 12:27:15 +0000
Subject: [PATCH] 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
---
backend/Cminor.v | 4 +-
backend/Constprop.v | 8 +
backend/Op.v | 7 +-
backend/PPC.v | 31 +++-
backend/PPCgen.v | 2 +
backend/PPCgenproof1.v | 5 +
backend/Selection.v | 1 +
backend/Selectionproof.v | 1 +
caml/CMlexer.mll | 1 +
caml/CMparser.mly | 4 +-
caml/CMtypecheck.ml | 2 +
caml/Floataux.ml | 3 +
caml/PrintPPC.ml | 22 +++
cfrontend/Cminorgenproof.v | 1 +
common/Mem.v | 346 +++++++++++++++++++++++++++++++++++++
common/Values.v | 6 +
extraction/.depend | 13 +-
extraction/extraction.v | 1 +
lib/Floats.v | 1 +
19 files changed, 449 insertions(+), 10 deletions(-)
diff --git a/backend/Cminor.v b/backend/Cminor.v
index df541a117..c1e3bd18a 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 18fa589ff..e7feb1011 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 51b5e5305..2094d5970 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 7a330639a..cfd07405f 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 1789fb13b..f6d1fec01 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 d3ecbdd8f..215a9a7be 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 23d8d22f8..a55b19180 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 4674e1d95..07c3e7b9a 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 ba67a6991..9854117c3 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 e7c656d69..0b3eafd82 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 625c36fc8..dccaadcf2 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 0226de27b..6b3b825f1 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 1d2e32ca1..030dcc672 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 a158b133c..54f5ceb0f 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 22a8e1f0d..d369b808d 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 80c5c93e6..19772446c 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 d26acb922..4f6abc225 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 fc2920efb..abb792c01 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 f11ead4a0..6857236d3 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.
--
GitLab