begin implementing minf/maxf

5 files changed, 128 insertions, 11 deletions

diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v
new file mode 100644
index 00000000..efea278b
--- /dev/null
+++ b/mppa_k1c/ExtFloats.v
@@ -0,0 +1,33 @@
+Require Import Floats.
+
+Module ExtFloat.
+(** TODO check with the actual K1c *)
+
+Definition min (x : float) (y : float) : float :=
+  match Float.compare x y with
+  | Some Eq | Some Lt => x
+  | Some Gt | None => y
+  end.
+
+Definition max (x : float) (y : float) : float :=
+  match Float.compare x y with
+  | Some Eq | Some Gt => x
+  | Some Lt | None => y
+  end.
+End ExtFloat.
+
+Module ExtFloat32.
+(** TODO check with the actual K1c *)
+
+Definition min (x : float32) (y : float32) : float32 :=
+  match Float32.compare x y with
+  | Some Eq | Some Lt => x
+  | Some Gt | None => y
+  end.
+
+Definition max (x : float32) (y : float32) : float32 :=
+  match Float32.compare x y with
+  | Some Eq | Some Gt => x
+  | Some Lt | None => y
+  end.
+End ExtFloat32.
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 3370fae3..a785375b 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -1,6 +1,7 @@
 Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
+Require Import ExtFloats.
 
 Inductive shift1_4 : Type :=
 | SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4.
@@ -671,3 +672,27 @@ Definition revsubx sh v1 v2 :=
 
 Definition revsubxl sh v1 v2 :=
   Val.subl v2 (Val.shll v1 (Vint sh)).
+
+Definition minf v1 v2 :=
+  match v1, v2 with
+  | (Vfloat f1), (Vfloat f2) => Vfloat (ExtFloat.min f1 f2)
+  | _, _ => Vundef
+  end.
+
+Definition maxf v1 v2 :=
+  match v1, v2 with
+  | (Vfloat f1), (Vfloat f2) => Vfloat (ExtFloat.max f1 f2)
+  | _, _ => Vundef
+  end.
+
+Definition minfs v1 v2 :=
+  match v1, v2 with
+  | (Vsingle f1), (Vsingle f2) => Vsingle (ExtFloat32.min f1 f2)
+  | _, _ => Vundef
+  end.
+
+Definition maxfs v1 v2 :=
+  match v1, v2 with
+  | (Vsingle f1), (Vsingle f2) => Vsingle (ExtFloat32.max f1 f2)
+  | _, _ => Vundef
+  end.
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 4748f38b..84e32d0f 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -121,9 +121,9 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Omaddlimm n => op2 (default nv)
   | Omsubl => op3 (default nv)
   | Onegf | Oabsf => op1 (default nv)
-  | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
+  | Oaddf | Osubf | Omulf | Odivf | Ominf | Omaxf => op2 (default nv)
   | Onegfs | Oabsfs => op1 (default nv)
-  | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
+  | Oaddfs | Osubfs | Omulfs | Odivfs | Ominfs | Omaxfs => op2 (default nv)
   | Ofloatofsingle | Osingleoffloat => op1 (default nv)
   | Ointoffloat | Ointuoffloat => op1 (default nv)
   | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 35fbb596..4beef520 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -179,12 +179,16 @@ Inductive operation : Type :=
   | Osubf                    (**r [rd = r1 - r2] *)
   | Omulf                    (**r [rd = r1 * r2] *)
   | Odivf                    (**r [rd = r1 / r2] *)
+  | Ominf
+  | Omaxf
   | Onegfs                   (**r [rd = - r1] *)
   | Oabsfs                   (**r [rd = abs(r1)] *)
   | Oaddfs                   (**r [rd = r1 + r2] *)
   | Osubfs                   (**r [rd = r1 - r2] *)
   | Omulfs                   (**r [rd = r1 * r2] *)
   | Odivfs                   (**r [rd = r1 / r2] *)
+  | Ominfs
+  | Omaxfs
   | 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: *)
@@ -426,12 +430,16 @@ Definition eval_operation
   | Osubf, v1::v2::nil => Some (Val.subf v1 v2)
   | Omulf, v1::v2::nil => Some (Val.mulf v1 v2)
   | 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)
   | Onegfs, v1::nil => Some (Val.negfs v1)
   | Oabsfs, v1::nil => Some (Val.absfs v1)
   | Oaddfs, v1::v2::nil => Some (Val.addfs v1 v2)
   | Osubfs, v1::v2::nil => Some (Val.subfs v1 v2)
   | Omulfs, v1::v2::nil => Some (Val.mulfs v1 v2)
   | Odivfs, v1::v2::nil => Some (Val.divfs v1 v2)
+  | Ominfs, v1::v2::nil => Some (ExtValues.minfs v1 v2)
+  | Omaxfs, v1::v2::nil => Some (ExtValues.maxfs v1 v2)
   | Osingleoffloat, v1::nil => Some (Val.singleoffloat v1)
   | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1)
   | Ointoffloat, v1::nil => Val.intoffloat v1
@@ -630,16 +638,20 @@ Definition type_of_operation (op: operation) : list typ * typ :=
 
   | Onegf => (Tfloat :: nil, Tfloat)
   | Oabsf => (Tfloat :: nil, Tfloat)
-  | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
-  | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
-  | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
-  | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
+  | Oaddf
+  | Osubf
+  | Omulf
+  | Odivf
+  | Ominf
+  | Omaxf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Onegfs => (Tsingle :: nil, Tsingle)
   | Oabsfs => (Tsingle :: nil, Tsingle)
-  | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle)
-  | Osubfs => (Tsingle :: Tsingle :: nil, Tsingle)
-  | Omulfs => (Tsingle :: Tsingle :: nil, Tsingle)
-  | Odivfs => (Tsingle :: Tsingle :: nil, Tsingle)
+  | Oaddfs
+  | Osubfs
+  | Omulfs
+  | Odivfs
+  | Ominfs
+  | Omaxfs => (Tsingle :: Tsingle :: nil, Tsingle)
   | Osingleoffloat => (Tfloat :: nil, Tsingle)
   | Ofloatofsingle => (Tsingle :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
@@ -906,6 +918,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* mulf, divf *)
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
+  (* minf, maxf *)
+  - destruct v0; destruct v1...
+  - destruct v0; destruct v1...
   (* negfs, absfs *)
   - destruct v0...
   - destruct v0...
@@ -915,6 +930,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* mulfs, divfs *)
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
+  (* minfs, maxfs *)
+  - destruct v0; destruct v1...
+  - destruct v0; destruct v1...
   (* singleoffloat, floatofsingle *)
   - destruct v0...
   - destruct v0...
@@ -1517,6 +1535,9 @@ Proof.
   (* mulf, divf *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
+  (* minf, maxf *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; simpl; auto.
   (* negfs, absfs *)
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
@@ -1526,6 +1547,9 @@ Proof.
   (* mulfs, divfs *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
+  (* minfs, maxfs *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; 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 439138da..0e9ce506 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -12,7 +12,12 @@
 
 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.
 
 (** Value analysis for RISC V operators *)
 
@@ -235,12 +240,16 @@ 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
   | 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
   | Osingleoffloat, v1::nil => singleoffloat v1
   | Ofloatofsingle, v1::nil => floatofsingle v1
   | Ointoffloat, v1::nil => intoffloat v1
@@ -278,6 +287,32 @@ 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.
+
+Hint Resolve minf_sound maxf_sound minfs_sound maxfs_sound : va.
+
 Theorem eval_static_condition_sound:
   forall cond vargs m aargs,
   list_forall2 (vmatch bc) vargs aargs ->