diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2014-12-18 13:52:12 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2014-12-18 13:52:12 +0100 |
commit | 04292034ef23e8cfdab593b7d248368085631881 (patch) | |
tree | 4e2d24c2ba129f68da014ea13212a25731d74b9e | |
parent | c1daedb244d1f7586c12749642b0d78ae910e60a (diff) | |
parent | 3262e1e2e71b4fad5d5c47603aafb4dcb2539e27 (diff) | |
download | compcert-04292034ef23e8cfdab593b7d248368085631881.tar.gz compcert-04292034ef23e8cfdab593b7d248368085631881.zip |
Merge pull request #3 from AbsInt/pure-makefiles
Merge of the pure-makefiles branch, which uses Makefiles instead of ocamlbuild to build the Caml code.
-rw-r--r-- | .gitignore | 11 | ||||
-rw-r--r-- | Makefile | 72 | ||||
-rw-r--r-- | Makefile.extr | 168 | ||||
-rw-r--r-- | _tags | 9 | ||||
-rwxr-xr-x | configure | 47 | ||||
-rw-r--r-- | myocamlbuild.ml | 14 | ||||
-rw-r--r-- | tools/modorder.ml | 112 | ||||
-rw-r--r-- | tools/ndfun.ml | 23 |
8 files changed, 371 insertions, 85 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,9 +23,6 @@ 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" @@ -33,20 +30,6 @@ COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source COQCHK="$(COQBIN)coqchk" $(COQINCLUDES) CP=cp -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) @@ -75,7 +58,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 \ @@ -151,38 +134,30 @@ 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 \ - && $(CP) _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 \ - && $(CP) _build/driver/Driver.p.native ccomp.prof +ccomp: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr ccomp +ccomp.byte: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr ccomp.byte -ccomp.byte: extraction/STAMP compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \ - && $(CP) _build/driver/Driver.d.byte ccomp.byte +cchecklink: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr cchecklink +cchecklink.byte: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr cchecklink.byte + +clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE + $(MAKE) -f Makefile.extr clightgen +clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE + $(MAKE) -f Makefile.extr clightgen.byte runtime: $(MAKE) -C runtime -cchecklink: compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \ - && $(CP) _build/checklink/Validator.native cchecklink - -cchecklink.byte: compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \ - && $(CP) _build/checklink/Validator.d.byte cchecklink.byte - -clightgen: extraction/STAMP compcert.ini exportclight/Clightdefs.vo - $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \ - && $(CP) _build/exportclight/Clightgen.native clightgen - -clightgen.byte: extraction/STAMP compcert.ini exportclight/Clightdefs.vo - $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \ - && $(CP) _build/exportclight/Clightgen.d.byte clightgen.byte +FORCE: -.PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte +.PHONY: proof extraction runtime FORCE documentation: doc/coq2html $(FILES) mkdir -p doc/html @@ -195,10 +170,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) @@ -251,14 +228,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..35ae5f7b --- /dev/null +++ b/Makefile.extr @@ -0,0 +1,168 @@ +####################################################################### +# # +# 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 + +# Directories containing plain Caml code (no preprocessing) + +DIRS=extraction \ + lib common $(ARCH) backend cfrontend cparser driver \ + exportclight + +# Directories containing Caml code that must be preprocessed by Camlp4 + +ifeq ($(CCHECKLINK),true) +DIRS_P4=checklink +else +DIRS_P4= +endif + +ALLDIRS=$(DIRS) $(DIRS_P4) + +INCLUDES=$(patsubst %,-I %, $(ALLDIRS)) + +# Control of warnings: +# warning 3 = deprecated feature. Turned off for OCaml 4.02 (bytes vs strings) +# warning 20 = unused function argument. There are some in extracted code + +WARNINGS=-w -3 +extraction/%.cmx: WARNINGS +=-w -20 +extraction/%.cmo: WARNINGS +=-w -20 + +COMPFLAGS=-g $(INCLUDES) $(WARNINGS) + +# Using the bitstring library and syntax extension (for checklink) + +BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o + +# Using .opt compilers if available + +ifeq ($(OCAML_OPT_COMP),true) +DOTOPT=.opt +else +DOTOPT= +endif + +# Compilers used for non-preprocessed code + +OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS) +OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS) +OCAMLDEP=ocamldep$(DOTOPT) $(INCLUDES) + +# Compilers used for Camlp4-preprocessed code. Note that we cannot +# use the .opt compilers (because ocamlfind doesn't support them). + +OCAMLC_P4=ocamlfind ocamlc $(COMPFLAGS) $(BITSTRING) +OCAMLOPT_P4=ocamlfind ocamlopt $(COMPFLAGS) $(BITSTRING) +OCAMLDEP_P4=ocamlfind ocamldep $(INCLUDES) $(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) + +# Beginning of part that assumes .depend.extr already exists + +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 + +# End of part that assumes .depend.extr already exists + +checklink/%.cmi: checklink/%.mli + @echo "OCAMLC $<" + @$(OCAMLC_P4) -c $< +checklink/%.cmo: checklink/%.ml + @echo "OCAMLC $<" + @$(OCAMLC_P4) -c $< +checklink/%.cmx: checklink/%.ml + @echo "OCAMLOPT $<" + @$(OCAMLOPT_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 + +# Generation of .depend.extr + +depend: $(GENERATED) + @echo "Analyzing OCaml dependencies" + @for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr +ifneq ($(strip $(DIRS_P4)),) + @for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .depend.extr +endif + + @@ -1,9 +0,0 @@ -true: use_menhir -<**/*.cmx>: debug -<**/*.native>: debug -<driver/Driver.*{byte,native}>: use_unix,use_str -<exportclight/Clightgen.*{byte,native}>: use_unix,use_str -<checklink/*.ml>: pkg_bitstring -<checklink/Validator.*{byte,native}>: pkg_unix,pkg_str,pkg_bitstring -<extraction/*.ml>: warn(-20) -<**/*.ml>: warn(-3) @@ -213,7 +213,7 @@ fi missingtools=false echo "Testing Coq... " | tr -d '\n' -coq_ver=`coqc -v | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p'` +coq_ver=`coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p'` case "$coq_ver" in 8.4pl*) echo "version $coq_ver -- good!";; @@ -223,14 +223,14 @@ case "$coq_ver" in missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure Coq version 8.4pl4 is installed." + echo "Error: make sure Coq version 8.4 pl5 is installed." missingtools=true;; esac echo "Testing OCaml... " | tr -d '\n' -ocaml_ver=`ocamlc -version` +ocaml_ver=`ocamlopt -version 2>/dev/null` case "$ocaml_ver" in - 4.*) + [4-9].*) echo "version $ocaml_ver -- good!";; ?.*) echo "version $ocaml_ver -- UNSUPPORTED" @@ -242,17 +242,48 @@ case "$ocaml_ver" in missingtools=true;; esac +echo "Testing OCaml .opt compilers... " | tr -d '\n' +ocaml_opt_ver=`ocamlopt.opt -version 2>/dev/null` +if test "$ocaml_opt_ver" = "$ocaml_ver"; then + echo "yes" + ocaml_opt_comp=true +else + echo "no, will do without" + ocaml_opt_comp=false +fi + echo "Testing Menhir... " | tr -d '\n' -menhir_ver=`menhir --version | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` +menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` case "$menhir_ver" in - 20*) + 201[4-9]*|20[2-9]*) echo "version $menhir_ver -- good!";; + ?*) + echo "version $menhir_ver -- UNSUPPORTED" + echo "Error: CompCert requires Menhir version 20140422 or later." + missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure Menhir is installed." + echo "Error: make sure Menhir version 20140422 or later is installed." missingtools=true;; esac +echo "Testing GNU make... " | tr -d '\n' +make='' +for mk in make gmake gnumake; do + make_ver=`($mk -v 2>/dev/null | head -1 | sed -n -e 's/^GNU Make //p') 2>/dev/null` + 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 @@ -282,6 +313,7 @@ PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir SHAREDIR=$sharedir +OCAML_OPT_COMP=$ocaml_opt_comp EOF if test "$target" != "manual"; then @@ -403,6 +435,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/myocamlbuild.ml b/myocamlbuild.ml deleted file mode 100644 index ef286185..00000000 --- a/myocamlbuild.ml +++ /dev/null @@ -1,14 +0,0 @@ -open Ocamlbuild_plugin;; -dispatch begin function -| After_rules -> - flag ["ocaml"; "parser"; "menhir"] (A("--explain")); - - (* libraries and syntax extensions accessed via ocamlfind *) - flag ["ocaml"; "link"; "pkg_unix"] & S[A"-package"; A "unix"]; - flag ["ocaml"; "link"; "pkg_str"] & S[A"-package"; A "str"]; - flag ["ocaml"; "compile"; "pkg_bitstring"] & S[A"-package"; A"bitstring,bitstring.syntax"; A"-syntax"; A"bitstring.syntax,camlp4o"]; - flag ["ocaml"; "ocamldep"; "pkg_bitstring"] & S[A"-package"; A"bitstring,bitstring.syntax"; A"-syntax"; A"bitstring.syntax,camlp4o"]; - flag ["ocaml"; "link"; "pkg_bitstring"] & S[A"-package"; A"bitstring"] - -| _ -> () -end 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() + diff --git a/tools/ndfun.ml b/tools/ndfun.ml index 78fb03d5..4ee07e54 100644 --- a/tools/ndfun.ml +++ b/tools/ndfun.ml @@ -1,3 +1,20 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Preprocessor for .vp files *) + open Printf (* Error reporting *) @@ -9,11 +26,7 @@ let error file line msg = (* Replace newlines with spaces *) let oneline s = - let t = String.create (String.length s) in - for i = 0 to String.length s - 1 do - t.[i] <- (match s.[i] with '\n' -> ' ' | c -> c) - done; - t + String.map (function '\n' -> ' ' | c -> c) s (* Trim leading and terminating spaces, and compress multiple spaces *) |