diff --git a/Changelog b/Changelog
index 3e6840d93e902e4d87ec71dc06f65753aa34df3f..3be2d361323ce406e6e400d07d6310a7d961177e 100644
--- a/Changelog
+++ b/Changelog
@@ -1,5 +1,5 @@
-Release 1.4,
-========================
+Release 1.4, 2009-04-20
+=======================
- Modularized the processor dependencies in the back-end.
diff --git a/Makefile b/Makefile
index 26a3f4dfd125ed125f34e89dbd015dd164bd48c7..14b8c29be03debb15ee8d11bc1b14659009b0743 100644
--- a/Makefile
+++ b/Makefile
@@ -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 f51a15b7e2e77a6b1e6c2ac53b49e21168458a0e..da0b5d102af2028b526a70b93e3ee99a5b6f5d1a 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 e9feb53460d4f8fc4c19ff3cf93d95100d0edc07..efaf42e4b0b0ee3fe79f9413b1f81fe1dc817f7f 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 f300af940c57e72c947992e9a5c677eb5a99b49e..a5741f5978711b90289ceb9b33c648b8e42cec66 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.
@@ -171,6 +171,13 @@ code.
<A HREF="html/RTLgenproof.html">RTLgenproof</A></TD>
</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>
diff --git a/extraction/Makefile b/extraction/Makefile
deleted file mode 100644
index 0aee0be6f2ac58949be4f3c99b696b9df4552523..0000000000000000000000000000000000000000
--- 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 58da9c0615db528aa90fc0ab5c098bbf38af641b..d74e192edad6871807b82c76c3c2d3929d8ac6e8 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 0000000000000000000000000000000000000000..1ee3c484da3912f55dde4e7271b1fd68961f27d9
--- /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 d724b8fdeb8994a62913d2f8d773672804d7a586..0000000000000000000000000000000000000000
--- a/extraction/uncapitalize
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-echo $1 | sed -e 'h
-s/\(.\).*/\1/
-y/ABCDEFGHIJKLMNOPQRSTUVWXYZ/abcdefghijklmnopqrstuvwxyz/
-G
-s/\n.//'