From d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 17 Apr 2009 13:27:48 +0000 Subject: Various clean-ups git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 4 ++-- Makefile | 37 +++++++++++++++++++++++++++---------- arm/PrintAsm.ml | 3 +-- cfrontend/Cil2Csyntax.ml | 10 +++++----- doc/index.html | 11 +++++++++-- extraction/Makefile | 48 ------------------------------------------------ extraction/extraction.v | 2 ++ extraction/fixextract | 15 +++++++++++++++ extraction/uncapitalize | 6 ------ 9 files changed, 61 insertions(+), 75 deletions(-) delete mode 100644 extraction/Makefile create mode 100755 extraction/fixextract delete mode 100755 extraction/uncapitalize diff --git a/Changelog b/Changelog index 3e6840d9..3be2d361 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 26a3f4df..14b8c29b 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 f51a15b7..da0b5d10 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 e9feb534..efaf42e4 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 f300af94..a5741f59 100644 --- a/doc/index.html +++ b/doc/index.html @@ -60,7 +60,7 @@ overview papers above were written.

the Compcert Web site.

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 license.

@@ -119,7 +119,7 @@ code, control-flow graph, finitely many physical registers, infinitely many stack slots).
See also: Locations (representation of locations). -
  • LTLin: like LTL, but the CFG is +
  • LTLin: like LTL, but the CFG is replaced by a linear list of instructions with explicit branches and labels.
  • Linear: like LTLin, with explicit spilling, reloading and enforcement of calling conventions. @@ -171,6 +171,13 @@ code. RTLgenproof + + Recognition of tail calls + RTL to RTL + Tailcall + Tailcallproof + + Constant propagation RTL to RTL diff --git a/extraction/Makefile b/extraction/Makefile deleted file mode 100644 index 0aee0be6..00000000 --- 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 58da9c06..d74e192e 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 00000000..1ee3c484 --- /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 d724b8fd..00000000 --- a/extraction/uncapitalize +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh -echo $1 | sed -e 'h -s/\(.\).*/\1/ -y/ABCDEFGHIJKLMNOPQRSTUVWXYZ/abcdefghijklmnopqrstuvwxyz/ -G -s/\n.//' -- cgit