From 361726e23dc8ad15a61788349184e7790bec42c9 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 22 Sep 2020 17:05:16 +0200
Subject: Use exact arithmetic for printing positive numbers

And also for the computations in name_temporary.
Overflowing OCaml's integer types is unlikely in actual use but
happened in the past owing to another mistake (see issue #370).
---
 exportclight/ExportClight.ml | 108 ++++++++++++++++++++++---------------------
 1 file changed, 56 insertions(+), 52 deletions(-)

(limited to 'exportclight')

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 4a85b591..4ff901eb 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -43,6 +43,48 @@ let print_list fn p l =
       in plist l;
       fprintf p ")@]"
 
+(* Numbers *)
+
+let coqint p n =
+  let n = camlint_of_coqint n in
+  if n >= 0l
+  then fprintf p "(Int.repr %ld)" n
+  else fprintf p "(Int.repr (%ld))" n
+
+let coqptrofs p n =
+  let s = Z.to_string n in
+  if Z.ge n Z.zero
+  then fprintf p "(Ptrofs.repr %s)" s
+  else fprintf p "(Ptrofs.repr (%s))" s
+
+let coqint64 p n =
+  let n = camlint64_of_coqint n in
+  if n >= 0L
+  then fprintf p "(Int64.repr %Ld)" n
+  else fprintf p "(Int64.repr (%Ld))" n
+
+let coqfloat p n =
+  fprintf p "(Float.of_bits %a)" coqint64 (Floats.Float.to_bits n)
+
+let coqsingle p n =
+  fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n)
+
+let positive p n =
+  fprintf p "%s%%positive" (Z.to_string (Z.Zpos n))
+
+let coqN p n =
+  fprintf p "%s%%N" (Z.to_string (Z.of_N n))
+
+let coqZ p n =
+  if Z.ge n Z.zero
+  then fprintf p "%s" (Z.to_string n)
+  else fprintf p "(%s)" (Z.to_string n)
+
+(* Coq strings *)
+
+let coqstring p s =
+  fprintf p "\"%s\"" (camlstring_of_coqstring s)
+
 (* Identifiers *)
 
 exception Not_an_identifier
@@ -69,7 +111,7 @@ let ident p id =
     let s = Hashtbl.find temp_names id in
     fprintf p "%s" s
   with Not_found ->
-    fprintf p "%ld%%positive" (P.to_int32 id)
+    positive p id
 
 let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) =
   List.iter f
@@ -85,67 +127,29 @@ let define_idents p =
           fprintf p "Definition _%s : ident := $\"%s\".@ "
                     (sanitize name) name
         else
-          fprintf p "Definition _%s : ident := %ld%%positive.@ "
-                    (sanitize name) (P.to_int32 id)
+          fprintf p "Definition _%s : ident := %a.@ "
+                    (sanitize name) positive id
       with Not_an_identifier ->
         ());
   iter_hashtbl_sorted
     temp_names
     (fun (id, name) ->
-      fprintf p "Definition %s : ident := %ld%%positive.@ "
-                name (P.to_int32 id));
+      fprintf p "Definition %s : ident := %a.@ "
+                name positive id);
   fprintf p "@ "
 
 let name_temporary t =
   if not (Hashtbl.mem string_of_atom t) && not (Hashtbl.mem temp_names t)
   then begin
-    let t1 = P.to_int t and t0 = P.to_int (first_unused_ident ()) in
-    Hashtbl.add temp_names t (sprintf "_t'%d" (t1 - t0 + 1))
+    let t0 = first_unused_ident () in
+    let d = Z.succ (Z.sub (Z.Zpos t) (Z.Zpos t0)) in
+    Hashtbl.add temp_names t ("_t'" ^ Z.to_string d)
   end
 
 let name_opt_temporary = function
   | None -> ()
   | Some id -> name_temporary id
 
-(* Numbers *)
-
-let coqint p n =
-  let n = camlint_of_coqint n in
-  if n >= 0l
-  then fprintf p "(Int.repr %ld)" n
-  else fprintf p "(Int.repr (%ld))" n
-
-let coqptrofs p n =
-  let s = Z.to_string n in
-  if Z.ge n Z.zero
-  then fprintf p "(Ptrofs.repr %s)" s
-  else fprintf p "(Ptrofs.repr (%s))" s
-
-let coqint64 p n =
-  let n = camlint64_of_coqint n in
-  if n >= 0L
-  then fprintf p "(Int64.repr %Ld)" n
-  else fprintf p "(Int64.repr (%Ld))" n
-
-let coqfloat p n =
-  fprintf p "(Float.of_bits %a)" coqint64 (Floats.Float.to_bits n)
-
-let coqsingle p n =
-  fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n)
-
-let coqN p n =
-  fprintf p "%ld%%N" (N.to_int32 n)
-
-let coqZ p n =
-  if Z.ge n Z.zero
-  then fprintf p "%s" (Z.to_string n)
-  else fprintf p "(%s)" (Z.to_string n)
-
-(* Coq strings *)
-
-let coqstring p s =
-  fprintf p "\"%s\"" (camlstring_of_coqstring s)
-
 (* Raw attributes *)
 
 let attribute p a =
@@ -269,14 +273,14 @@ let external_function p = function
   | EF_memcpy(sz, al) ->
       fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
   | EF_annot(kind, text, targs) ->
-      fprintf p "(EF_annot %ld%%positive %a %a)"
-                (P.to_int32 kind) coqstring text (print_list asttype) targs
+      fprintf p "(EF_annot %a %a %a)"
+                positive kind coqstring text (print_list asttype) targs
   | EF_annot_val(kind, text, targ) ->
-      fprintf p "(EF_annot_val %ld%%positive %a %a)"
-                (P.to_int32 kind) coqstring text asttype targ
+      fprintf p "(EF_annot_val %a %a %a)"
+                positive kind coqstring text asttype targ
   | EF_debug(kind, text, targs) ->
-      fprintf p "(EF_debug %ld%%positive %ld%%positive %a)"
-                (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs
+      fprintf p "(EF_debug %a %a %a)"
+                positive kind positive text (print_list asttype) targs
   | EF_inline_asm(text, sg, clob) ->
       fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]"
               coqstring text
-- 
cgit