From 595db90221d4f45682ec5aaac0b485ff32af09e5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 29 Aug 2019 17:47:58 +0200 Subject: begin implementing minf/maxf --- mppa_k1c/ExtFloats.v | 33 +++++++++++++++++++++++++++++++++ mppa_k1c/ExtValues.v | 25 +++++++++++++++++++++++++ mppa_k1c/NeedOp.v | 4 ++-- mppa_k1c/Op.v | 40 ++++++++++++++++++++++++++++++++-------- mppa_k1c/ValueAOp.v | 37 ++++++++++++++++++++++++++++++++++++- 5 files changed, 128 insertions(+), 11 deletions(-) create mode 100644 mppa_k1c/ExtFloats.v 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 -> -- cgit