1 files changed, 133 insertions, 1 deletions

diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 439138da..2c9bdf3e 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -12,7 +12,37 @@
 
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
-Require Import Op ExtValues RTL ValueDomain.
+Require Import Op ExtValues ExtFloats RTL ValueDomain.
+
+Definition minf := binop_float ExtFloat.min.
+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 (fun x y z => Float.fma y z x).
+Definition fmsubf := triple_op_float (fun x y z => Float.fma (Float.neg y) z x).
+Definition fmaddfs := triple_op_single (fun x y z => Float32.fma y z x).
+Definition fmsubfs := triple_op_single (fun x y z => Float32.fma (Float32.neg y) z x).
+
+Definition invfs (y : aval) :=
+  match y with
+  | FS f => FS (ExtFloat32.inv f)
+  | _ => ntop1 y
+  end.
 
 (** Value analysis for RISC V operators *)
 
@@ -235,12 +265,21 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osubf, v1::v2::nil => subf v1 v2
   | Omulf, v1::v2::nil => mulf v1 v2
   | 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
   | Osubfs, v1::v2::nil => subfs v1 v2
   | Omulfs, v1::v2::nil => mulfs v1 v2
   | Odivfs, v1::v2::nil => divfs v1 v2
+  | 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
@@ -278,6 +317,99 @@ Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
 Hypothesis STACK: bc sp = BCstack.
 
+Lemma minf_sound:
+  forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y).
+Proof.
+  apply (binop_float_sound bc ExtFloat.min); assumption.
+Qed.
+
+Lemma maxf_sound:
+  forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.maxf v w) (maxf x y).
+Proof.
+  apply (binop_float_sound bc ExtFloat.max); assumption.
+Qed.
+
+Lemma minfs_sound:
+  forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minfs v w) (minfs x y).
+Proof.
+  apply (binop_single_sound bc ExtFloat32.min); assumption.
+Qed.
+
+Lemma maxfs_sound:
+  forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.maxfs v w) (maxfs x y).
+Proof.
+  apply (binop_single_sound bc ExtFloat32.max); assumption.
+Qed.
+
+Lemma invfs_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.invfs v) (invfs x).
+Proof.
+  intros v x;
+  intro MATCH;
+  inversion MATCH;
+  simpl;
+  constructor.
+Qed.
+
+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,
   list_forall2 (vmatch bc) vargs aargs ->