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/csymtable.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 6c9e73b50d..cbffdc731e 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -184,7 +184,16 @@ and eval_to_patch env (buff,pl,fv) =
     | Reloc_proj_name p -> slot_for_proj_name p
   in
   let tc = patch buff pl slots in
-  let vm_env = Array.map (slot_for_fv env) fv in
+  let vm_env =
+    (* Beware, this may look like a call to [Array.map], but it's not.
+       Calling [Array.map f] when the first argument returned by [f]
+       is a float would lead to [vm_env] being an unboxed Double_array
+       (Tag_val = Double_array_tag) whereas eval_tcode expects a
+       regular array (Tag_val = 0).
+       See test-suite/primitive/float/coq_env_double_array.v
+       for an actual instance. *)
+    let a = Array.make (Array.length fv) crazy_val in
+    Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in
   eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
 
 and val_of_constr env c =
-- 
cgit v1.2.3