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
From 92f563727f9fb2ebbf15eddb75987a3530ca8273 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sun, 26 Apr 2015 10:57:56 +0200
Subject: Improve compatibility with MacOS X.
---
runtime/include/stdarg.h | 3 +++
1 file changed, 3 insertions(+)
diff --git a/runtime/include/stdarg.h b/runtime/include/stdarg.h
index 7668c62c..b2e7eadd 100644
--- a/runtime/include/stdarg.h
+++ b/runtime/include/stdarg.h
@@ -45,7 +45,10 @@ typedef __builtin_va_list __gnuc_va_list;
#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)
--
cgit
From 1cdf4f22706dea5371f6d553538ac68f1f0a159f Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sat, 9 May 2015 09:25:21 +0200
Subject: Typo in #ifndef guard.
---
runtime/include/varargs.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/runtime/include/varargs.h b/runtime/include/varargs.h
index f790a5b4..6909583a 100644
--- a/runtime/include/varargs.h
+++ b/runtime/include/varargs.h
@@ -29,7 +29,7 @@
/* -- old-style variable argument handling */
-#ifdef _VARARGS_H
+#ifndef _VARARGS_H
#define _VARARGS_H
#error "CompCert does not implement ."
--
cgit
From 6ae45c3aa11d0c70b83b6b7e91a784b23a67146d Mon Sep 17 00:00:00 2001
From: Bernhard Schommer
Date: Sun, 31 May 2015 20:00:24 +0200
Subject: Allow the option -o to be also the prefix of the file name for
compability with different build systems.
---
driver/Driver.ml | 2 ++
1 file changed, 2 insertions(+)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d225ec4f..aaaeb5b5 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -502,6 +502,8 @@ let cmdline_actions =
Exact "-E", Set option_E;
Exact "-S", Set option_S;
Exact "-o", String(fun s -> option_o := Some s);
+ Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
+ option_o := Some s);
(* Preprocessing options *)
Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options);
--
cgit
From 74b6f4fd4f43d3075cc6aba6becfb40aacf2cb9a Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Fri, 5 Jun 2015 13:48:52 +0200
Subject: Update Changelog for release 2.5.
---
Changelog | 83 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 79 insertions(+), 4 deletions(-)
diff --git a/Changelog b/Changelog
index 4b8c3ff2..ccd77487 100644
--- a/Changelog
+++ b/Changelog
@@ -1,12 +1,87 @@
+Release 2.5, 2015-06-xx
+=======================
+
+Language features:
+- Extended inline assembly in the style of GCC. (See section 6.5
+ of the user's manual.) The implementation is not as complete
+ as that of GCC or Clang. In particular, the only constraints
+ supported over operands are "r" (register), "m" (memory), and
+ "i" (integer immediate).
+
+Code generation and optimization:
+- Revised translation of '||' and '&&' to Clight so as to
+ produce well-typed Clight code.
+- More prudent value analysis of uninitialized declarations of
+ "const" global variables.
+- Revised handling of "common" global declarations, fixes an issue
+ with uninitialized declarations of "const" global variables.
+
+Improvements in confidence:
+- Formalized the typing rules for CompCert C in Coq and verified
+ a type-checker, which is used to produce the type annotations
+ in CompCert C ASTs, rather than trusting the types produced by
+ the Elab pass.
+- Coq proof of correctness for the Unusedglob pass (elimination
+ of unreferenced static global definitions). The Coq AST for
+ compilation units now records which globals are static.
+- More careful semantics of comparisons between a non-null pointer
+ and the null pointer. The comparison is undefined if the non-null
+ pointer is out of bounds.
+
+Usability:
+- Generation of DWARF v2 debugging information in "-g" mode.
+ The information describes C types, global variables, functions,
+ but not yet function-local variables. This is currently available
+ only for the PowerPC/Diab target.
+- Added command-line options to turn individual optimizations on or off,
+ and a "-O0" option to turn them all off.
+- Revised handling of arguments to __builtin_annot so that no code
+ is generated for an argument that is a global variable or a local
+ variable whose address is taken.
- In string and character literals, treat illegal escape sequences
(e.g. "\%" or "\0") as an error instead of a warning.
-- Upgraded Flocq to version 2.4.0.
+- Warn if floating-point literals overflow or underflow when converted
+ to FP numbers.
- cchecklink: added option "-files-from" to read .sdump file names
from a file or from standard input.
-- Revised handling of "common" global declarations, fixes an issue
- with uninitialized declarations of "const" global variables.
-- Use a Makefile instead of ocamlbuild to compile the OCaml code.
+- In "-g -S" mode, annotate the generated .s file with comments
+ containing the C source code.
+- Recognize and accept more of GCC's alternate keywords, e.g. __signed,
+ __volatile__, etc.
+
+ABI conformance:
+- Improved ABI conformance for passing values of struct or union types
+ as function arguments or results.
+- Support the "va_arg" macro from in the case of arguments
+ of struct or union types.
+
+Coq development:
+- In the CompCert C and Clight ASTs, struct and union types are now
+ represented by name instead of by structure. A separate environment
+ maps these names to struct/union definitions. This avoids
+ bad algorithmic complexity of operations over structural types.
+- Introduce symbol environments (type Senv.t) as a restricted view on
+ global environments (type Genv.t).
+- Upgraded the Flocq library to version 2.4.0.
+Bug fixing:
+- Issue #4: exponential behaviors with deeply-nested struct types.
+- Issue #6: mismatch on the definition of wchar_t
+- Issue #10: definition of composite type missing from the environment.
+- Issue #13: improved handling of wide string literals
+- Issue #15: variable-argument functions are not eligible for inlining.
+- Issue #19: support empty "switch" statements
+- Issue #20: ABI incompatibility wrt struct passing on IA32.
+- Issue #28: missing type decay in __builtin_memcpy_aligned applied to arrays.
+- Issue #42: emit error if "static" definition follows non-"static" declaration.
+- Issue #44: OSX assembler does not recognize ".global" directive.
+- Protect against redefinition of the __i64_xxx helper library functions.
+- Revised handling of nonstandard attributes in C type compatibility check.
+
+Miscellaneous:
+- When preprocessing with gcc or clang, use "-std=c99" mode to force
+ C99 conformance.
+- Use a Makefile instead of ocamlbuild to compile the OCaml code.
Release 2.4, 2014-09-17
--
cgit
From 9f30d4984863ec655a03996646805202dc2a07c9 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sat, 6 Jun 2015 09:22:52 +0200
Subject: Error if, in the same scope, a typedef is redefined as a variable, or
a variable is redefined as a typedef.
---
cparser/Elab.ml | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index fe74a786..bcf90f5e 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -778,7 +778,9 @@ and elab_enum_item env ((s, exp), loc) nextval =
"value of enumerator '%s' is not a compile-time constant" s;
(nextval, Some exp') in
if redef Env.lookup_ident env s then
- error loc "redefinition of enumerator '%s'" s;
+ error loc "redefinition of identifier '%s'" s;
+ if redef Env.lookup_typedef env s then
+ error loc "redefinition of typedef '%s' as different kind of symbol" s;
if not (int_representable v (8 * sizeof_ikind enum_ikind) (is_signed_ikind enum_ikind)) then
warning loc "the value of '%s' is not representable with type %a"
s Cprint.typ (TInt(enum_ikind, []));
@@ -1784,11 +1786,15 @@ let enter_typedefs loc env sto dl =
error loc "initializer in typedef";
if redef Env.lookup_typedef env s then
error loc "redefinition of typedef '%s'" s;
+ if redef Env.lookup_ident env s then
+ error loc "redefinition of identifier '%s' as different kind of symbol" s;
let (id, env') = Env.enter_typedef env s ty in
emit_elab loc (Gtypedef(id, ty));
env') env dl
let enter_or_refine_ident local loc env s sto ty =
+ if redef Env.lookup_typedef env s then
+ error loc "redefinition of typedef '%s' as different kind of symbol" s;
match previous_def Env.lookup_ident env s with
| Some(id, II_ident(old_sto, old_ty))
when sto = Storage_extern || Env.in_current_scope env id ->
@@ -1817,7 +1823,7 @@ let enter_or_refine_ident local loc env s sto ty =
in
(id, new_sto, Env.add_ident env id new_sto new_ty)
| Some(id, II_enum v) when Env.in_current_scope env id ->
- error loc "illegal redefinition of enumerator '%s'" s;
+ error loc "redefinition of enumerator '%s'" s;
(id, sto, Env.add_ident env id sto ty)
| _ ->
let (id, env') = Env.enter_ident env s sto ty in (id, sto, env')
--
cgit
From 584eac7027cd4d29c5ca8744453ffeea8f18b501 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sun, 7 Jun 2015 09:25:53 +0200
Subject: Represent external worlds by a coinductive type rather than an
inductive type. As noticed by R. Krebbers, an inductive type for external
worlds implies that all sequences of program-world interactions are finite,
which is not the case.
---
common/Determinism.v | 2 +-
driver/Interp.ml | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/common/Determinism.v b/common/Determinism.v
index d0099ba9..7ea19663 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -36,7 +36,7 @@ Require Import Behaviors.
that this external call succeeds, has result [r], and changes
the world to [w]. *)
-Inductive world: Type :=
+CoInductive world: Type :=
World (io: ident -> list eventval -> option (eventval * world))
(vload: memory_chunk -> ident -> int -> option (eventval * world))
(vstore: memory_chunk -> ident -> int -> eventval -> option world).
diff --git a/driver/Interp.ml b/driver/Interp.ml
index b16d2cae..f453af95 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -402,7 +402,7 @@ let do_inline_assembly txt sg ge w args m = None
(* Implementing external functions producing observable events *)
let rec world ge m =
- Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)
+ lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m))
and world_io ge m id args =
None
--
cgit
From 15bac6d799c0ca6239967d34261de5b787caa868 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Thu, 11 Jun 2015 11:17:41 +0200
Subject: Update for release 2.5.
---
Changelog | 17 +++++++++++------
1 file changed, 11 insertions(+), 6 deletions(-)
diff --git a/Changelog b/Changelog
index ccd77487..c0810c2a 100644
--- a/Changelog
+++ b/Changelog
@@ -1,4 +1,4 @@
-Release 2.5, 2015-06-xx
+Release 2.5, 2015-06-12
=======================
Language features:
@@ -38,20 +38,25 @@ Usability:
- Revised handling of arguments to __builtin_annot so that no code
is generated for an argument that is a global variable or a local
variable whose address is taken.
-- In string and character literals, treat illegal escape sequences
+- In string and character literals, treat illegal escape sequences
(e.g. "\%" or "\0") as an error instead of a warning.
- Warn if floating-point literals overflow or underflow when converted
to FP numbers.
-- cchecklink: added option "-files-from" to read .sdump file names
- from a file or from standard input.
-- In "-g -S" mode, annotate the generated .s file with comments
+- Added missing check for static redefinition following a non-static
+ declaration.
+- Added missing check for redefinition of a typedef as an ordinary
+ identifier within the same scope.
+- In "-g -S" mode, annotate the generated .s file with comments
containing the C source code.
- Recognize and accept more of GCC's alternate keywords, e.g. __signed,
__volatile__, etc.
+- cchecklink: added option "-files-from" to read .sdump file names
+ from a file or from standard input.
ABI conformance:
- Improved ABI conformance for passing values of struct or union types
- as function arguments or results.
+ as function arguments or results. Full conformance is achieved on
+ IA32/ELF, IA32/MacOSX, PowerPC/EABI, PowerPC/Linux, and ARM/EABI.
- Support the "va_arg" macro from in the case of arguments
of struct or union types.
--
cgit
From a3d4f94f470f1ad1b9406c67589c9ebc44c94113 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Thu, 11 Jun 2015 16:18:46 +0200
Subject: Update for release 2.5.
---
doc/index.html | 21 +++++++++++++++------
1 file changed, 15 insertions(+), 6 deletions(-)
diff --git a/doc/index.html b/doc/index.html
index 296d89e0..29a2fb30 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
The CompCert verified compiler
Commented Coq development
-Version 2.3, 2015-05-05
+Version 2.5, 2015-06-12
Introduction
@@ -63,7 +63,8 @@ written.
the CompCert Web site.
This document and the CompCert sources are
-copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut
+copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
+Institut
National de Recherche en Informatique et en Automatique (INRIA) and
distributed under the terms of the
following license.
@@ -115,7 +116,8 @@ semantics.
The CompCert C source language:
syntax and
semantics and
-determinized semantics.
+determinized semantics and
+type system.
See also: type expressions and
operators (syntax and semantics) and
reference interpreter.
@@ -245,12 +247,19 @@ code.
- Dead code elimination |
+ Redundancy elimination |
RTL to RTL |
Deadcode |
Deadcodeproof |
+
+ Removal of unused static globals |
+ RTL to RTL |
+ Unusedglob |
+ Unusedglobproof |
+
+
Register allocation (validation a posteriori) |
RTL to LTL |
@@ -315,9 +324,9 @@ See also: NeedOp: processor-dependent part
Type systems
-Simple type systems are used to statically capture well-formedness
-conditions on some intermediate languages.
+The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
+- RTLtyping: typing for CompCert C + type-checking functions.
- RTLtyping: typing for RTL + type
reconstruction.
- Lineartyping: typing for Linear.
--
cgit
From 9622c474fd1b51ed7cf29eb7c5ecff5279ac1c73 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Thu, 11 Jun 2015 16:19:06 +0200
Subject: Preserve ordinary comments within proof scripts.
---
doc/coq2html.css | 5 +++++
doc/coq2html.mll | 32 ++++++++++++++++++++++++++------
2 files changed, 31 insertions(+), 6 deletions(-)
diff --git a/doc/coq2html.css b/doc/coq2html.css
index 0f6680e8..c5627bfb 100644
--- a/doc/coq2html.css
+++ b/doc/coq2html.css
@@ -7,6 +7,7 @@
div.proofscript contents of proof script
span.docright contents of (**r *) comments
span.bracket contents of [ ] within comments
+ span.comment contents of (* *) comments
span.kwd Coq keyword
span.tactic Coq tactic
span.id any other identifier
@@ -86,6 +87,10 @@ span.kwd {
color: #cf1d1d;
}
+span.comment {
+ color: #008000;
+}
+
a:visited {color : #416DFF; text-decoration : none; }
a:link {color : #416DFF; text-decoration : none; }
a:hover {text-decoration : none; }
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index 329e9eaa..2f1bfdbc 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -206,15 +206,23 @@ let start_verbatim () =
let end_verbatim () =
fprintf !oc "\n"
+let start_comment () =
+ fprintf !oc ""
+
let start_bracket () =
fprintf !oc ""
let end_bracket () =
fprintf !oc ""
+let in_proof = ref false
let proof_counter = ref 0
let start_proof kwd =
+ in_proof := true;
incr proof_counter;
fprintf !oc
"
%s
\n"
@@ -222,7 +230,8 @@ let start_proof kwd =
fprintf !oc "\n" !proof_counter
let end_proof kwd =
- fprintf !oc "%s
\n" kwd
+ fprintf !oc "%s\n" kwd;
+ in_proof := false
let start_html_page modname =
fprintf !oc "\
@@ -300,7 +309,8 @@ and coq = parse
end_doc_right();
coq lexbuf }
| "(*"
- { comment lexbuf;
+ { if !in_proof then start_comment();
+ comment lexbuf;
coq lexbuf }
| path as id
{ ident (Lexing.lexeme_start lexbuf) id; coq lexbuf }
@@ -325,13 +335,23 @@ and bracket = parse
and comment = parse
| "*)"
- { () }
+ { if !in_proof then end_comment() }
| "(*"
- { comment lexbuf; comment lexbuf }
+ { if !in_proof then start_comment();
+ comment lexbuf; comment lexbuf }
| eof
{ () }
- | _
- { comment lexbuf }
+ | "\n"
+ { if !in_proof then newline();
+ comment lexbuf }
+ | space* as s
+ { if !in_proof then space s;
+ comment lexbuf }
+ | eof
+ { () }
+ | _ as c
+ { if !in_proof then character c;
+ comment lexbuf }
and doc_bol = parse
| "<<" space* "\n"
--
cgit
From 702adfde11a7d44a78227de9d44f1038c8b57fdb Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Thu, 11 Jun 2015 17:31:12 +0200
Subject: Turn the error on anonymous structs/unions into a warning. Otherwise
we get too many errors on glibc's standard headers. A real error will occur
when the anonymous struct/union is accessed.
---
cparser/Elab.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index bcf90f5e..aa015b83 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -640,7 +640,7 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) =
error loc "non-default storage in struct or union";
if fieldlist = [] then
if is_anonymous_composite spec then
- error loc "ISO C99 does not support anonymous structs/unions"
+ warning loc "ISO C99 does not support anonymous structs/unions"
else
warning loc "declaration does not declare any members";
--
cgit
From a46f192841298b3246de267f73099d41d46212e4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Thu, 11 Jun 2015 17:38:39 +0200
Subject: More updates for release 2.5.
---
Changelog | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/Changelog b/Changelog
index c0810c2a..3523546d 100644
--- a/Changelog
+++ b/Changelog
@@ -42,10 +42,6 @@ Usability:
(e.g. "\%" or "\0") as an error instead of a warning.
- Warn if floating-point literals overflow or underflow when converted
to FP numbers.
-- Added missing check for static redefinition following a non-static
- declaration.
-- Added missing check for redefinition of a typedef as an ordinary
- identifier within the same scope.
- In "-g -S" mode, annotate the generated .s file with comments
containing the C source code.
- Recognize and accept more of GCC's alternate keywords, e.g. __signed,
@@ -82,6 +78,11 @@ Bug fixing:
- Issue #44: OSX assembler does not recognize ".global" directive.
- Protect against redefinition of the __i64_xxx helper library functions.
- Revised handling of nonstandard attributes in C type compatibility check.
+- Emit an error on "preprocessing numbers" that are invalid numerical literals.
+- Added missing check for static redefinition following a non-static
+ declaration.
+- Added missing check for redefinition of a typedef as an ordinary
+ identifier within the same scope.
Miscellaneous:
- When preprocessing with gcc or clang, use "-std=c99" mode to force
--
cgit
From 0e9ededa8c1d194453f5113bf57c93d0803f03b1 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Fri, 12 Jun 2015 10:10:12 +0200
Subject: Update the years.
---
LICENSE | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/LICENSE b/LICENSE
index 9887738b..21670791 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,8 +1,8 @@
All files in this distribution are part of the CompCert verified compiler.
The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007,
-2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en
-Informatique et en Automatique (INRIA).
+2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Institut National de
+Recherche en Informatique et en Automatique (INRIA).
The CompCert verified compiler is distributed under the terms of the
INRIA Non-Commercial License Agreement given below. This is a
--
cgit