From cfc681ae18c59f4a19143a7245be23eb6a4045a0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 30 Aug 2019 10:10:06 +0200 Subject: add finvw ; not yet generated --- mppa_k1c/Asm.v | 4 +++- mppa_k1c/Asmblockdeps.v | 1 + mppa_k1c/Asmblockgen.v | 3 +++ mppa_k1c/Asmvliw.v | 2 ++ mppa_k1c/ExtFloats.v | 6 +++++- mppa_k1c/ExtValues.v | 6 ++++++ mppa_k1c/NeedOp.v | 1 + mppa_k1c/Op.v | 7 +++++++ mppa_k1c/PostpassSchedulingOracle.ml | 7 ++++--- mppa_k1c/TargetPrinter.ml | 2 ++ mppa_k1c/ValueAOp.v | 22 +++++++++++++++++++++- 11 files changed, 55 insertions(+), 6 deletions(-) (limited to 'mppa_k1c') 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, -- cgit