From b7aea86a0c6ace274e585fddfd0d88d13528cc90 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 12 Feb 2022 16:20:38 +0100 Subject: fix bad changes --- kvx/PostpassSchedulingOracle.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kvx') diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml index e752624c..47849dd5 100644 --- a/kvx/PostpassSchedulingOracle.ml +++ b/kvx/PostpassSchedulingOracle.ml @@ -87,10 +87,10 @@ let arith_rr_real = function | Pfloatuwrnsz -> Floatuwz | Pfloatudrnsz -> Floatudz | Pfloatdrnsz -> Floatdz - | Pfixedwrzz | Pfixedwrne -> Fixedw - | Pfixeduwrzz | Pfixeduwrne -> Fixeduw - | Pfixeddrzz | Pfixeddrne -> Fixedd - | Pfixedudrzz| Pfixedudrne -> Fixedud + | Pfixedwrzz -> Fixedw + | Pfixeduwrzz -> Fixeduw + | Pfixeddrzz -> Fixedd + | Pfixedudrzz -> Fixedud | Pfixeddrzz_i32 -> Fixedd | Pfixedudrzz_i32 -> Fixedud -- cgit 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 From fc384f172b72f90c8de52ec846344b7ffda76070 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 16:19:17 +0100 Subject: compiled absdiff --- kvx/Asmblockgen.v | 14 +++++++++++++- kvx/Asmvliw.v | 2 +- 2 files changed, 14 insertions(+), 2 deletions(-) (limited to 'kvx') diff --git a/kvx/Asmblockgen.v b/kvx/Asmblockgen.v index ab827b1c..fd41dfdd 100644 --- a/kvx/Asmblockgen.v +++ b/kvx/Asmblockgen.v @@ -535,6 +535,12 @@ Definition transl_op | Oornimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Porniw rd rs n ::i k) + | Oabsdiff, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pabdw rd rs1 rs2 ::i k) + | Oabsdiffimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pabdiw rd rs n ::i k) | Oshl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psllw rd rs1 rs2 ::i k) @@ -672,6 +678,12 @@ Definition transl_op | Oornlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pornil rd rs n ::i k) + | Oabsdiffl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pabdl rd rs1 rs2 ::i k) + | Oabsdifflimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pabdil rd rs n ::i k) | Oshll, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pslll rd rs1 rs2 ::i k) @@ -889,7 +901,7 @@ Definition transl_op do rC <- ireg_of aC; do op <- conditional_move_imm64 (negate_condition0 cond0) rC rT imm; OK (op ::i k) - + | _, _ => Error(msg "Asmgenblock.transl_op") end. diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index bbd40692..0ce2ed69 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -1087,7 +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) + | Pabdil => ExtValues.absdiffl v (Vlong i) end. Definition cmove bt v1 v2 v3 := -- cgit From ed6e20995761614ee7ea6235b978a463f071c123 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 17:49:40 +0100 Subject: abs builtins --- kvx/Builtins1.v | 14 ++++++++++++-- kvx/CBuiltins.ml | 4 ++++ kvx/ExtValues.v | 53 ++++++++++++++++++++++++++++++++++++++------------- kvx/SelectOp.vp | 20 +++++++++++++++++++ kvx/SelectOpproof.v | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++- kvx/ValueAOp.v | 4 ++-- 6 files changed, 132 insertions(+), 18 deletions(-) (limited to 'kvx') diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index 441345bf..b5fc7459 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -16,7 +16,7 @@ (** Platform-specific built-in functions *) Require Import String Coqlib. -Require Import AST Integers Floats Values ExtFloats. +Require Import AST Integers Floats Values ExtFloats ExtValues. Require Import Builtins0. Inductive platform_builtin : Type := @@ -25,7 +25,9 @@ Inductive platform_builtin : Type := | BI_fminf | BI_fmaxf | BI_fma -| BI_fmaf. +| BI_fmaf +| BI_abs +| BI_absl. Local Open Scope string_scope. @@ -36,6 +38,8 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmaxf", BI_fmaxf) :: ("__builtin_fma", BI_fma) :: ("__builtin_fmaf", BI_fmaf) + :: ("__builtin_abs", BI_abs) + :: ("__builtin_absl", BI_absl) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -48,6 +52,10 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle cc_default + | BI_abs => + mksignature (Tint :: nil) Tint cc_default + | BI_absl => + mksignature (Tlong :: nil) Tlong cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -58,4 +66,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma + | BI_abs => mkbuiltin_n1t Tint Tint ExtValues.int_abs + | BI_absl => mkbuiltin_n1t Tlong Tlong ExtValues.long_abs end. diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml index 7398e0f4..4d016453 100644 --- a/kvx/CBuiltins.ml +++ b/kvx/CBuiltins.ml @@ -133,6 +133,10 @@ let builtins = { "__builtin_fmaf", (TFloat(FFloat, []), [TFloat(FFloat, []); TFloat(FFloat, []); TFloat(FFloat, [])], false); + "__builtin_abs", + (TInt(IInt, []), [TInt(IInt, [])], false); + "__builtin_absl", + (TInt(ILong, []), [TInt(ILong, [])], false); ] } diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index 434d283e..c493f708 100644 --- a/kvx/ExtValues.v +++ b/kvx/ExtValues.v @@ -21,14 +21,14 @@ Require Import Lia. Open Scope Z_scope. -Definition int_abs_diff (x y : Z) := Z.abs (x - y). -Definition int_abs_diff2 (x y : Z) := +Definition Z_abs_diff (x y : Z) := Z.abs (x - y). +Definition Z_abs_diff2 (x y : Z) := if x <=? y then y - x else x - y. -Lemma int_abs_diff2_correct : - forall x y : Z, (int_abs_diff x y) = (int_abs_diff2 x y). +Lemma Z_abs_diff2_correct : + forall x y : Z, (Z_abs_diff x y) = (Z_abs_diff2 x y). Proof. intros. - unfold int_abs_diff, int_abs_diff2. + unfold Z_abs_diff, Z_abs_diff2. unfold Z.leb. pose proof (Z.compare_spec x y) as Hspec. inv Hspec. @@ -755,20 +755,47 @@ 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 := +Definition int_abs i1 := Int.repr (Z.abs (Int.signed i1)). +Definition long_abs i1 := Int64.repr (Z.abs (Int64.signed i1)). + +Definition int_absdiff i1 i2 := + Int.repr (Z_abs_diff (Int.signed i1) (Int.signed i2)). + +Definition long_absdiff i1 i2 := + Int64.repr (Z_abs_diff (Int64.signed i1) (Int64.signed i2)). + +Lemma int_absdiff_zero : + forall i, int_abs i = int_absdiff i Int.zero. +Proof. + intro. unfold int_abs, int_absdiff, Z_abs_diff. + change (Int.signed Int.zero) with 0%Z. + rewrite Z.sub_0_r. + reflexivity. +Qed. + +Lemma long_absdiff_zero : + forall i, long_abs i = long_absdiff i Int64.zero. +Proof. + intro. unfold long_abs, long_absdiff, Z_abs_diff. + change (Int64.signed Int64.zero) with 0%Z. + rewrite Z.sub_0_r. + reflexivity. +Qed. + +Definition double_op_int f v1 v2 := match v1, v2 with - | (Vint i1), (Vint i2) => Vint (Int.repr (f (Int.signed i1) (Int.signed i2))) + | (Vint i1), (Vint i2) => Vint (f i1 i2) | _, _ => Vundef end. -Definition double_op_longZ f v1 v2 := +Definition double_op_long f v1 v2 := match v1, v2 with - | (Vlong i1), (Vlong i2) => Vlong (Int64.repr (f (Int64.signed i1) (Int64.signed i2))) + | (Vlong i1), (Vlong i2) => Vlong (f i1 i2) | _, _ => Vundef end. -Definition absdiff := double_op_intZ int_abs_diff. -Definition absdiffl := double_op_longZ int_abs_diff. +Definition absdiff := double_op_int int_absdiff. +Definition absdiffl := double_op_long long_absdiff. Definition abs v1 := match v1 with @@ -786,7 +813,7 @@ 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. + f_equal. unfold int_absdiff, Z_abs_diff. change (Int.unsigned Int.zero) with 0%Z. rewrite Z.sub_0_r. reflexivity. @@ -796,7 +823,7 @@ 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. + f_equal. unfold long_absdiff, Z_abs_diff. change (Int64.unsigned Int64.zero) with 0%Z. rewrite Z.sub_0_r. reflexivity. diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index 4e1087f9..f243089d 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -742,6 +742,24 @@ Nondetfunction gen_fmaf args := | _ => None end. +Definition select_abs (e1 : expr) := + Eop (Oabsdiffimm Int.zero) (e1 ::: Enil). + +Definition select_absl (e1 : expr) := + Eop (Oabsdifflimm Int64.zero) (e1 ::: Enil). + +Definition gen_abs args := + match args with + | e1:::Enil => Some (select_abs e1) + | _ => None + end. + +Definition gen_absl args := + match args with + | e1:::Enil => Some (select_absl e1) + | _ => None + end. + Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := match b with | BI_fmin => Some (Eop Ominf args) @@ -750,6 +768,8 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr | BI_fmaxf => Some (Eop Omaxfs args) | BI_fma => gen_fma args | BI_fmaf => gen_fmaf args + | BI_abs => gen_abs args + | BI_absl => gen_absl args end. End SELECT. diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index 0ede1e2d..4ddf6ece 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1883,6 +1883,58 @@ Proof. destruct v2; simpl; trivial. Qed. +Lemma eval_abs: + forall al a vl v le, + gen_abs al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem BI_abs vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + unfold gen_abs. + intros until le. + intros SELECT Heval BUILTIN. + inv Heval. discriminate. + inv H0. 2: discriminate. + cbn in BUILTIN. + inv BUILTIN. + inv SELECT. + econstructor; split. + { repeat (econstructor + eassumption). + } + destruct v1; try constructor. + cbn. + unfold int_abs, int_absdiff, Z_abs_diff. + change (Int.signed Int.zero) with 0%Z. + rewrite Z.sub_0_r. + constructor. +Qed. + +Lemma eval_absl: + forall al a vl v le, + gen_absl al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem BI_absl vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + unfold gen_abs. + intros until le. + intros SELECT Heval BUILTIN. + inv Heval. discriminate. + inv H0. 2: discriminate. + cbn in BUILTIN. + inv BUILTIN. + inv SELECT. + econstructor; split. + { repeat (econstructor + eassumption). + } + destruct v1; try constructor. + cbn. + unfold long_abs, long_absdiff, Z_abs_diff. + change (Int64.signed Int64.zero) with 0%Z. + rewrite Z.sub_0_r. + constructor. +Qed. + Theorem eval_platform_builtin: forall bf al a vl v le, platform_builtin bf al = Some a -> @@ -1896,6 +1948,7 @@ Proof. repeat (try econstructor; try eassumption)). - apply eval_fma; assumption. - apply eval_fmaf; assumption. + - apply eval_abs; assumption. + - apply eval_absl; assumption. Qed. - End CMCONSTR. diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index f0fed567..ddfe94f3 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -157,10 +157,10 @@ Definition eval_static_insfl stop start prev fld := else Vtop. Definition absdiff := binop_int - (fun i1 i2 => Int.repr (ExtValues.int_abs_diff (Int.signed i1) (Int.signed i2))). + (fun i1 i2 => ExtValues.int_absdiff i1 i2). Definition absdiffl := binop_long - (fun i1 i2 => Int64.repr (ExtValues.int_abs_diff (Int64.signed i1) (Int64.signed i2))). + (fun i1 i2 => ExtValues.long_absdiff i1 i2). Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with -- cgit From 2867dee21f6fb696db554679d8535306c7a9d4ea Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 18:15:17 +0100 Subject: long -> single precision float done with instructions --- kvx/FPExtra.v | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++ kvx/SelectLong.vp | 5 ++++- kvx/SelectLongproof.v | 5 ++++- 3 files changed, 65 insertions(+), 2 deletions(-) (limited to 'kvx') diff --git a/kvx/FPExtra.v b/kvx/FPExtra.v index 05fd8842..9e3b55b6 100644 --- a/kvx/FPExtra.v +++ b/kvx/FPExtra.v @@ -15,9 +15,11 @@ Definition e_addl a b := Eop Oaddl (a ::: b ::: Enil). Definition e_orl a b := Eop Oorl (a ::: b ::: Enil). Definition e_constl n := Eop (Olongconst (Int64.repr n)) Enil. Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil). +Definition e_float_of_long a := Eop Ofloatoflong (a ::: Enil). Definition e_single_of_float a := Eop Osingleoffloat (a ::: Enil). Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil). Definition e_cmpluimm c v n := Eop (Ocmp (Ccompluimm c n)) (v ::: Enil). +Definition e_absl a := Eop (Oabsdifflimm Int64.zero) (a ::: Enil). Definition a_var := Eletvar 0%nat. @@ -58,3 +60,58 @@ Proof. lia. Qed. +Definition e_single_of_long a := + Elet a (e_single_of_float (e_float_of_long + (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle (e_absl a_var) (Int64.repr (2^53))) a_var + (e_andl (e_orl a_var (e_addl (e_andl a_var (e_constl 2047)) + (e_constl 2047))) + (e_constl (-2048))))))%Z. + +Theorem e_single_of_long_correct : + forall (ge : genv) (sp: val) cmenv memenv + (le : letenv) (expr_a : expr) (va : val) + (EVAL_a : eval_expr ge sp cmenv memenv le expr_a va), + eval_expr ge sp cmenv memenv le (e_single_of_long expr_a) + (Val.maketotal (Val.singleoflong va)). +Proof. + intros. + unfold e_single_of_long. + repeat econstructor. eassumption. + cbn. + destruct va; cbn. + all: try reflexivity. + f_equal. + unfold Int64.ltu. + change (Int64.unsigned (Int64.repr 9007199254740992))%Z with 9007199254740992%Z. + destruct zlt as [LT | GE]; cbn. + { change (Int.eq Int.zero Int.zero) with true. cbn. + f_equal. + symmetry. + apply Float32.of_long_double_2. + unfold long_absdiff, Z_abs_diff in LT. + change (Int64.signed Int64.zero) with 0%Z in LT. + rewrite Z.sub_0_r in LT. + rewrite Int64.unsigned_repr in LT. + lia. + pose proof (Int64.signed_range i). + change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + change Int64.max_unsigned with (18446744073709551615)%Z. + lia. + } + change (Int.eq Int.one Int.zero) with false. cbn. + f_equal. + symmetry. + apply Float32.of_long_double_1. + unfold long_absdiff, Z_abs_diff in GE. + change (Int64.signed Int64.zero) with 0%Z in GE. + rewrite Z.sub_0_r in GE. + rewrite Int64.unsigned_repr in GE. + lia. + pose proof (Int64.signed_range i). + change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + change Int64.max_unsigned with (18446744073709551615)%Z. + lia. +Qed. + diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp index 3598025a..9df3212b 100644 --- a/kvx/SelectLong.vp +++ b/kvx/SelectLong.vp @@ -452,7 +452,10 @@ Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e). Definition use_inlined_fp_conversions := true. Opaque use_inlined_fp_conversions. -Definition singleoflong (e: expr) := SplitLong.singleoflong e. +Definition singleoflong (e: expr) := + if use_inlined_fp_conversions + then FPExtra.e_single_of_long e + else SplitLong.singleoflong e. Definition singleoflongu (e: expr) := if use_inlined_fp_conversions diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v index b858158b..ca32d69a 100644 --- a/kvx/SelectLongproof.v +++ b/kvx/SelectLongproof.v @@ -933,7 +933,10 @@ Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. Proof. unfold singleoflong; red; intros. - eapply SplitLongproof.eval_singleoflong; eauto. + destruct use_inlined_fp_conversions. + - econstructor. split. apply FPExtra.e_single_of_long_correct. + eassumption. rewrite H0. cbn. constructor. + - eapply SplitLongproof.eval_singleoflong; eauto. Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. -- cgit