Merge pull request #43 from AbsInt/standard-headers

Merge of the "standard-headers" branch. This  provides CompCert-compatible implementations of the following standard headers: float.h, stdarg.h, stdbool.h, stddef.h, varargs.h.

These are the headers that are provided by GCC, Clang, and TCC. Other standard headers are provided by Glibc and similar C standard libraries.

So far in CompCert we rely on the headers provided by whatever C compiler is installed on the host platform. This causes some difficulties that this branch addresses:
1- Diab C's stdarg.h is not compatible with CompCert
2- On IA32 and PowerPC, CompCert's "long double" type differs from the "long double" type specified by the ABI. Hence, the platform's float.h gives "long double" parameters that do not match CompCert.

Author: xavierleroy

Makefile

@@ -202,6 +202,7 @@ compcert.ini: Makefile.config VERSION
          echo "abi=$(ABI)"; \
          echo "system=$(SYSTEM)"; \
          echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
+         echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \
          echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
          echo "advanced_debug=$(ADVANCED_DEBUG)"; \
          echo "struct_passing_style=$(STRUCT_PASSING)"; \
@@ -220,15 +221,13 @@ depend: $(FILES) exportclight/Clightdefs.v
 
 install:
 	install -d $(BINDIR)
-	install ./ccomp $(BINDIR)
+	install -m 0755 ./ccomp $(BINDIR)
 	install -d $(SHAREDIR)
-	install ./compcert.ini $(SHAREDIR)
+	install -m 0644 ./compcert.ini $(SHAREDIR)
 ifeq ($(CCHECKLINK),true)
-	install ./cchecklink $(BINDIR)
+	install -m 0755 ./cchecklink $(BINDIR)
 endif
-ifeq ($(HAS_RUNTIME_LIB),true)
 	$(MAKE) -C runtime install
-endif
 
 clean:
 	rm -f $(patsubst %, %/*.vo, $(DIRS))

configure

@@ -18,6 +18,7 @@ libdir='$(PREFIX)/lib/compcert'
 toolprefix=''
 target=''
 has_runtime_lib=true
+has_standard_headers=true
 build_checklink=true
 advanced_debug=false
 
@@ -49,6 +50,7 @@ Options:
   -libdir <dir>    Install libraries in <dir>
   -toolprefix <pref>  Prefix names of tools ("gcc", etc) with <pref>
   -no-runtime-lib  Do not compile nor install the runtime support library
+  -no-standard-headers Do not install nor use the standard .h headers
 '
 
 # Parse command-line arguments
@@ -66,6 +68,8 @@ while : ; do
         toolprefix="$2"; shift;;
     -no-runtime-lib)
         has_runtime_lib=false;;
+    -no-standard-headers)
+        has_standard_headers=false;;
     -no-checklink)
         build_checklink=false;;
     *)
@@ -357,6 +361,7 @@ CASMRUNTIME=$casmruntime
 CLINKER=$clinker
 LIBMATH=$libmath
 HAS_RUNTIME_LIB=$has_runtime_lib
+HAS_STANDARD_HEADERS=$has_standard_headers
 CCHECKLINK=$cchecklink
 ASM_SUPPORTS_CFI=$asm_supports_cfi
 ADVANCED_DEBUG=$advanced_debug
@@ -428,9 +433,12 @@ CLINKER=gcc
 # Math library.  Set to empty under MacOS X
 LIBMATH=-lm
 
-# Do not change
+# Turn on/off the installation and use of the runtime support library
 HAS_RUNTIME_LIB=true
 
+# Turn on/off the installation and use of the standard header files
+HAS_STANDARD_HEADERS=true
+
 # Whether the assembler $(CASM) supports .cfi debug directives
 ASM_SUPPORTS_CFI=false
 #ASM_SUPPORTS_CFI=true
@@ -471,6 +479,8 @@ CompCert configuration:
     Binaries installed in......... $bindirexp
     Runtime library provided...... $has_runtime_lib
     Library files installed in.... $libdirexp
+    Standard headers provided..... $has_standard_headers
+    Standard headers installed in. $libdirexp/include
     cchecklink tool supported..... $cchecklink
     Build command to use.......... $make
 

driver/Configuration.ml

@@ -82,6 +82,11 @@ let has_runtime_lib =
   | "true" -> true
   | "false" -> false
   | v -> bad_config "has_runtime_lib" [v]
+let has_standard_headers = 
+  match get_config_string "has_standard_headers" with
+  | "true" -> true
+  | "false" -> false
+  | v -> bad_config "has_standard_headers" [v]
 let stdlib_path =
   if has_runtime_lib then
     get_config_string "stdlib_path"

driver/Configuration.mli

@@ -31,6 +31,8 @@ val stdlib_path: string
   (** Path to CompCert's library *)
 val has_runtime_lib: bool
   (** True if CompCert's library is available. *)
+val has_standard_headers: bool
+  (** True if CompCert's standard header files is available. *)
 val advanced_debug: bool
   (** True if advanced debug is implement for the Target *)
 

driver/Driver.ml

@@ -93,8 +93,8 @@ let preprocess ifile ofile =
   let cmd = List.concat [
     Configuration.prepro;
     ["-D__COMPCERT__"];
-    (if Configuration.has_runtime_lib
-     then ["-I" ^ !stdlib_path]
+    (if Configuration.has_standard_headers
+     then ["-I" ^ Filename.concat !stdlib_path "include" ]
      else []);
     List.rev !prepro_options;
     [ifile]

runtime/Makefile

@@ -1,15 +1,16 @@
 include ../Makefile.config
 
 CFLAGS=-O1 -g -Wall
-INCLUDES=
 OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
   i64_shr.o i64_smod.o i64_stod.o i64_stof.o \
   i64_udivmod.o i64_udiv.o i64_umod.o i64_utod.o i64_utof.o \
   vararg.o
 LIB=libcompcert.a
+INCLUDES=include/float.h include/stdarg.h include/stdbool.h \
+  include/stddef.h include/varargs.h
 
 ifeq ($(strip $(HAS_RUNTIME_LIB)),true)
-all: $(LIB) $(INCLUDES)
+all: $(LIB)
 else
 all:
 endif
@@ -28,11 +29,19 @@ clean::
 	rm -f *.o $(LIB)
 
 ifeq ($(strip $(HAS_RUNTIME_LIB)),true)
-install:
+install::
 	install -d $(LIBDIR)
-	install -c $(LIB) $(INCLUDES) $(LIBDIR)
+	install -m 0644 $(LIB) $(LIBDIR)
 else
-install:
+install::
+endif
+
+ifeq ($(strip $(HAS_STANDARD_HEADERS)),true)
+install::
+	install -d $(LIBDIR)/include
+	install -m 0644 $(INCLUDES) $(LIBDIR)/include
+else
+install::
 endif
 
 test/test_int64: test/test_int64.c $(LIB)

runtime/include/float.h

@@ -0,0 +1,82 @@
+/* This file is part of the Compcert verified compiler.
+ *
+ * Copyright (c) 2015 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/* <float.h> -- characteristics of floating types (ISO C99 7.7) */
+
+#ifndef _FLOAT_H
+#define _FLOAT_H
+
+/* FP numbers are in binary */
+#define FLT_RADIX 2
+
+/* No excess precision is used during FP arithmetic */
+#define FLT_EVAL_METHOD 0
+
+/* FP operations round to nearest even */
+#define FLT_ROUNDS 1
+
+/* Number of decimal digits sufficient to represent FP numbers */
+#define DECIMAL_DIG 17
+
+/* The "float" type is IEEE binary32 */
+#define FLT_MANT_DIG 24
+#define FLT_DIG 6
+#define FLT_ROUNDS 1
+#define FLT_EPSILON 0x1p-23F
+#define FLT_MIN_EXP (-125)
+#define FLT_MIN 0x1p-126F
+#define FLT_MIN_10_EXP (-37)
+#define FLT_MAX_EXP 128
+#define FLT_MAX 0x1.fffffep+127F
+#define FLT_MAX_10_EXP 38
+
+/* The "double" type is IEEE binary64 */
+#define DBL_MANT_DIG 53
+#define DBL_DIG 15
+#define DBL_EPSILON 0x1p-52
+#define DBL_MIN_EXP (-1021)
+#define DBL_MIN 0x1p-1022
+#define DBL_MIN_10_EXP (-307)
+#define DBL_MAX_EXP 1024
+#define DBL_MAX 0x1.fffffffffffffp+1023
+#define DBL_MAX_10_EXP 308
+
+/* The "long double" type, when supported, is IEEE binary64 */
+#define LDBL_MANT_DIG 53
+#define LDBL_DIG 15
+#define LDBL_EPSILON 0x1p-52L
+#define LDBL_MIN_EXP (-1021)
+#define LDBL_MIN 0x1p-1022L
+#define LDBL_MIN_10_EXP (-307)
+#define LDBL_MAX_EXP 1024
+#define LDBL_MAX 0x1.fffffffffffffp+1023L
+#define LDBL_MAX_10_EXP 308
+
+#endif
+

runtime/include/stdarg.h

@@ -0,0 +1,61 @@
+/* This file is part of the Compcert verified compiler.
+ *
+ * Copyright (c) 2015 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/* <stdarg.h> -- variable argument handling (ISO C99 7.15) */
+
+#ifndef _STDARG_H
+
+/* Glibc compatibility: if __need___va_list is set,
+   just define __gnuc_va_list and don't consider this file as included. */
+#ifndef __need___va_list
+#define _STDARG_H
+#endif
+#undef __need___va_list
+
+#ifndef __GNUC_VA_LIST
+#define __GNUC_VA_LIST
+typedef __builtin_va_list __gnuc_va_list;
+#endif
+
+#ifdef _STDARG_H
+
+#ifndef _VA_LIST_T
+#define _VA_LIST_T
+typedef __builtin_va_list va_list;
+#endif
+
+#define va_start(v,l) __builtin_va_start(v,l)
+#define va_end(v) __builtin_va_end(v)
+#define va_arg(v,l) __builtin_va_arg(v,l)
+#define va_copy(d,s) __builtin_va_copy(d,s)
+
+#endif
+
+#endif
+

runtime/include/stdbool.h

@@ -0,0 +1,39 @@
+/* This file is part of the Compcert verified compiler.
+ *
+ * Copyright (c) 2015 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/* <stdbool.h> -- Boolean type and values (ISO C99 7.16) */
+
+#ifndef _STDBOOL_H
+#define _STDBOOL_H
+
+#define bool _Bool
+#define true 1
+#define false 0
+
+#endif