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/cemitcodes.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'kernel/cemitcodes.ml')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 181211d237..82dd7bd85d 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -234,7 +234,18 @@ let check_prim_op = function
   | Int63lt        -> opCHECKLTINT63
   | Int63le        -> opCHECKLEINT63
   | Int63compare   -> opCHECKCOMPAREINT63
-  | _ -> 0 (* TODO: BERTHOLON add float64 operations *)
+  | Float64opp     -> opCHECKOPPFLOAT
+  | Float64abs     -> opCHECKABSFLOAT
+  | Float64compare -> opCHECKCOMPAREFLOAT
+  | Float64add     -> opCHECKADDFLOAT
+  | Float64sub     -> opCHECKSUBFLOAT
+  | Float64mul     -> opCHECKMULFLOAT
+  | Float64div     -> opCHECKDIVFLOAT
+  | Float64sqrt    -> opCHECKSQRTFLOAT
+  | Float64ofInt63 -> opCHECKFLOATOFINT63
+  | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA
+  | Float64frshiftexp -> opCHECKFRSHIFTEXP
+  | Float64ldshiftexp -> opCHECKLDSHIFTEXP
 
 let emit_instr env = function
   | Klabel lbl -> define_label env lbl
-- 
cgit v1.2.3