diff options
| -rw-r--r-- | Changelog | 4 | ||||
| -rw-r--r-- | Makefile | 37 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 3 | ||||
| -rw-r--r-- | cfrontend/Cil2Csyntax.ml | 10 | ||||
| -rw-r--r-- | doc/index.html | 11 | ||||
| -rw-r--r-- | extraction/Makefile | 48 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 | ||||
| -rwxr-xr-x | extraction/fixextract | 15 | ||||
| -rwxr-xr-x | extraction/uncapitalize | 6 |
9 files changed, 61 insertions, 75 deletions
@@ -1,5 +1,5 @@ -Release 1.4, -======================== +Release 1.4, 2009-04-20 +======================= - Modularized the processor dependencies in the back-end. @@ -12,10 +12,15 @@ include Makefile.config +DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver + +INCLUDES=$(patsubst %,-I %, $(DIRS)) + COQC=coqc $(INCLUDES) COQDEP=coqdep $(INCLUDES) -#COQC=/Users/sandrineblazy/SWtrunkcoq/bin/coqc $(INCLUDES) COQDOC=coqdoc +COQEXEC=coqtop $(INCLUDES) -batch -load-vernac-source + OCAMLBUILD=ocamlbuild OCB_OPTIONS=\ -no-hygiene \ @@ -25,11 +30,8 @@ OCB_OPTIONS=\ -lflags -I,`pwd`/cil/obj/$(ARCHOS) \ -libs unix,str,cil -DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver - VPATH=$(DIRS) GPATH=$(DIRS) -INCLUDES=$(patsubst %,-I %, $(DIRS)) # General-purpose libraries (in lib/) @@ -83,16 +85,18 @@ FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) proof: $(FILES:.v=.vo) extraction: - $(MAKE) -C extraction + rm -f extraction/*.ml extraction/*.mli + $(COQEXEC) extraction/extraction.v + cd extraction && ./fixextract cil: $(MAKE) -j1 -C cil -ccomp: +ccomp: driver/Configuration.ml $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ && rm -f ccomp && ln -s _build/driver/Driver.native ccomp -ccomp.byte: +ccomp.byte: driver/Configuration.ml $(OCAMLBUILD) $(OCB_OPTIONS) Driver.byte \ && rm -f ccomp.byte && ln -s _build/driver/Driver.byte ccomp.byte @@ -108,8 +112,7 @@ all: $(MAKE) ccomp $(MAKE) runtime -documentation: doc/removeproofs - @ln -f $(FILES) doc/ +documentation: doc/removeproofs documentation-link @mkdir -p doc/html cd doc; $(COQDOC) --html -d html \ $(FILES:%.v=--glob-from %.glob) $(FILES) @@ -117,6 +120,9 @@ documentation: doc/removeproofs cp doc/coqdoc.css doc/html/coqdoc.css doc/removeproofs doc/html/*.html +documentation-link: $(FILES) + @ln -f $^ doc/ + doc/removeproofs: doc/removeproofs.ml ocamlopt -o doc/removeproofs doc/removeproofs.ml @@ -133,6 +139,16 @@ latexdoc: @echo "COQC $*.v" @$(COQC) -dump-glob doc/$(*F).glob $*.v +driver/Configuration.ml: Makefile.config + (echo 'let stdlib_path = "$(LIBDIR)"'; \ + echo 'let prepro = "$(CPREPRO)"'; \ + echo 'let asm = "$(CASM)"'; \ + echo 'let linker = "$(CLINKER)"'; \ + echo 'let arch = "$(ARCH)"'; \ + echo 'let variant = "$(VARIANT)"'; \ + echo 'let system = "$(SYSTEM)"') \ + > driver/Configuration.ml + depend: $(COQDEP) $(patsubst %, %/*.v, $(DIRS)) \ | sed -e 's|$(ARCH)/$(VARIANT)/|$$(ARCH)/$$(VARIANT)/|g' \ @@ -150,7 +166,8 @@ clean: rm -rf _build rm -rf doc/html doc/*.glob rm -f doc/removeproofs.ml doc/removeproofs - $(MAKE) -C extraction clean + rm -f driver/Configuration.ml + rm -f extraction/*.ml extraction/*.mli $(MAKE) -C runtime clean $(MAKE) -C test/cminor clean $(MAKE) -C test/c clean diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index f51a15b..da0b5d1 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -178,8 +178,7 @@ let call_helper oc fn dst arg1 arg2 = (* Move result to dst *) begin match dst with | IR0 -> () - | _ -> - fprintf oc " mov %a, r0\n" ireg dst + | _ -> fprintf oc " mov %a, r0\n" ireg dst end; (* Restore the other caller-save registers *) fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave; diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml index e9feb53..efaf42e 100644 --- a/cfrontend/Cil2Csyntax.ml +++ b/cfrontend/Cil2Csyntax.ml @@ -557,11 +557,11 @@ let makeFuncall1 tyfun (Expr(_, tlhs) as elhs) efun eargs = | TFun (t, _, _, _) -> let tres = convertTyp t in if tlhs = tres then - Scall(Datatypes.Some elhs, efun, eargs) + Scall(Some elhs, efun, eargs) else begin let tmp = make_temp t in let elhs' = Expr(Evar tmp, tres) in - Ssequence(Scall(Datatypes.Some elhs', efun, eargs), + Ssequence(Scall(Some elhs', efun, eargs), Sassign(elhs, Expr(Ecast(tlhs, elhs'), tlhs))) end | _ -> internal_error "wrong type for function in call" @@ -590,7 +590,7 @@ let rec processInstrList l = | Call (None, e, eList, loc) -> updateLoc(loc); let (efun, params) = convertExpFuncall e eList in - Scall(Datatypes.None, efun, params) + Scall(None, efun, params) | Call (Some lv, e, eList, loc) -> updateLoc(loc); let (efun, params) = convertExpFuncall e eList in @@ -679,8 +679,8 @@ and convertStmt s = | Return (eOpt, loc) -> updateLoc(loc); let eOpt' = match eOpt with - | None -> Datatypes.None - | Some e -> Datatypes.Some (convertExp e) + | None -> None + | Some e -> Some (convertExp e) in Sreturn eOpt' | Goto (_, loc) -> diff --git a/doc/index.html b/doc/index.html index f300af9..a5741f5 100644 --- a/doc/index.html +++ b/doc/index.html @@ -60,7 +60,7 @@ overview papers above were written.</P> <A HREF="http://compcert.inria.fr/">the Compcert Web site</A>.</P> <P>This document and the Compcert sources are -copyright 2005, 2006, 2007, 2008 Institut National de Recherche en +copyright 2005, 2006, 2007, 2008, 2009 Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following <A HREF="LICENSE">license</A>. </P> @@ -119,7 +119,7 @@ code, control-flow graph, finitely many physical registers, infinitely many stack slots). <BR> See also: <A HREF="html/Locations.html">Locations</A> (representation of locations). -<LI> <A HREF="html/LTL.html">LTLin</A>: like LTL, but the CFG is +<LI> <A HREF="html/LTLin.html">LTLin</A>: like LTL, but the CFG is replaced by a linear list of instructions with explicit branches and labels. <LI> <A HREF="html/Linear.html">Linear</A>: like LTLin, with explicit spilling, reloading and enforcement of calling conventions. @@ -172,6 +172,13 @@ code. </TR> <TR valign="top"> + <TD>Recognition of tail calls</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/Tailcall.html">Tailcall</A></TD> + <TD><A HREF="html/Tailcallproof.html">Tailcallproof</A></TD> +</TR> + +<TR valign="top"> <TD>Constant propagation</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/Constprop.html">Constprop</A></TD> diff --git a/extraction/Makefile b/extraction/Makefile deleted file mode 100644 index 0aee0be..0000000 --- a/extraction/Makefile +++ /dev/null @@ -1,48 +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 INRIA Non-Commercial License Agreement. # -# # -####################################################################### - -include ../Makefile.config - -DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver - -COQINCL=$(patsubst %,-I ../%,$(DIRS)) -COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source - -all: Configuration.ml extraction - -extraction: - rm -f [:lower:]*.mli [:lower:]*.ml - $(COQEXEC) extraction.v - @echo "Fixing file names..." - @mv list.ml CoqList.ml - @mv list.mli CoqList.mli - @mv string.ml CoqString.ml - @mv string.mli CoqString.mli - @mv int.ml CoqInt.ml - @mv int.mli CoqInt.mli - @echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..." - @./convert *.mli *.ml - @echo "Patching files..." - @for i in *.patch; do patch < $$i; done - -Configuration.ml: ../Makefile.config - (echo 'let stdlib_path = "$(LIBDIR)"'; \ - echo 'let prepro = "$(CPREPRO)"'; \ - echo 'let asm = "$(CASM)"'; \ - echo 'let linker = "$(CLINKER)"'; \ - echo 'let arch = "$(ARCH)"'; \ - echo 'let variant = "$(VARIANT)"'; \ - echo 'let system = "$(SYSTEM)"') \ - > Configuration.ml - -clean: - rm -f *.mli *.ml diff --git a/extraction/extraction.v b/extraction/extraction.v index 58da9c0..d74e192 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -22,6 +22,7 @@ Require Compiler. Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. +Extract Inductive option => "option" [ "Some" "None" ]. Extract Inductive List.list => "list" [ "[]" "(::)" ]. (* Float *) @@ -82,4 +83,5 @@ Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y". Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". (* Go! *) +Cd "extraction". Recursive Extraction Library Compiler. diff --git a/extraction/fixextract b/extraction/fixextract new file mode 100755 index 0000000..1ee3c48 --- /dev/null +++ b/extraction/fixextract @@ -0,0 +1,15 @@ +#!/bin/sh + +echo "Fixing file names..." +mv list.ml CoqList.ml +mv list.mli CoqList.mli +mv string.ml CoqString.ml +mv string.mli CoqString.mli +mv int.ml CoqInt.ml +mv int.mli CoqInt.mli + +echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..." +./convert *.mli *.ml + +echo "Patching files..." +for i in *.patch; do patch < $i; done diff --git a/extraction/uncapitalize b/extraction/uncapitalize deleted file mode 100755 index d724b8f..0000000 --- a/extraction/uncapitalize +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh -echo $1 | sed -e 'h -s/\(.\).*/\1/ -y/ABCDEFGHIJKLMNOPQRSTUVWXYZ/abcdefghijklmnopqrstuvwxyz/ -G -s/\n.//' |