From ba9cd4f93ef991fa3794d333e8da19878df06e2d Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Sep 2010 09:29:08 +0000 Subject: Simplified stdlib wrapper; use it only under MacOS X git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Makefile | 3 +- configure | 35 ++++++++++--- driver/Driver.ml | 31 ++++++++---- runtime/Makefile | 14 ++++-- runtime/calloc.c | 28 ----------- runtime/stdio.c | 151 +++---------------------------------------------------- runtime/stdio.h | 92 ++++----------------------------- 7 files changed, 76 insertions(+), 278 deletions(-) delete mode 100644 runtime/calloc.c diff --git a/Makefile b/Makefile index 958bf9d..4237f2a 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,8 @@ driver/Configuration.ml: Makefile.config echo 'let linker = "$(CLINKER)"'; \ echo 'let arch = "$(ARCH)"'; \ echo 'let variant = "$(VARIANT)"'; \ - echo 'let system = "$(SYSTEM)"') \ + echo 'let system = "$(SYSTEM)"'; \ + echo 'let need_stdlib_wrapper = $(NEED_STDLIB_WRAPPER)') \ > driver/Configuration.ml depend: $(FILES) diff --git a/configure b/configure index d061396..d49428d 100755 --- a/configure +++ b/configure @@ -73,7 +73,8 @@ case "$target" in cprepro="gcc -arch ppc -U__GNUC__ -U__BLOCKS__ -E" casm="gcc -arch ppc -c" clinker="gcc -arch ppc" - libmath="";; + libmath="" + need_stdlib_wrapper="true";; powerpc-linux|ppc-linux) arch="powerpc" variant="eabi" @@ -82,7 +83,8 @@ case "$target" in cprepro="gcc -U__GNUC__ -E" casm="gcc -c" clinker="gcc" - libmath="-lm";; + libmath="-lm" + need_stdlib_wrapper="false";; arm-linux) arch="arm" variant="linux" @@ -91,7 +93,8 @@ case "$target" in cprepro="gcc -U__GNUC__ -E" casm="gcc -c" clinker="gcc" - libmath="-lm";; + libmath="-lm" + need_stdlib_wrapper="false";; ia32-linux) arch="ia32" variant="standard" @@ -100,7 +103,8 @@ case "$target" in cprepro="gcc -m32 -U__GNUC__ -E" casm="gcc -m32 -c" clinker="gcc -m32" - libmath="-lm";; + libmath="-lm" + need_stdlib_wrapper="false";; ia32-bsd) arch="ia32" variant="standard" @@ -109,7 +113,8 @@ case "$target" in cprepro="gcc -m32 -U__GNUC__ -E" casm="gcc -m32 -c" clinker="gcc -m32" - libmath="-lm";; + libmath="-lm" + need_stdlib_wrapper="false";; ia32-macosx) arch="ia32" variant="standard" @@ -118,7 +123,8 @@ case "$target" in cprepro="gcc -arch i386 -U__GNUC__ -U__BLOCKS__ -E" casm="gcc -arch i386 -c" clinker="gcc -arch i386" - libmath="";; + libmath="" + need_stdlib_wrapper="true";; manual) ;; "") @@ -150,6 +156,7 @@ CPREPRO=$cprepro CASM=$casm CLINKER=$clinker LIBMATH=$libmath +NEED_STDLIB_WRAPPER=$need_stdlib_wrapper EOF else cat >> Makefile.config <<'EOF' @@ -157,12 +164,14 @@ cat >> Makefile.config <<'EOF' # Target architecture # ARCH=powerpc # ARCH=arm +# ARCH=ia32 ARCH= # Target ABI # VARIANT=macosx # for PowerPC / MacOS X # VARIANT=eabi # for PowerPC / Linux and other SVR4 or EABI platforms # VARIANT=linux # for ARM +# VARIANT=standard # for IA32 VARIANT= # Target operating system and development environment @@ -172,6 +181,11 @@ VARIANT= # SYSTEM=diab # Possible choices for ARM: # SYSTEM=linux +# Possible choices for IA32: +# SYSTEM=linux +# SYSTEM=bsd +# SYSTEM=macosx +# SYSTEM=cygwin SYSTEM= # C compiler for compiling library files @@ -186,10 +200,14 @@ CASM=gcc -c # Linker CLINKER=gcc -# Math library +# Math library. Set to empty under MacOS X LIBMATH=-lm -# CIL configuration target -- do not change +# Do we need the thin wrapper around standard library and standard includes +# defined in directory runtime/ ? +# NEED_STDLIB_WRAPPER=true # for MacOS X +# NEED_STDLIB_WRAPPER=false # for other systems +NEED_STDLIB_WRAPPER= EOF fi @@ -218,6 +236,7 @@ CompCert configuration: Assembler..................... $casm Linker........................ $clinker Math library.................. $libmath + Needs wrapper around stdlib... $need_stdlib_wrapper Binaries installed in......... $bindirexp Library files installed in.... $libdirexp diff --git a/driver/Driver.ml b/driver/Driver.ml index 56bdb01..fcdc335 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -13,7 +13,7 @@ open Printf open Clflags -(* Location of the standard library *) +(* Location of the compatibility library *) let stdlib_path = ref( try @@ -47,9 +47,11 @@ let print_error oc msg = let preprocess ifile ofile = let cmd = - sprintf "%s -D__COMPCERT__ -I%s %s %s > %s" + sprintf "%s -D__COMPCERT__ %s %s %s > %s" Configuration.prepro - !stdlib_path + (if Configuration.need_stdlib_wrapper + then sprintf "-I%s" !stdlib_path + else "") (quote_options !prepro_options) ifile ofile in if command cmd <> 0 then begin @@ -102,7 +104,7 @@ let compile_c_file sourcename ifile ofile = set_dest PrintRTL.destination_cse option_dcse ".cse.rtl"; set_dest PrintLTLin.destination option_dalloc ".alloc.ltl"; (* Convert to Asm *) - let ppc = + let asm = match Compiler.transf_c_program csyntax with | Errors.OK x -> x | Errors.Error msg -> @@ -110,7 +112,7 @@ let compile_c_file sourcename ifile ofile = exit 2 in (* Save asm *) let oc = open_out ofile in - PrintAsm.print_program oc ppc; + PrintAsm.print_program oc asm; close_out oc (* From Cminor to asm *) @@ -161,11 +163,13 @@ let assemble ifile ofile = let linker exe_name files = let cmd = - sprintf "%s -o %s %s -L%s -lcompcert" + sprintf "%s -o %s %s %s" Configuration.linker (Filename.quote exe_name) (quote_options files) - !stdlib_path in + (if Configuration.need_stdlib_wrapper + then sprintf "-L%s -lcompcert" !stdlib_path + else "") in if command cmd <> 0 then exit 2 (* Processing of a .c file *) @@ -225,25 +229,32 @@ Preprocessing options: -U Undefine preprocessor symbol Language support options (use -fno- to turn off -f) : -fbitfields Emulate bit fields in structs [off] - -flonglong Treat 'long long' as 'long' and 'long double' as 'double' [off] + -flonglong Partial emulation of 'long long' types [on] -fstruct-passing Emulate passing structs and unions by value [off] -fstruct-assign Emulate assignment between structs or unions [off] -fvararg-calls Emulate calls to variable-argument functions [on] Code generation options: - -fmadd Use fused multiply-add and multiply-sub instructions + -fmadd Use fused multiply-add and multiply-sub instructions [off] -fsmall-data Set maximal size for allocation in small data area -fsmall-const Set maximal size for allocation in small constant area Tracing options: -dparse Save C file after parsing and elaboration in .parse.c -dc Save generated Compcert C in .compcert.c -dclight Save generated Clight in .light.c + -dcminor Save generated Cminor in .cm + -drtl Save unoptimized generated RTL in .rtl + -dtailcall Save RTL after tail call optimization in .tailcall.rtl + -dcastopt Save RTL after cast optimization in .castopt.rtl + -dconstprop Save RTL after constant propagation in .constprop.rtl + -dcse Save RTL after CSE optimization in .cse.rtl + -dalloc Save LTL after register allocation in .alloc.ltl -dasm Save generated assembly in .s Linking options: -l Link library -L Add to search path for libraries -o Generate executable in (default: a.out) General options: - -stdlib Set the path of the Compcert run-time library + -stdlib Set the path of the Compcert run-time library [MacOS X only] -v Print external commands before invoking them " diff --git a/runtime/Makefile b/runtime/Makefile index 5f1ddc6..ef8e21b 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -1,19 +1,27 @@ include ../Makefile.config CFLAGS=-O1 -g -Wall -OBJS=stdio.o calloc.o +OBJS=stdio.o LIB=libcompcert.a INCLUDES=stdio.h +ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true) +all: $(LIB) $(INCLUDES) +else +all: +endif + $(LIB): $(OBJS) rm -f $(LIB) ar rcs $(LIB) $(OBJS) -stdio.o: stdio.h - clean: rm -f *.o $(LIB) +ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true) install: install -d $(LIBDIR) install -c $(LIB) $(INCLUDES) $(LIBDIR) +else +install: +endif diff --git a/runtime/calloc.c b/runtime/calloc.c deleted file mode 100644 index 8e5e0b6..0000000 --- a/runtime/calloc.c +++ /dev/null @@ -1,28 +0,0 @@ -/* *********************************************************************/ -/* */ -/* The Compcert verified compiler */ -/* */ -/* Xavier Leroy, INRIA Paris-Rocquencourt */ -/* */ -/* Copyright Institut National de Recherche en Informatique et en */ -/* Automatique. All rights reserved. This file is distributed */ -/* under the terms of the GNU General Public License as published by */ -/* the Free Software Foundation, either version 2 of the License, or */ -/* (at your option) any later version. This file is also distributed */ -/* under the terms of the INRIA Non-Commercial License Agreement. */ -/* */ -/* *********************************************************************/ - -#include -#include -#include - -void * compcert_alloc(int sz) -{ - void * res = malloc(sz); - if (res == NULL) { - fprintf(stderr, "Out of memory in compcert_alloc().\n"); - abort(); - } - return res; -} diff --git a/runtime/stdio.c b/runtime/stdio.c index 5a2f33e..881a7fa 100644 --- a/runtime/stdio.c +++ b/runtime/stdio.c @@ -13,150 +13,11 @@ /* */ /* *********************************************************************/ -#include -#include -#define _INSIDE_COMPCERT_COMPATIBILITY_LIBRARY -#include "stdio.h" +/* Thin wrapper around stdio, redefining stdin, stdout and stderr. + Needed under MacOS X because of linking issues with dynamic libraries. */ -static compcert_FILE * compcert_alloc_file(FILE * f) -{ - struct compcert_FILE_ * r; - r = malloc(sizeof(struct compcert_FILE_)); - if (r == NULL) return NULL; - r->fstr = (void *) f; - return r; -} +#include "/usr/include/stdio.h" -compcert_FILE * compcert_stdin; -compcert_FILE * compcert_stdout; -compcert_FILE * compcert_stderr; - -static __attribute__((constructor)) void compcert_stdio_init(void) -{ - compcert_stdin = compcert_alloc_file(stdin); - compcert_stdout = compcert_alloc_file(stdout); - compcert_stderr = compcert_alloc_file(stderr); -} - -void compcert_clearerr(compcert_FILE * f) -{ - clearerr((FILE *)(f->fstr)); -} - -int compcert_fclose(compcert_FILE * f) -{ - int errcode = fclose((FILE *)(f->fstr)); - free(f); - return errcode; -} - -int compcert_feof(compcert_FILE * f) -{ - return feof((FILE *)(f->fstr)); -} - -int compcert_ferror(compcert_FILE * f) -{ - return ferror((FILE *)(f->fstr)); -} - -int compcert_fflush(compcert_FILE * f) -{ - return fflush((FILE *)(f->fstr)); -} - -int compcert_fgetc(compcert_FILE * f) -{ - return fgetc((FILE *)(f->fstr)); -} - -char *compcert_fgets(char * s, int n, compcert_FILE * f) -{ - return fgets(s, n, (FILE *)(f->fstr)); -} - -compcert_FILE *compcert_fopen(const char * p, const char * m) -{ - FILE * f = fopen(p, m); - if (f == NULL) return NULL; - return compcert_alloc_file(f); -} - -int compcert_fprintf(compcert_FILE * f, const char * s, ...) -{ - va_list ap; - int retcode; - va_start(ap, s); - retcode = vfprintf((FILE *)(f->fstr), s, ap); - va_end(ap); - return retcode; -} - -int compcert_fputc(int c, compcert_FILE * f) -{ - return fputc(c, (FILE *)(f->fstr)); -} - -int compcert_fputs(const char * s, compcert_FILE * f) -{ - return fputs(s, (FILE *)(f->fstr)); -} - -size_t compcert_fread(void * s, size_t p, size_t q, compcert_FILE * f) -{ - return fread(s, p, q, (FILE *)(f->fstr)); -} - -compcert_FILE *compcert_freopen(const char * s, const char * m, - compcert_FILE * f) -{ - FILE * nf = freopen(s, m, (FILE *)(f->fstr)); - if (nf == NULL) return NULL; - f->fstr = nf; - return f; -} - -int compcert_fscanf(compcert_FILE * f, const char * s, ...) -{ - va_list ap; - int retcode; - va_start(ap, s); - retcode = vfscanf((FILE *)(f->fstr), s, ap); - va_end(ap); - return retcode; -} - -int compcert_fseek(compcert_FILE * f, long p, int q) -{ - return fseek((FILE *)(f->fstr), p, q); -} - -long compcert_ftell(compcert_FILE *f) -{ - return ftell((FILE *)(f->fstr)); -} - -size_t compcert_fwrite(const void * b, size_t p, size_t q, compcert_FILE * f) -{ - return fwrite(b, p, q, (FILE *)(f->fstr)); -} - -int compcert_getc(compcert_FILE * f) -{ - return getc((FILE *)(f->fstr)); -} - -int compcert_putc(int c , compcert_FILE * f) -{ - return putc(c, (FILE *)(f->fstr)); -} - -void compcert_rewind(compcert_FILE * f) -{ - rewind((FILE *)(f->fstr)); -} - -int compcert_ungetc(int c, compcert_FILE * f) -{ - return ungetc(c, (FILE *)(f->fstr)); -} +FILE * compcert_stdin(void) { return stdin; } +FILE * compcert_stdout(void) { return stdout; } +FILE * compcert_stderr(void) { return stderr; } diff --git a/runtime/stdio.h b/runtime/stdio.h index 9aa3ae1..daf0198 100644 --- a/runtime/stdio.h +++ b/runtime/stdio.h @@ -13,97 +13,23 @@ /* */ /* *********************************************************************/ +/* Thin wrapper around stdio, redefining stdin, stdout and stderr. + Needed under MacOS X because of linking issues with dynamic libraries. */ + #ifndef _COMPCERT_STDIO_H #define _COMPCERT_STDIO_H -#ifdef __GNUC__ -#include_next "stdio.h" -#else #include "/usr/include/stdio.h" -#endif -typedef struct compcert_FILE_ { void * fstr; } compcert_FILE; +extern FILE * compcert_stdin(void); +extern FILE * compcert_stdout(void); +extern FILE * compcert_stderr(void); -extern compcert_FILE * compcert_stdin; -extern compcert_FILE * compcert_stdout; -extern compcert_FILE * compcert_stderr; -extern void compcert_clearerr(compcert_FILE *); -extern int compcert_fclose(compcert_FILE *); -extern int compcert_feof(compcert_FILE *); -extern int compcert_ferror(compcert_FILE *); -extern int compcert_fflush(compcert_FILE *); -extern int compcert_fgetc(compcert_FILE *); -extern char *compcert_fgets(char * , int, compcert_FILE *); -extern compcert_FILE *compcert_fopen(const char * , const char * ); -extern int compcert_fprintf(compcert_FILE * , const char * , ...); -extern int compcert_fputc(int, compcert_FILE *); -extern int compcert_fputs(const char * , compcert_FILE * ); -extern size_t compcert_fread(void * , size_t, size_t, compcert_FILE * ); -extern compcert_FILE *compcert_freopen(const char * , const char * , - compcert_FILE * ); -extern int compcert_fscanf(compcert_FILE * , const char * , ...); -extern int compcert_fseek(compcert_FILE *, long, int); -extern long compcert_ftell(compcert_FILE *); -extern size_t compcert_fwrite(const void * , size_t, size_t, compcert_FILE * ); -extern int compcert_getc(compcert_FILE *); -extern int compcert_putc(int, compcert_FILE *); -extern void compcert_rewind(compcert_FILE *); -extern int compcert_ungetc(int, compcert_FILE *); - -#ifndef _INSIDE_COMPCERT_COMPATIBILITY_LIBRARY -#define FILE compcert_FILE #undef stdin -#define stdin compcert_stdin +#define stdin (compcert_stdin()) #undef stdout -#define stdout compcert_stdout +#define stdout (compcert_stdout()) #undef stderr -#define stderr compcert_stderr -#undef clearerr -#define clearerr compcert_clearerr -#undef fclose -#define fclose compcert_fclose -#undef feof -#define feof compcert_feof -#undef ferror -#define ferror compcert_ferror -#undef fflush -#define fflush compcert_fflush -#undef fgetc -#define fgetc compcert_fgetc -#undef fgets -#define fgets compcert_fgets -#undef fopen -#define fopen compcert_fopen -#undef fprintf -#define fprintf compcert_fprintf -#undef fputc -#define fputc compcert_fputc -#undef fputs -#define fputs compcert_fputs -#undef fread -#define fread compcert_fread -#undef freopen -#define freopen compcert_freopen -#undef fscanf -#define fscanf compcert_fscanf -#undef fseek -#define fseek compcert_fseek -#undef ftell -#define ftell compcert_ftell -#undef fwrite -#define fwrite compcert_fwrite -#undef getc -#define getc compcert_getc -#undef getchar -#define getchar() compcert_getc(compcert_stdin) -#undef putc -#define putc compcert_putc -#undef putchar -#define putchar(c) compcert_putc(c, compcert_stdout) -#undef rewind -#define rewind compcert_rewind -#undef ungetc -#define ungetc compcert_ungetc -#endif +#define stderr (compcert_stderr()) #endif -- cgit v1.2.3