diff options
| -rw-r--r-- | Changelog | 93 | ||||
| -rw-r--r-- | LICENSE | 4 | ||||
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | common/Determinism.v | 2 | ||||
| -rwxr-xr-x | configure | 12 | ||||
| -rw-r--r-- | cparser/Elab.ml | 12 | ||||
| -rw-r--r-- | doc/coq2html.css | 5 | ||||
| -rw-r--r-- | doc/coq2html.mll | 32 | ||||
| -rw-r--r-- | doc/index.html | 21 | ||||
| -rw-r--r-- | driver/Configuration.ml | 5 | ||||
| -rw-r--r-- | driver/Configuration.mli | 2 | ||||
| -rw-r--r-- | driver/Driver.ml | 6 | ||||
| -rw-r--r-- | driver/Interp.ml | 2 | ||||
| -rw-r--r-- | runtime/Makefile | 19 | ||||
| -rw-r--r-- | runtime/include/float.h | 82 | ||||
| -rw-r--r-- | runtime/include/stdarg.h | 61 | ||||
| -rw-r--r-- | runtime/include/stdbool.h | 39 | ||||
| -rw-r--r-- | runtime/include/stddef.h | 81 | ||||
| -rw-r--r-- | runtime/include/varargs.h | 38 |
19 files changed, 487 insertions, 38 deletions
@@ -1,12 +1,93 @@ -- In string and character literals, treat illegal escape sequences +Release 2.5, 2015-06-12 +======================= + +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. +- 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. -- 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. + 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. Full conformance is achieved on + IA32/ELF, IA32/MacOSX, PowerPC/EABI, PowerPC/Linux, and ARM/EABI. +- Support the "va_arg" macro from <stdarg.h> 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. +- 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 + C99 conformance. +- Use a Makefile instead of ocamlbuild to compile the OCaml code. Release 2.4, 2014-09-17 @@ -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 @@ -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/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). @@ -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 diff --git a/cparser/Elab.ml b/cparser/Elab.ml index fe74a786..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"; @@ -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') 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 "</pre>\n" +let start_comment () = + fprintf !oc "<span class=\"comment\">(*" + +let end_comment () = + fprintf !oc "*)</span>" + let start_bracket () = fprintf !oc "<span class=\"bracket\">" let end_bracket () = fprintf !oc "</span>" +let in_proof = ref false let proof_counter = ref 0 let start_proof kwd = + in_proof := true; incr proof_counter; fprintf !oc "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n" @@ -222,7 +230,8 @@ let start_proof kwd = fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter let end_proof kwd = - fprintf !oc "%s</div>\n" kwd + fprintf !oc "%s</div>\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" 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; } <H1 align="center">The CompCert verified compiler</H1> <H2 align="center">Commented Coq development</H2> -<H3 align="center">Version 2.3, 2015-05-05</H3> +<H3 align="center">Version 2.5, 2015-06-12</H3> <H2>Introduction</H2> @@ -63,7 +63,8 @@ written.</P> <A HREF="http://compcert.inria.fr/">the CompCert Web site</A>.</P> <P>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 <A HREF="LICENSE">license</A>. @@ -115,7 +116,8 @@ semantics. <LI> The CompCert C source language: <A HREF="html/Csyntax.html">syntax</A> and <A HREF="html/Csem.html">semantics</A> and -<A HREF="html/Cstrategy.html">determinized semantics</A>.<BR> +<A HREF="html/Cstrategy.html">determinized semantics</A> and +<A HREF="html/Ctyping.html">type system</A>.<BR> See also: <A HREF="html/Ctypes.html">type expressions</A> and <A HREF="html/Cop.html">operators (syntax and semantics)</A> and <A HREF="html/Cexec.html">reference interpreter</A>. @@ -245,13 +247,20 @@ code. </TR> <TR valign="top"> - <TD>Dead code elimination</TD> + <TD>Redundancy elimination</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/Deadcode.html">Deadcode</A></TD> <TD><A HREF="html/Deadcodeproof.html">Deadcodeproof</A></TD> </TR> <TR valign="top"> + <TD>Removal of unused static globals</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/Unusedglob.html">Unusedglob</A></TD> + <TD><A HREF="html/Unusedglobproof.html">Unusedglobproof</A></TD> +</TR> + +<TR valign="top"> <TD>Register allocation (validation a posteriori)</TD> <TD>RTL to LTL</TD> <TD><A HREF="html/Allocation.html">Allocation</A></TD> @@ -315,9 +324,9 @@ See also: <A HREF="html/NeedOp.html"><I>NeedOp</I></A>: processor-dependent part <H3>Type systems</H3> -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. <UL> +<LI> <A HREF="html/Ctyping.html">RTLtyping</A>: typing for CompCert C + type-checking functions. <LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type reconstruction. <LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear. 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 90badb85..352483bf 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] @@ -515,6 +515,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); 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 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 <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 + diff --git a/runtime/include/stdarg.h b/runtime/include/stdarg.h new file mode 100644 index 00000000..b2e7eadd --- /dev/null +++ b/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 + 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 <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 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 <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. + */ + +/* <stddef.h> -- 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..6909583a --- /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 <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. + */ + +/* <varargs.h> -- old-style variable argument handling */ + +#ifndef _VARARGS_H +#define _VARARGS_H + +#error "CompCert does not implement <varargs.h>." +#error "Please use <stdarg.h> instead." + +#endif |