Various clean-ups

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9 files changed, 61 insertions, 75 deletions

diff --git a/Changelog b/Changelog
index 3e6840d..3be2d36 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 26a3f4d..14b8c29 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 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.//'