Commit ba9cd4f9 authored by xleroy's avatar xleroy
Browse files

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
parent 601569c2
......@@ -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)
......
......@@ -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
......
......@@ -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
"
......
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
/* *********************************************************************/
/* */
/* 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;
}
......@@ -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; }
......@@ -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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment