From cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Thu, 19 Jul 2018 13:33:17 +0200 Subject: Add primitive floats to 'vm_compute' * This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM. --- kernel/byterun/coq_fix_code.c | 7 +- kernel/byterun/coq_interp.c | 163 ++++++++++++++++++++++++++++++++----- kernel/byterun/coq_uint63_native.h | 3 + kernel/byterun/coq_values.h | 9 +- 4 files changed, 158 insertions(+), 24 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 0865487c98..bca2cc3bd9 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -63,7 +63,12 @@ void init_arity () { arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= - arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1; + arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= + arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= + arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= + arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= + arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= + arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[PROJ]=2; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 4b45608ae5..55b973dcdb 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -17,6 +17,7 @@ #include #include #include +#include #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -167,38 +168,34 @@ if (sp - num_args < coq_stack_threshold) { \ #endif #endif -#define CheckInt1() do{ \ - if (Is_uint63(accu)) pc++; \ +#define CheckPrimArgs(cond, apply_lbl) do{ \ + if (cond) pc++; \ else{ \ *--sp=accu; \ accu = Field(coq_global_data, *pc++); \ - goto apply1; \ - } \ - }while(0) - -#define CheckInt2() do{ \ - if (Is_uint63(accu) && Is_uint63(sp[0])) pc++; \ - else{ \ - *--sp=accu; \ - accu = Field(coq_global_data, *pc++); \ - goto apply2; \ + goto apply_lbl; \ } \ }while(0) - - -#define CheckInt3() do{ \ - if (Is_uint63(accu) && Is_uint63(sp[0]) && Is_uint63(sp[1]) ) pc++; \ - else{ \ - *--sp=accu; \ - accu = Field(coq_global_data, *pc++); \ - goto apply3; \ - } \ - }while(0) +#define CheckInt1() CheckPrimArgs(Is_uint63(accu), apply1) +#define CheckInt2() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]), apply2) +#define CheckInt3() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]) \ + && Is_uint63(sp[1]), apply3) +#define CheckFloat1() CheckPrimArgs(Is_double(accu), apply1) +#define CheckFloat2() CheckPrimArgs(Is_double(accu) && Is_double(sp[0]), apply2) #define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0) #define AllocPair() Alloc_small(accu, 2, coq_tag_pair) +/* Beware: we cannot use caml_copy_double here as it doesn't use + Alloc_small, hence doesn't protect the stack via + Setup_for_gc/Restore_after_gc. */ +#define Coq_copy_double(val) do{ \ + double Coq_copy_double_f__ = (val); \ + Alloc_small(accu, Double_wosize, Double_tag); \ + Store_double_val(accu, Coq_copy_double_f__); \ + }while(0); + #define Swap_accu_sp do{ \ value swap_accu_sp_tmp__ = accu; \ accu = *sp; \ @@ -1533,6 +1530,128 @@ value coq_interprete } + Instruct (CHECKOPPFLOAT) { + print_instr("CHECKOPPFLOAT"); + CheckFloat1(); + Coq_copy_double(-Double_val(accu)); + Next; + } + + Instruct (CHECKABSFLOAT) { + print_instr("CHECKABSFLOAT"); + CheckFloat1(); + Coq_copy_double(fabs(Double_val(accu))); + Next; + } + + Instruct (CHECKCOMPAREFLOAT) { + double x, y; + print_instr("CHECKCOMPAREFLOAT"); + CheckFloat2(); + x = Double_val(accu); + y = Double_val(*sp++); + if(x < y) { + Alloc_small(accu, 1, coq_tag_Some); + Field(accu, 0) = coq_Lt; + } + else if(x > y) { + Alloc_small(accu, 1, coq_tag_Some); + Field(accu, 0) = coq_Gt; + } + else if(x == y) { + Alloc_small(accu, 1, coq_tag_Some); + Field(accu, 0) = coq_Eq; + } + else { // nan value + accu = coq_None; + } + Next; + } + + Instruct (CHECKADDFLOAT) { + print_instr("CHECKADDFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) + Double_val(*sp++)); + Next; + } + + Instruct (CHECKSUBFLOAT) { + print_instr("CHECKSUBFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) - Double_val(*sp++)); + Next; + } + + Instruct (CHECKMULFLOAT) { + print_instr("CHECKMULFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) * Double_val(*sp++)); + Next; + } + + Instruct (CHECKDIVFLOAT) { + print_instr("CHECKDIVFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) / Double_val(*sp++)); + Next; + } + + Instruct (CHECKSQRTFLOAT) { + print_instr("CHECKSQRTFLOAT"); + CheckFloat1(); + Coq_copy_double(sqrt(Double_val(accu))); + Next; + } + + Instruct (CHECKFLOATOFINT63) { + print_instr("CHECKFLOATOFINT63"); + CheckInt1(); + Coq_copy_double(uint63_to_double(accu)); + Next; + } + + Instruct (CHECKFLOATNORMFRMANTISSA) { + double f; + print_instr("CHECKFLOATNORMFRMANTISSA"); + CheckFloat1(); + f = fabs(Double_val(accu)); + if (f >= 0.5 && f < 1) { + accu = uint63_of_double(ldexp(f, DBL_MANT_DIG)); + } + else { + accu = Val_int(0); + } + Next; + } + + Instruct (CHECKFRSHIFTEXP) { + int exp; + double f; + print_instr("CHECKFRSHIFTEXP"); + CheckFloat1(); + f = frexp(Double_val(accu), &exp); + if (fpclassify(f) == FP_NORMAL) { + exp += FLOAT_EXP_SHIFT; + } + else { + exp = 0; + } + Coq_copy_double(f); + *--sp = accu; + Alloc_small(accu, 2, coq_tag_pair); + Field(accu, 0) = *sp++; + Field(accu, 1) = Val_int(exp); + Next; + } + + Instruct (CHECKLDSHIFTEXP) { + print_instr("CHECKLDSHIFTEXP"); + CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2); + Coq_copy_double(ldexp(Double_val(accu), + uint63_of_value(*sp++) - FLOAT_EXP_SHIFT)); + Next; + } + /* Debugging and machine control */ Instruct(STOP){ diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 9fbd3f83d8..a14ed5c262 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -138,3 +138,6 @@ value uint63_div21(value xh, value xl, value y, value* ql) { } } #define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q)) + +#define uint63_to_double(val) ((double) uint63_of_value(val)) +#define uint63_of_double(f) (Val_long((long int) f)) diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 0cf6ccf532..14f3f152bf 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -14,6 +14,8 @@ #include #include +#include + #define Default_tag 0 #define Accu_tag 0 @@ -29,8 +31,9 @@ /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) +#define Is_double(v) (Tag_val(v) == Double_tag) -/* */ +/* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 #define coq_tag_pair 1 @@ -39,5 +42,9 @@ #define coq_Eq Val_int(0) #define coq_Lt Val_int(1) #define coq_Gt Val_int(2) +#define coq_tag_Some 1 +#define coq_None Val_int(0) + +#define FLOAT_EXP_SHIFT (1022 + 52) #endif /* _COQ_VALUES_ */ -- cgit v1.2.3 From dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Fri, 3 Aug 2018 17:38:48 +0200 Subject: Put axioms on ldshiftexp and frshiftexp Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas. The shift value has been increased to 2 * emax + prec because in ldexp we want to be able to transform the smallest denormalized to the biggest float value in one call. --- kernel/byterun/coq_values.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 14f3f152bf..fa51b2d31f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -45,6 +45,6 @@ #define coq_tag_Some 1 #define coq_None Val_int(0) -#define FLOAT_EXP_SHIFT (1022 + 52) +#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ #endif /* _COQ_VALUES_ */ -- cgit v1.2.3 From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 14:31:37 +0200 Subject: Change return type of primitive float comparison Replace `option comparison` with `float_comparison` (:= `FEq | FLt | FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison. --- kernel/byterun/coq_interp.c | 11 ++++------- kernel/byterun/coq_values.h | 6 ++++-- 2 files changed, 8 insertions(+), 9 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 55b973dcdb..74edd79872 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1551,19 +1551,16 @@ value coq_interprete x = Double_val(accu); y = Double_val(*sp++); if(x < y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Lt; + accu = coq_FLt; } else if(x > y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Gt; + accu = coq_FGt; } else if(x == y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Eq; + accu = coq_FEq; } else { // nan value - accu = coq_None; + accu = coq_FNotComparable; } Next; } diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index fa51b2d31f..c79a8f1b4f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -42,8 +42,10 @@ #define coq_Eq Val_int(0) #define coq_Lt Val_int(1) #define coq_Gt Val_int(2) -#define coq_tag_Some 1 -#define coq_None Val_int(0) +#define coq_FEq Val_int(0) +#define coq_FLt Val_int(1) +#define coq_FGt Val_int(2) +#define coq_FNotComparable Val_int(3) #define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ -- cgit v1.2.3 From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 18:56:07 +0200 Subject: Implement classify on primitive float --- kernel/byterun/coq_fix_code.c | 1 + kernel/byterun/coq_interp.c | 25 +++++++++++++++++++++++++ kernel/byterun/coq_values.h | 9 +++++++++ 3 files changed, 35 insertions(+) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index bca2cc3bd9..fb39ca8358 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -65,6 +65,7 @@ void init_arity () { arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= + arity[CHECKCLASSIFYFLOAT]= arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 74edd79872..b862480fda 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1565,6 +1565,31 @@ value coq_interprete Next; } + Instruct (CHECKCLASSIFYFLOAT) { + double x; + print_instr("CHECKCLASSIFYFLOAT"); + CheckFloat1(); + x = Double_val(accu); + switch (fpclassify(x)) { + case FP_NORMAL: + accu = signbit(x) ? coq_NNormal : coq_PNormal; + break; + case FP_SUBNORMAL: + accu = signbit(x) ? coq_NSubn : coq_PSubn; + break; + case FP_ZERO: + accu = signbit(x) ? coq_NZero : coq_PZero; + break; + case FP_INFINITE: + accu = signbit(x) ? coq_NInf : coq_PInf; + break; + default: /* FP_NAN */ + accu = coq_NaN; + break; + } + Next; + } + Instruct (CHECKADDFLOAT) { print_instr("CHECKADDFLOAT"); CheckFloat2(); diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index c79a8f1b4f..b027673ac7 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -46,6 +46,15 @@ #define coq_FLt Val_int(1) #define coq_FGt Val_int(2) #define coq_FNotComparable Val_int(3) +#define coq_PNormal Val_int(0) +#define coq_NNormal Val_int(1) +#define coq_PSubn Val_int(2) +#define coq_NSubn Val_int(3) +#define coq_PZero Val_int(4) +#define coq_NZero Val_int(5) +#define coq_PInf Val_int(6) +#define coq_NInf Val_int(7) +#define coq_NaN Val_int(8) #define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ -- cgit v1.2.3 From 5f1270242f71a0a1da7c868967e1071d28ed83fb Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 23:37:49 +0200 Subject: Add next_{up,down} primitive float functions --- kernel/byterun/coq_fix_code.c | 3 ++- kernel/byterun/coq_interp.c | 14 ++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index fb39ca8358..3fe77afc2d 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -69,7 +69,8 @@ void init_arity () { arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= - arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=1; + arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]= + arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[PROJ]=2; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index b862480fda..06042bb753 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1674,6 +1674,20 @@ value coq_interprete Next; } + Instruct (CHECKNEXTUPFLOAT) { + print_instr("CHECKNEXTUPFLOAT"); + CheckFloat1(); + Coq_copy_double(nextafter(Double_val(accu), INFINITY)); + Next; + } + + Instruct (CHECKNEXTDOWNFLOAT) { + print_instr("CHECKNEXTDOWNFLOAT"); + CheckFloat1(); + Coq_copy_double(nextafter(Double_val(accu), -INFINITY)); + Next; + } + /* Debugging and machine control */ Instruct(STOP){ -- cgit v1.2.3 From dca0135a263717b3a1a1d7c4f054f039dc08109e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 4 Apr 2019 00:14:47 +0200 Subject: Make primitive float work on x86_32 Flag -fexcess-precision=standard is not enough on x86_32 where -msse2 -mfpmath=sse is required (-msse is not enough) to avoid double rounding issues in the VM. Most floating-point operation are now implemented in C because OCaml is suffering double rounding issues on x86_32 with 80 bits extended precision registers used for floating-point values, causing double rounding making floating-point arithmetic incorrect with respect to its specification. Add a runtime test for double roundings. --- kernel/byterun/coq_float64.h | 32 ++++++++++++++++++++++++++++++++ kernel/byterun/coq_interp.c | 35 ++++++++++++++++++++++------------- kernel/byterun/coq_uint63_emul.h | 15 +++++++++++++++ kernel/byterun/coq_uint63_native.h | 25 +++++++++++++++++++++++-- 4 files changed, 92 insertions(+), 15 deletions(-) create mode 100644 kernel/byterun/coq_float64.h (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h new file mode 100644 index 0000000000..6814c31642 --- /dev/null +++ b/kernel/byterun/coq_float64.h @@ -0,0 +1,32 @@ +#ifndef _COQ_FLOAT64_ +#define _COQ_FLOAT64_ + +#include + +#define DECLARE_FBINOP(name, e) \ + double coq_##name(double x, double y) { \ + return e; \ + } \ + \ + value coq_##name##_byte(value x, value y) { \ + return caml_copy_double(coq_##name(Double_val(x), Double_val(y))); \ + } + +#define DECLARE_FUNOP(name, e) \ + double coq_##name(double x) { \ + return e; \ + } \ + \ + value coq_##name##_byte(value x) { \ + return caml_copy_double(coq_##name(Double_val(x))); \ + } + +DECLARE_FBINOP(fmul, x * y) +DECLARE_FBINOP(fadd, x + y) +DECLARE_FBINOP(fsub, x - y) +DECLARE_FBINOP(fdiv, x / y) +DECLARE_FUNOP(fsqrt, sqrt(x)) +DECLARE_FUNOP(next_up, nextafter(x, INFINITY)) +DECLARE_FUNOP(next_down, nextafter(x, -INFINITY)) + +#endif /* _COQ_FLOAT64_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 06042bb753..e67325eb9a 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,6 +23,7 @@ #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" +#include "coq_float64.h" #ifdef ARCH_SIXTYFOUR #include "coq_uint63_native.h" @@ -1593,42 +1594,42 @@ value coq_interprete Instruct (CHECKADDFLOAT) { print_instr("CHECKADDFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) + Double_val(*sp++)); + Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKSUBFLOAT) { print_instr("CHECKSUBFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) - Double_val(*sp++)); + Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKMULFLOAT) { print_instr("CHECKMULFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) * Double_val(*sp++)); + Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKDIVFLOAT) { print_instr("CHECKDIVFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) / Double_val(*sp++)); + Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKSQRTFLOAT) { print_instr("CHECKSQRTFLOAT"); CheckFloat1(); - Coq_copy_double(sqrt(Double_val(accu))); + Coq_copy_double(coq_fsqrt(Double_val(accu))); Next; } Instruct (CHECKFLOATOFINT63) { print_instr("CHECKFLOATOFINT63"); CheckInt1(); - Coq_copy_double(uint63_to_double(accu)); + Uint63_to_double(accu); Next; } @@ -1638,10 +1639,10 @@ value coq_interprete CheckFloat1(); f = fabs(Double_val(accu)); if (f >= 0.5 && f < 1) { - accu = uint63_of_double(ldexp(f, DBL_MANT_DIG)); + Uint63_of_double(ldexp(f, DBL_MANT_DIG)); } else { - accu = Val_int(0); + Uint63_of_int(Val_int(0)); } Next; } @@ -1660,31 +1661,39 @@ value coq_interprete } Coq_copy_double(f); *--sp = accu; +#ifdef ARCH_SIXTYFOUR Alloc_small(accu, 2, coq_tag_pair); - Field(accu, 0) = *sp++; Field(accu, 1) = Val_int(exp); +#else + Uint63_of_int(Val_int(exp)); + *--sp = accu; + Alloc_small(accu, 2, coq_tag_pair); + Field(accu, 1) = *sp++; +#endif + Field(accu, 0) = *sp++; Next; } Instruct (CHECKLDSHIFTEXP) { print_instr("CHECKLDSHIFTEXP"); CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2); - Coq_copy_double(ldexp(Double_val(accu), - uint63_of_value(*sp++) - FLOAT_EXP_SHIFT)); + Swap_accu_sp; + Int_of_uint63(accu); + Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT)); Next; } Instruct (CHECKNEXTUPFLOAT) { print_instr("CHECKNEXTUPFLOAT"); CheckFloat1(); - Coq_copy_double(nextafter(Double_val(accu), INFINITY)); + Coq_copy_double(coq_next_up(Double_val(accu))); Next; } Instruct (CHECKNEXTDOWNFLOAT) { print_instr("CHECKNEXTDOWNFLOAT"); CheckFloat1(); - Coq_copy_double(nextafter(Double_val(accu), -INFINITY)); + Coq_copy_double(coq_next_down(Double_val(accu))); Next; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 528cc6fc1f..e09803ae2d 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -156,3 +156,18 @@ DECLARE_BINOP(mulc_ml) *(h) = Field(uint63_return_value__, 0); \ accu = Field(uint63_return_value__, 1); \ }while(0) + +DECLARE_UNOP(to_float) +#define Uint63_to_double(x) CALL_UNOP(to_float, x) + +DECLARE_UNOP(of_float) +#define Uint63_of_double(f) do{ \ + Coq_copy_double(f); \ + CALL_UNOP(of_float, accu); \ + }while(0) + +DECLARE_UNOP(of_int) +#define Uint63_of_int(x) CALL_UNOP(of_int, x) + +DECLARE_UNOP(to_int_saturate) +#define Int_of_uint63(x) CALL_PREDICATE(accu, to_int_saturate, x) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index a14ed5c262..0ab374194e 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -139,5 +139,26 @@ value uint63_div21(value xh, value xl, value y, value* ql) { } #define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q)) -#define uint63_to_double(val) ((double) uint63_of_value(val)) -#define uint63_of_double(f) (Val_long((long int) f)) +#define Uint63_to_double(x) Coq_copy_double((double) uint63_of_value(x)) + +double coq_uint63_to_float(value x) { + return (double) uint63_of_value(x); +} + +value coq_uint63_to_float_byte(value x) { + return caml_copy_double(coq_uint63_to_float(x)); +} + +#define Uint63_of_double(f) do{ \ + accu = Val_long((uint64_t)(f)); \ + }while(0) + +#define Uint63_of_int(x) (accu = (x)) + +#define Int_of_uint63(x) do{ \ + uint64_t int_of_uint63__ = uint63_of_value(x); \ + if ((int_of_uint63__ & 0xFFFFFFFF80000000L) == 0) \ + accu = (int)int_of_uint63__; \ + else \ + accu = 0x7FFFFFFF; \ + }while(0) -- cgit v1.2.3 From a2ba4016a64f84193261db9a52196adc39cb5767 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 12 Sep 2019 19:02:18 +0200 Subject: Reimplement is_float is_float was relying on Obj.tag triggering a check that we are in the OCaml heap which is expensive. On extreme examples, this can lead to a global 2x speedup. Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in diagnosing this. --- kernel/byterun/coq_float64.h | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h index 6814c31642..9fc390bd33 100644 --- a/kernel/byterun/coq_float64.h +++ b/kernel/byterun/coq_float64.h @@ -29,4 +29,8 @@ DECLARE_FUNOP(fsqrt, sqrt(x)) DECLARE_FUNOP(next_up, nextafter(x, INFINITY)) DECLARE_FUNOP(next_down, nextafter(x, -INFINITY)) +value coq_is_double(value x) { + return Val_long(Is_double(x)); +} + #endif /* _COQ_FLOAT64_ */ -- cgit v1.2.3 From f8fdc27f922694edf74a7b608de1596e0a1ac0e3 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Apr 2019 15:29:53 +0200 Subject: Make primitive float work on Windows --- kernel/byterun/coq_interp.c | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e67325eb9a..6e6adb1293 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1652,6 +1652,12 @@ value coq_interprete double f; print_instr("CHECKFRSHIFTEXP"); CheckFloat1(); + /* frexp(infinity) incorrectly returns nan on mingw */ +#if defined(__MINGW32__) || defined(__MINGW64__) + if (fpclassify(Double_val(accu)) == FP_INFINITE) { + f = Double_val(accu); + } else +#endif f = frexp(Double_val(accu), &exp); if (fpclassify(f) == FP_NORMAL) { exp += FLOAT_EXP_SHIFT; -- cgit v1.2.3 From f155ba664a782f000e278d97ee5666e2e7d2adea Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Jul 2019 15:08:44 +0200 Subject: Add "==", "<", "<=" in PrimFloat.v * Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux --- kernel/byterun/coq_fix_code.c | 2 ++ kernel/byterun/coq_float64.h | 12 ++++++++++++ kernel/byterun/coq_interp.c | 27 +++++++++++++++++++++++++++ 3 files changed, 41 insertions(+) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 3fe77afc2d..931b509f48 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -44,6 +44,7 @@ void init_arity () { arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= + arity[LTFLOAT]=arity[LEFLOAT]= arity[ISINT]=arity[AREINT2]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= @@ -64,6 +65,7 @@ void init_arity () { arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= + arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]= arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= arity[CHECKCLASSIFYFLOAT]= arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h index 9fc390bd33..c41079c8ff 100644 --- a/kernel/byterun/coq_float64.h +++ b/kernel/byterun/coq_float64.h @@ -3,6 +3,15 @@ #include +#define DECLARE_FREL(name, e) \ + int coq_##name(double x, double y) { \ + return e; \ + } \ + \ + value coq_##name##_byte(value x, value y) { \ + return coq_##name(Double_val(x), Double_val(y)); \ + } + #define DECLARE_FBINOP(name, e) \ double coq_##name(double x, double y) { \ return e; \ @@ -21,6 +30,9 @@ return caml_copy_double(coq_##name(Double_val(x))); \ } +DECLARE_FREL(feq, x == y) +DECLARE_FREL(flt, x < y) +DECLARE_FREL(fle, x <= y) DECLARE_FBINOP(fmul, x * y) DECLARE_FBINOP(fadd, x + y) DECLARE_FBINOP(fsub, x - y) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 6e6adb1293..c21aeecb16 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1545,6 +1545,33 @@ value coq_interprete Next; } + Instruct (CHECKEQFLOAT) { + print_instr("CHECKEQFLOAT"); + CheckFloat2(); + accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLTFLOAT) { + print_instr("CHECKLTFLOAT"); + CheckFloat2(); + } + Instruct (LTFLOAT) { + print_instr("LTFLOAT"); + accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLEFLOAT) { + print_instr("CHECKLEFLOAT"); + CheckFloat2(); + } + Instruct (LEFLOAT) { + print_instr("LEFLOAT"); + accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + Next; + } + Instruct (CHECKCOMPAREFLOAT) { double x, y; print_instr("CHECKCOMPAREFLOAT"); -- cgit v1.2.3 From d39fab9a7c39d8da868c4481b96cf1086c21b1a4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 10 Oct 2019 20:11:02 +0200 Subject: Fix ldshiftexp * Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel --- kernel/byterun/coq_interp.c | 3 ++- kernel/byterun/coq_uint63_emul.h | 4 ++-- kernel/byterun/coq_uint63_native.h | 9 ++++----- 3 files changed, 8 insertions(+), 8 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index c21aeecb16..ca1308696c 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1711,7 +1711,8 @@ value coq_interprete print_instr("CHECKLDSHIFTEXP"); CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2); Swap_accu_sp; - Int_of_uint63(accu); + Uint63_to_int_min(accu, Val_int(2 * FLOAT_EXP_SHIFT)); + accu = Int_val(accu); Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT)); Next; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index e09803ae2d..143a6d098c 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -169,5 +169,5 @@ DECLARE_UNOP(of_float) DECLARE_UNOP(of_int) #define Uint63_of_int(x) CALL_UNOP(of_int, x) -DECLARE_UNOP(to_int_saturate) -#define Int_of_uint63(x) CALL_PREDICATE(accu, to_int_saturate, x) +DECLARE_BINOP(to_int_min) +#define Uint63_to_int_min(n, m) CALL_BINOP(to_int_min, n, m) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 0ab374194e..5be7587091 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -155,10 +155,9 @@ value coq_uint63_to_float_byte(value x) { #define Uint63_of_int(x) (accu = (x)) -#define Int_of_uint63(x) do{ \ - uint64_t int_of_uint63__ = uint63_of_value(x); \ - if ((int_of_uint63__ & 0xFFFFFFFF80000000L) == 0) \ - accu = (int)int_of_uint63__; \ +#define Uint63_to_int_min(n, m) do { \ + if (uint63_lt((n),(m))) \ + accu = (n); \ else \ - accu = 0x7FFFFFFF; \ + accu = (m); \ }while(0) -- cgit v1.2.3 From 324072c12a164f98d0ffa8125d319ffb49df87d8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 31 Oct 2019 17:04:48 +0100 Subject: Communicate CFLAGS to dune --- kernel/byterun/dune | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'kernel/byterun') diff --git a/kernel/byterun/dune b/kernel/byterun/dune index 20bdf28e54..d0145176ea 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -1,3 +1,16 @@ +; Dune doesn't use configure's output, but it is still necessary for +; some Coq files to work; will be fixed in the future. +(rule + (targets dune.c_flags) + (mode fallback) + (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) + (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no)))) + +(env + (dev (c_flags (:include dune.c_flags))) + (release (c_flags (:include dune.c_flags))) + (ireport (c_flags (:include dune.c_flags)))) + (library (name byterun) (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") -- cgit v1.2.3