diff options
| -rw-r--r-- | mppa_k1c/ExtValues.v | 20 | ||||
| -rw-r--r-- | mppa_k1c/NeedOp.v | 55 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 26 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 85 |
4 files changed, 179 insertions, 7 deletions
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 9cec5669..3e4b70b5 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -1,7 +1,7 @@ Require Import Coqlib. Require Import Integers. Require Import Values. -Require Import ExtFloats. +Require Import Floats ExtFloats. Inductive shift1_4 : Type := | SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4. @@ -702,3 +702,21 @@ Definition invfs v1 := | (Vsingle f1) => Vsingle (ExtFloat32.inv f1) | _ => Vundef end. + +Definition triple_op_float f v1 v2 v3 := + match v1, v2, v3 with + | (Vfloat f1), (Vfloat f2), (Vfloat f3) => Vfloat (f f1 f2 f3) + | _, _, _ => Vundef + end. + +Definition triple_op_single f v1 v2 v3 := + match v1, v2, v3 with + | (Vsingle f1), (Vsingle f2), (Vsingle f3) => Vsingle (f f1 f2 f3) + | _, _, _ => Vundef + end. + +Definition fmaddf := triple_op_float Float.fma. +Definition fmaddfs := triple_op_single Float32.fma. + +Definition fmsubf := triple_op_float (fun f1 f2 f3 => Float.fma f1 (Float.neg f2) f3). +Definition fmsubfs := triple_op_single (fun f1 f2 f3 => Float32.fma f1 (Float32.neg f2) f3). diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 856f5b54..d2d4d5f5 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -122,9 +122,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Omsubl => op3 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf | Ominf | Omaxf => op2 (default nv) + | Ofmaddf | Ofmsubf => op3 (default nv) | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs | Ominfs | Omaxfs => op2 (default nv) | Oinvfs => op1 (default nv) + | Ofmaddfs | Ofmsubfs => op3 (default nv) | Ofloatofsingle | Osingleoffloat => op1 (default nv) | Ointoffloat | Ointuoffloat => op1 (default nv) | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv) @@ -286,7 +288,53 @@ Remark default_idem: forall nv, default (default nv) = default nv. Proof. destruct nv; simpl; trivial. Qed. - + +Lemma vagree_triple_op_float : + forall f a b c x y z nv, + (vagree a x (default nv)) -> + (vagree b y (default nv)) -> + (vagree c z (default nv)) -> + (vagree (ExtValues.triple_op_float f a b c) + (ExtValues.triple_op_float f x y z) nv). +Proof. + induction nv; + intros Hax Hby Hcz. + - trivial. + - simpl in *. destruct a; simpl; trivial. + destruct b; simpl; trivial. + destruct c; simpl; trivial. + - simpl in *. destruct a; simpl; trivial. + destruct b; simpl; trivial. + destruct c; simpl; trivial. + inv Hax. inv Hby. inv Hcz. + simpl. + constructor. +Qed. + +Lemma vagree_triple_op_single : + forall f a b c x y z nv, + (vagree a x (default nv)) -> + (vagree b y (default nv)) -> + (vagree c z (default nv)) -> + (vagree (ExtValues.triple_op_single f a b c) + (ExtValues.triple_op_single f x y z) nv). +Proof. + induction nv; + intros Hax Hby Hcz. + - trivial. + - simpl in *. destruct a; simpl; trivial. + destruct b; simpl; trivial. + destruct c; simpl; trivial. + - simpl in *. destruct a; simpl; trivial. + destruct b; simpl; trivial. + destruct c; simpl; trivial. + inv Hax. inv Hby. inv Hcz. + simpl. + constructor. +Qed. + +Hint Resolve vagree_triple_op_float vagree_triple_op_single : na. + Lemma needs_of_operation_sound: forall op args v nv args', eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v -> @@ -345,7 +393,10 @@ Proof. apply mull_sound; trivial. rewrite default_idem; trivial. rewrite default_idem; trivial. - (* select *) +- apply vagree_triple_op_float; assumption. +- apply vagree_triple_op_float; assumption. +- apply vagree_triple_op_single; assumption. +- apply vagree_triple_op_single; assumption. - destruct (eval_condition0 _ _ _) as [b|] eqn:EC. erewrite needs_of_condition0_sound by eauto. apply select_sound; auto. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index de372157..b3258259 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -181,6 +181,8 @@ Inductive operation : Type := | Odivf (**r [rd = r1 / r2] *) | Ominf | Omaxf + | Ofmaddf + | Ofmsubf | Onegfs (**r [rd = - r1] *) | Oabsfs (**r [rd = abs(r1)] *) | Oaddfs (**r [rd = r1 + r2] *) @@ -190,6 +192,8 @@ Inductive operation : Type := | Ominfs | Omaxfs | Oinvfs + | Ofmaddfs + | Ofmsubfs | Osingleoffloat (**r [rd] is [r1] truncated to single-precision float *) | Ofloatofsingle (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) @@ -433,6 +437,9 @@ Definition eval_operation | Odivf, v1::v2::nil => Some (Val.divf v1 v2) | Ominf, v1::v2::nil => Some (ExtValues.minf v1 v2) | Omaxf, v1::v2::nil => Some (ExtValues.maxf v1 v2) + | Ofmaddf, v1::v2::v3::nil => Some (ExtValues.fmaddf v1 v2 v3) + | Ofmsubf, v1::v2::v3::nil => Some (ExtValues.fmsubf v1 v2 v3) + | Onegfs, v1::nil => Some (Val.negfs v1) | Oabsfs, v1::nil => Some (Val.absfs v1) | Oaddfs, v1::v2::nil => Some (Val.addfs v1 v2) @@ -442,6 +449,9 @@ Definition eval_operation | Ominfs, v1::v2::nil => Some (ExtValues.minfs v1 v2) | Omaxfs, v1::v2::nil => Some (ExtValues.maxfs v1 v2) | Oinvfs, v1::nil => Some (ExtValues.invfs v1) + | Ofmaddfs, v1::v2::v3::nil => Some (ExtValues.fmaddfs v1 v2 v3) + | Ofmsubfs, v1::v2::v3::nil => Some (ExtValues.fmsubfs v1 v2 v3) + | Osingleoffloat, v1::nil => Some (Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 @@ -646,6 +656,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Odivf | Ominf | Omaxf => (Tfloat :: Tfloat :: nil, Tfloat) + | Ofmaddf | Ofmsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat) + | Onegfs => (Tsingle :: nil, Tsingle) | Oabsfs => (Tsingle :: nil, Tsingle) | Oaddfs @@ -655,6 +667,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ominfs | Omaxfs => (Tsingle :: Tsingle :: nil, Tsingle) | Oinvfs => (Tsingle :: nil, Tsingle) + | Ofmaddfs | Ofmsubfs => (Tsingle :: Tsingle :: Tsingle :: nil, Tsingle) + | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) @@ -924,6 +938,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* minf, maxf *) - destruct v0; destruct v1... - destruct v0; destruct v1... + (* fmaddf, fmsubf *) + - destruct v0; destruct v1; destruct v2... + - destruct v0; destruct v1; destruct v2... (* negfs, absfs *) - destruct v0... - destruct v0... @@ -938,6 +955,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... (* invfs *) - destruct v0... + (* fmaddfs, fmsubfs *) + - destruct v0; destruct v1; destruct v2... + - destruct v0; destruct v1; destruct v2... (* singleoffloat, floatofsingle *) - destruct v0... - destruct v0... @@ -1543,6 +1563,9 @@ Proof. (* minf, maxf *) - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. + (* fmaddf, fmsubf *) + - inv H4; inv H3; inv H2; simpl; auto. + - inv H4; inv H3; inv H2; simpl; auto. (* negfs, absfs *) - inv H4; simpl; auto. - inv H4; simpl; auto. @@ -1557,6 +1580,9 @@ Proof. - inv H4; inv H2; simpl; auto. (* invfs *) - inv H4; simpl; auto. + (* fmaddfs, fmsubfs *) + - inv H4; inv H3; inv H2; simpl; auto. + - inv H4; inv H3; inv H2; simpl; auto. (* singleoffloat, floatofsingle *) - inv H4; simpl; auto. - inv H4; simpl; auto. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index edbdc0b2..4c5fcf71 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -19,14 +19,30 @@ Definition maxf := binop_float ExtFloat.max. Definition minfs := binop_single ExtFloat32.min. Definition maxfs := binop_single ExtFloat32.max. +Definition ntop3 (x y z: aval) : aval := Ifptr (plub (provenance x) (plub (provenance y) (provenance z))). + +Definition triple_op_float (sem: float -> float -> float -> float) (x y z: aval) := + match x, y, z with + | F a, F b, F c => F (sem a b c) + | _, _, _ => ntop3 x y z + end. + +Definition triple_op_single (sem: float32 -> float32 -> float32 -> float32) (x y z: aval) := + match x, y, z with + | FS a, FS b, FS c => FS (sem a b c) + | _, _, _ => ntop3 x y z + end. + +Definition fmaddf := triple_op_float Float.fma. +Definition fmsubf := triple_op_float (fun x y z => Float.fma x (Float.neg y) z). +Definition fmaddfs := triple_op_single Float32.fma. +Definition fmsubfs := triple_op_single (fun x y z => Float32.fma x (Float32.neg y) z). + Definition invfs (y : aval) := match y with | FS f => FS (ExtFloat32.inv f) | _ => ntop1 y end. - -Definition binop_float (sem: float -> float -> float) (x y: aval) := - match x, y with F n, F m => F (sem n m) | _, _ => ntop2 x y end. (** Value analysis for RISC V operators *) @@ -251,6 +267,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Odivf, v1::v2::nil => divf v1 v2 | Ominf, v1::v2::nil => minf v1 v2 | Omaxf, v1::v2::nil => maxf v1 v2 + | Ofmaddf, v1::v2::v3::nil => fmaddf v1 v2 v3 + | Ofmsubf, v1::v2::v3::nil => fmsubf v1 v2 v3 | Onegfs, v1::nil => negfs v1 | Oabsfs, v1::nil => absfs v1 | Oaddfs, v1::v2::nil => addfs v1 v2 @@ -260,6 +278,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ominfs, v1::v2::nil => minfs v1 v2 | Omaxfs, v1::v2::nil => maxfs v1 v2 | Oinvfs, v1::nil => invfs v1 + | Ofmaddfs, v1::v2::v3::nil => fmaddfs v1 v2 v3 + | Ofmsubfs, v1::v2::v3::nil => fmsubfs v1 v2 v3 | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 @@ -331,7 +351,64 @@ Proof. constructor. Qed. -Hint Resolve minf_sound maxf_sound minfs_sound maxfs_sound invfs_sound : va. +Lemma triple_op_float_sound: + forall f a x b y c z, + vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.triple_op_float f a b c) + (triple_op_float f x y z). +Proof. + intros until z. + intros Hax Hby Hcz. + inv Hax; simpl; try constructor; + inv Hby; simpl; try constructor; + inv Hcz; simpl; try constructor. +Qed. + +Lemma triple_op_single_sound: + forall f a x b y c z, + vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.triple_op_single f a b c) + (triple_op_single f x y z). +Proof. + intros until z. + intros Hax Hby Hcz. + inv Hax; simpl; try constructor; + inv Hby; simpl; try constructor; + inv Hcz; simpl; try constructor. +Qed. + +Lemma fmaddf_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmaddf a b c) (fmaddf x y z). +Proof. + intros. unfold ExtValues.fmaddf, fmaddf. + apply triple_op_float_sound; assumption. +Qed. + +Lemma fmaddfs_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmaddfs a b c) (fmaddfs x y z). +Proof. + intros. unfold ExtValues.fmaddfs, fmaddfs. + apply triple_op_single_sound; assumption. +Qed. + +Lemma fmsubf_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmsubf a b c) (fmsubf x y z). +Proof. + intros. unfold ExtValues.fmsubf, fmsubf. + apply triple_op_float_sound; assumption. +Qed. + +Lemma fmsubfs_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmsubfs a b c) (fmsubfs x y z). +Proof. + intros. unfold ExtValues.fmsubfs, fmsubfs. + apply triple_op_single_sound; assumption. +Qed. +Hint Resolve minf_sound maxf_sound minfs_sound maxfs_sound invfs_sound fmaddf_sound fmaddfs_sound fmsubf_sound fmsubfs_sound : va. Theorem eval_static_condition_sound: forall cond vargs m aargs, |