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