diff options
| -rw-r--r-- | backend/Cminor.v | 4 | ||||
| -rw-r--r-- | backend/Constprop.v | 8 | ||||
| -rw-r--r-- | backend/Op.v | 7 | ||||
| -rw-r--r-- | backend/PPC.v | 31 | ||||
| -rw-r--r-- | backend/PPCgen.v | 2 | ||||
| -rw-r--r-- | backend/PPCgenproof1.v | 5 | ||||
| -rw-r--r-- | backend/Selection.v | 1 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 1 | ||||
| -rw-r--r-- | caml/CMlexer.mll | 1 | ||||
| -rw-r--r-- | caml/CMparser.mly | 4 | ||||
| -rw-r--r-- | caml/CMtypecheck.ml | 2 | ||||
| -rw-r--r-- | caml/Floataux.ml | 3 | ||||
| -rw-r--r-- | caml/PrintPPC.ml | 22 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 1 | ||||
| -rw-r--r-- | common/Mem.v | 346 | ||||
| -rw-r--r-- | common/Values.v | 6 | ||||
| -rw-r--r-- | extraction/.depend | 13 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 | ||||
| -rw-r--r-- | lib/Floats.v | 1 |
19 files changed, 449 insertions, 10 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v index df541a1..c1e3bd1 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 18fa589..e7feb10 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 51b5e53..2094d59 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 7a33063..cfd0740 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 1789fb1..f6d1fec 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 d3ecbdd..215a9a7 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 23d8d22..a55b191 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 4674e1d..07c3e7b 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 ba67a69..9854117 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 e7c656d..0b3eafd 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 625c36f..dccaadc 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 0226de2..6b3b825 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 1d2e32c..030dcc6 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 a158b13..54f5ceb 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 22a8e1f..d369b80 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 80c5c93..1977244 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 d26acb9..4f6abc2 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 fc2920e..abb792c 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 f11ead4..6857236 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. |