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 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'kernel/byterun/coq_fix_code.c') 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; -- 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 + 1 file changed, 1 insertion(+) (limited to 'kernel/byterun/coq_fix_code.c') 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]= -- 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 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel/byterun/coq_fix_code.c') 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; -- 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 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/byterun/coq_fix_code.c') 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]= -- cgit v1.2.3