add finvw ; not yet generated

11 files changed, 55 insertions, 6 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 35eebb11..b7818aaf 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -231,7 +231,8 @@ Inductive instruction : Type :=
   | Pfminw              (rd rs1 rs2: ireg)          (**r Float min word *)

   | Pfmaxd              (rd rs1 rs2: ireg)          (**r Float max double *)

   | Pfmaxw              (rd rs1 rs2: ireg)          (**r Float max word *)

-

+  | Pfinvw              (rd rs1: ireg)              (**r Float invert word *)

+                        

   (** Arith RRI32 *)

   | Pcompiw (it: itest) (rd rs: ireg) (imm: int)    (**r comparison imm word *)

 

@@ -327,6 +328,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs

   | PArithRR Asmvliw.Pfnegd rd rs  => Pfnegd rd rs

   | PArithRR Asmvliw.Pfnegw rd rs => Pfnegw rd rs

+  | PArithRR Asmvliw.Pfinvw rd rs => Pfinvw rd rs

   | PArithRR Asmvliw.Pfnarrowdw rd rs => Pfnarrowdw rd rs

   | PArithRR Asmvliw.Pfwidenlwd rd rs => Pfwidenlwd rd rs

   | PArithRR Asmvliw.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index cb219f00..61caeaf1 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1343,6 +1343,7 @@ Definition string_of_name_rr (n: arith_name_rr): pstring :=
   | Pfabsw => "Pfabsw"
   | Pfnegd => "Pfnegd"
   | Pfnegw => "Pfnegw"
+  | Pfinvw => "Pfinvw"
   | Pfnarrowdw => "Pfnarrowdw"
   | Pfwidenlwd => "Pfwidenlwd"
   | Pfloatwrnsz => "Pfloatwrnsz"
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 1f3f7539..c2a36ff7 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -793,6 +793,9 @@ Definition transl_op
   | Onegfs, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfnegw rd rs ::i k)
+  | Oinvfs, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfinvw rd rs ::i k)
 
   | Osingleofint, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index a733b54c..cb9ce7ae 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -392,6 +392,7 @@ Inductive arith_name_rr : Type :=
   | Pfabsw                                          (**r float absolute word *)
   | Pfnegd                                          (**r float negate double *)
   | Pfnegw                                          (**r float negate word *)
+  | Pfinvw                                          (**r float invert word *)
   | Pfnarrowdw                                      (**r float narrow 64 -> 32 bits *)
   | Pfwidenlwd                                      (**r Floating Point widen from 32 bits to 64 bits *)
   | Pfloatwrnsz                                     (**r Floating Point conversion from integer (int -> SINGLE) *)
@@ -996,6 +997,7 @@ Definition arith_eval_rr n v :=
   | Pfnegw => Val.negfs v
   | Pfabsd => Val.absf v
   | Pfabsw => Val.absfs v
+  | Pfinvw => ExtValues.invfs v
   | Pfnarrowdw => Val.singleoffloat v
   | Pfwidenlwd => Val.floatofsingle v
   | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end
diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v
index 090844f6..b2fc6581 100644
--- a/mppa_k1c/ExtFloats.v
+++ b/mppa_k1c/ExtFloats.v
@@ -1,4 +1,4 @@
-Require Import Floats.
+Require Import Floats Integers ZArith.
 
 Module ExtFloat.
 (** TODO check with the actual K1c;
@@ -31,4 +31,8 @@ Definition max (x : float32) (y : float32) : float32 :=
   | Some Eq | Some Gt => x
   | Some Lt | None => y
   end.
+
+Definition inv (x : float32) : float32 :=
+  Float32.div (Float32.of_int (Int.repr (1%Z))) x.
+
 End ExtFloat32.
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index a785375b..9cec5669 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -696,3 +696,9 @@ Definition maxfs v1 v2 :=
   | (Vsingle f1), (Vsingle f2) => Vsingle (ExtFloat32.max f1 f2)
   | _, _ => Vundef
   end.
+
+Definition invfs v1 :=
+  match v1 with
+  | (Vsingle f1) => Vsingle (ExtFloat32.inv f1)
+  | _ => Vundef
+  end.
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 84e32d0f..856f5b54 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -124,6 +124,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oaddf | Osubf | Omulf | Odivf | Ominf | Omaxf => op2 (default nv)
   | Onegfs | Oabsfs => op1 (default nv)
   | Oaddfs | Osubfs | Omulfs | Odivfs | Ominfs | Omaxfs => op2 (default nv)
+  | Oinvfs => op1 (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 4beef520..de372157 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -189,6 +189,7 @@ Inductive operation : Type :=
   | Odivfs                   (**r [rd = r1 / r2] *)
   | Ominfs
   | Omaxfs
+  | Oinvfs
   | 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: *)
@@ -440,6 +441,7 @@ Definition eval_operation
   | 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)
+  | Oinvfs, v1::nil => Some (ExtValues.invfs v1)
   | Osingleoffloat, v1::nil => Some (Val.singleoffloat v1)
   | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1)
   | Ointoffloat, v1::nil => Val.intoffloat v1
@@ -652,6 +654,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Odivfs
   | Ominfs
   | Omaxfs => (Tsingle :: Tsingle :: nil, Tsingle)
+  | Oinvfs => (Tsingle :: nil, Tsingle)
   | Osingleoffloat => (Tfloat :: nil, Tsingle)
   | Ofloatofsingle => (Tsingle :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
@@ -933,6 +936,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* minfs, maxfs *)
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
+  (* invfs *)
+  - destruct v0...
   (* singleoffloat, floatofsingle *)
   - destruct v0...
   - destruct v0...
@@ -1550,6 +1555,8 @@ Proof.
   (* minfs, maxfs *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
+  (* invfs *)
+  - inv H4; simpl; auto.    
   (* singleoffloat, floatofsingle *)
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 21cabfe9..e2baa2c0 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -31,7 +31,7 @@ type real_instruction =
   (* FPU *)
   | Fabsd | Fabsw | Fnegw | Fnegd
   | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
-  | Fmind | Fminw | Fmaxd | Fmaxw
+  | Fmind | Fminw | Fmaxd | Fmaxw | Finvw
   | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz
   | Fcompw | Fcompd
 
@@ -62,6 +62,7 @@ let arith_rr_real = function
   | Pfabsd ->           Fabsd
   | Pfnegw ->           Fnegw
   | Pfnegd ->           Fnegd
+  | Pfinvw ->           Finvw
   | Pfnarrowdw ->       Fnarrowdw
   | Pfwidenlwd ->       Fwidenlwd
   | Pfloatwrnsz ->      Floatwz
@@ -586,7 +587,7 @@ let rec_to_usage r =
   | Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd
   | Fmind | Fmaxd | Fminw | Fmaxw -> alu_lite
   | Fnarrowdw -> alu_full
-  | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw -> mau
+  | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Finvw -> mau
 
 
 let real_inst_to_latency = function
@@ -607,7 +608,7 @@ let real_inst_to_latency = function
   | Set -> 4 (* According to the manual should be 3, but I measured 4 *)
   | Icall | Call | Cb | Igoto | Goto | Ret -> 42 (* Should not matter since it's the final instruction of the basic block *)
   | Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd | Fnarrowdw -> 1
-  | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw -> 4
+  | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Finvw -> 4
 
 let rec_to_info r : inst_info =
   let usage = rec_to_usage r
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 3ff016c2..3d3b56a2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -636,6 +636,8 @@ module Target (*: TARGET*) =
          fprintf oc "	fmaxd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pfmaxw (rd, rs1, rs2) ->
          fprintf oc "	fmaxw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pfinvw (rd, rs1) ->
+         fprintf oc "	finvw	%a = %a\n" ireg rd ireg rs1
 
       (* Arith RRI32 instructions *)
       | Pcompiw (it, rd, rs, imm) ->
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,