From d8fafb0add258e47287a2d57454194db8f1dd635 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Mar 2019 16:44:07 +0100 Subject: Implemented float comparisons (no branching yet, and no negation) --- mppa_k1c/Asm.v | 2 ++ mppa_k1c/Asmblock.v | 49 ++++++++++++++++++++++++++++++++++++ mppa_k1c/Asmblockdeps.v | 2 ++ mppa_k1c/Asmblockgen.v | 48 +++++++++++++++-------------------- mppa_k1c/Asmblockgenproof.v | 1 + mppa_k1c/Asmblockgenproof1.v | 32 +++++++++++++++++++++++ mppa_k1c/PostpassSchedulingOracle.ml | 12 ++++++++- mppa_k1c/TargetPrinter.ml | 15 +++++++++++ 8 files changed, 132 insertions(+), 29 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index dcce98d0..49f2d23c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -131,6 +131,7 @@ Inductive instruction : Type := (** Arith RRR *) | Pcompw (it: itest) (rd rs1 rs2: ireg) (**r comparison word *) | Pcompl (it: itest) (rd rs1 rs2: ireg) (**r comparison long *) + | Pfcompw (ft: ftest) (rd rs1 rs2: ireg) (**r comparison float *) | Paddw (rd rs1 rs2: ireg) (**r add word *) | Psubw (rd rs1 rs2: ireg) (**r sub word *) @@ -251,6 +252,7 @@ Definition basic_to_instruction (b: basic) := (* RRR *) | PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2 | PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2 + | PArithRRR (Asmblock.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2 | PArithRRR Asmblock.Paddw rd rs1 rs2 => Paddw rd rs1 rs2 | PArithRRR Asmblock.Psubw rd rs1 rs2 => Psubw rd rs1 rs2 | PArithRRR Asmblock.Pmulw rd rs1 rs2 => Pmulw rd rs1 rs2 diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 54bf247f..274d90a1 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -126,6 +126,17 @@ Inductive itest: Type := | ITnone (**r Not Any Bits Set in Mask *) . +Inductive ftest: Type := + | FTone (**r Ordered and Not Equal *) + | FTueq (**r Unordered or Equal *) + | FToeq (**r Ordered and Equal *) + | FTune (**r Unordered or Not Equal *) + | FTolt (**r Ordered and Less Than *) + | FTuge (**r Unordered or Greater Than or Equal *) + | FToge (**r Ordered and Greater Than or Equal *) + | FTult (**r Unordered or Less Than *) + . + (** Offsets for load and store instructions. An offset is either an immediate integer or the low part of a symbol. *) @@ -320,6 +331,7 @@ Inductive arith_name_rf64 : Type := Inductive arith_name_rrr : Type := | Pcompw (it: itest) (**r comparison word *) | Pcompl (it: itest) (**r comparison long *) + | Pfcompw (it: ftest) (**r comparison float32 *) | Paddw (**r add word *) | Psubw (**r sub word *) @@ -816,6 +828,31 @@ Definition itest_for_cmp (c: comparison) (s: signedness) := | Cgt, Unsigned => ITgtu end. +Inductive oporder_ftest := + | Normal (ft: ftest) + | Reversed (ft: ftest) +. + +Definition ftest_for_cmp (c: comparison) := + match c with + | Ceq => Normal FToeq + | Cne => Normal FTune + | Clt => Normal FTolt + | Cle => Reversed FToge + | Cgt => Reversed FTolt + | Cge => Normal FToge + end. + +Definition notftest_for_cmp (c: comparison) := + match c with + | Ceq => Normal FTune + | Cne => Normal FToeq + | Clt => Normal FTuge + | Cle => Reversed FTult + | Cgt => Reversed FTuge + | Cge => Normal FTult + end. + (* CoMPare Signed Words to Zero *) Definition btest_for_cmpswz (c: comparison) := match c with @@ -910,6 +947,17 @@ Definition compare_long (t: itest) (v1 v2: val) (m: mem): val := end . +Definition compare_single (t: ftest) (v1 v2: val): val := + match t with + | FTone | FTueq => Vundef (* unused *) + | FToeq => Val.cmpfs Ceq v1 v2 + | FTune => Val.cmpfs Cne v1 v2 + | FTolt => Val.cmpfs Clt v1 v2 + | FTuge => Val.notbool (Val.cmpfs Clt v1 v2) + | FToge => Val.cmpfs Cge v1 v2 + | FTult => Val.notbool (Val.cmpfs Cge v1 v2) + end. + (** Execution of arith instructions TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma... @@ -980,6 +1028,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset match n with | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2 m) | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2 m) + | Pfcompw c => rs#d <- (compare_single c rs#s1 rs#s2) | Paddw => rs#d <- (Val.add rs#s1 rs#s2) | Psubw => rs#d <- (Val.sub rs#s1 rs#s2) | Pmulw => rs#d <- (Val.mul rs#s1 rs#s2) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 67ca94e2..69d3d0cc 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -159,6 +159,8 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRR n, [Val v1; Val v2] => match n with + | Pfcompw c => Some (Val (compare_single c v1 v2)) + | Paddw => Some (Val (Val.add v1 v2)) | Psubw => Some (Val (Val.sub v1 v2)) | Pmulw => Some (Val (Val.mul v1 v2)) diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 56d061c2..fb6ba16e 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -282,6 +282,18 @@ Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) := Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k. +Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompw ft rd r1 r2 ::i k + | Reversed ft => Pfcompw ft rd r2 r1 ::i k + end. + +Definition transl_cond_notfloat32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompw ft rd r1 r2 ::i k + | Reversed ft => Pfcompw ft rd r2 r1 ::i k + end. + Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) := match cond, args with @@ -309,10 +321,14 @@ Definition transl_cond_op | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (transl_condimm_int64u c rd r1 n k) + | Ccompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_float32 c rd r1 r2 k) +(* | Cnotcompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_notfloat32 c rd r1 r2 k) *) (* FIXME - because of proofs, might have to use a xor instead *) | Ccompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompf") | Cnotcompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompf") - | Ccompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompfs") - | Cnotcompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompfs") (*| Ccompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_float c rd r1 r2 in @@ -388,13 +404,7 @@ Definition transl_op OK (Pmulw rd rs1 rs2 ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") -(*| Omulhs, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhw rd rs1 rs2 :: k) - | Omulhu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhuw rd rs1 rs2 :: k) -*)| Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") + | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pdivw rd rs1 rs2 :: k) *) | Odivu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odivu: 32-bits division not supported yet. Please use 64-bits.") @@ -483,25 +493,7 @@ Definition transl_op | Odivlu, _ => Error (msg "Asmblockgen.transl_op: Odivlu") | Omodl, _ => Error (msg "Asmblockgen.transl_op: Omodl") | Omodlu, _ => Error (msg "Asmblockgen.transl_op: Omodlu") -(*| Omullhs, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhl rd rs1 rs2 :: k) - | Omullhu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhul rd rs1 rs2 :: k) - | Odivl, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivl rd rs1 rs2 :: k) - | Odivlu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivul rd rs1 rs2 :: k) - | Omodl, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Preml rd rs1 rs2 :: k) - | Omodlu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premul rd rs1 rs2 :: k) -*)| Oandl, a1 :: a2 :: nil => + | Oandl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandl rd rs1 rs2 ::i k) | Oandlimm n, a1 :: nil => diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 9cba8402..2b79c78e 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -950,6 +950,7 @@ Proof. - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate. - simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate. unfold transl_cond_op in EQ0. exploreInst; try discriminate. + unfold transl_cond_float32. exploreInst; try discriminate. - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate. all: unfold transl_memory_access in EQ0; exploreInst; try discriminate. - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 175eca73..f7207c88 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -968,6 +968,36 @@ Proof. split; intros; Simpl. Qed. +Lemma swap_comparison_cmpfs: + forall v1 v2 cmp, + Val.lessdef (Val.cmpfs cmp v1 v2) (Val.cmpfs (swap_comparison cmp) v2 v1). +Proof. + intros. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. + rewrite Float32.cmp_swap. auto. +Qed. + +Lemma transl_cond_float32_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_float32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.cmpfs cmp rs#r1 rs#r2) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpfs. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpfs. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +Qed. + Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> @@ -1003,6 +1033,8 @@ Proof. exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite MKTOT; eauto. ++ (* cmpfloat *) + exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. Qed. (* diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index c3473b9f..d9c22666 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -55,6 +55,7 @@ let arith_rr_str = function let arith_rrr_str = function | Pcompw it -> "Pcompw" | Pcompl it -> "Pcompl" + | Pfcompw ft -> "Pfcompw" | Paddw -> "Paddw" | Psubw -> "Psubw" | Pmulw -> "Pmulw" @@ -305,6 +306,10 @@ let alu_lite : int array = let resmap = fun r -> match r with | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | _ -> 0 in Array.of_list (List.map resmap resource_names) +let alu_lite_x : int array = let resmap = fun r -> match r with + | "ISSUE" -> 2 | "TINY" -> 1 | "LITE" -> 1 | _ -> 0 + in Array.of_list (List.map resmap resource_names) + let alu_full : int array = let resmap = fun r -> match r with | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | "ALU" -> 1 | _ -> 0 in Array.of_list (List.map resmap resource_names) @@ -373,6 +378,7 @@ type real_instruction = | Fabsd | Fabsw | Fnegw | Fnegd | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz + | Fcompw let ab_inst_to_real = function | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw @@ -381,6 +387,7 @@ let ab_inst_to_real = function | "Pandl" | "Pandil" -> Andd | "Pcompw" | "Pcompiw" -> Compw | "Pcompl" | "Pcompil" -> Compd + | "Pfcompw" -> Fcompw | "Pmulw" -> Mulw | "Pmull" -> Muld | "Porw" | "Poriw" -> Orw @@ -470,6 +477,9 @@ let rec_to_usage r = | Compd -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) + | Fcompw -> (match encoding with None -> alu_lite + | Some U6 | Some S10 | Some U27L5 -> alu_lite_x + | _ -> raise InvalidEncoding) | Make -> (match encoding with Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y @@ -502,7 +512,7 @@ let real_inst_to_latency = function | Nop -> 0 (* Only goes through ID *) | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make - | Sxwd | Zxwd + | Sxwd | Zxwd | Fcompw -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index acb128de..ac2e3b27 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -173,6 +173,18 @@ module Target (*: TARGET*) = | ITnone -> "none" let icond oc c = fprintf oc "%s" (icond_name c) + + let fcond_name = let open Asmblock in function + | FTone -> "one" + | FTueq -> "ueq" + | FToeq -> "oeq" + | FTune -> "une" + | FTolt -> "olt" + | FTuge -> "uge" + | FToge -> "oge" + | FTult -> "ult" + + let fcond oc c = fprintf oc "%s" (fcond_name c) let bcond_name = let open Asmblock in function | BTwnez -> "wnez" @@ -345,6 +357,9 @@ module Target (*: TARGET*) = | Pcompl (it, rd, rs1, rs2) -> fprintf oc " compd.%a %a = %a, %a\n" icond it ireg rd ireg rs1 ireg rs2 + | Pfcompw (ft, rd, rs1, rs2) -> + fprintf oc " fcompw.%a %a = %a, %a\n" fcond ft ireg rd ireg rs1 ireg rs2 + | Paddw (rd, rs1, rs2) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psubw (rd, rs1, rs2) -> -- cgit