diff options
Diffstat (limited to 'kvx/Op.v')
| -rw-r--r-- | kvx/Op.v | 30 |
1 files changed, 30 insertions, 0 deletions
@@ -209,6 +209,11 @@ Inductive operation : Type := | Olonguofsingle (**r [rd = unsigned_long_of_float32(r1)] *) | Osingleoflong (**r [rd = float32_of_signed_long(r1)] *) | Osingleoflongu (**r [rd = float32_of_unsigned_int(r1)] *) + | Ointofsingle_ne (**r [rd = signed_int_of_float64(r1)] *) + | Ointuofsingle_ne (**r [rd = unsigned_int_of_float64(r1)] *) + | Olongoffloat_ne (**r [rd = signed_long_of_float64(r1)] *) + | Olonguoffloat_ne (**r [rd = unsigned_long_of_float64(r1)] *) + (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) | Oextfz (stop : Z) (start : Z) @@ -470,6 +475,11 @@ Definition eval_operation | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1)) | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1)) | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) + | Ointofsingle_ne, v1::nil => Some (Val.maketotal (Val.intofsingle_ne v1)) + | Ointuofsingle_ne, v1::nil => Some (Val.maketotal (Val.intuofsingle_ne v1)) + | Olongoffloat_ne, v1::nil => Some (Val.maketotal (Val.longoffloat_ne v1)) + | Olonguoffloat_ne, v1::nil => Some (Val.maketotal (Val.longuoffloat_ne v1)) + | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) | (Oextfz stop start), v0::nil => Some (extfz stop start v0) | (Oextfs stop start), v0::nil => Some (extfs stop start v0) @@ -691,6 +701,12 @@ Definition type_of_operation (op: operation) : list typ * typ := | Olonguofsingle => (Tsingle :: nil, Tlong) | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) + + | Ointofsingle_ne => (Tsingle :: nil, Tint) + | Ointuofsingle_ne => (Tsingle :: nil, Tint) + | Olongoffloat_ne => (Tfloat :: nil, Tlong) + | Olonguoffloat_ne => (Tfloat :: nil, Tlong) + | Ocmp c => (type_of_condition c, Tint) | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint) | Oextfzl _ _ | Oextfsl _ _ => (Tlong :: nil, Tlong) @@ -992,6 +1008,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* singleoflong, singleoflongu *) - destruct v0; cbn... - destruct v0; cbn... + (* intofsingle_ne, intuofsingle_ne *) + - destruct v0; cbn... destruct (Float32.to_int_ne f); cbn; trivial. + - destruct v0; cbn... destruct (Float32.to_intu_ne f); cbn; trivial. + (* longoffloat_ne, longuoffloat_ne *) + - destruct v0; cbn... destruct (Float.to_long_ne f); cbn; trivial. + - destruct v0; cbn... destruct (Float.to_longu_ne f); cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* extfz *) @@ -1686,6 +1708,14 @@ Proof. (* singleoflong, singleoflongu *) - inv H4; cbn; auto. - inv H4; cbn; auto. + + (* intofsingle_ne, intuofsingle_ne *) + - inv H4; cbn; auto. destruct (Float32.to_int_ne f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float32.to_intu_ne f0); cbn; auto. + (* longoffloat_ne, longuoffloat_ne *) + - inv H4; cbn; auto. destruct (Float.to_long_ne f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float.to_longu_ne f0); cbn; auto. + (* cmp *) - subst v1. destruct (eval_condition cond vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. |