diff options
Diffstat (limited to 'backend')
| -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 |
8 files changed, 55 insertions, 4 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: |