From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- runtime/Makefile | 13 +++++ runtime/calloc.c | 13 +++++ runtime/stdio.c | 152 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ runtime/stdio.h | 67 ++++++++++++++++++++++++ 4 files changed, 245 insertions(+) create mode 100644 runtime/Makefile create mode 100644 runtime/calloc.c create mode 100644 runtime/stdio.c create mode 100644 runtime/stdio.h (limited to 'runtime') diff --git a/runtime/Makefile b/runtime/Makefile new file mode 100644 index 0000000..c45c9fb --- /dev/null +++ b/runtime/Makefile @@ -0,0 +1,13 @@ +CFLAGS=-arch ppc -O1 -g -Wall +#CFLAGS=-O1 -g -Wall +OBJS=stdio.o calloc.o +LIB=libcompcert.a + +$(LIB): $(OBJS) + rm -f $(LIB) + ar rcs $(LIB) $(OBJS) + +stdio.o: stdio.h + +clean: + rm -f *.o $(LIB) diff --git a/runtime/calloc.c b/runtime/calloc.c new file mode 100644 index 0000000..2526ceb --- /dev/null +++ b/runtime/calloc.c @@ -0,0 +1,13 @@ +#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 new file mode 100644 index 0000000..c153257 --- /dev/null +++ b/runtime/stdio.c @@ -0,0 +1,152 @@ +#include +#include +#define _INSIDE_COMPCERT_COMPATIBILITY_LIBRARY +#include "stdio.h" + +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; +} + +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)); +} + +int compcert_vfprintf(compcert_FILE * f, const char * s, va_list va) +{ + return vfprintf((FILE *)(f->fstr), s, va); +} diff --git a/runtime/stdio.h b/runtime/stdio.h new file mode 100644 index 0000000..2442dcb --- /dev/null +++ b/runtime/stdio.h @@ -0,0 +1,67 @@ +#ifndef _COMPCERT_STDIO_H +#define _COMPCERT_STDIO_H + +#include "/usr/include/stdio.h" + +typedef struct compcert_FILE_ { void * fstr; } compcert_FILE; + +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 *); +extern int compcert_vfprintf(compcert_FILE *, const char *, va_list); + +#ifndef _INSIDE_COMPCERT_COMPATIBILITY_LIBRARY +#define FILE compcert_FILE +#undef stdin +#define stdin compcert_stdin +#undef stdout +#define stdout compcert_stdout +#undef stderr +#define stderr compcert_stderr +#define clearerr compcert_clearerr +#define fclose compcert_fclose +#define feof compcert_feof +#define ferror compcert_ferror +#define fflush compcert_fflush +#define fgetc compcert_fgetc +#define fgets compcert_fgets +#define fopen compcert_fopen +#define fprintf compcert_fprintf +#define fputc compcert_fputc +#define fputs compcert_fputs +#define fread compcert_fread +#define freopen compcert_freopen +#define fscanf compcert_fscanf +#define fseek compcert_fseek +#define ftell compcert_ftell +#define fwrite compcert_fwrite +#define getc compcert_getc +#define putc compcert_putc +#define rewind compcert_rewind +#define ungetc compcert_ungetc +#define vfprintf compcert_vfprintf +#endif + +#endif -- cgit v1.2.3