From 59948b3348964f4b16f408ffe690f2c78ca80959 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Mar 2019 17:41:27 +0100 Subject: Added double comparisons --- mppa_k1c/Asm.v | 2 ++ mppa_k1c/Asmblock.v | 15 +++++++- mppa_k1c/Asmblockdeps.v | 1 + mppa_k1c/Asmblockgen.v | 40 ++++++++++----------- mppa_k1c/Asmblockgenproof.v | 2 ++ mppa_k1c/Asmblockgenproof1.v | 70 ++++++++++++++++++++++++++++++++++++ mppa_k1c/PostpassSchedulingOracle.ml | 9 +++-- mppa_k1c/TargetPrinter.ml | 2 ++ 8 files changed, 118 insertions(+), 23 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 49f2d23c..31bc855d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -132,6 +132,7 @@ Inductive instruction : Type := | 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 *) + | Pfcompl (ft: ftest) (rd rs1 rs2: ireg) (**r comparison float64 *) | Paddw (rd rs1 rs2: ireg) (**r add word *) | Psubw (rd rs1 rs2: ireg) (**r sub word *) @@ -253,6 +254,7 @@ Definition basic_to_instruction (b: basic) := | 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.Pfcompl ft) rd rs1 rs2 => Pfcompl 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 274d90a1..86c47613 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -331,7 +331,8 @@ 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 *) + | Pfcompw (ft: ftest) (**r comparison float32 *) + | Pfcompl (ft: ftest) (**r comparison float64 *) | Paddw (**r add word *) | Psubw (**r sub word *) @@ -958,6 +959,17 @@ Definition compare_single (t: ftest) (v1 v2: val): val := | FTult => Val.notbool (Val.cmpfs Cge v1 v2) end. +Definition compare_float (t: ftest) (v1 v2: val): val := + match t with + | FTone | FTueq => Vundef (* unused *) + | FToeq => Val.cmpf Ceq v1 v2 + | FTune => Val.cmpf Cne v1 v2 + | FTolt => Val.cmpf Clt v1 v2 + | FTuge => Val.notbool (Val.cmpf Clt v1 v2) + | FToge => Val.cmpf Cge v1 v2 + | FTult => Val.notbool (Val.cmpf Cge v1 v2) + end. + (** Execution of arith instructions TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma... @@ -1029,6 +1041,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | 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) + | Pfcompl c => rs#d <- (compare_float 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 69d3d0cc..c2477e66 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -160,6 +160,7 @@ 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)) + | Pfcompl c => Some (Val (compare_float c v1 v2)) | Paddw => Some (Val (Val.add v1 v2)) | Psubw => Some (Val (Val.sub v1 v2)) diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 73ecd67f..edffd879 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -294,6 +294,18 @@ Definition transl_cond_notfloat32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) | Reversed ft => Pfcompw ft rd r2 r1 ::i k end. +Definition transl_cond_float64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompl ft rd r1 r2 ::i k + | Reversed ft => Pfcompl ft rd r2 r1 ::i k + end. + +Definition transl_cond_notfloat64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompl ft rd r1 r2 ::i k + | Reversed ft => Pfcompl ft rd r2 r1 ::i k + end. + Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) := match cond, args with @@ -326,26 +338,14 @@ Definition transl_cond_op 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") -(*| 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 - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompf 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 - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) -*)| _, _ => + OK (transl_cond_notfloat32 c rd r1 r2 k) + | Ccompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_float64 c rd r1 r2 k) + | Cnotcompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_notfloat64 c rd r1 r2 k) + | _, _ => Error(msg "Asmblockgen.transl_cond_op") end. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 1e3a40d4..1ac9a211 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -950,6 +950,8 @@ 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_float64. exploreInst; try discriminate. + unfold transl_cond_notfloat64. exploreInst; try discriminate. unfold transl_cond_float32. exploreInst; try discriminate. unfold transl_cond_notfloat32. exploreInst; try discriminate. - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e6093290..76404257 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1034,6 +1034,72 @@ Proof. destruct (Float32.cmp _ _ _); auto. Qed. +Lemma swap_comparison_cmpf: + forall v1 v2 cmp, + Val.lessdef (Val.cmpf cmp v1 v2) (Val.cmpf (swap_comparison cmp) v2 v1). +Proof. + intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. + rewrite Float.cmp_swap. auto. +Qed. + +Lemma transl_cond_float64_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_float64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.cmpf 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_cmpf. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpf. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +Qed. + +Lemma transl_cond_nofloat64_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_notfloat64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpf_bool 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. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float.cmp_ne_eq. auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float.cmp_ne_eq. simpl. destruct (Float.cmp Ceq f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float.cmp Clt f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float.cmp_swap. + destruct (Float.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float.cmp_swap. + destruct (Float.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float.cmp _ _ _); auto. +Qed. + Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> @@ -1069,6 +1135,10 @@ 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_float64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. ++ (* cmpnosingle *) + exploit transl_cond_nofloat64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpsingle *) exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpnosingle *) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index d9c22666..db50e3a5 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -56,6 +56,7 @@ let arith_rrr_str = function | Pcompw it -> "Pcompw" | Pcompl it -> "Pcompl" | Pfcompw ft -> "Pfcompw" + | Pfcompl ft -> "Pfcompl" | Paddw -> "Paddw" | Psubw -> "Psubw" | Pmulw -> "Pmulw" @@ -378,7 +379,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 + | Fcompw | Fcompd let ab_inst_to_real = function | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw @@ -388,6 +389,7 @@ let ab_inst_to_real = function | "Pcompw" | "Pcompiw" -> Compw | "Pcompl" | "Pcompil" -> Compd | "Pfcompw" -> Fcompw + | "Pfcompl" -> Fcompd | "Pmulw" -> Mulw | "Pmull" -> Muld | "Porw" | "Poriw" -> Orw @@ -480,6 +482,9 @@ let rec_to_usage r = | Fcompw -> (match encoding with None -> alu_lite | Some U6 | Some S10 | Some U27L5 -> alu_lite_x | _ -> raise InvalidEncoding) + | Fcompd -> (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 @@ -512,7 +517,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 | Fcompw + | Sxwd | Zxwd | Fcompw | Fcompd -> 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 ac2e3b27..5d59e7d2 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -359,6 +359,8 @@ module Target (*: TARGET*) = | Pfcompw (ft, rd, rs1, rs2) -> fprintf oc " fcompw.%a %a = %a, %a\n" fcond ft ireg rd ireg rs1 ireg rs2 + | Pfcompl (ft, rd, rs1, rs2) -> + fprintf oc " fcompd.%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 -- cgit