diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 10:10:06 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 10:10:06 +0200 |
commit | cfc681ae18c59f4a19143a7245be23eb6a4045a0 (patch) | |
tree | 9de825a02fe2abd027cad7cb142c1220b7c5035f /mppa_k1c/ValueAOp.v | |
parent | c0984982ea5b8481bfc75c0ea4254eb5db07d875 (diff) | |
download | compcert-kvx-cfc681ae18c59f4a19143a7245be23eb6a4045a0.tar.gz compcert-kvx-cfc681ae18c59f4a19143a7245be23eb6a4045a0.zip |
add finvw ; not yet generated
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
-rw-r--r-- | mppa_k1c/ValueAOp.v | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 0e9ce506..edbdc0b2 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -19,6 +19,15 @@ Definition maxf := binop_float ExtFloat.max. Definition minfs := binop_single ExtFloat32.min. Definition maxfs := binop_single ExtFloat32.max. +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 *) Definition eval_static_condition (cond: condition) (vl: list aval): abool := @@ -250,6 +259,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | 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 | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 @@ -311,7 +321,17 @@ Proof. apply (binop_single_sound bc ExtFloat32.max); assumption. Qed. -Hint Resolve minf_sound maxf_sound minfs_sound maxfs_sound : va. +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. + +Hint Resolve minf_sound maxf_sound minfs_sound maxfs_sound invfs_sound : va. Theorem eval_static_condition_sound: forall cond vargs m aargs, |