Protect against redefinition of the __i64_xxx helper library functions.

This is achieved by declaring these functions in C2C.ml, then
re-checking their declarations in the global environment during
the Selection pass.

In passing, the "hf" parameter for SelectLong functions was removed
and replaced by fixed identifiers corresponding to the actual names
of the helper functions.

1 files changed, 54 insertions, 1 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 118b6d2d..584c265a 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -188,7 +188,60 @@ let builtins_generic = {
     "__compcert_va_float64",
         (TFloat(FDouble, []),
           [TPtr(TVoid [], [])],
-          false)
+          false);
+  (* Helper functions for int64 arithmetic *)
+    "__i64_dtos",
+        (TInt(ILongLong, []),
+         [TFloat(FDouble, [])],
+         false);
+    "__i64_dtou",
+        (TInt(IULongLong, []),
+         [TFloat(FDouble, [])],
+         false);
+    "__i64_stod",
+        (TFloat(FDouble, []),
+         [TInt(ILongLong, [])],
+         false);
+    "__i64_utod",
+        (TFloat(FDouble, []),
+         [TInt(IULongLong, [])],
+         false);
+    "__i64_stof",
+        (TFloat(FFloat, []),
+         [TInt(ILongLong, [])],
+         false);
+    "__i64_utof",
+        (TFloat(FFloat, []),
+         [TInt(IULongLong, [])],
+         false);
+    "__i64_sdiv",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(ILongLong, [])],
+         false);
+    "__i64_udiv",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IULongLong, [])],
+         false);
+    "__i64_smod",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(ILongLong, [])],
+         false);
+    "__i64_umod",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IULongLong, [])],
+         false);
+    "__i64_shl",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(IInt, [])],
+         false);
+    "__i64_shr",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IInt, [])],
+         false);
+    "__i64_sar",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(IInt, [])],
+         false)
   ]
 }