From 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Mon, 16 Jul 2018 13:30:37 +0200 Subject: Add tests for primitive floats Add utility ldexp and frexp functions to prevent dealing with the shift of ldshiftexp and frshiftexp everywhere. Also move primitive integer tests to place all primitive tests in the same directory. --- test-suite/primitive/float/valid_binary_conv.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 test-suite/primitive/float/valid_binary_conv.v (limited to 'test-suite/primitive/float/valid_binary_conv.v') diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v new file mode 100644 index 0000000000..ad81e55667 --- /dev/null +++ b/test-suite/primitive/float/valid_binary_conv.v @@ -0,0 +1,20 @@ +Require Import ZArith Floats. + +Definition two := Eval compute in (one + one)%float. +Definition half := Eval compute in (one / two)%float. +Definition huge := Eval compute in ldexp one (1023)%Z. +Definition tiny := Eval compute in ldexp one (-1022)%Z. +Definition denorm := Eval compute in ldexp one (-1074)%Z. + +Check (eq_refl : valid_binary (Prim2SF zero) = true). +Check (eq_refl : valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl : valid_binary (Prim2SF one) = true). +Check (eq_refl : valid_binary (Prim2SF (-one)) = true). +Check (eq_refl : valid_binary (Prim2SF infinity) = true). +Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl : valid_binary (Prim2SF huge) = true). +Check (eq_refl : valid_binary (Prim2SF tiny) = true). +Check (eq_refl : valid_binary (Prim2SF denorm) = true). +Check (eq_refl : valid_binary (Prim2SF nan) = true). +Check (eq_refl : valid_binary (Prim2SF two) = true). +Check (eq_refl : valid_binary (Prim2SF half) = true). -- cgit v1.2.3 From 55d32c9f3a91058f69f34c17c17701d0dc81874d Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Thu, 19 Jul 2018 13:33:17 +0200 Subject: Add tests for primitive floats with 'vm_compute' Tests are updated to include VM computations and check for double rounding. --- test-suite/primitive/float/valid_binary_conv.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'test-suite/primitive/float/valid_binary_conv.v') diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v index ad81e55667..53fad1a74c 100644 --- a/test-suite/primitive/float/valid_binary_conv.v +++ b/test-suite/primitive/float/valid_binary_conv.v @@ -18,3 +18,16 @@ Check (eq_refl : valid_binary (Prim2SF denorm) = true). Check (eq_refl : valid_binary (Prim2SF nan) = true). Check (eq_refl : valid_binary (Prim2SF two) = true). Check (eq_refl : valid_binary (Prim2SF half) = true). + +Check (eq_refl true <: valid_binary (Prim2SF zero) = true). +Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl true <: valid_binary (Prim2SF one) = true). +Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true). +Check (eq_refl true <: valid_binary (Prim2SF infinity) = true). +Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl true <: valid_binary (Prim2SF huge) = true). +Check (eq_refl true <: valid_binary (Prim2SF tiny) = true). +Check (eq_refl true <: valid_binary (Prim2SF denorm) = true). +Check (eq_refl true <: valid_binary (Prim2SF nan) = true). +Check (eq_refl true <: valid_binary (Prim2SF two) = true). +Check (eq_refl true <: valid_binary (Prim2SF half) = true). -- cgit v1.2.3 From f0bf1511e59e528e090a87cfcc220f93c2431ecd Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 9 Jun 2019 10:41:10 +0200 Subject: Add tests for primitive floats with 'native_compute' Tests are updated to include native computations. --- test-suite/primitive/float/valid_binary_conv.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'test-suite/primitive/float/valid_binary_conv.v') diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v index 53fad1a74c..82e00b8532 100644 --- a/test-suite/primitive/float/valid_binary_conv.v +++ b/test-suite/primitive/float/valid_binary_conv.v @@ -31,3 +31,16 @@ Check (eq_refl true <: valid_binary (Prim2SF denorm) = true). Check (eq_refl true <: valid_binary (Prim2SF nan) = true). Check (eq_refl true <: valid_binary (Prim2SF two) = true). Check (eq_refl true <: valid_binary (Prim2SF half) = true). + +Check (eq_refl true <<: valid_binary (Prim2SF zero) = true). +Check (eq_refl true <<: valid_binary (Prim2SF neg_zero) = true). +Check (eq_refl true <<: valid_binary (Prim2SF one) = true). +Check (eq_refl true <<: valid_binary (Prim2SF (-one)) = true). +Check (eq_refl true <<: valid_binary (Prim2SF infinity) = true). +Check (eq_refl true <<: valid_binary (Prim2SF neg_infinity) = true). +Check (eq_refl true <<: valid_binary (Prim2SF huge) = true). +Check (eq_refl true <<: valid_binary (Prim2SF tiny) = true). +Check (eq_refl true <<: valid_binary (Prim2SF denorm) = true). +Check (eq_refl true <<: valid_binary (Prim2SF nan) = true). +Check (eq_refl true <<: valid_binary (Prim2SF two) = true). +Check (eq_refl true <<: valid_binary (Prim2SF half) = true). -- cgit v1.2.3