1 files changed, 36 insertions, 1 deletions
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 ->