diff options
| -rw-r--r-- | .gitignore | 11 | ||||
| -rw-r--r-- | Makefile | 80 | ||||
| -rw-r--r-- | Makefile.extr | 134 | ||||
| -rwxr-xr-x | configure | 18 | ||||
| -rw-r--r-- | tools/modorder.ml | 112 |
5 files changed, 296 insertions, 59 deletions
@@ -19,10 +19,10 @@ cchecklink.byte clightgen clightgen.byte tools/ndfun +tools/modorder Makefile.config -# ocamlbuild's temp dir -_build/ # Generated files +.depend.extr compcert.ini ia32/ConstpropOp.v ia32/SelectOp.v @@ -32,6 +32,13 @@ arm/ConstpropOp.v arm/SelectOp.v backend/SelectDiv.v backend/SelectLong.v +backend/CMlexer.ml +backend/CMparser.ml +backend/CMparser.mli +cparser/Lexer.ml +cparser/pre_parser.ml +cparser/pre_parser.mli +lib/Tokenize.ml # Documentation doc/coq2html doc/coq2html.ml @@ -23,29 +23,12 @@ RECDIRS=lib common $(ARCH) backend cfrontend driver flocq exportclight cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) -CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction - -MENHIR=menhir COQC="$(COQBIN)coqc" -q $(COQINCLUDES) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source COQCHK="$(COQBIN)coqchk" $(COQINCLUDES) -OCAMLBUILD=ocamlbuild -OCB_OPTIONS=\ - -j 2 \ - -no-hygiene \ - -no-links \ - $(CAMLINCLUDES) -OCB_OPTIONS_CHECKLINK=\ - $(OCB_OPTIONS) \ - -I checklink \ - -use-ocamlfind -OCB_OPTIONS_CLIGHTGEN=\ - $(OCB_OPTIONS) \ - -I exportclight - VPATH=$(DIRS) GPATH=$(DIRS) @@ -74,7 +57,7 @@ LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \ Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v -# Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT)) +# Back-end modules (in backend/, $(ARCH)/) BACKEND=\ Cminor.v Op.v CminorSel.v \ @@ -129,14 +112,6 @@ DRIVER=Compopts.v Compiler.v Complements.v FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ $(PARSERVALIDATOR) $(PARSER) -# Symbolic links vs. copy - -ifneq (,$(findstring CYGWIN,$(shell uname -s))) -SLN=cp -else -SLN=ln -s -endif - all: $(MAKE) proof $(MAKE) extraction @@ -157,38 +132,28 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach $(COQEXEC) extraction/extraction.v touch extraction/STAMP -ccomp: extraction/STAMP compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ - && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp +.depend.extr: extraction/STAMP tools/modorder + $(MAKE) -f Makefile.extr depend -ccomp.prof: extraction/STAMP compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \ - && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof +ccomp: .depend.extr compcert.ini + $(MAKE) -f Makefile.extr ccomp +ccomp.byte: .depend.extr compcert.ini + $(MAKE) -f Makefile.extr ccomp.byte -ccomp.byte: extraction/STAMP compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \ - && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte +cchecklink: .depend.extr compcert.ini + $(MAKE) -f Makefile.extr cchecklink +cchecklink.byte: .depend.extr compcert.ini + $(MAKE) -f Makefile.extr cchecklink.byte + +clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo + $(MAKE) -f Makefile.extr clightgen +clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo + $(MAKE) -f Makefile.extr clightgen.byte runtime: $(MAKE) -C runtime -cchecklink: compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \ - && rm -f cchecklink && $(SLN) _build/checklink/Validator.native cchecklink - -cchecklink.byte: compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \ - && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte - -clightgen: extraction/STAMP compcert.ini exportclight/Clightdefs.vo - $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \ - && rm -f clightgen && $(SLN) _build/exportclight/Clightgen.native clightgen - -clightgen.byte: extraction/STAMP compcert.ini exportclight/Clightdefs.vo - $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \ - && rm -f clightgen.byte && $(SLN) _build/exportclight/Clightgen.d.byte clightgen.byte - -.PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte +.PHONY: proof extraction runtime documentation: doc/coq2html $(FILES) mkdir -p doc/html @@ -201,10 +166,12 @@ doc/coq2html: doc/coq2html.ml ocamlopt -o doc/coq2html str.cmxa doc/coq2html.ml doc/coq2html.ml: doc/coq2html.mll - ocamllex doc/coq2html.mll + ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml +tools/modorder: tools/modorder.ml + ocamlopt -o tools/modorder str.cmxa tools/modorder.ml latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) @@ -257,14 +224,13 @@ endif clean: rm -f $(patsubst %, %/*.vo, $(DIRS)) - rm -f ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte - rm -rf _build rm -rf doc/html doc/*.glob rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o rm -f compcert.ini - rm -f extraction/STAMP extraction/*.ml extraction/*.mli - rm -f tools/ndfun tools/*.cm? tools/*.o + rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr + rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o rm -f $(ARCH)/ConstpropOp.v $(ARCH)/SelectOp.v backend/SelectDiv.v backend/SelectLong.v + $(MAKE) -f Makefile.extr clean $(MAKE) -C runtime clean $(MAKE) -C test clean diff --git a/Makefile.extr b/Makefile.extr new file mode 100644 index 00000000..60fee407 --- /dev/null +++ b/Makefile.extr @@ -0,0 +1,134 @@ +####################################################################### +# # +# 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. # +# # +####################################################################### + +# Second-stage Makefile, after Coq extraction + +include Makefile.config + +DIRS=extraction \ + lib common $(ARCH) backend cfrontend cparser driver \ + exportclight + +ALLDIRS=$(DIRS) +ifeq ($(CCHECKLINK),true) +ALLDIRS+=checklink +endif + +INCLUDES=$(patsubst %,-I %, $(ALLDIRS)) + +WARNINGS=-w -3 +extraction/%.cmx: WARNINGS +=-w -20 +extraction/%.cmo: WARNINGS +=-w -20 + +BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o + +OCAMLC=ocamlc -g $(INCLUDES) $(WARNINGS) +OCAMLOPT=ocamlopt -g $(INCLUDES) $(WARNINGS) +OCAMLDEP=ocamldep $(INCLUDES) + +OCAMLC_P4=ocamlfind $(OCAMLC) $(BITSTRING) +OCAMLOPT_P4=ocamlfind $(OCAMLOPT) $(BITSTRING) +OCAMLDEP_P4=ocamlfind $(OCAMLDEP) $(BITSTRING) + +MENHIR=menhir --explain +OCAMLLEX=ocamllex -q +MODORDER=tools/modorder .depend.extr + +PARSERS=backend/CMparser.mly cparser/pre_parser.mly +LEXERS=backend/CMlexer.mll cparser/Lexer.mll lib/Tokenize.mll + +LIBS=str.cmxa + +EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte +GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) + +ifeq ($(wildcard .depend.extr),.depend.extr) + +CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) + +ccomp: $(CCOMP_OBJS) + @echo "Linking $@" + @$(OCAMLOPT) -o $@ $(LIBS) $+ + +ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) + @echo "Linking $@" + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ + +ifeq ($(CCHECKLINK),true) + +CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx) + +cchecklink: $(CCHECKLINK_OBJS) + @echo "Linking $@" + @$(OCAMLOPT_P4) -linkpkg -o $@ $(LIBS) $+ + +cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo) + @echo "Linking $@" + @$(OCAMLC_P4) -linkpkg -o $@ $(LIBS:.cmxa=.cma) $+ + +endif + +CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx) + +clightgen: $(CLIGHTGEN_OBJS) + @echo "Linking $@" + @$(OCAMLOPT) -o $@ $(LIBS) $+ + +clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo) + @echo "Linking $@" + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ + +include .depend.extr + +endif + +checklink/%.cmx: checklink/%.ml + @echo "OCAMLOPT $<" + @$(OCAMLOPT_P4) -c $< +checklink/%.cmo: checklink/%.ml + @echo "OCAMLC $<" + @$(OCAMLC_P4) -c $< +checklink/%.cmi: checklink/%.mli + @echo "OCAMLC $<" + @$(OCAMLC_P4) -c $< + +%.cmi: %.mli + @echo "OCAMLC $<" + @$(OCAMLC) -c $< +%.cmo: %.ml + @echo "OCAMLC $<" + @$(OCAMLC) -c $< +%.cmx: %.ml + @echo "OCAMLOPT $<" + @$(OCAMLOPT) -c $< + +%.ml %.mli: %.mly + $(MENHIR) $< +%.ml: %.mll + $(OCAMLLEX) $< + +clean: + rm -f $(EXECUTABLES) + rm -f $(GENERATED) + for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done + +depend: $(GENERATED) + @echo "Analyzing OCaml dependencies" + @for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr +ifeq ($(CCHECKLINK),true) + @$(OCAMLDEP_P4) checklink/*.mli checklink/*.ml >> .depend.extr +endif + + @@ -253,6 +253,23 @@ case "$menhir_ver" in missingtools=true;; esac +echo "Testing GNU make..." | tr -d '\n' +make='' +for mk in make gmake gnumake; do + make_ver=`$mk -v | head -1 | sed -n -e 's/^GNU Make //p'` + case "$make_ver" in + 3.8*|3.9*|[4-9].*) + echo "version $make_ver (command '$mk') -- good!" + make="$mk" + break;; + esac +done +if test -z "$make"; then + echo "NOT FOUND" + echo "Error: make sure GNU Make version 3.80 or later is installed." + missingtools=true +fi + if $missingtools; then echo "One or several required tools are missing or too old. Aborting." exit 2 @@ -403,6 +420,7 @@ CompCert configuration: Runtime library provided...... $has_runtime_lib Library files installed in.... $libdirexp cchecklink tool supported..... $cchecklink + Build command to use.......... $make If anything above looks wrong, please edit file ./Makefile.config to correct. diff --git a/tools/modorder.ml b/tools/modorder.ml new file mode 100644 index 00000000..34e157d0 --- /dev/null +++ b/tools/modorder.ml @@ -0,0 +1,112 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Parse dependencies generated by ocamldep and produce a linking order *) + +open Printf + +type status = Todo | Inprogress | Done + +type node = { + deps: string list; + result: string; + mutable status: status +} + +(* Parsing *) + +let re_continuation_line = Str.regexp "\\(.*\\)\\\\[ \t]*$" + +let re_depend_line = Str.regexp "\\([^ ]+\\) *:\\(.*\\)$" + +let re_whitespace = Str.regexp "[ \t\n]+" + +let parse_dependencies depfile = + let deps = (Hashtbl.create 63 : (string, node) Hashtbl.t) in + let ic = open_in depfile in + + let rec read_line () = + let l = input_line ic in + if Str.string_match re_continuation_line l 0 then begin + let l' = Str.matched_group 1 l in + l' ^ read_line () + end else + l in + + let enter_line l = + if not (Str.string_match re_depend_line l 0) then begin + eprintf "Warning: ill-formed dependency line '%s'\n" l + end else begin + let lhs = Str.matched_group 1 l + and rhs = Str.matched_group 2 l in + let node = { + deps = Str.split re_whitespace rhs; + result = rhs; + status = Todo + } in + Hashtbl.add deps lhs node + end in + + begin try + while true do enter_line (read_line ()) done + with End_of_file -> + () + end; + close_in ic; + deps + +(* Suffix of a file name *) + +let re_suffix = Str.regexp "\\.[a-zA-Z]+$" + +let filename_suffix s = + try + ignore (Str.search_forward re_suffix s 0); Str.matched_string s + with Not_found -> + "" + +(* Topological sorting *) + +let emit_dependencies deps targets = + + let rec dsort target suff = + match (try Some(Hashtbl.find deps target) with Not_found -> None) with + | None -> () + | Some node -> + match node.status with + | Done -> () + | Inprogress -> + eprintf "Warning: cyclic dependency on '%s', ignored\n" target + | Todo -> + node.status <- Inprogress; + List.iter + (fun dep -> + if Filename.check_suffix dep suff then dsort dep suff) + node.deps; + printf "%s " target; + node.status <- Done + in + Array.iter (fun t -> dsort t (filename_suffix t)) targets + +let _ = + if Array.length Sys.argv < 3 then begin + eprintf "Usage: modorder <dependency file> <target>...\n"; + exit 2 + end; + emit_dependencies + (parse_dependencies Sys.argv.(1)) + (Array.sub Sys.argv 2 (Array.length Sys.argv - 2)); + print_newline() + |