From f6686d81092ccaaf3a22b4e34aecc7c5895b08ba Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 15:48:43 +0100 Subject: begin adding abdw abdd --- kvx/Asm.v | 12 +++++++ kvx/Asmblockdeps.v | 4 +++ kvx/Asmvliw.v | 10 ++++++ kvx/ExtValues.v | 79 ++++++++++++++++++++++++++++++++++++++--- kvx/NeedOp.v | 4 +++ kvx/Op.v | 24 ++++++++++++- kvx/PostpassSchedulingOracle.ml | 10 ++++-- kvx/TargetPrinter.ml | 10 ++++++ kvx/ValueAOp.v | 35 ++++++++++++++++++ 9 files changed, 180 insertions(+), 8 deletions(-) (limited to 'kvx') diff --git a/kvx/Asm.v b/kvx/Asm.v index fd20316c..c8303d37 100644 --- a/kvx/Asm.v +++ b/kvx/Asm.v @@ -243,6 +243,9 @@ Inductive instruction : Type := | 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 *) + + | Pabdw (rd rs1 rs2: ireg) (**r Absolute difference word *) + | Pabdl (rd rs1 rs2: ireg) (**r Absolute difference long *) (** Arith RRI32 *) | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *) @@ -270,6 +273,7 @@ Inductive instruction : Type := | Psrxil (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word round to 0*) | Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *) | Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *) + | Pabdiw (rd rs: ireg) (imm: int) (**r Absolute difference word *) (** Arith RRI64 *) | Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *) @@ -293,6 +297,7 @@ Inductive instruction : Type := | Pcmoveuiw (bt: btest) (rcond rd : ireg) (imm: int) (** conditional move, unsigned semantics *) | Pcmoveil (bt: btest) (rcond rd : ireg) (imm: int64) (** conditional move *) | Pcmoveuil (bt: btest) (rcond rd : ireg) (imm: int64) (** conditional move, unsigned semantics *) + | Pabdil (rd rs : ireg) (imm: int64) (**r Absolute difference long *) . (** Correspondance between Asmblock and Asm *) @@ -417,6 +422,9 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmvliw.Pfmaxd rd rs1 rs2 => Pfmaxd rd rs1 rs2 | PArithRRR Asmvliw.Pfmaxw rd rs1 rs2 => Pfmaxw rd rs1 rs2 + | PArithRRR Asmvliw.Pabdw rd rs1 rs2 => Pabdw rd rs1 rs2 + | PArithRRR Asmvliw.Pabdl rd rs1 rs2 => Pabdl rd rs1 rs2 + (* RRI32 *) | PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm | PArithRRI32 Asmvliw.Paddiw rd rs imm => Paddiw rd rs imm @@ -442,6 +450,8 @@ Definition basic_to_instruction (b: basic) := | PArithRRI32 Asmvliw.Psrxil rd rs imm => Psrxil rd rs imm | PArithRRI32 Asmvliw.Psrail rd rs imm => Psrail rd rs imm + | PArithRRI32 Asmvliw.Pabdiw rd rs imm => Pabdiw rd rs imm + (* RRI64 *) | PArithRRI64 (Asmvliw.Pcompil it) rd rs imm => Pcompil it rd rs imm | PArithRRI64 Asmvliw.Paddil rd rs imm => Paddil rd rs imm @@ -458,6 +468,8 @@ Definition basic_to_instruction (b: basic) := | PArithRRI64 Asmvliw.Pandnil rd rs imm => Pandnil rd rs imm | PArithRRI64 Asmvliw.Pornil rd rs imm => Pornil rd rs imm + | PArithRRI64 Asmvliw.Pabdil rd rs imm => Pabdil rd rs imm + (** ARRR *) | PArithARRR Asmvliw.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2 | PArithARRR Asmvliw.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2 diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index a9786e0a..b1895ee6 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -1609,6 +1609,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pfminw => "Pfminw" | Pfmaxd => "Pfmaxd" | Pfmaxw => "Pfmaxw" + | Pabdw => "Pabdw" + | Pabdl => "Pabdl" end. Definition string_of_name_rri32 (n: arith_name_rri32): pstring := @@ -1636,6 +1638,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Psrlil => "Psrlil" | Psrail => "Psrail" | Psrxil => "Psrxil" + | Pabdiw => "Pabdiw" end. Definition string_of_name_rri64 (n: arith_name_rri64): pstring := @@ -1654,6 +1657,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := | Pnxoril => "Pnxoril" | Pandnil => "Pandnil" | Pornil => "Pornil" + | Pabdil => "Pabdil" end. Definition string_of_name_arrr (n: arith_name_arrr): pstring := diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index 45b230e6..bbd40692 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -472,6 +472,9 @@ Inductive arith_name_rrr : Type := | Pfminw (**r float min word *) | Pfmaxd (**r float max double *) | Pfmaxw (**r float max word *) + + | Pabdw (**r absolute value of difference *) + | Pabdl (**r absolute value of difference *) . Inductive arith_name_rri32 : Type := @@ -499,6 +502,7 @@ Inductive arith_name_rri32 : Type := | Psrlil (**r shift right logical immediate long *) | Psrail (**r shift right arithmetic immediate long *) | Psrxil (**r shift right arithmetic immediate long round to 0*) + | Pabdiw (**r absolute value of difference *) . Inductive arith_name_rri64 : Type := @@ -516,6 +520,7 @@ Inductive arith_name_rri64 : Type := | Pnxoril (**r nxor immediate long *) | Pandnil (**r andn immediate long *) | Pornil (**r orn immediate long *) + | Pabdil (**r absolute value of difference *) . Inductive arith_name_arrr : Type := @@ -1033,6 +1038,9 @@ Definition arith_eval_rrr n v1 v2 := | Prevsubxw shift => ExtValues.revsubx (int_of_shift1_4 shift) v1 v2 | Prevsubxl shift => ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2 + + | Pabdw => ExtValues.absdiff v1 v2 + | Pabdl => ExtValues.absdiffl v1 v2 end. Definition arith_eval_rri32 n v i := @@ -1060,6 +1068,7 @@ Definition arith_eval_rri32 n v i := | Psrail => Val.shrl v (Vint i) | Paddxiw shift => ExtValues.addx (int_of_shift1_4 shift) v (Vint i) | Prevsubxiw shift => ExtValues.revsubx (int_of_shift1_4 shift) v (Vint i) + | Pabdiw => ExtValues.absdiff v (Vint i) end. Definition arith_eval_rri64 n v i := @@ -1078,6 +1087,7 @@ Definition arith_eval_rri64 n v i := | Pornil => Val.orl (Val.notl v) (Vlong i) | Paddxil shift => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i) | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i) + | Pabdil => ExtValues.absdiff v (Vlong i) end. Definition cmove bt v1 v2 v3 := diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index b4e14898..434d283e 100644 --- a/kvx/ExtValues.v +++ b/kvx/ExtValues.v @@ -21,14 +21,14 @@ Require Import Lia. Open Scope Z_scope. -Definition abs_diff (x y : Z) := Z.abs (x - y). -Definition abs_diff2 (x y : Z) := +Definition int_abs_diff (x y : Z) := Z.abs (x - y). +Definition int_abs_diff2 (x y : Z) := if x <=? y then y - x else x - y. -Lemma abs_diff2_correct : - forall x y : Z, (abs_diff x y) = (abs_diff2 x y). +Lemma int_abs_diff2_correct : + forall x y : Z, (int_abs_diff x y) = (int_abs_diff2 x y). Proof. intros. - unfold abs_diff, abs_diff2. + unfold int_abs_diff, int_abs_diff2. unfold Z.leb. pose proof (Z.compare_spec x y) as Hspec. inv Hspec. @@ -754,3 +754,72 @@ Definition fmaddfs := triple_op_single (fun f1 f2 f3 => Float32.fma f2 f3 f1). Definition fmsubf := triple_op_float (fun f1 f2 f3 => Float.fma (Float.neg f2) f3 f1). Definition fmsubfs := triple_op_single (fun f1 f2 f3 => Float32.fma (Float32.neg f2) f3 f1). + +Definition double_op_intZ f v1 v2 := + match v1, v2 with + | (Vint i1), (Vint i2) => Vint (Int.repr (f (Int.signed i1) (Int.signed i2))) + | _, _ => Vundef + end. + +Definition double_op_longZ f v1 v2 := + match v1, v2 with + | (Vlong i1), (Vlong i2) => Vlong (Int64.repr (f (Int64.signed i1) (Int64.signed i2))) + | _, _ => Vundef + end. + +Definition absdiff := double_op_intZ int_abs_diff. +Definition absdiffl := double_op_longZ int_abs_diff. + +Definition abs v1 := + match v1 with + | Vint x => Vint (Int.repr (Z.abs (Int.signed x))) + | _ => Vundef + end. + +Definition absl v1 := + match v1 with + | Vlong x => Vlong (Int64.repr (Z.abs (Int64.signed x))) + | _ => Vundef + end. + +Lemma absdiff_zero_correct: + forall v, abs v = absdiff v (Vint Int.zero). +Proof. + intro. destruct v; cbn; try reflexivity. + f_equal. unfold int_abs_diff. + change (Int.unsigned Int.zero) with 0%Z. + rewrite Z.sub_0_r. + reflexivity. +Qed. + +Lemma absdiffl_zero_correct: + forall v, absl v = absdiffl v (Vlong Int64.zero). +Proof. + intro. destruct v; cbn; try reflexivity. + f_equal. unfold int_abs_diff. + change (Int64.unsigned Int64.zero) with 0%Z. + rewrite Z.sub_0_r. + reflexivity. +Qed. + +Remark absdiff_inject: + forall f v1 v1' v2 v2' + (INJ1 : Val.inject f v1 v1') + (INJ2 : Val.inject f v2 v2'), + Val.inject f (absdiff v1 v2) (absdiff v1' v2'). +Proof. + intros. + inv INJ1; cbn; try constructor. + inv INJ2; cbn; constructor. +Qed. + +Remark absdiffl_inject: + forall f v1 v1' v2 v2' + (INJ1 : Val.inject f v1 v1') + (INJ2 : Val.inject f v2 v2'), + Val.inject f (absdiffl v1 v2) (absdiffl v1' v2'). +Proof. + intros. + inv INJ1; cbn; try constructor. + inv INJ2; cbn; constructor. +Qed. diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index 4578b4e8..cc86fc88 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -137,6 +137,10 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Osel c ty => nv :: nv :: needs_of_condition0 c | Oselimm c imm | Osellimm c imm => nv :: needs_of_condition0 c + | Oabsdiff => op2 (default nv) + | Oabsdiffimm _ => op1 (default nv) + | Oabsdiffl => op2 (default nv) + | Oabsdifflimm _ => op1 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := diff --git a/kvx/Op.v b/kvx/Op.v index 4458adb3..86db0c0a 100644 --- a/kvx/Op.v +++ b/kvx/Op.v @@ -219,7 +219,11 @@ Inductive operation : Type := | Oinsfl (stop : Z) (start : Z) | Osel (c0 : condition0) (ty : typ) | Oselimm (c0 : condition0) (imm: int) - | Osellimm (c0 : condition0) (imm: int64). + | Osellimm (c0 : condition0) (imm: int64) + | Oabsdiff + | Oabsdiffimm (imm: int) + | Oabsdiffl + | Oabsdifflimm (imm: int64). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -476,6 +480,10 @@ Definition eval_operation | Osel c ty, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 v2 ty) | Oselimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint) | Osellimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong) + | Oabsdiff, v0::v1::nil => Some(ExtValues.absdiff v0 v1) + | (Oabsdiffimm n1), v0::nil => Some(ExtValues.absdiff v0 (Vint n1)) + | Oabsdiffl, v0::v1::nil => Some(ExtValues.absdiffl v0 v1) + | (Oabsdifflimm n1), v0::nil => Some(ExtValues.absdiffl v0 (Vlong n1)) | _, _ => None end. @@ -691,6 +699,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osel c ty => (ty :: ty :: arg_type_of_condition0 c :: nil, ty) | Oselimm c ty => (Tint :: arg_type_of_condition0 c :: nil, Tint) | Osellimm c ty => (Tlong :: arg_type_of_condition0 c :: nil, Tlong) + | Oabsdiff => (Tint :: Tint :: nil, Tint) + | Oabsdiffimm _ => (Tint :: nil, Tint) + | Oabsdiffl => (Tlong :: Tlong :: nil, Tlong) + | Oabsdifflimm _ => (Tlong :: nil, Tlong) end. (* FIXME: two Tptr ?! *) @@ -1026,6 +1038,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - unfold Val.select. destruct (eval_condition0 _ _ m). + apply Val.normalize_type. + constructor. + (* oabsdiff *) + - destruct v0; destruct v1; cbn; trivial. + - destruct v0; cbn; trivial. + - destruct v0; destruct v1; cbn; trivial. + - destruct v0; cbn; trivial. Qed. Definition is_trapping_op (op : operation) := @@ -1738,6 +1755,11 @@ Proof. symmetry. eapply eval_condition0_inj; eassumption. + left. trivial. + (* Oabsdiff *) + - apply ExtValues.absdiff_inject; trivial. + - apply ExtValues.absdiff_inject; trivial. + - apply ExtValues.absdiffl_inject; trivial. + - apply ExtValues.absdiffl_inject; trivial. Qed. Lemma eval_addressing_inj: diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml index 47849dd5..3eb0b95f 100644 --- a/kvx/PostpassSchedulingOracle.ml +++ b/kvx/PostpassSchedulingOracle.ml @@ -34,6 +34,7 @@ type real_instruction = | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sbfxw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Sbfxd | Srad | Srld | Slld | Srsd | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd + | Abdw | Abdd | Maddw | Maddd | Msbfw | Msbfd | Cmoved | Make | Nop | Extfz | Extfs | Insf | Addxw | Addxd @@ -143,6 +144,8 @@ let arith_rrr_real = function | Pfminw -> Fminw | Pfmaxd -> Fmaxd | Pfmaxw -> Fmaxw + | Pabdw -> Abdw + | Pabdl -> Abdd let arith_rri32_real = function | Pcompiw it -> Compw @@ -168,6 +171,7 @@ let arith_rri32_real = function | Psrlil -> Srld | Psrail -> Srad | Psrxil -> Srsd + | Pabdiw -> Abdw let arith_rri64_real = function | Pcompil it -> Compd @@ -184,6 +188,7 @@ let arith_rri64_real = function | Pnxoril -> Nxord | Pandnil -> Andnd | Pornil -> Ornd + | Pabdil -> Abdd let arith_arr_real = function @@ -603,11 +608,11 @@ let rec_to_usage r = (match encoding with None | Some U6 | Some S10 -> alu_lite | Some U27L5 | Some U27L10 -> alu_lite_x | Some E27U27L10 -> alu_lite_y) - | Addxw -> + | Addxw | Abdw -> (match encoding with None | Some U6 | Some S10 -> alu_lite | Some U27L5 | Some U27L10 -> alu_lite_x | _ -> raise InvalidEncoding) - | Addxd -> + | Addxd | Abdd -> (match encoding with None | Some U6 | Some S10 -> alu_lite | Some U27L5 | Some U27L10 -> alu_lite_x | Some E27U27L10 -> alu_lite_y) @@ -681,6 +686,7 @@ let real_inst_to_latency = function | Addd | Andd | Compd | Ord | Sbfd | Sbfxd | Srad | Srsd | Srld | Slld | Xord | Make | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd | Fmind | Fmaxd | Fminw | Fmaxw + | Abdw | Abdd -> 1 | Floatwz | Floatuwz | Fixeduw | Fixedw | Floatdz | Floatudz | Fixedd | Fixedud -> 4 | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml index 9e2e3776..8a311dbb 100644 --- a/kvx/TargetPrinter.ml +++ b/kvx/TargetPrinter.ml @@ -731,6 +731,12 @@ module Target (*: TARGET*) = | Pfinvw (rd, rs1) -> fprintf oc " finvw %a = %a\n" ireg rd ireg rs1 + | Pabdw (rd, rs1, rs2) -> + fprintf oc " abdw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pabdl (rd, rs1, rs2) -> + fprintf oc " abdd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + + (* Arith RRI32 instructions *) | Pcompiw (it, rd, rs, imm) -> fprintf oc " compw.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint imm @@ -762,6 +768,8 @@ module Target (*: TARGET*) = fprintf oc " andnw %a = %a, %a\n" ireg rd ireg rs coqint imm | Porniw (rd, rs, imm) -> fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pabdiw (rd, rs, imm) -> + fprintf oc " abdw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psraiw (rd, rs, imm) -> fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psrxiw (rd, rs, imm) -> @@ -815,6 +823,8 @@ module Target (*: TARGET*) = fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pornil (rd, rs, imm) -> fprintf oc " ornd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pabdil (rd, rs, imm) -> + fprintf oc " abdd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pmaddil (rd, rs, imm) -> fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs coqint64 imm diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index 87554258..f0fed567 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -156,6 +156,12 @@ Definition eval_static_insfl stop start prev fld := end else Vtop. +Definition absdiff := binop_int + (fun i1 i2 => Int.repr (ExtValues.int_abs_diff (Int.signed i1) (Int.signed i2))). + +Definition absdiffl := binop_long + (fun i1 i2 => Int64.repr (ExtValues.int_abs_diff (Int64.signed i1) (Int64.signed i2))). + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -308,6 +314,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osel c ty, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 v2 | Oselimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (I imm) | Osellimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (L imm) + | Oabsdiff, v1::v2::nil => absdiff v1 v2 + | (Oabsdiffimm n2), v1::nil => absdiff v1 (I n2) + | Oabsdiffl, v1::v2::nil => absdiffl v1 v2 + | (Oabsdifflimm n2), v1::nil => absdiffl v1 (L n2) | _, _ => Vbot end. @@ -319,6 +329,26 @@ Hypothesis GENV: genv_match bc ge. Variable sp: block. Hypothesis STACK: bc sp = BCstack. +Lemma absdiff_sound: + forall v x w y + (vMATCH : vmatch bc v x) + (wMATCH : vmatch bc w y), + vmatch bc (ExtValues.absdiff v w) (absdiff x y). +Proof. + intros. + apply binop_int_sound; trivial. +Qed. + +Lemma absdiffl_sound: + forall v x w y + (vMATCH : vmatch bc v x) + (wMATCH : vmatch bc w y), + vmatch bc (ExtValues.absdiffl v w) (absdiffl x y). +Proof. + intros. + apply binop_long_sound; trivial. +Qed. + Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). Proof. @@ -593,6 +623,11 @@ Proof. - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. (* select long imm *) - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. + (* Oabsdiff *) + - apply absdiff_sound; auto with va. + - apply absdiff_sound; auto with va. + - apply absdiffl_sound; auto with va. + - apply absdiffl_sound; auto with va. Qed. End SOUNDNESS. -- cgit