From f2a2cca20b8ae576c603b4f119cb2a7c73515f18 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 11 Feb 2022 22:46:42 +0100 Subject: remove useless stuff --- kvx/Archi.v | 2 +- kvx/SelectLong.vp | 4 ---- kvx/SelectLongproof.v | 18 ++++++------------ 3 files changed, 7 insertions(+), 17 deletions(-) diff --git a/kvx/Archi.v b/kvx/Archi.v index 6d59a3d1..b1739421 100644 --- a/kvx/Archi.v +++ b/kvx/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for MPPA KVX. Mostly copied from the Risc-V backend *) Require Import ZArith List. -Require Import Binary Bits. +From Flocq Require Import Binary Bits. Definition ptr64 := true. diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp index b3638eca..16517aa5 100644 --- a/kvx/SelectLong.vp +++ b/kvx/SelectLong.vp @@ -433,19 +433,15 @@ Definition cmpl (c: comparison) (e1 e2: expr) := (** ** Floating-point conversions *) Definition longoffloat (e: expr) := - if Archi.splitlong then SplitLong.longoffloat e else Eop Olongoffloat (e:::Enil). Definition longuoffloat (e: expr) := - if Archi.splitlong then SplitLong.longuoffloat e else Eop Olonguoffloat (e:::Enil). Definition floatoflong (e: expr) := - if Archi.splitlong then SplitLong.floatoflong e else Eop Ofloatoflong (e:::Enil). Definition floatoflongu (e: expr) := - if Archi.splitlong then SplitLong.floatoflongu e else Eop Ofloatoflongu (e:::Enil). Definition longofsingle (e: expr) := longoffloat (floatofsingle e). diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v index c3abdbc7..a88863b4 100644 --- a/kvx/SelectLongproof.v +++ b/kvx/SelectLongproof.v @@ -884,32 +884,28 @@ Qed. Theorem eval_longoffloat: partial_unary_constructor_sound longoffloat Val.longoffloat. Proof. - unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_longoffloat; eauto. + unfold longoffloat; red; intros. TrivialExists. simpl. rewrite H0. reflexivity. Qed. Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat. Proof. - unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_longuoffloat; eauto. + unfold longuoffloat; red; intros. TrivialExists. simpl. rewrite H0. reflexivity. Qed. Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong. Proof. - unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_floatoflong; eauto. + unfold floatoflong; red; intros. TrivialExists. simpl. rewrite H0. reflexivity. Qed. Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu. Proof. - unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_floatoflongu; eauto. + unfold floatoflongu; red; intros. TrivialExists. simpl. rewrite H0. reflexivity. Qed. @@ -936,16 +932,14 @@ Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. Proof. - unfold singleoflong; red; intros. (* destruct Archi.splitlong eqn:SL. *) + unfold singleoflong; red; intros. eapply SplitLongproof.eval_singleoflong; eauto. -(* TrivialExists. *) Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. Proof. - unfold singleoflongu; red; intros. (* destruct Archi.splitlong eqn:SL. *) + unfold singleoflongu; red; intros. eapply SplitLongproof.eval_singleoflongu; eauto. -(* TrivialExists. *) Qed. End CMCONSTR. -- cgit From 5ba8c76d3eaf78d1a57678af5d9b006e29c4a02f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 12 Feb 2022 11:37:43 +0100 Subject: extra FP code --- kvx/FPExtra.v | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 kvx/FPExtra.v diff --git a/kvx/FPExtra.v b/kvx/FPExtra.v new file mode 100644 index 00000000..05fd8842 --- /dev/null +++ b/kvx/FPExtra.v @@ -0,0 +1,60 @@ +Require Import Coqlib. +Require Import Compopts. +Require Import AST Integers Floats. +Require Import Op CminorSel. +Require Import OpHelpers. +Require Import SelectOp SplitLong. +Require Import Values ExtValues. +Require Import DecBoolOps. + +Local Open Scope cminorsel_scope. +Local Open Scope string_scope. + +Definition e_andl a b := Eop Oandl (a ::: b ::: Enil). +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_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 a_var := Eletvar 0%nat. + +Definition e_single_of_longu a := + Elet a (e_single_of_float (e_float_of_longu + (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle 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_longu_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_longu expr_a) + (Val.maketotal (Val.singleoflongu va)). +Proof. + intros. + unfold e_single_of_longu. + 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_longu_double_2. + lia. + } + change (Int.eq Int.one Int.zero) with false. cbn. + f_equal. + symmetry. + apply Float32.of_longu_double_1. + lia. +Qed. + -- cgit From 50377ef4b9430fa019e26fac3028739f0308e9b1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 12 Feb 2022 12:06:32 +0100 Subject: unsigned long -> float without function calls --- configure | 1 + kvx/SelectLong.vp | 9 ++++++++- kvx/SelectLongproof.v | 5 ++++- 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/configure b/configure index 61a6697c..685ce390 100755 --- a/configure +++ b/configure @@ -821,6 +821,7 @@ CFLAGS= -D __KVX_COS__ SIMU=kvx-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ + FPExtra.v \\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp index 16517aa5..3598025a 100644 --- a/kvx/SelectLong.vp +++ b/kvx/SelectLong.vp @@ -23,6 +23,7 @@ Require Import OpHelpers. Require Import SelectOp SplitLong. Require Import ExtValues. Require Import DecBoolOps. +Require FPExtra. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -448,9 +449,15 @@ Definition longofsingle (e: expr) := longoffloat (floatofsingle e). 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 singleoflongu (e: expr) := SplitLong.singleoflongu e. +Definition singleoflongu (e: expr) := + if use_inlined_fp_conversions + then FPExtra.e_single_of_longu e + else SplitLong.singleoflongu e. End SELECT. diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v index a88863b4..b858158b 100644 --- a/kvx/SelectLongproof.v +++ b/kvx/SelectLongproof.v @@ -939,7 +939,10 @@ Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. Proof. unfold singleoflongu; red; intros. - eapply SplitLongproof.eval_singleoflongu; eauto. + destruct use_inlined_fp_conversions. + - econstructor. split. apply FPExtra.e_single_of_longu_correct. + eassumption. rewrite H0. cbn. constructor. + - eapply SplitLongproof.eval_singleoflongu; eauto. Qed. End CMCONSTR. -- cgit From 337c490d12c437dcbb5941e204ec1b1c4efa992b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 12 Feb 2022 13:14:43 +0100 Subject: fix bad reservation table for finvw --- kvx/PostpassSchedulingOracle.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml index 3f4520a6..e752624c 100644 --- a/kvx/PostpassSchedulingOracle.ml +++ b/kvx/PostpassSchedulingOracle.ml @@ -47,7 +47,8 @@ type real_instruction = | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Fmind | Fminw | Fmaxd | Fmaxw | Finvw | Ffmaw | Ffmad | Ffmsw | Ffmsd - | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz + | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz + | Fixedw | Fixeduw | Fixedd | Fixedud | Fcompw | Fcompd type ab_inst_rec = { @@ -86,12 +87,12 @@ let arith_rr_real = function | Pfloatuwrnsz -> Floatuwz | Pfloatudrnsz -> Floatudz | Pfloatdrnsz -> Floatdz - | Pfixedwrzz -> Fixedwz - | Pfixeduwrzz -> Fixeduwz - | Pfixeddrzz -> Fixeddz - | Pfixedudrzz -> Fixedudz - | Pfixeddrzz_i32 -> Fixeddz - | Pfixedudrzz_i32 -> Fixedudz + | Pfixedwrzz | Pfixedwrne -> Fixedw + | Pfixeduwrzz | Pfixeduwrne -> Fixeduw + | Pfixeddrzz | Pfixeddrne -> Fixedd + | Pfixedudrzz| Pfixedudrne -> Fixedud + | Pfixeddrzz_i32 -> Fixedd + | Pfixedudrzz_i32 -> Fixedud let arith_rrr_real = function | Pcompw it -> Compw @@ -643,7 +644,7 @@ let rec_to_usage r = (* TODO: check *) | Srsw | Srsd | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding) | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) - | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau + | Fixeduw | Fixedw | Floatwz | Floatuwz | Fixedd | Fixedud | Floatdz | Floatudz -> mau | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> (match encoding with None | Some U6 | Some S10 -> lsu_auxw | Some U27L5 | Some U27L10 -> lsu_auxw_x @@ -656,8 +657,8 @@ let rec_to_usage r = | Get -> bcu_tiny_tiny_mau_xnop | Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd | Fmind | Fmaxd | Fminw | Fmaxw -> alu_lite - | Fnarrowdw -> alu_full - | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Finvw + | Finvw | Fnarrowdw -> alu_full + | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Ffmad | Ffmaw | Ffmsd | Ffmsw -> mau @@ -681,7 +682,7 @@ let real_inst_to_latency = function | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd | Fmind | Fmaxd | Fminw | Fmaxw -> 1 - | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 + | 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 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3 | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See kvx-Optimization.pdf page 19 *) -- cgit 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(-) 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(-) 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(-) 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(-) 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(-) 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 From 916f120316108f1db9537eccb5151e7b59f82a1f Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 28 Feb 2022 17:20:04 +0100 Subject: new expansion example --- test/gourdinl/postpass_exp.c | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/test/gourdinl/postpass_exp.c b/test/gourdinl/postpass_exp.c index 522ac2a6..bc234091 100644 --- a/test/gourdinl/postpass_exp.c +++ b/test/gourdinl/postpass_exp.c @@ -1,5 +1,11 @@ -int main(int x, int y) { - int z = x << 32; +long foo(int x, char y, long *t) { + int z = x / 4096; + y = x / 256; + t[0] = t[1] * t[2]; + if (x + z < 7) { + if (y < 7) + return 421 + t[0]; + } y = y - z; - return x + y; + return x + y - t[0]; } -- cgit