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

7 files changed, 76 insertions, 278 deletions

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<symb>       Undefine preprocessor symbol
 Language support options (use -fno-<opt> to turn off -f<opt>) :
   -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 <n>  Set maximal size <n> for allocation in small data area
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
 Tracing options:
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
   -dc            Save generated Compcert C in <file>.compcert.c
   -dclight       Save generated Clight in <file>.light.c
+  -dcminor       Save generated Cminor in <file>.cm
+  -drtl          Save unoptimized generated RTL in <file>.rtl
+  -dtailcall     Save RTL after tail call optimization in <file>.tailcall.rtl
+  -dcastopt      Save RTL after cast optimization in <file>.castopt.rtl
+  -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
+  -dcse          Save RTL after CSE optimization in <file>.cse.rtl
+  -dalloc        Save LTL after register allocation in <file>.alloc.ltl
   -dasm          Save generated assembly in <file>.s
 Linking options:
   -l<lib>        Link library <lib>
   -L<dir>        Add <dir> to search path for libraries
   -o <file>      Generate executable in <file> (default: a.out)
 General options:
-  -stdlib <dir>  Set the path of the Compcert run-time library
+  -stdlib <dir>  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 <stdio.h>
-#include <stddef.h>
-#include <stdlib.h>
-
-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 <stdarg.h>
-#include <stdlib.h>
-#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