From 1909a882df9e40c079b7fbcdfba3d1742c52a0fb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Apr 2015 12:38:16 +0200 Subject: Provide and use compiler-dependent standard headers. This branch provides implementations of the following standard headers: These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux). --- Makefile | 9 +++--- configure | 12 ++++++- driver/Configuration.ml | 5 +++ driver/Configuration.mli | 2 ++ driver/Driver.ml | 4 +-- runtime/Makefile | 19 ++++++++--- runtime/include/float.h | 82 +++++++++++++++++++++++++++++++++++++++++++++++ runtime/include/stdarg.h | 58 +++++++++++++++++++++++++++++++++ runtime/include/stdbool.h | 39 ++++++++++++++++++++++ runtime/include/stddef.h | 81 ++++++++++++++++++++++++++++++++++++++++++++++ runtime/include/varargs.h | 38 ++++++++++++++++++++++ 11 files changed, 336 insertions(+), 13 deletions(-) create mode 100644 runtime/include/float.h create mode 100644 runtime/include/stdarg.h create mode 100644 runtime/include/stdbool.h create mode 100644 runtime/include/stddef.h create mode 100644 runtime/include/varargs.h diff --git a/Makefile b/Makefile index afd26c4c..2205ed64 100644 --- a/Makefile +++ b/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)) diff --git a/configure b/configure index ffc1d0d3..84fed376 100755 --- a/configure +++ b/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 Install libraries in -toolprefix Prefix names of tools ("gcc", etc) with -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 diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 2cea2b80..70131fc6 100644 --- a/driver/Configuration.ml +++ b/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" diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 20c45518..72810456 100644 --- a/driver/Configuration.mli +++ b/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 *) diff --git a/driver/Driver.ml b/driver/Driver.ml index d225ec4f..380209ab 100644 --- a/driver/Driver.ml +++ b/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] diff --git a/runtime/Makefile b/runtime/Makefile index 9a872427..2fdaa4ec 100644 --- a/runtime/Makefile +++ b/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) diff --git a/runtime/include/float.h b/runtime/include/float.h new file mode 100644 index 00000000..d78a80d7 --- /dev/null +++ b/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 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 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. + */ + +/* -- 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 + diff --git a/runtime/include/stdarg.h b/runtime/include/stdarg.h new file mode 100644 index 00000000..7668c62c --- /dev/null +++ b/runtime/include/stdarg.h @@ -0,0 +1,58 @@ +/* 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 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 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. + */ + +/* -- 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 + +typedef __builtin_va_list va_list; + +#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 + diff --git a/runtime/include/stdbool.h b/runtime/include/stdbool.h new file mode 100644 index 00000000..b9ff9399 --- /dev/null +++ b/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 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 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. + */ + +/* -- Boolean type and values (ISO C99 7.16) */ + +#ifndef _STDBOOL_H +#define _STDBOOL_H + +#define bool _Bool +#define true 1 +#define false 0 + +#endif diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h new file mode 100644 index 00000000..3da06c6f --- /dev/null +++ b/runtime/include/stddef.h @@ -0,0 +1,81 @@ +/* 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 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 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. + */ + +/* -- common definitions (ISO C99 7.17) */ + +#ifndef _STDDEF_H + +/* Glibc compatibility: if one of the __need_ macros is set, + just define the corresponding type or macro + and don't consider this file as fully included yet. */ +#if !defined(__need_size_t) && !defined(__need_ptrdiff_t) && !defined(__need_wchar_t) && !defined(__need_NULL) +#define _STDDEF_H +#endif + +#if defined(_STDDEF_H) || defined(__need_size_t) +#ifndef _SIZE_T +#define _SIZE_T +typedef unsigned long size_t; +#endif +#undef __need_size_t +#endif + +#if defined(_STDDEF_H) || defined(__need_ptrdiff_t) +#ifndef _PTRDIFF_T +#define _PTRDIFF_T +typedef signed long ptrdiff_t; +#endif +#undef __need_ptrdiff_t +#endif + +#if defined(_STDDEF_H) || defined(__need_wchar_t) +#ifndef _WCHAR_T +#define _WCHAR_T +#ifdef _WIN32 +typedef unsigned short wchar_t; +#else +typedef signed int wchar_t; +#endif +#endif +#undef __need_wchar_t +#endif + +#if defined(_STDDEF_H) || defined(__need_NULL) +#ifndef NULL +#define NULL 0 +#endif +#undef __need_NULL +#endif + +#if defined(_STDDEF_H) && !defined(offsetof) +#define offsetof(ty,member) ((size_t) &(((ty)*) NULL)->member) +#endif + +#endif + diff --git a/runtime/include/varargs.h b/runtime/include/varargs.h new file mode 100644 index 00000000..f790a5b4 --- /dev/null +++ b/runtime/include/varargs.h @@ -0,0 +1,38 @@ +/* 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 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 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. + */ + +/* -- old-style variable argument handling */ + +#ifdef _VARARGS_H +#define _VARARGS_H + +#error "CompCert does not implement ." +#error "Please use instead." + +#endif -- cgit