diff options
-rw-r--r-- | .gitlab-ci.yml | 10 | ||||
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | backend/ValueDomain.v | 156 | ||||
-rw-r--r-- | common/Values.v | 48 | ||||
-rwxr-xr-x | configure | 3 | ||||
-rw-r--r-- | flocq.sh | 2 | ||||
-rw-r--r-- | kvx/Archi.v | 2 | ||||
-rw-r--r-- | kvx/Asm.v | 12 | ||||
-rw-r--r-- | kvx/Asmblockdeps.v | 4 | ||||
-rw-r--r-- | kvx/Asmblockgen.v | 12 | ||||
-rw-r--r-- | kvx/Asmvliw.v | 9 | ||||
-rw-r--r-- | kvx/Builtins1.v | 18 | ||||
-rw-r--r-- | kvx/CBuiltins.ml | 6 | ||||
-rw-r--r-- | kvx/ExtFloats.v | 5 | ||||
-rw-r--r-- | kvx/ExtIEEE754.v | 12 | ||||
-rw-r--r-- | kvx/ExtValues.v | 65 | ||||
-rw-r--r-- | kvx/ExtZ.v | 12 | ||||
-rw-r--r-- | kvx/FPDivision32.v | 613 | ||||
-rw-r--r-- | kvx/NeedOp.v | 2 | ||||
-rw-r--r-- | kvx/Op.v | 30 | ||||
-rw-r--r-- | kvx/PostpassSchedulingOracle.ml | 19 | ||||
-rw-r--r-- | kvx/SelectOp.vp | 8 | ||||
-rw-r--r-- | kvx/SelectOpproof.v | 33 | ||||
-rw-r--r-- | kvx/TargetPrinter.ml | 8 | ||||
-rw-r--r-- | kvx/ValueAOp.v | 4 | ||||
-rw-r--r-- | lib/Floats.v | 18 | ||||
-rw-r--r-- | lib/IEEE754_extra.v | 384 |
27 files changed, 1478 insertions, 19 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c8ccedb8..41df7d8e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -269,16 +269,18 @@ build_kvx: image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace libzip4 + - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace libzip4 bison flex libmpfr-dev libboost-dev + # bison, flex, libmpfr-dev, libboost-dev for gappa - ./.download_from_Kalray.sh - (cd download ; rm -f *dkms*.deb *eclipse*.deb *llvm*.deb *board-mgmt* *oce-host* *pocl* *flash-util* *barebox* *-kann-* *-kaf-* *-stb-* *-opencv* *-eigen* *-task* *-blis* *-lz4*) - sudo dpkg -i download/*.deb - rm -rf download - eval `opam config env` - - opam update - - opam install -y menhir + - opam update && opam pin add coq-flocq 3.4.0 --no-action + - opam install -y menhir gappa coq-gappa coq-flocq script: - - source /opt/kalray/accesscore/kalray.sh && ./config_kvx.sh + - rm -rf flocq + - source /opt/kalray/accesscore/kalray.sh && ./config_kvx.sh --use-external-Flocq - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS" - make -j "$NJOBS" clightgen - source /opt/kalray/accesscore/kalray.sh && make -C test CCOMPOPTS=-static SIMU='kvx-cluster -- ' EXECUTE='kvx-cluster -- ' all test @@ -33,7 +33,7 @@ BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \ export cparser -RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \ +RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver exportclight \ cparser COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d)) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 7a55147b..fcc70ac8 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2269,6 +2269,24 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intofsingle_ne (x: aval) := + match x with + | FS f => + match Float32.to_int_ne f with + | Some i => I i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma intofsingle_ne_sound: + forall v x w, vmatch v x -> Val.intofsingle_ne v = Some w -> vmatch w (intofsingle_ne x). +Proof. + unfold Val.intofsingle_ne; intros. destruct v; try discriminate. + destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition intuofsingle (x: aval) := match x with | FS f => @@ -2287,6 +2305,24 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intuofsingle_ne (x: aval) := + match x with + | FS f => + match Float32.to_intu_ne f with + | Some i => I i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma intuofsingle_ne_sound: + forall v x w, vmatch v x -> Val.intuofsingle_ne v = Some w -> vmatch w (intuofsingle_ne x). +Proof. + unfold Val.intuofsingle_ne; intros. destruct v; try discriminate. + destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition singleofint (x: aval) := match x with | I i => FS(Float32.of_int i) @@ -2349,6 +2385,42 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition longoffloat_ne (x: aval) := + match x with + | F f => + match Float.to_long_ne f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longoffloat_ne_sound: + forall v x w, vmatch v x -> Val.longoffloat_ne v = Some w -> vmatch w (longoffloat_ne x). +Proof. + unfold Val.longoffloat_ne; intros. destruct v; try discriminate. + destruct (Float.to_long_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + +Definition longuoffloat_ne (x: aval) := + match x with + | F f => + match Float.to_longu_ne f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longuoffloat_ne_sound: + forall v x w, vmatch v x -> Val.longuoffloat_ne v = Some w -> vmatch w (longuoffloat_ne x). +Proof. + unfold Val.longuoffloat_ne; intros. destruct v; try discriminate. + destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition floatoflong (x: aval) := match x with | L i => F(Float.of_long i) @@ -2566,6 +2638,46 @@ Definition longuofsingle_total (x: aval) := | _ => ntop1 x end. +Definition intofsingle_ne_total (x: aval) := + match x with + | FS f => + match Float32.to_int_ne f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intuofsingle_ne_total (x: aval) := + match x with + | FS f => + match Float32.to_intu_ne f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longoffloat_ne_total (x: aval) := + match x with + | F f => + match Float.to_long_ne f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longuoffloat_ne_total (x: aval) := + match x with + | F f => + match Float.to_longu_ne f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + Lemma intoffloat_total_sound: forall v x (MATCH : vmatch v x), @@ -2606,6 +2718,26 @@ Proof. all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. Qed. +Lemma intofsingle_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.intofsingle_ne v)) (intofsingle_ne_total x). +Proof. + unfold Val.intofsingle_ne, intofsingle_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + +Lemma intuofsingle_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.intuofsingle_ne v)) (intuofsingle_ne_total x). +Proof. + unfold Val.intofsingle, intofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + Lemma singleofint_total_sound: forall v x, vmatch v x -> vmatch (Val.maketotal (Val.singleofint v)) (singleofint x). @@ -2648,6 +2780,26 @@ Proof. all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. Qed. +Lemma longoffloat_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.longoffloat_ne v)) (longoffloat_ne_total x). +Proof. + unfold Val.longoffloat_ne, longoffloat_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_long_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + +Lemma longuoffloat_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.longuoffloat_ne v)) (longuoffloat_ne_total x). +Proof. + unfold Val.longoffloat_ne, longoffloat_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + Lemma longofsingle_total_sound: forall v x (MATCH : vmatch v x), @@ -5200,6 +5352,10 @@ Global Hint Resolve cnot_sound symbol_address_sound intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound + intofsingle_ne_sound intuofsingle_ne_sound + longoffloat_ne_sound longuoffloat_ne_sound + intofsingle_ne_total_sound intuofsingle_ne_total_sound + longoffloat_ne_total_sound longuoffloat_ne_total_sound longofwords_sound loword_sound hiword_sound intoffloat_total_sound intuoffloat_total_sound diff --git a/common/Values.v b/common/Values.v index 87ebea00..cf5a1255 100644 --- a/common/Values.v +++ b/common/Values.v @@ -244,6 +244,18 @@ Definition intuoffloat (v: val) : option val := | _ => None end. +Definition intoffloat_ne (v: val) : option val := + match v with + | Vfloat f => option_map Vint (Float.to_int_ne f) + | _ => None + end. + +Definition intuoffloat_ne (v: val) : option val := + match v with + | Vfloat f => option_map Vint (Float.to_intu_ne f) + | _ => None + end. + Definition floatofint (v: val) : option val := match v with | Vint n => Some (Vfloat (Float.of_int n)) @@ -268,6 +280,18 @@ Definition intuofsingle (v: val) : option val := | _ => None end. +Definition intofsingle_ne (v: val) : option val := + match v with + | Vsingle f => option_map Vint (Float32.to_int_ne f) + | _ => None + end. + +Definition intuofsingle_ne (v: val) : option val := + match v with + | Vsingle f => option_map Vint (Float32.to_intu_ne f) + | _ => None + end. + Definition singleofint (v: val) : option val := match v with | Vint n => Some (Vsingle (Float32.of_int n)) @@ -623,6 +647,30 @@ Definition longuofsingle (v: val) : option val := | _ => None end. +Definition longoffloat_ne (v: val) : option val := + match v with + | Vfloat f => option_map Vlong (Float.to_long_ne f) + | _ => None + end. + +Definition longuoffloat_ne (v: val) : option val := + match v with + | Vfloat f => option_map Vlong (Float.to_longu_ne f) + | _ => None + end. + +Definition longofsingle_ne (v: val) : option val := + match v with + | Vsingle f => option_map Vlong (Float32.to_long_ne f) + | _ => None + end. + +Definition longuofsingle_ne (v: val) : option val := + match v with + | Vsingle f => option_map Vlong (Float32.to_longu_ne f) + | _ => None + end. + Definition floatoflong (v: val) : option val := match v with | Vlong n => Some (Vfloat (Float.of_long n)) @@ -822,7 +822,8 @@ SIMU=kvx-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ - Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ + Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v\\ + FPDivision32.v ExtValues.v ExtFloats.v\\ AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v EOF fi diff --git a/flocq.sh b/flocq.sh new file mode 100644 index 00000000..64b7534e --- /dev/null +++ b/flocq.sh @@ -0,0 +1,2 @@ +COQINCLUDES="-R /home/monniaux/.opam/4.12.0+flambda/lib/coq/user-contrib/Flocq flocq" +export COQINCLUDES 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. @@ -163,6 +163,8 @@ Inductive instruction : Type := | Pfloatuwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (u32 -> 32) *) | Pfloatudrnsz (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (64 bits) *) | Pfloatdrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (64 bits) *) + + (* round to zero *) | Pfixedwrzz (rd rs: ireg) (**r Integer conversion from floating point *) | Pfixeduwrzz (rd rs: ireg) (**r Integer conversion from floating point (f32 -> 32 bits unsigned *) | Pfixeddrzz (rd rs: ireg) (**r Integer conversion from floating point (i64 -> 64 bits) *) @@ -170,6 +172,12 @@ Inductive instruction : Type := | Pfixedudrzz (rd rs: ireg) (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *) | Pfixedudrzz_i32 (rd rs: ireg) (**r unsigned Integer conversion from floating point (u32 -> 64 bits) *) + (* round to nearest, prefer even numbers *) + | Pfixedwrne (rd rs: ireg) (**r Integer conversion from floating point *) + | Pfixeduwrne (rd rs: ireg) (**r Integer conversion from floating point (f32 -> 32 bits unsigned *) + | Pfixeddrne (rd rs: ireg) (**r Integer conversion from floating point (i64 -> 64 bits) *) + | Pfixedudrne (rd rs: ireg) (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *) + (** Arith RI32 *) | Pmake (rd: ireg) (imm: int) (**r load immediate *) @@ -352,6 +360,10 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmvliw.Pfixedudrzz rd rs => Pfixedudrzz rd rs | PArithRR Asmvliw.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs | PArithRR Asmvliw.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs + | PArithRR Asmvliw.Pfixedwrne rd rs => Pfixedwrne rd rs + | PArithRR Asmvliw.Pfixeduwrne rd rs => Pfixeduwrne rd rs + | PArithRR Asmvliw.Pfixeddrne rd rs => Pfixeddrne rd rs + | PArithRR Asmvliw.Pfixedudrne rd rs => Pfixedudrne rd rs (* RI32 *) | PArithRI32 Asmvliw.Pmake rd imm => Pmake rd imm diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index a9786e0a..ac0b359e 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -1537,6 +1537,10 @@ Definition string_of_name_rr (n: arith_name_rr): pstring := | Pfixedudrzz => "Pfixedudrzz" | Pfixeddrzz_i32 => "Pfixeddrzz_i32" | Pfixedudrzz_i32 => "Pfixedudrzz_i32" + | Pfixedwrne => "Pfixedwrne" + | Pfixeduwrne => "Pfixeduwrne" + | Pfixeddrne => "Pfixeddrne" + | Pfixedudrne => "Pfixedudrne" end. Definition string_of_name_ri32 (n: arith_name_ri32): pstring := diff --git a/kvx/Asmblockgen.v b/kvx/Asmblockgen.v index ab827b1c..a8f1a045 100644 --- a/kvx/Asmblockgen.v +++ b/kvx/Asmblockgen.v @@ -799,6 +799,12 @@ Definition transl_op | Ointuofsingle, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixeduwrzz rd rs ::i k) + | Ointofsingle_ne, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedwrne rd rs ::i k) + | Ointuofsingle_ne, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeduwrne rd rs ::i k) | Olongoffloat, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixeddrzz rd rs ::i k) @@ -811,6 +817,12 @@ Definition transl_op | Olonguoffloat, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixedudrzz rd rs ::i k) + | Olongoffloat_ne, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeddrne rd rs ::i k) + | Olonguoffloat_ne, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedudrne rd rs ::i k) | Ofloatofsingle, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index 45b230e6..6d60445a 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -402,7 +402,10 @@ Inductive arith_name_rr : Type := | Pfixedudrzz (**r Integer conversion from floating point (float -> unsigned long) *) | Pfixeddrzz_i32 (**r Integer conversion from floating point (float -> int) *) | Pfixedudrzz_i32 (**r Integer conversion from floating point (float -> unsigned int) *) -. + | Pfixedwrne (**r Integer conversion from floating point *) + | Pfixeduwrne (**r Integer conversion from floating point (f32 -> 32 bits unsigned *) + | Pfixeddrne (**r Integer conversion from floating point (i64 -> 64 bits) *) + | Pfixedudrne. (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *) Inductive arith_name_ri32 : Type := | Pmake (**r load immediate *) @@ -955,6 +958,10 @@ Definition arith_eval_rr n v := | Pfixedudrzz => Val.maketotal (Val.longuoffloat v) | Pfixeddrzz_i32 => Val.maketotal (Val.intoffloat v) | Pfixedudrzz_i32 => Val.maketotal (Val.intuoffloat v) + | Pfixedudrne => Val.maketotal (Val.longuoffloat_ne v) + | Pfixeddrne => Val.maketotal (Val.longoffloat_ne v) + | Pfixeduwrne => Val.maketotal (Val.intuofsingle_ne v) + | Pfixedwrne => Val.maketotal (Val.intofsingle_ne v) end. Definition arith_eval_ri32 n i := diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index 441345bf..163dcbd8 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -25,7 +25,10 @@ Inductive platform_builtin : Type := | BI_fminf | BI_fmaxf | BI_fma -| BI_fmaf. +| BI_fmaf +| BI_lround_ne +| BI_luround_ne +| BI_fp_udiv32. Local Open Scope string_scope. @@ -36,6 +39,9 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmaxf", BI_fmaxf) :: ("__builtin_fma", BI_fma) :: ("__builtin_fmaf", BI_fmaf) + :: ("__builtin_lround_ne", BI_lround_ne) + :: ("__builtin_luround_ne", BI_luround_ne) + :: ("__builtin_fp_udiv32", BI_fp_udiv32) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -48,6 +54,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_lround_ne | BI_luround_ne => + mksignature (Tfloat :: nil) Tlong cc_default + | BI_fp_udiv32 => + mksignature (Tint :: Tint :: nil) Tint cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -58,4 +68,10 @@ 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_lround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_long_ne + | BI_luround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_longu_ne + | BI_fp_udiv32 => mkbuiltin_n2p Tint Tint Tint + (fun n1 n2 => if Int.eq n2 Int.zero + then None + else Some (Int.divu n1 n2)) end. diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml index 7398e0f4..fad86d3c 100644 --- a/kvx/CBuiltins.ml +++ b/kvx/CBuiltins.ml @@ -133,6 +133,12 @@ let builtins = { "__builtin_fmaf", (TFloat(FFloat, []), [TFloat(FFloat, []); TFloat(FFloat, []); TFloat(FFloat, [])], false); + "__builtin_lround_ne", + (TInt(ILong, []), [TFloat(FDouble, [])], false); + "__builtin_luround_ne", + (TInt(IULong, []), [TFloat(FDouble, [])], false); + "__builtin_fp_udiv32", + (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); ] } diff --git a/kvx/ExtFloats.v b/kvx/ExtFloats.v index b08503a5..332d3e3d 100644 --- a/kvx/ExtFloats.v +++ b/kvx/ExtFloats.v @@ -13,6 +13,8 @@ (* *) (* *************************************************************) +From Flocq Require Import Core Digits Operations Round Bracket Sterbenz + Binary Round_odd. Require Import Floats Integers ZArith. Module ExtFloat. @@ -30,6 +32,8 @@ Definition max (x : float) (y : float) : float := | Some Eq | Some Gt => x | Some Lt | None => y end. + +Definition one := Float.of_int (Int.repr (1%Z)). End ExtFloat. Module ExtFloat32. @@ -50,5 +54,4 @@ Definition max (x : float32) (y : float32) : float32 := Definition one := Float32.of_int (Int.repr (1%Z)). Definition inv (x : float32) : float32 := Float32.div one x. - End ExtFloat32. diff --git a/kvx/ExtIEEE754.v b/kvx/ExtIEEE754.v new file mode 100644 index 00000000..095fd0cc --- /dev/null +++ b/kvx/ExtIEEE754.v @@ -0,0 +1,12 @@ +Require Import Coq.ZArith.Zdiv. + +Open Scope Z. + +Definition Zdiv_ne (a b : Z) := + let q := Z.div a b in + let q1 := Z.succ q in + match Z.compare (a-b*q) (b*q1-a) with + | Lt => q + | Gt => q1 + | Eq => (if Z.even q then q else q1) + end. diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index b4e14898..c478f70b 100644 --- a/kvx/ExtValues.v +++ b/kvx/ExtValues.v @@ -754,3 +754,68 @@ 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). + +From Flocq Require Import Core Digits Operations Round Bracket Sterbenz + Binary Round_odd. +Require Import IEEE754_extra Zdiv Psatz Floats ExtFloats. + +Definition div_approx_reals (a b : Z) (x : R) := + let q:=ZnearestE x in + let r:=a-q*b in + if r <? 0 + then q-1 + else q. + +Lemma floor_ball1: + forall x : R, forall y : Z, + (Rabs (x - IZR y) < 1)%R -> Zfloor x = (y-1)%Z \/ Zfloor x = y. +Proof. + intros x y BALL. + apply Rabs_lt_inv in BALL. + case (Rcompare_spec x (IZR y)); intro CMP. + - left. apply Zfloor_imp. + ring_simplify (y-1+1). + rewrite minus_IZR. lra. + - subst. + rewrite Zfloor_IZR. right. reflexivity. + - right. apply Zfloor_imp. + rewrite plus_IZR. lra. +Qed. + +Theorem div_approx_reals_correct: + forall a b : Z, forall x : R, + b > 0 -> + (Rabs (x - IZR a/ IZR b) < 1/2)%R -> + div_approx_reals a b x = (a/b)%Z. +Proof. + intros a b x bPOS GAP. + assert (0 < IZR b)%R by (apply IZR_lt ; lia). + unfold div_approx_reals. + pose proof (Znearest_imp2 (fun x => negb (Z.even x)) x) as NEAR. + assert (Rabs (IZR (ZnearestE x) - IZR a/ IZR b) < 1)%R as BALL. + { pose proof (Rabs_triang (IZR (ZnearestE x) - x) + (x - IZR a/ IZR b)) as TRI. + ring_simplify (IZR (ZnearestE x) - x + (x - IZR a / IZR b))%R in TRI. + lra. + } + clear GAP NEAR. + rewrite Rabs_minus_sym in BALL. + pose proof (floor_ball1 _ _ BALL) as FLOOR. + clear BALL. + rewrite Zfloor_div in FLOOR by lia. + pose proof (Z_div_mod_eq_full a b) as DIV_MOD. + assert (0 < b) as bPOS' by lia. + pose proof (Z.mod_pos_bound a b bPOS') as MOD_BOUNDS. + case Z.ltb_spec; intro; destruct FLOOR; lia. +Qed. + +Definition my_div (a b : val) := + let b_d := Val.maketotal (Val.floatofintu b) in + let invb_d := Val.floatofsingle (invfs (Val.maketotal (Val.singleofintu b))) in + let alpha := fmsubf (Vfloat ExtFloat.one) invb_d b_d in + let x := fmaddf invb_d alpha invb_d in + Val.mulf (Val.maketotal (Val.floatofintu a)) x. + +(* +Compute (my_div (Vint (Int.repr 3)) (Vint (Int.repr 5))). +*) diff --git a/kvx/ExtZ.v b/kvx/ExtZ.v new file mode 100644 index 00000000..095fd0cc --- /dev/null +++ b/kvx/ExtZ.v @@ -0,0 +1,12 @@ +Require Import Coq.ZArith.Zdiv. + +Open Scope Z. + +Definition Zdiv_ne (a b : Z) := + let q := Z.div a b in + let q1 := Z.succ q in + match Z.compare (a-b*q) (b*q1-a) with + | Lt => q + | Gt => q1 + | Eq => (if Z.even q then q else q1) + end. diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v new file mode 100644 index 00000000..7c37c619 --- /dev/null +++ b/kvx/FPDivision32.v @@ -0,0 +1,613 @@ +From Flocq Require Import Core Digits Operations Round Bracket Sterbenz + Binary Round_odd Bits. +Require Archi. +Require Import Coqlib. +Require Import Compopts. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Op. +Require Import CminorSel. +Require Import OpHelpers. +Require Import ExtFloats. +Require Import DecBoolOps. +Require Import Chunks. +Require Import Builtins. +Require Import Values Globalenvs. +Require Compopts. +Require Import Psatz. +Require Import IEEE754_extra. + +From Gappa Require Import Gappa_tactic. + +Local Open Scope cminorsel_scope. + +Local Open Scope string_scope. +Local Open Scope error_monad_scope. + +Definition approx_inv b := + let invb_s := Eop Oinvfs ((Eop Osingleofintu ((Eletvar 0%nat):::Enil)):::Enil) in + let invb_d := Eop Ofloatofsingle (invb_s ::: Enil) in + let b_d := Eop Ofloatoflongu ((Eop Ocast32unsigned ((Eletvar 1%nat):::Enil)):::Enil) in + let invb_d_var := Eletvar (0%nat) in + let one := Eop (Ofloatconst ExtFloat.one) Enil in + let alpha := Eop Ofmsubf (one ::: invb_d_var ::: b_d ::: Enil) in + let x := Eop Ofmaddf (invb_d_var ::: alpha ::: invb_d_var ::: Enil) in + Elet b (Elet invb_d x). + +Definition approx_inv_thresh := (1/17179869184)%R. + +(* +Lemma BofZ_exact_zero: + forall (prec emax : Z) (prec_gt_0_ : Prec_gt_0 prec) + (Hmax : (prec < emax)%Z), + B2R (BofZ prec emax 0%Z (Hmax := Hmax)) = 0%R /\ + is_finite (BofZ prec emax 0%Z (Hmax := Hmax)) = true /\ + Bsign prec emax (BofZ prec emax 0%Z (Hmax := Hmax)) = false. +Proof. + intros. + apply BofZ_exact. + pose proof (Z.pow_nonneg 2 prec). + lia. +Qed. + *) + +Lemma Rabs_relax: + forall b b' (INEQ : (b < b')%R) x, + (-b <= x <= b)%R -> (Rabs x < b')%R. +Proof. + intros. + apply Rabs_lt. + lra. +Qed. + +Theorem approx_inv_correct : + forall (ge : genv) (sp: val) cmenv memenv + (le : letenv) (expr_b : expr) (b : int) + (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b)) + (b_nz : ((Int.unsigned b) > 0)%Z), + exists f : float, + eval_expr ge sp cmenv memenv le (approx_inv expr_b) (Vfloat f) /\ + is_finite _ _ f = true /\ (Rabs((B2R _ _ f) - (1 / IZR (Int.unsigned b))) <= approx_inv_thresh)%R. +Proof. + intros. unfold approx_inv. + econstructor. constructor. + { repeat econstructor. + { eassumption. } + { reflexivity. } } + set (invb_d := (Float.of_single (ExtFloat32.inv (Float32.of_intu b)))). + set (b' := Int.unsigned b) in *. + pose proof (Int.unsigned_range b) as RANGE. + fold b' in RANGE. + change Int.modulus with 4294967296%Z in RANGE. + assert (0 <= b' <= Int64.max_unsigned)%Z as b'RANGE. + { change Int64.max_unsigned with 18446744073709551615%Z. + lia. } + assert (1 <= IZR b' <= 4294967295)%R as RANGE'. + { split. + { apply IZR_le. lia. } + apply IZR_le. lia. + } + cbn. + + set (b_d := (Float.of_longu (Int64.repr b'))) in *. + Local Transparent Float.of_longu. + unfold Float.of_longu in b_d. + + assert(SILLY : (- 2 ^ 24 <= 1 <= 2 ^ 24)%Z) by lia. + destruct (BofZ_exact 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1 SILLY) as (C0E & C0F & _). + clear SILLY. + + assert(SILLY : (- 2 ^ 53 <= 1 <= 2 ^ 53)%Z) by lia. + destruct (BofZ_exact 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1 SILLY) as (C9E & C9F & _). + clear SILLY. + + pose proof (BofZ_correct 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') as C1. + rewrite Rlt_bool_true in C1; cycle 1. + { clear C1. cbn. + eapply (Rabs_relax (IZR 4294967296)). + lra. + gappa. + } + rewrite Zlt_bool_false in C1 by lia. + destruct C1 as (C1E & C1F & _). + + Local Transparent Float32.of_intu Float32.of_int Float32.div. + unfold ExtFloat32.inv, ExtFloat32.one, Float32.of_intu, Float32.of_int, Float32.div in invb_d. + fold b' in invb_d. + change (Int.signed (Int.repr 1%Z)) with 1%Z in invb_d. + pose proof (Bdiv_correct 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float32.binop_nan mode_NE + (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1) + (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b')) as C2. + rewrite Rlt_bool_true in C2; cycle 1. + { clear C2. rewrite C1E. + apply (Rabs_relax (bpow radix2 10)). + { cbn; lra. } + unfold F2R. cbn. unfold F2R. cbn. + gappa. + } + assert (B2R 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') <> 0%R) as NONZ. + { clear C2. + rewrite C1E. + cbn. + assert (1 <= round radix2 (FLT_exp (-149) 24) ZnearestE (IZR b'))%R by gappa. + lra. + } + destruct (C2 NONZ) as (C2E & C2F & _). + clear C2 NONZ. + Local Transparent Float.of_single. + unfold Float.of_single in invb_d. + pose proof (Bconv_correct 24 128 53 1024 (@eq_refl Datatypes.comparison Lt) + (@eq_refl Datatypes.comparison Lt) Float.of_single_nan mode_NE + (Bdiv 24 128 (@eq_refl Datatypes.comparison Lt) + (@eq_refl Datatypes.comparison Lt) Float32.binop_nan mode_NE + (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) + (@eq_refl Datatypes.comparison Lt) 1) + (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) + (@eq_refl Datatypes.comparison Lt) b'))) as C3. + fold invb_d in C3. + rewrite Rlt_bool_true in C3; cycle 1. + { clear C3. + rewrite C2E. + rewrite C1E. + rewrite C0E. + apply (Rabs_relax (bpow radix2 10)). + { apply bpow_lt; lia. } + cbn. + gappa. + } + change (is_finite 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1)) with true in C2F. + destruct (C3 C2F) as (C3E & C3F & _). + clear C3. + unfold Float.fma. + assert (is_finite _ _ (Float.neg invb_d) = true) as invb_d_F. + { Local Transparent Float.neg. + unfold Float.neg. + rewrite is_finite_Bopp. + assumption. + } + + assert(SILLY : (- 2 ^ 53 <= b' <= 2 ^ 53)%Z) by lia. + destruct (BofZ_exact 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b' SILLY) as (C4E & C4F & _). + clear SILLY. + + assert (is_finite 53 1024 b_d = true) as b_d_F. + { unfold b_d. + rewrite Int64.unsigned_repr by lia. + assumption. + } + + assert (is_finite 53 1024 ExtFloat.one = true) as one_F by reflexivity. + + pose proof (Bfma_correct 53 1024 (@eq_refl Datatypes.comparison Lt) + (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE + (Float.neg invb_d) b_d ExtFloat.one invb_d_F b_d_F one_F) as C5. + + rewrite Rlt_bool_true in C5; cycle 1. + { clear C5. + unfold Float.neg. + rewrite B2R_Bopp. + rewrite C3E. + rewrite C2E. + rewrite C0E. + rewrite C1E. + unfold ExtFloat.one. + change (Float.of_int (Int.repr 1)) with (BofZ 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1). + rewrite C9E. + unfold b_d. + rewrite Int64.unsigned_repr by lia. + rewrite C4E. + apply (Rabs_relax (bpow radix2 10)). + { apply bpow_lt; lia. } + cbn. + gappa. + } + destruct C5 as (C5E & C5F & _). + + pose proof (Bfma_correct 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE + (Bfma 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE + (Float.neg invb_d) b_d ExtFloat.one) invb_d invb_d C5F C3F C3F) as C6. + rewrite Rlt_bool_true in C6; cycle 1. + { clear C6. + rewrite C3E. + rewrite C2E. + rewrite C1E. + rewrite C0E. + rewrite C5E. + unfold Float.neg. + rewrite B2R_Bopp. + rewrite C3E. + rewrite C2E. + rewrite C0E. + rewrite C1E. + unfold b_d. + rewrite Int64.unsigned_repr by lia. + rewrite C4E. + unfold ExtFloat.one. + change (Float.of_int (Int.repr 1)) with (BofZ 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1). + rewrite C9E. + apply (Rabs_relax (bpow radix2 10)). + { apply bpow_lt; lia. } + cbn. + gappa. + } + destruct C6 as (C6E & C6F & _). + split. + { exact C6F. } + rewrite C6E. + rewrite C5E. + rewrite C3E. + rewrite C2E. + rewrite C1E. + rewrite C0E. + unfold Float.neg. + rewrite B2R_Bopp. + unfold ExtFloat.one. + Local Transparent Float.of_int. + unfold Float.of_int. + rewrite (Int.signed_repr 1) by (cbn ; lia). + rewrite C9E. + rewrite C3E. + rewrite C2E. + rewrite C0E. + rewrite C1E. + unfold b_d. + rewrite Int64.unsigned_repr by lia. + rewrite C4E. + cbn. + set (rd := round radix2 (FLT_exp (-1074) 53) ZnearestE) in *. + set (rs := round radix2 (FLT_exp (-149) 24) ZnearestE) in *. + set (bi := IZR b') in *. + set (invb0 := rd (rs (1/ rs bi))%R) in *. + set (alpha := (- invb0 * bi + 1)%R) in *. + set (alpha' := ((1/bi - rd (rs (1/ rs bi)))/(1/bi))%R) in *. + assert (alpha = alpha')%R as expand_alpha. + { + unfold alpha, alpha', invb0. + field. + lra. + } + assert(-1/2097152 <= alpha' <= 1/2097152)%R as alpha_BOUND. + { unfold alpha', rd, rs. + gappa. + } + set (delta := (rd (rd alpha * invb0 + invb0) - (alpha * invb0 + invb0))%R). + assert(-1/1125899906842624 <= delta <= 1/1125899906842624)%R as delta_BOUND. + { unfold delta, invb0. rewrite expand_alpha. unfold rd, rs. + gappa. + } + replace (rd (rd alpha * invb0 + invb0) - 1/bi)%R with + (delta + ((alpha * invb0 + invb0)-1/bi))%R by (unfold delta; ring). + replace (alpha * invb0 + invb0 - 1 / bi)%R with (alpha * (invb0 - 1/bi) + (alpha * (1/bi) + invb0 - 1 / bi))%R by ring. + replace (alpha * (1 / bi) + invb0 - 1 / bi)%R with 0%R; cycle 1. + { unfold alpha. + field. + lra. + } + rewrite expand_alpha. + unfold invb0, rd, rs, approx_inv_thresh. + apply Rabs_le. + gappa. +Qed. + +Definition fp_divu32 a b := + let a_var := Eletvar (1%nat) in + let b_var := Eletvar (0%nat) in + let a_d := Eop Ofloatoflongu ((Eop Ocast32unsigned (a_var ::: Enil)) ::: Enil) in + let qr := Eop Olonguoffloat_ne ((Eop Omulf (a_d:::(approx_inv b_var):::Enil)):::Enil) in + let qr_var := Eletvar 0%nat in + let rem := Eop Omsubl ((Eop Ocast32unsigned ((Eletvar (2%nat)):::Enil))::: + qr_var ::: + (Eop Ocast32unsigned ((Eletvar (1%nat)):::Enil)):::Enil) in + let qr_m1 := Eop (Oaddlimm (Int64.repr (-1)%Z)) (qr_var:::Enil) in + let cases := Eop (Osel (Ccompl0 Clt) Tlong) + (qr_m1 ::: qr_var ::: rem ::: Enil) in (* (Elet qr cases) *) + Eop Olowlong ((Elet a (Elet (lift b) (Elet qr cases))) ::: Enil). + +Open Scope Z. + +Definition div_approx_reals (a b : Z) (x : R) := + let q:=ZnearestE x in + let r:=a-q*b in + if r <? 0 + then q-1 + else q. + +Lemma floor_ball1: + forall x : R, forall y : Z, + (Rabs (x - IZR y) < 1)%R -> Zfloor x = (y-1)%Z \/ Zfloor x = y. +Proof. + intros x y BALL. + apply Rabs_lt_inv in BALL. + case (Rcompare_spec x (IZR y)); intro CMP. + - left. apply Zfloor_imp. + ring_simplify (y-1+1). + rewrite minus_IZR. lra. + - subst. + rewrite Zfloor_IZR. right. reflexivity. + - right. apply Zfloor_imp. + rewrite plus_IZR. lra. +Qed. + +Theorem div_approx_reals_correct: + forall a b : Z, forall x : R, + b > 0 -> + (Rabs (x - IZR a/ IZR b) < 1/2)%R -> + div_approx_reals a b x = (a/b)%Z. +Proof. + intros a b x bPOS GAP. + assert (0 < IZR b)%R by (apply IZR_lt ; lia). + unfold div_approx_reals. + pose proof (Znearest_imp2 (fun x => negb (Z.even x)) x) as NEAR. + assert (Rabs (IZR (ZnearestE x) - IZR a/ IZR b) < 1)%R as BALL. + { pose proof (Rabs_triang (IZR (ZnearestE x) - x) + (x - IZR a/ IZR b)) as TRI. + ring_simplify (IZR (ZnearestE x) - x + (x - IZR a / IZR b))%R in TRI. + lra. + } + clear GAP NEAR. + rewrite Rabs_minus_sym in BALL. + pose proof (floor_ball1 _ _ BALL) as FLOOR. + clear BALL. + rewrite Zfloor_div in FLOOR by lia. + pose proof (Z_div_mod_eq_full a b) as DIV_MOD. + assert (0 < b) as bPOS' by lia. + pose proof (Z.mod_pos_bound a b bPOS') as MOD_BOUNDS. + case Z.ltb_spec; intro; destruct FLOOR; lia. +Qed. + +Opaque approx_inv. + +Theorem Znearest_le + : forall choice (x y : R), (x <= y)%R -> Znearest choice x <= Znearest choice y. +Proof. + intros. + destruct (Z_le_gt_dec (Znearest choice x) (Znearest choice y)) as [LE | GT]. + assumption. + exfalso. + assert (1 <= IZR (Znearest choice x) - IZR(Znearest choice y))%R as GAP. + { rewrite <- minus_IZR. + apply IZR_le. + lia. + } + pose proof (Znearest_imp2 choice x) as Rx. + pose proof (Znearest_imp2 choice y) as Ry. + apply Rabs_def2b in Rx. + apply Rabs_def2b in Ry. + assert (x = y) by lra. + subst y. + lia. +Qed. + +Theorem fp_divu32_correct : + forall (ge : genv) (sp: val) cmenv memenv + (le : letenv) (expr_a expr_b : expr) (a b : int) + (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vint a)) + (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b)) + (b_nz : (Int.unsigned b > 0)%Z), + eval_expr ge sp cmenv memenv le (fp_divu32 expr_a expr_b) + (Vint (Int.divu a b)). +Proof. + intros. + assert (eval_expr ge sp cmenv memenv (Vint b :: Vint a :: le) + (Eletvar 0) (Vint b)) as EVAL_b'. + { constructor. reflexivity. } + destruct (approx_inv_correct ge sp cmenv memenv (Vint b :: Vint a :: le) (Eletvar 0) b EVAL_b' b_nz) as (inv_b & inv_b_eval & inv_b_finite & inv_b_correct). + unfold fp_divu32. + repeat econstructor. + { exact EVAL_a. } + { apply eval_lift. exact EVAL_b. } + exact inv_b_eval. + cbn. f_equal. + rewrite <- Float.of_intu_of_longu. + unfold Float.to_longu_ne. + rewrite ZofB_ne_range_correct by lia. + set (prod := (Float.mul (Float.of_intu a) inv_b)). + pose proof (Int.unsigned_range a) as a_range. + pose proof (Int.unsigned_range b) as b_range. + change Int.modulus with 4294967296 in a_range. + change Int.modulus with 4294967296 in b_range. + set (prod' := (B2R _ _ prod)). + set (prod_r := ZnearestE prod') in *. + + Local Transparent Float.mul Float.of_intu. + unfold Float.mul, Float.of_intu in prod. + set (a' := Int.unsigned a) in *. + set (b' := Int.unsigned b) in *. + assert (IZR_a' : (0 <= IZR a' <= 4294967295)%R). + { split; apply IZR_le; lia. } + assert (IZR_b' : (1 <= IZR b' <= 4294967295)%R). + { split; apply IZR_le; lia. } + assert (SILLY : -2^53 <= a' <= 2^53). + { cbn; lia. } + destruct (BofZ_exact 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) a' SILLY) as (C0E & C0F & _). + clear SILLY. + pose proof (Bmult_correct 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_nan mode_NE + (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt)a') inv_b) as C1. + set (inv_b_r := B2R 53 1024 inv_b) in *. + assert (INV_RANGE : (1/4294967296 <= 1/IZR b' <= 1)%R). + { split; unfold Rdiv. + - apply Rmult_le_compat_l. lra. + apply Rinv_le. apply IZR_lt. lia. + apply IZR_le. lia. + - replace 1%R with (1 / 1)%R at 2 by field. + apply Rmult_le_compat_l. lra. + apply Rinv_le. apply IZR_lt. lia. + apply IZR_le. lia. + } + apply Rabs_def2b in inv_b_correct. + rewrite Rlt_bool_true in C1; cycle 1. + { clear C1. + rewrite C0E. + apply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. lia. } + replace inv_b_r with (1 / IZR b' + (inv_b_r - 1 / IZR b'))%R by ring. + set (delta := (inv_b_r - 1 / IZR b')%R) in *. + unfold approx_inv_thresh in inv_b_correct. + cbn. + assert (b'_RANGE : (1 <= IZR b' <= 4294967295)%R). + { split; apply IZR_le; lia. + } + assert (a'_RANGE : (0 <= IZR a' <= 4294967295)%R). + { split; apply IZR_le; lia. + } + gappa. + } + rewrite C0F in C1. + cbn in C1. + rewrite C0E in C1. + rewrite inv_b_finite in C1. + fold prod in C1. + fold prod' in C1. + destruct C1 as (C1E & C1F & _). + rewrite C1F. cbn. + + assert(prod'_range : (0 <= prod' <= 17179869181/4)%R). + { + rewrite C1E. + replace inv_b_r with (1/IZR b' + (inv_b_r - 1 / IZR b'))%R by ring. + assert (a'_RANGE : (0 <= IZR a' <= 4294967295)%R). + { split; apply IZR_le; lia. + } + unfold approx_inv_thresh in inv_b_correct. + set (true_inv := (1 / IZR b')%R) in *. + set (delta := (inv_b_r - true_inv)%R) in *. + gappa. + } + + assert(0 <= prod_r <= 4294967295) as prod_r_range. + { unfold prod_r. + rewrite <- (Znearest_IZR (fun x => negb (Z.even x)) 0). + replace 4294967295 with (ZnearestE (17179869181 / 4)%R); cycle 1. + { apply Znearest_imp. + apply Rabs_lt. + lra. + } + split; apply Znearest_le; lra. + } + + replace (_ && _ ) with true; cycle 1. + { + symmetry. + rewrite andb_true_iff. + split; apply Zle_imp_le_bool; lia. + } + cbn. + f_equal. + unfold Int.divu. + assert(Rabs + (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - (IZR a' * inv_b_r)) <= 1/512)%R as R1 by gappa. + + assert ( (Rabs (B2R 53 1024 prod - IZR (Int.unsigned a) / IZR (Int.unsigned b)) < 1 / 2)%R) as NEAR. + { + unfold prod. + pose proof (Bmult_correct 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_nan mode_NE (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) a') inv_b) as C2. + rewrite C0E in C2. + rewrite Rlt_bool_true in C2; cycle 1. + { clear C2. + apply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. reflexivity. } + cbn. + fold inv_b_r. + replace inv_b_r with (1 / IZR b' + (inv_b_r - 1 / IZR b'))%R by ring. + set (delta := (inv_b_r - 1 / IZR b')%R) in *. + unfold approx_inv_thresh in *. + gappa. + } + destruct C2 as (C2E & C2F & _). + rewrite C2E. + fold inv_b_r a' b'. + replace ((round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (IZR a' * inv_b_r)) - + (IZR a' / IZR b'))%R with + (((round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (IZR a' * inv_b_r)) - + (IZR a' * inv_b_r)) + + (IZR a' * (inv_b_r - 1 / IZR b')))%R by (field ; lra). + set(delta := (inv_b_r - 1 / IZR b')%R) in *. + cbn. + unfold approx_inv_thresh in *. + assert (Rabs(IZR a' * delta) <= 3/8)%R as R2. + { apply Rabs_le. + split; nra. + } + rewrite <- C1E. + rewrite <- C1E in R1. + pose proof (Rabs_triang (prod' - IZR a' * inv_b_r) (IZR a' * delta))%R. + lra. + } + pose proof (div_approx_reals_correct (Int.unsigned a) (Int.unsigned b) prod' b_nz NEAR) as DIV_CORRECT. + rewrite <- DIV_CORRECT. + + unfold div_approx_reals in *. + fold a' b' prod' prod_r. + unfold Int64.mul. + rewrite Int64.unsigned_repr by (cbn; lia). + rewrite Int64.unsigned_repr by (cbn; lia). + unfold Int64.sub. + rewrite Int64.unsigned_repr by (cbn; lia). + rewrite Int64.unsigned_repr by (cbn; nia). + assert (FMA_RANGE : Int64.min_signed <= a' - prod_r * b' <= Int64.max_signed). + { cbn. + unfold prod_r. + rewrite <- C1E in R1. + assert (IZR (-9223372036854775808) <= IZR (a' - ZnearestE prod' * b') <= IZR 9223372036854775807)%R. + 2: split; apply le_IZR; lra. + rewrite minus_IZR. + rewrite mult_IZR. + replace (IZR (ZnearestE prod')) with (prod' + (IZR (ZnearestE prod') - prod'))%R by ring. + pose proof (Znearest_imp2 (fun x => negb (Z.even x)) prod') as R2. + set (delta1 := (IZR (ZnearestE prod') - prod')%R) in *. + replace prod' with ((prod' - IZR a' * inv_b_r) + IZR a' * (inv_b_r - 1 / IZR b') + + IZR a' / IZR b')%R by (field; lra). + set (delta2 := (inv_b_r - 1 / IZR b')%R) in *. + set (delta3 := (prod' - IZR a' * inv_b_r)%R) in *. + replace (IZR a' - (delta3 + IZR a' * delta2 + IZR a' / IZR b' + delta1) * IZR b')%R with + (- (delta3 + IZR a' * delta2 + delta1) * IZR b')%R by (field; lra). + unfold approx_inv_thresh in *. + assert (Rabs(IZR a' * delta2) <= 1/4)%R as R4. + { apply Rabs_le. + split; + nra. } + set (delta4 := (IZR a' * delta2)%R) in *. + apply Rabs_def2b in R1. + apply Rabs_def2b in R2. + apply Rabs_def2b in R4. + split; nra. + } + fold a' b' prod_r in DIV_CORRECT. + + pose proof (Zlt_cases (a' - prod_r * b') 0) as CMP. + destruct (Z.ltb (a' - prod_r * b') 0). + - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with true; cycle 1. + { unfold Int64.lt. + change (Int64.signed Int64.zero) with 0. + rewrite Int64.signed_repr by exact FMA_RANGE. + rewrite zlt_true by lia. + reflexivity. + } + cbn. + f_equal. + rewrite Int64.add_signed. + rewrite (Int64.signed_repr prod_r) by (cbn ; lia). + rewrite Int64.signed_repr by (cbn ; lia). + unfold Int64.loword. + rewrite Int64.unsigned_repr. reflexivity. + split. + 2: cbn; lia. + replace (prod_r + (-1)) with (prod_r - 1) by lia. + rewrite DIV_CORRECT. + apply Z.div_pos; lia. + + - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with false; cycle 1. + { unfold Int64.lt. + change (Int64.signed Int64.zero) with 0. + rewrite Int64.signed_repr by exact FMA_RANGE. + rewrite zlt_false by lia. + reflexivity. + } + cbn. + unfold Int64.loword. + rewrite Int64.unsigned_repr by (cbn; lia). + reflexivity. +Qed. + + diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index 4578b4e8..455af70e 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -131,6 +131,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv) | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) + | Ointofsingle_ne | Ointuofsingle_ne => op1 (default nv) + | Olongoffloat_ne | Olonguoffloat_ne => op1 (default nv) | Ocmp c => needs_of_condition c | Oextfz _ _ | Oextfs _ _ | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv) | Oinsf _ _ | Oinsfl _ _ => op2 (default nv) @@ -209,6 +209,11 @@ Inductive operation : Type := | Olonguofsingle (**r [rd = unsigned_long_of_float32(r1)] *) | Osingleoflong (**r [rd = float32_of_signed_long(r1)] *) | Osingleoflongu (**r [rd = float32_of_unsigned_int(r1)] *) + | Ointofsingle_ne (**r [rd = signed_int_of_float64(r1)] *) + | Ointuofsingle_ne (**r [rd = unsigned_int_of_float64(r1)] *) + | Olongoffloat_ne (**r [rd = signed_long_of_float64(r1)] *) + | Olonguoffloat_ne (**r [rd = unsigned_long_of_float64(r1)] *) + (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) | Oextfz (stop : Z) (start : Z) @@ -466,6 +471,11 @@ Definition eval_operation | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1)) | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1)) | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) + | Ointofsingle_ne, v1::nil => Some (Val.maketotal (Val.intofsingle_ne v1)) + | Ointuofsingle_ne, v1::nil => Some (Val.maketotal (Val.intuofsingle_ne v1)) + | Olongoffloat_ne, v1::nil => Some (Val.maketotal (Val.longoffloat_ne v1)) + | Olonguoffloat_ne, v1::nil => Some (Val.maketotal (Val.longuoffloat_ne v1)) + | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) | (Oextfz stop start), v0::nil => Some (extfz stop start v0) | (Oextfs stop start), v0::nil => Some (extfs stop start v0) @@ -683,6 +693,12 @@ Definition type_of_operation (op: operation) : list typ * typ := | Olonguofsingle => (Tsingle :: nil, Tlong) | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) + + | Ointofsingle_ne => (Tsingle :: nil, Tint) + | Ointuofsingle_ne => (Tsingle :: nil, Tint) + | Olongoffloat_ne => (Tfloat :: nil, Tlong) + | Olonguoffloat_ne => (Tfloat :: nil, Tlong) + | Ocmp c => (type_of_condition c, Tint) | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint) | Oextfzl _ _ | Oextfsl _ _ => (Tlong :: nil, Tlong) @@ -980,6 +996,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* singleoflong, singleoflongu *) - destruct v0; cbn... - destruct v0; cbn... + (* intofsingle_ne, intuofsingle_ne *) + - destruct v0; cbn... destruct (Float32.to_int_ne f); cbn; trivial. + - destruct v0; cbn... destruct (Float32.to_intu_ne f); cbn; trivial. + (* longoffloat_ne, longuoffloat_ne *) + - destruct v0; cbn... destruct (Float.to_long_ne f); cbn; trivial. + - destruct v0; cbn... destruct (Float.to_longu_ne f); cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* extfz *) @@ -1669,6 +1691,14 @@ Proof. (* singleoflong, singleoflongu *) - inv H4; cbn; auto. - inv H4; cbn; auto. + + (* intofsingle_ne, intuofsingle_ne *) + - inv H4; cbn; auto. destruct (Float32.to_int_ne f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float32.to_intu_ne f0); cbn; auto. + (* longoffloat_ne, longuoffloat_ne *) + - inv H4; cbn; auto. destruct (Float.to_long_ne f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float.to_longu_ne f0); cbn; auto. + (* cmp *) - subst v1. destruct (eval_condition cond vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml index 3f4520a6..f53da14b 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 @@ -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 *) diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index 4e1087f9..70941c48 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -742,6 +742,8 @@ Nondetfunction gen_fmaf args := | _ => None end. +Require FPDivision32. + Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := match b with | BI_fmin => Some (Eop Ominf args) @@ -750,6 +752,12 @@ 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_lround_ne => Some (Eop Olongoffloat_ne args) + | BI_luround_ne => Some (Eop Olonguoffloat_ne args) + | BI_fp_udiv32 => (match args with + | a:::b:::Enil => Some (FPDivision32.fp_divu32 a b) + | _ => None + end) end. End SELECT. diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index 0ede1e2d..658bf0b3 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1883,6 +1883,9 @@ Proof. destruct v2; simpl; trivial. Qed. + +Require FPDivision32. + Theorem eval_platform_builtin: forall bf al a vl v le, platform_builtin bf al = Some a -> @@ -1896,6 +1899,36 @@ Proof. repeat (try econstructor; try eassumption)). - apply eval_fma; assumption. - apply eval_fmaf; assumption. + - cbn in *; + destruct vl; trivial. destruct vl; trivial. + destruct v0; try discriminate; + cbn; rewrite H0; reflexivity. + - cbn in *; + destruct vl; trivial. destruct vl; trivial. + destruct v0; try discriminate; + cbn; rewrite H0; reflexivity. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int.eq in EVAL. + change (Int.unsigned Int.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vint (Int.divu i i0)). split. + { + apply FPDivision32.fp_divu32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. Qed. End CMCONSTR. diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml index 9e2e3776..01733858 100644 --- a/kvx/TargetPrinter.ml +++ b/kvx/TargetPrinter.ml @@ -586,6 +586,14 @@ module Target (*: TARGET*) = fprintf oc " fixedd.rz %a = %a, 0\n" ireg rd ireg rs | Pfixedudrzz(rd, rs) | Pfixedudrzz_i32(rd, rs) -> fprintf oc " fixedud.rz %a = %a, 0\n" ireg rd ireg rs + | Pfixedudrne(rd, rs) -> + fprintf oc " fixedud.rn %a = %a, 0\n" ireg rd ireg rs + | Pfixeddrne(rd, rs) -> + fprintf oc " fixedd.rn %a = %a, 0\n" ireg rd ireg rs + | Pfixeduwrne(rd, rs) -> + fprintf oc " fixeduw.rn %a = %a, 0\n" ireg rd ireg rs + | Pfixedwrne(rd, rs) -> + fprintf oc " fixedw.rn %a = %a, 0\n" ireg rd ireg rs (* Arith RI32 instructions *) | Pmake (rd, imm) -> diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index 87554258..4909a25b 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -298,6 +298,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Olonguofsingle, v1::nil => longuofsingle_total v1 | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 + | Ointofsingle_ne, v1::nil => intofsingle_ne_total v1 + | Ointuofsingle_ne, v1::nil => intuofsingle_ne_total v1 + | Olongoffloat_ne, v1::nil => longoffloat_ne_total v1 + | Olonguoffloat_ne, v1::nil => longuoffloat_ne_total v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0 | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0 diff --git a/lib/Floats.v b/lib/Floats.v index 9ee5302d..b12c6585 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -360,6 +360,15 @@ Definition to_long (f:float): option int64 := (**r conversion to signed 64-bit i Definition to_longu (f:float): option int64 := (**r conversion to unsigned 64-bit int *) option_map Int64.repr (ZofB_range _ _ f 0 Int64.max_unsigned). +Definition to_int_ne (f:float): option int := (**r conversion to signed 32-bit int *) + option_map Int.repr (ZofB_ne_range _ _ f Int.min_signed Int.max_signed). +Definition to_intu_ne (f:float): option int := (**r conversion to unsigned 32-bit int *) + option_map Int.repr (ZofB_ne_range _ _ f 0 Int.max_unsigned). +Definition to_long_ne (f:float): option int64 := (**r conversion to signed 64-bit int *) + option_map Int64.repr (ZofB_ne_range _ _ f Int64.min_signed Int64.max_signed). +Definition to_longu_ne (f:float): option int64 := (**r conversion to unsigned 64-bit int *) + option_map Int64.repr (ZofB_ne_range _ _ f 0 Int64.max_unsigned). + Definition of_int (n:int): float := (**r conversion from signed 32-bit int *) BofZ 53 1024 __ __ (Int.signed n). Definition of_intu (n:int): float:= (**r conversion from unsigned 32-bit int *) @@ -1136,6 +1145,15 @@ Definition to_long (f:float32): option int64 := (**r conversion to signed 64-bit Definition to_longu (f:float32): option int64 := (**r conversion to unsigned 64-bit int *) option_map Int64.repr (ZofB_range _ _ f 0 Int64.max_unsigned). +Definition to_int_ne (f:float32): option int := (**r conversion to signed 32-bit int *) + option_map Int.repr (ZofB_ne_range _ _ f Int.min_signed Int.max_signed). +Definition to_intu_ne (f:float32): option int := (**r conversion to unsigned 32-bit int *) + option_map Int.repr (ZofB_ne_range _ _ f 0 Int.max_unsigned). +Definition to_long_ne (f:float32): option int64 := (**r conversion to signed 64-bit int *) + option_map Int64.repr (ZofB_ne_range _ _ f Int64.min_signed Int64.max_signed). +Definition to_longu_ne (f:float32): option int64 := (**r conversion to unsigned 64-bit int *) + option_map Int64.repr (ZofB_ne_range _ _ f 0 Int64.max_unsigned). + Definition of_int (n:int): float32 := (**r conversion from signed 32-bit int to single-precision float *) BofZ 24 128 __ __ (Int.signed n). Definition of_intu (n:int): float32 := (**r conversion from unsigned 32-bit int to single-precision float *) diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index b0d1944e..7e0e7260 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -24,6 +24,8 @@ Require Import Psatz. Require Import Bool. Require Import Eqdep_dec. +Require Import Coq.Logic.FunctionalExtensionality. + Local Open Scope Z_scope. Section Extra_ops. @@ -879,6 +881,388 @@ Proof. unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto. Qed. +(** ZofB_ne : convert float to integer, round to nearest *) + +Definition Zdiv_ne (a b : Z) := + let q := Z.div a b in + let q1 := Z.succ q in + match Z.compare (a-b*q) (b*q1-a) with + | Lt => q + | Gt => q1 + | Eq => (if Z.even q then q else q1) + end. + +Definition ZofB_ne (f: binary_float): option Z := + match f with + | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Z.pow_pos radix2 e)%Z + | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m)) + | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zdiv_ne (Zpos m) (Z.pow_pos radix2 e)))%Z + | B754_zero _ _ _ => Some 0%Z + | _ => None + end. + +Lemma Znearest_IZR : + forall choice n, (Znearest choice (IZR n)) = n. +Proof. + intros. + unfold Znearest. + case Rcompare_spec ; intro ORDER. + - apply Zfloor_IZR. + - destruct choice. + + apply Zceil_IZR. + + apply Zfloor_IZR. + - apply Zceil_IZR. +Qed. + +Lemma ZnearestE_IZR: + forall n, (ZnearestE (IZR n)) = n. +Proof. + apply Znearest_IZR. +Qed. + +Lemma Zfloor_opp : + forall x : R, (Zfloor (- x)) = - (Zceil x). +Proof. + unfold Zceil, Zfloor. + intro x. + rewrite Z.opp_involutive. + reflexivity. +Qed. + +Lemma Zceil_opp : + forall x : R, (Zceil (- x)) = - (Zfloor x). +Proof. + unfold Zceil, Zfloor. + intro x. + rewrite Ropp_involutive. + reflexivity. +Qed. + +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro. + rewrite Znearest_opp. + f_equal. + f_equal. + apply functional_extensionality. + intro. + rewrite Z.even_opp. + fold (Z.succ x0). + rewrite Z.even_succ. + f_equal. + apply Z.negb_odd. +Qed. + +Lemma Zceil_non_floor: + forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + apply Zceil_imp. + split. + { rewrite minus_IZR. + rewrite plus_IZR. + lra. + } + rewrite plus_IZR. + pose proof (Zfloor_ub x). + lra. +Qed. + +(** more complicated way of proving +Lemma Zceil_non_ceil: + forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + cut (Zfloor x = (Zceil x) - 1). { intros; lia. } + apply Zfloor_imp. + split. + { rewrite minus_IZR. + pose proof (Zceil_lb x). + lra. + } + rewrite plus_IZR. + rewrite minus_IZR. + lra. +Qed. + +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro x. + unfold ZnearestE. + case (Rcompare_spec (x - IZR (Zfloor x)) (/ 2)); intro CMP. + - pose proof (Zfloor_lb x) as LB. + destruct (Rcompare_spec x (IZR (Zfloor x))) as [ ABSURD | EXACT | INEXACT]. + lra. + { set (n := Zfloor x) in *. + rewrite EXACT. + rewrite <- opp_IZR. + rewrite Zfloor_IZR. + rewrite opp_IZR. + rewrite Rcompare_Lt by lra. + reflexivity. + } + rewrite Rcompare_Gt. + { apply Zceil_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by assumption. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Eq. + { rewrite Zceil_opp. + rewrite Zfloor_opp. + rewrite Z.even_opp. + rewrite Zceil_non_floor by lra. + rewrite Z.even_succ. + rewrite Z.negb_odd. + destruct (Z.even (Zfloor x)); reflexivity. + } + rewrite Zfloor_opp. + rewrite opp_IZR. + ring_simplify. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Lt. + { apply Zfloor_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. +Qed. + *) + +Ltac field_simplify_den := field_simplify ; [idtac | lra]. +Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra]. + +Hint Rewrite <- plus_IZR minus_IZR opp_IZR mult_IZR : l_IZR. +Ltac l_IZR := autorewrite with l_IZR. + +Theorem ZofB_ne_correct: + forall f, + ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. +Proof. + destruct f as [s|s|s p H|s m e H]; simpl; auto. +- f_equal. symmetry. apply (ZnearestE_IZR 0). +- destruct e; f_equal. + + unfold F2R; cbn. rewrite Rmult_1_r. rewrite ZnearestE_IZR. auto. + + unfold F2R; cbn. rewrite <- mult_IZR. rewrite ZnearestE_IZR. auto. + + unfold F2R; cbn. rewrite IZR_cond_Zopp. rewrite <- cond_Ropp_mult_l. + assert (EQ: forall x, ZnearestE (cond_Ropp s x) = cond_Zopp s (ZnearestE x)). + { intros. destruct s; cbn; auto. apply ZnearestE_opp. } + rewrite EQ. f_equal. + generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros. + set (p2p := (Z.pow_pos 2 p)) in *. + set (zm := Z.pos m) in *. + assert (p2p > 0) as POS by lia. + assert (0 < IZR p2p)%R as POS2. + { apply IZR_lt. assumption. } + unfold Zdiv_ne, Z.succ in *. + case Z.compare_spec; intro CMP. + * pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE. + destruct (Z_mod_lt zm p2p POS) as [MOD1 MOD2]. + set (q := zm / p2p) in *. + set (r := zm mod p2p) in *. + rewrite inbetween_int_NE with (m := q) (l := loc_Inexact Eq). + { cbn. unfold cond_incr. + destruct Z.even; reflexivity. + } + constructor. + split. + ** assert (0 < IZR zm / IZR p2p - IZR q)%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + l_IZR. + apply IZR_lt. + lia. + ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + l_IZR. + apply IZR_lt. + lia. + ** apply Rcompare_Eq. + assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra]. + field_simplify_den. + l_IZR. + replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia. + field. apply IZR_neq. lia. + * symmetry. + apply Znearest_imp with (n := zm / p2p). + apply Rabs_lt. split. + ** pose proof (Z_mult_div_ge zm p2p POS). + assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R. + 2: lra. + field_simplify_den. + apply Rmult_le_pos. + { l_IZR. + apply IZR_le. + lia. + } + assert (0 < / IZR p2p)%R. + 2: lra. + apply Rinv_0_lt_compat. assumption. + ** assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT. + { l_IZR. + apply IZR_lt. + lia. } + assert (0 < -(IZR zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + lra. + * symmetry. + apply Znearest_imp. + apply Rabs_lt. split. + ** assert (0 < (IZR zm - IZR p2p * IZR (zm / p2p)) - (IZR p2p * (IZR (zm / p2p) + 1) - IZR zm))%R. + { ring_simplify. + l_IZR. + apply IZR_lt. + lia. + } + assert (0 < (/ 2) + IZR zm * / IZR p2p - IZR (zm / p2p + 1))%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + rewrite plus_IZR. + lra. + ** assert (0 < IZR (zm / p2p + 1) - (IZR zm * / IZR p2p))%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + l_IZR. + apply IZR_lt. + pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE. + ring_simplify. + set (q := (zm / p2p)) in *. + pose proof (Z_mod_lt zm p2p POS) as MOD. + lia. +Qed. + + +Lemma Znearest_imp2: + forall choice x, (Rabs (IZR (Znearest choice x) - x) <= /2)%R. +Proof. + intros. + unfold Znearest. + pose proof (Zfloor_lb x) as FL. + pose proof (Zceil_ub x) as CU. + pose proof (Zceil_non_floor x) as NF. + case Rcompare_spec; intro CMP; apply Rabs_le; split; try lra. + - destruct choice; lra. + - destruct choice. 2: lra. + rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. + - rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. +Qed. + +Lemma Rabs_le_rev : forall a b, (Rabs a <= b -> -b <= a <= b)%R. +Proof. + intros a b ABS. + unfold Rabs in ABS. + destruct Rcase_abs in ABS; lra. +Qed. + +Theorem ZofB_ne_ball: + forall f n, ZofB_ne f = Some n -> (IZR n-1/2 <= B2R _ _ f <= IZR n+1/2)%R. +Proof. + intros. rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H. + pose proof (Znearest_imp2 (fun x => negb (Z.even x)) (B2R prec emax f)) as ABS. + pose proof (Rabs_le_rev _ _ ABS). + lra. +Qed. + +(* +Theorem ZofB_ne_minus: + forall minus_nan m f p q, + ZofB_ne f = Some p -> 0 <= p < 2*q -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R -> + ZofB_ne (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) = Some (p - q). +Proof. + intros. + assert (Q: -2^prec <= q <= 2^prec). + { split; auto. generalize (Zpower_ge_0 radix2 prec); simpl; lia. } + assert (RANGE: (IZR p -1/2 <= B2R _ _ f <= IZR p + 1/2)%R) by ( apply ZofB_ne_ball; auto ). + rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; try discriminate. + assert (PQ2: (IZR p + 1 <= IZR q * 2)%R). + { l_IZR. apply IZR_le. lia. } + assert (EXACT: round radix2 fexp (round_mode m) (B2R _ _ f - IZR q)%R = (B2R _ _ f - IZR q)%R). + { apply round_generic. apply valid_rnd_round_mode. + apply sterbenz_aux. now apply FLT_exp_valid. apply FLT_exp_monotone. apply generic_format_B2R. + apply integer_representable_n. auto. lra. } + destruct (BofZ_exact q Q) as (A & B & C). + generalize (Bminus_correct _ _ _ Hmax minus_nan m f (BofZ q) FIN B). + rewrite Rlt_bool_true. +- fold emin; fold fexp. intros (D & E & F). + rewrite ZofB_ne_correct. rewrite E. rewrite D. rewrite A. rewrite EXACT. + inversion H. f_equal. + rewrite ! Ztrunc_floor. apply Zfloor_minus. + lra. lra. +- rewrite A. fold emin; fold fexp. rewrite EXACT. + apply Rle_lt_trans with (bpow radix2 prec). + apply Rle_trans with (IZR q). apply Rabs_le. lra. + rewrite <- IZR_Zpower. apply IZR_le; auto. red in prec_gt_0_; lia. + apply bpow_lt. auto. +Qed. + *) + +Definition ZofB_ne_range (f: binary_float) (zmin zmax: Z): option Z := + match ZofB_ne f with + | None => None + | Some z => if Z.leb zmin z && Z.leb z zmax then Some z else None + end. + +Theorem ZofB_ne_range_correct: + forall f min max, + let n := ZnearestE (B2R _ _ f) in + ZofB_ne_range f min max = + if is_finite _ _ f && Z.leb min n && Z.leb n max then Some n else None. +Proof. + intros. unfold ZofB_ne_range. rewrite ZofB_ne_correct. fold n. + destruct (is_finite prec emax f); auto. +Qed. + +Lemma ZofB_ne_range_inversion: + forall f min max n, + ZofB_ne_range f min max = Some n -> + min <= n /\ n <= max /\ ZofB_ne f = Some n. +Proof. + intros. rewrite ZofB_ne_range_correct in H. rewrite ZofB_ne_correct. + destruct (is_finite prec emax f); try discriminate. + set (n1 := ZnearestE (B2R _ _ f)) in *. + destruct (min <=? n1) eqn:MIN; try discriminate. + destruct (n1 <=? max) eqn:MAX; try discriminate. + simpl in H. inversion H. subst n. + split. apply Zle_bool_imp_le; auto. + split. apply Zle_bool_imp_le; auto. + auto. +Qed. + + +(* +Theorem ZofB_ne_range_minus: + forall minus_nan m f p q, + ZofB_ne_range f 0 (2 * q - 1) = Some p -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R -> + ZofB_ne_range (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) (-q) (q - 1) = Some (p - q). +Proof. + intros. destruct (ZofB_ne_range_inversion _ _ _ _ H) as (A & B & C). + set (f' := Bminus prec emax prec_gt_0_ Hmax minus_nan m f (BofZ q)). + assert (D: ZofB_ne f' = Some (p - q)). + { apply ZofB_ne_minus. auto. lia. auto. auto. } + unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto. +Qed. + *) + (** ** Algebraic identities *) (** Commutativity of addition and multiplication *) |