Use standard float an integer datatypes in Votour representation.

It seems this passed under my radar, but the change of implementation of the
safe demarshaller introduced by native integers and floating point numbers is
dangerous.

For floats, it makes the demarshaller depend on float kernel representation.
This is just an alias to the standard OCaml float type, so this is currently
not problematic, but this makes the code fragile if ever we decide to change
it there. This would trigger unsound object casts without any complaint from
the type-checker. Furthermore, having such a low-level library depend on
the kernel library sounds like a anti-feature to me.

For native integers, the situation is direr. The demarshaller turns
unconditionally 64-bits integers into their Int63 representation, which
depends on the architecture. This means that when parsing vo files from
a architecture where these types are not the same, we are guaranteed to get
into unsound casts. Some of them *might* get caught by the value
representation checker, yet it is a footgun. The demarshaller should only
deal with OCaml representations and not try to mess with Coq specific
data types, otherwise we are going to face desynchronization and thus
unsound casts.

3 files changed, 15 insertions, 15 deletions

diff --git a/checker/analyze.ml b/checker/analyze.ml
index 4c06f1e250..91137a0ce2 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -106,8 +106,8 @@ end
 
 type repr =
 | RInt of int
-| RInt63 of Uint63.t
-| RFloat64 of Float64.t
+| Rint64 of Int64.t
+| RFloat64 of float
 | RBlock of (int * int) (* tag × len *)
 | RString of string
 | RPointer of int
@@ -121,8 +121,8 @@ type data =
 
 type obj =
 | Struct of int * data array (* tag × data *)
-| Int63 of Uint63.t (* Primitive integer *)
-| Float64 of Float64.t (* Primitive float *)
+| Int64 of Int64.t (* Primitive integer *)
+| Float64 of float (* Primitive float *)
 | String of string
 
 module type Input =
@@ -344,13 +344,13 @@ let parse_object chan =
     RCode addr
   | CODE_CUSTOM ->
     begin match input_cstring chan with
-    | "_j" -> RInt63 (Uint63.of_int64 (input_intL chan))
+    | "_j" -> Rint64 (input_intL chan)
     | s -> Printf.eprintf "Unhandled custom code: %s" s; assert false
     end
   | CODE_DOUBLE_BIG ->
-    RFloat64 (Float64.of_float (input_double_big chan))
+    RFloat64 (input_double_big chan)
   | CODE_DOUBLE_LITTLE ->
-    RFloat64 (Float64.of_float (input_double_little chan))
+    RFloat64 (input_double_little chan)
   | CODE_DOUBLE_ARRAY32_LITTLE
   | CODE_DOUBLE_ARRAY8_BIG
   | CODE_DOUBLE_ARRAY8_LITTLE
@@ -388,9 +388,9 @@ let parse chan =
   | RCode addr ->
     let data = Fun addr in
     data, None
-  | RInt63 i ->
+  | Rint64 i ->
     let data = Ptr !current_object in
-    let () = LargeArray.set memory !current_object (Int63 i) in
+    let () = LargeArray.set memory !current_object (Int64 i) in
     let () = incr current_object in
     data, None
   | RFloat64 f ->
@@ -461,7 +461,7 @@ let instantiate (p, mem) =
   for i = 0 to len - 1 do
     let obj = match LargeArray.get mem i with
     | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
-    | Int63 i -> Obj.repr i
+    | Int64 i -> Obj.repr i
     | Float64 f -> Obj.repr f
     | String str -> Obj.repr str
     in
@@ -481,7 +481,7 @@ let instantiate (p, mem) =
       for k = 0 to Array.length blk - 1 do
         Obj.set_field obj k (get_data blk.(k))
       done
-    | Int63 _
+    | Int64 _
     | Float64 _
     | String _ -> ()
   done;
diff --git a/checker/analyze.mli b/checker/analyze.mli
index e579f4896d..6626d1dff7 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -7,8 +7,8 @@ type data =
 
 type obj =
 | Struct of int * data array (* tag × data *)
-| Int63 of Uint63.t (* Primitive integer *)
-| Float64 of Float64.t (* Primitive float *)
+| Int64 of Int64.t (* Primitive integer *)
+| Float64 of float (* Primitive float *)
 | String of string
 
 module LargeArray :
diff --git a/checker/votour.ml b/checker/votour.ml
index fe6c487496..9adcc874ac 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -100,7 +100,7 @@ struct
             init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
         in
         fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
-      | Int63 _ -> k 0
+      | Int64 _ -> k 0
       | Float64 _ -> k 0
       | String s ->
         let size = 2 + (String.length s / ws) in
@@ -118,7 +118,7 @@ struct
   | Ptr p ->
     match LargeArray.get !memory p with
     | Struct (tag, os) -> BLOCK (tag, os)
-    | Int63 _ -> OTHER (* TODO: pretty-print int63 values *)
+    | Int64 _ -> OTHER (* TODO: pretty-print int63 values *)
     | Float64 _ -> OTHER (* TODO: pretty-print float64 values *)
     | String s -> STRING s