diff options
| -rw-r--r-- | Changelog | 8 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | VERSION | 3 | ||||
| -rw-r--r-- | backend/Constprop.v | 11 | ||||
| -rwxr-xr-x | configure | 32 | ||||
| -rw-r--r-- | driver/Driver.ml | 4 | ||||
| -rw-r--r-- | extraction/extraction.v | 3 | ||||
| -rw-r--r-- | ia32/Asm.v | 4 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 4 | ||||
| -rw-r--r-- | ia32/ConstpropOp.vp | 13 | ||||
| -rw-r--r-- | ia32/Op.v | 9 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 2 | ||||
| -rw-r--r-- | ia32/SelectOp.vp | 4 | ||||
| -rw-r--r-- | runtime/Makefile | 8 | ||||
| -rw-r--r-- | runtime/stdio.c | 23 | ||||
| -rw-r--r-- | runtime/stdio.h | 35 |
16 files changed, 53 insertions, 112 deletions
@@ -1,3 +1,11 @@ +Release 1.12 +======================== + +Other changes: +- IA32/MacOS X: now supports referencing global variables defined in shared + libraries; old hack for stdio is no longer needed. + + Release 1.11, 2012-07-13 ======================== @@ -190,7 +190,7 @@ driver/Configuration.ml: Makefile.config VERSION echo let arch = "\"$(ARCH)\""; \ echo let variant = "\"$(VARIANT)\""; \ echo let system = "\"$(SYSTEM)\""; \ - echo let need_stdlib_wrapper = $(NEED_STDLIB_WRAPPER); \ + echo let has_runtime_lib = $(HAS_RUNTIME_LIB); \ version=`cat VERSION`; \ echo let version = "\"$$version\"") \ > driver/Configuration.ml @@ -1 +1,2 @@ -1.11-devel +1.12 + diff --git a/backend/Constprop.v b/backend/Constprop.v index bc6a647..19e5d1a 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -251,6 +251,17 @@ Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident := | inr s => ros end. +Parameter generate_float_constants : unit -> bool. + +Definition const_for_result (a: approx) : option operation := + match a with + | I n => Some(Ointconst n) + | F n => if generate_float_constants tt then Some(Ofloatconst n) else None + | G symb ofs => Some(Oaddrsymbol symb ofs) + | S ofs => Some(Oaddrstack ofs) + | _ => None + end. + Definition transf_instr (gapp: global_approx) (app: D.t) (instr: instruction) := match instr with | Iop op args res s => @@ -62,6 +62,7 @@ done # Per-target configuration cchecklink=false +has_runtime_lib=false case "$target" in powerpc-macosx|ppc-macosx) @@ -72,8 +73,7 @@ case "$target" in cprepro="${toolprefix}gcc -arch ppc -U__GNUC__ -U__BLOCKS__ -E" casm="${toolprefix}gcc -arch ppc -c" clinker="${toolprefix}gcc -arch ppc" - libmath="" - need_stdlib_wrapper="true";; + libmath="";; powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi) arch="powerpc" variant="eabi" @@ -83,7 +83,6 @@ case "$target" in casm="${toolprefix}gcc -c" clinker="${toolprefix}gcc" libmath="-lm" - need_stdlib_wrapper="false" cchecklink=true;; powerpc-eabi-diab|ppc-eabi-diab) arch="powerpc" @@ -94,7 +93,6 @@ case "$target" in casm="${toolprefix}das" clinker="${toolprefix}dcc" libmath="-lm" - need_stdlib_wrapper="false" cchecklink=true;; arm-linux) arch="arm" @@ -104,8 +102,7 @@ case "$target" in cprepro="${toolprefix}gcc -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E" casm="${toolprefix}gcc -c" clinker="${toolprefix}gcc" - libmath="-lm" - need_stdlib_wrapper="false";; + libmath="-lm";; ia32-linux) arch="ia32" variant="standard" @@ -114,8 +111,7 @@ case "$target" in cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E" casm="${toolprefix}gcc -m32 -c" clinker="${toolprefix}gcc -m32" - libmath="-lm" - need_stdlib_wrapper="false";; + libmath="-lm";; ia32-bsd) arch="ia32" variant="standard" @@ -124,8 +120,7 @@ case "$target" in cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E" casm="${toolprefix}gcc -m32 -c" clinker="${toolprefix}gcc -m32" - libmath="-lm" - need_stdlib_wrapper="false";; + libmath="-lm";; ia32-macosx) arch="ia32" variant="standard" @@ -134,8 +129,7 @@ case "$target" in cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__BLOCKS__ -E" casm="${toolprefix}gcc -arch i386 -c" clinker="${toolprefix}gcc -arch i386" - libmath="" - need_stdlib_wrapper="true";; + libmath="";; ia32-cygwin) arch="ia32" variant="standard" @@ -144,8 +138,7 @@ case "$target" in cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E" casm="${toolprefix}gcc -m32 -c" clinker="${toolprefix}gcc -m32" - libmath="-lm" - need_stdlib_wrapper="false";; + libmath="-lm";; manual) ;; "") @@ -188,7 +181,7 @@ CPREPRO=$cprepro CASM=$casm CLINKER=$clinker LIBMATH=$libmath -NEED_STDLIB_WRAPPER=$need_stdlib_wrapper +HAS_RUNTIME_LIB=$has_runtime_lib CCHECKLINK=$cchecklink EOF else @@ -236,11 +229,8 @@ CLINKER=gcc # Math library. Set to empty under MacOS X LIBMATH=-lm -# 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= +# Obsolete; do not change +HAS_RUNTIME_LIB=false EOF fi @@ -269,8 +259,8 @@ CompCert configuration: Assembler..................... $casm Linker........................ $clinker Math library.................. $libmath - Needs wrapper around stdlib... $need_stdlib_wrapper Binaries installed in......... $bindirexp + Runtime library provided...... $has_runtime_lib Library files installed in.... $libdirexp cchecklink tool supported..... $cchecklink diff --git a/driver/Driver.ml b/driver/Driver.ml index 881a895..3ee4b6b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -60,7 +60,7 @@ let preprocess ifile ofile = let cmd = sprintf "%s -D__COMPCERT__ %s %s %s %s" Configuration.prepro - (if Configuration.need_stdlib_wrapper + (if Configuration.has_runtime_lib then sprintf "-I%s" !stdlib_path else "") (quote_options !prepro_options) @@ -210,7 +210,7 @@ let linker exe_name files = Configuration.linker (Filename.quote exe_name) (quote_options files) - (if Configuration.need_stdlib_wrapper + (if Configuration.has_runtime_lib then sprintf "-L%s -lcompcert" !stdlib_path else "") in if command cmd <> 0 then exit 2 diff --git a/extraction/extraction.v b/extraction/extraction.v index 02bdb60..b68c3a8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -16,6 +16,7 @@ Require Floats. Require RTLgen. Require Inlining. Require ConstpropOp. +Require Constprop. Require Coloring. Require Allocation. Require Compiler. @@ -59,7 +60,7 @@ Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_en (* Constprop *) Extract Constant ConstpropOp.propagate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 1". -Extract Constant ConstpropOp.generate_float_constants => +Extract Constant Constprop.generate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 2". (* Coloring *) @@ -108,7 +108,7 @@ Inductive instruction: Type := (** Moves *) | Pmov_rr (rd: ireg) (r1: ireg) (**r [mov] (32-bit int) *) | Pmov_ri (rd: ireg) (n: int) - | Pmov_raddr (rd: ireg) (id: ident) + | Pmov_ra (rd: ireg) (id: ident) | Pmov_rm (rd: ireg) (a: addrmode) | Pmov_mr (a: addrmode) (rs: ireg) | Pmovd_fr (rd: freg) (r1: ireg) (**r [movd] (32-bit int) *) @@ -459,7 +459,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr (rs#rd <- (rs r1))) m | Pmov_ri rd n => Next (nextinstr_nf (rs#rd <- (Vint n))) m - | Pmov_raddr rd id => + | Pmov_ra rd id => Next (nextinstr_nf (rs#rd <- (symbol_offset id Int.zero))) m | Pmov_rm rd a => exec_load Mint32 m a rs rd diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 5603d85..3fc3efb 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -322,9 +322,9 @@ Definition transl_op | Ofloatconst f, nil => do r <- freg_of res; OK ((if Float.eq_dec f Float.zero then Pxorpd_f r else Pmovsd_fi r f) :: k) - | Oaddrsymbol id, nil => + | Oindirectsymbol id, nil => do r <- ireg_of res; - OK (Pmov_raddr r id :: k) + OK (Pmov_ra r id :: k) | Ocast8signed, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k | Ocast8unsigned, a1 :: nil => diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index 0643296..ff5044f 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -145,19 +145,6 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) := | _, _ => Unknown end. -(** * Generation of constants *) - -Parameter generate_float_constants : unit -> bool. - -Definition const_for_result (a: approx) : option operation := - match a with - | I n => Some(Ointconst n) - | F n => if generate_float_constants tt then Some(Ofloatconst n) else None - | G symb ofs => Some(Olea (Aglobal symb ofs)) - | S ofs => Some(Olea (Ainstack ofs)) - | _ => None - end. - (** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of @@ -69,7 +69,7 @@ Inductive operation : Type := | Omove: operation (**r [rd = r1] *) | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) - | Oaddrsymbol: ident -> operation (**r [rd] is set to the address of the symbol *) + | Oindirectsymbol: ident -> operation (**r [rd] is set to the address of the symbol *) (*c Integer arithmetic: *) | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) | Ocast8unsigned: operation (**r [rd] is 8-bit zero extension of [r1] *) @@ -114,6 +114,7 @@ Inductive operation : Type := (** Derived operators. *) +Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id ofs). Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs). Definition Oaddimm (n: int) : operation := Olea (Aindexed n). @@ -193,7 +194,7 @@ Definition eval_operation | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) - | Oaddrsymbol id, nil => Some (symbol_address genv id Int.zero) + | Oindirectsymbol id, nil => Some (symbol_address genv id Int.zero) | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) @@ -277,7 +278,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) | Ofloatconst _ => (nil, Tfloat) - | Oaddrsymbol _ => (nil, Tint) + | Oindirectsymbol _ => (nil, Tint) | Ocast8signed => (Tint :: nil, Tint) | Ocast8unsigned => (Tint :: nil, Tint) | Ocast16signed => (Tint :: nil, Tint) @@ -542,7 +543,7 @@ Definition two_address_op (op: operation) : bool := | Omove => false | Ointconst _ => false | Ofloatconst _ => false - | Oaddrsymbol _ => false + | Oindirectsymbol _ => false | Ocast8signed => false | Ocast8unsigned => false | Ocast16signed => false diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index ec3cf2a..8b795ee 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -511,7 +511,7 @@ let print_instruction oc = function fprintf oc " movl %a, %a\n" ireg r1 ireg rd | Pmov_ri(rd, n) -> fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd - | Pmov_raddr(rd, id) -> + | Pmov_ra(rd, id) -> if target = MacOS then begin let id = extern_atom id in indirect_symbols := StringSet.add id !indirect_symbols; diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 19e64cc..6d44cf5 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -62,8 +62,8 @@ Parameter symbol_is_external: ident -> bool. Definition addrsymbol (id: ident) (ofs: int) := if symbol_is_external id then if Int.eq ofs Int.zero - then Eop (Oaddrsymbol id) Enil - else Eop (Olea (Aindexed ofs)) (Eop (Oaddrsymbol id) Enil ::: Enil) + then Eop (Oindirectsymbol id) Enil + else Eop (Olea (Aindexed ofs)) (Eop (Oindirectsymbol id) Enil ::: Enil) else Eop (Olea (Aglobal id ofs)) Enil. diff --git a/runtime/Makefile b/runtime/Makefile index ef8e21b..c128ba2 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -1,11 +1,11 @@ include ../Makefile.config CFLAGS=-O1 -g -Wall -OBJS=stdio.o +INCLUDES= +OBJS= LIB=libcompcert.a -INCLUDES=stdio.h -ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true) +ifeq ($(strip $(HAS_RUNTIME_LIB)),true) all: $(LIB) $(INCLUDES) else all: @@ -18,7 +18,7 @@ $(LIB): $(OBJS) clean: rm -f *.o $(LIB) -ifeq ($(strip $(NEED_STDLIB_WRAPPER)),true) +ifeq ($(strip $(HAS_RUNTIME_LIB)),true) install: install -d $(LIBDIR) install -c $(LIB) $(INCLUDES) $(LIBDIR) diff --git a/runtime/stdio.c b/runtime/stdio.c deleted file mode 100644 index 881a7fa..0000000 --- a/runtime/stdio.c +++ /dev/null @@ -1,23 +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. */ -/* */ -/* *********************************************************************/ - -/* Thin wrapper around stdio, redefining stdin, stdout and stderr. - Needed under MacOS X because of linking issues with dynamic libraries. */ - -#include "/usr/include/stdio.h" - -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 deleted file mode 100644 index daf0198..0000000 --- a/runtime/stdio.h +++ /dev/null @@ -1,35 +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. */ -/* */ -/* *********************************************************************/ - -/* 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 - -#include "/usr/include/stdio.h" - -extern FILE * compcert_stdin(void); -extern FILE * compcert_stdout(void); -extern FILE * compcert_stderr(void); - -#undef stdin -#define stdin (compcert_stdin()) -#undef stdout -#define stdout (compcert_stdout()) -#undef stderr -#define stderr (compcert_stderr()) - -#endif |