diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-30 13:10:26 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-30 13:10:26 +0200 |
commit | a2bed030e01bfe6e3addbe44f724de5c5fbeab65 (patch) | |
tree | aeffd4bcba1743dd5fdcc08e2f2e9f51962e4402 | |
parent | e5b59af8a21c42b504b1beeb89208dd0cb0c8b3b (diff) | |
download | compcert-kvx-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.tar.gz compcert-kvx-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.zip |
Change the way the tools like the linker, assembler, etc. are specified by including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
-rw-r--r-- | .gitignore | 2 | ||||
-rw-r--r-- | Makefile | 44 | ||||
-rwxr-xr-x | configure | 3 | ||||
-rw-r--r-- | driver/Configuration.ml | 86 |
4 files changed, 113 insertions, 22 deletions
@@ -23,7 +23,7 @@ Makefile.config # ocamlbuild's temp dir _build/ # Generated files -driver/Configuration.ml +compcert.ini ia32/ConstpropOp.v ia32/SelectOp.v powerpc/ConstpropOp.v @@ -157,34 +157,34 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach $(COQEXEC) extraction/extraction.v touch extraction/STAMP -ccomp: extraction/STAMP driver/Configuration.ml +ccomp: extraction/STAMP compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp -ccomp.prof: extraction/STAMP driver/Configuration.ml +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.byte: extraction/STAMP driver/Configuration.ml +ccomp.byte: extraction/STAMP compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \ && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte runtime: $(MAKE) -C runtime -cchecklink: driver/Configuration.ml +cchecklink: compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \ && rm -f cchecklink && $(SLN) _build/checklink/Validator.native cchecklink -cchecklink.byte: driver/Configuration.ml +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 driver/Configuration.ml exportclight/Clightdefs.vo +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 driver/Configuration.ml exportclight/Clightdefs.vo +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 @@ -220,20 +220,20 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod -w $*.v -driver/Configuration.ml: Makefile.config VERSION - (echo let stdlib_path = "\"$(LIBDIR)\""; \ - echo let prepro = "\"$(CPREPRO)\""; \ - echo let asm = "\"$(CASM)\""; \ - echo let linker = "\"$(CLINKER)\""; \ - echo let arch = "\"$(ARCH)\""; \ - echo let model = "\"$(MODEL)\""; \ - echo let abi = "\"$(ABI)\""; \ - echo let system = "\"$(SYSTEM)\""; \ - echo let has_runtime_lib = $(HAS_RUNTIME_LIB); \ - echo let asm_supports_cfi = $(ASM_SUPPORTS_CFI); \ +compcert.ini: Makefile.config VERSION + (echo stdlib_path=$(LIBDIR); \ + echo prepro=$(CPREPRO); \ + echo asm=$(CASM); \ + echo linker=$(CLINKER); \ + echo arch=$(ARCH); \ + echo model=$(MODEL); \ + echo abi=$(ABI); \ + echo system=$(SYSTEM); \ + echo has_runtime_lib=$(HAS_RUNTIME_LIB); \ + echo asm_supports_cfi=$(ASM_SUPPORTS_CFI); \ version=`cat VERSION`; \ - echo let version = "\"$$version\"") \ - > driver/Configuration.ml + echo version=$$version) \ + > compcert.ini cparser/Parser.v: cparser/Parser.vy $(MENHIR) --coq cparser/Parser.vy @@ -246,6 +246,8 @@ depend: $(FILES) exportclight/Clightdefs.v install: install -d $(BINDIR) install ./ccomp $(BINDIR) + install -d $(SHAREDIR) + install ./compcert.ini $(SHAREDIR) ifeq ($(CCHECKLINK),true) install ./cchecklink $(BINDIR) endif @@ -259,7 +261,7 @@ clean: rm -rf _build rm -rf doc/html doc/*.glob rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o - rm -f driver/Configuration.ml + rm -f compcert.ini rm -f extraction/STAMP extraction/*.ml extraction/*.mli rm -f tools/ndfun tools/*.cm? tools/*.o rm -f $(ARCH)/ConstpropOp.v $(ARCH)/SelectOp.v backend/SelectDiv.v backend/SelectLong.v @@ -274,11 +274,14 @@ fi # Generate Makefile.config +sharedir="$(dirname "$bindir")"/share + rm -f Makefile.config cat > Makefile.config <<EOF PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir +SHAREDIR=$sharedir EOF if test "$target" != "manual"; then diff --git a/driver/Configuration.ml b/driver/Configuration.ml new file mode 100644 index 00000000..c4bcf278 --- /dev/null +++ b/driver/Configuration.ml @@ -0,0 +1,86 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + + +let config_vars: (string, string) Hashtbl.t = Hashtbl.create 10 + + +(* Read in the .ini file, which is either in the same directory or in the directory ../share *) +let _ = + try + let file = + let dir = Sys.getcwd () + and name = Sys.argv.(0) in + let dirname = if Filename.is_relative name then + Filename.dirname (Filename.concat dir name) + else + Filename.dirname name + in + let share_dir = Filename.concat (Filename.concat dirname Filename.parent_dir_name) "share" in + try + open_in (Filename.concat dirname "compcert.ini") + with Sys_error _ -> + open_in (Filename.concat share_dir "compcert.ini") + in + (try + let ini_line = Str.regexp "\\([^=]+\\)=\\(.+\\)" in + while true do + let line = input_line file in + if Str.string_match ini_line line 0 then + let key = Str.matched_group 1 line + and value = Str.matched_group 2 line in + Hashtbl.add config_vars key value + else + Printf.eprintf "Wrong value %s in .ini file.\n" line + done + with End_of_file -> close_in file) + with Sys_error msg -> Printf.eprintf "Unable to open .ini file\n" + +let get_config key = + try + Hashtbl.find config_vars key + with Not_found -> + Printf.eprintf "Configuration option `%s' is not set\n" key; exit 2 + +let bad_config key v = + Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 + +let stdlib_path = get_config "stdlib_path" + +let prepro = get_config "prepro" +let asm = get_config "asm" +let linker = get_config "linker" +let arch = + let v = get_config "arch" in + (match v with + | "powerpc" + | "arm" + | "ia32" -> () + | _ -> bad_config "arch" v); + v + +let model = get_config "model" +let abi = get_config "abi" +let system = get_config "system" +let has_runtime_lib = + match get_config "has_runtime_lib" with + | "true" -> true + | "false" -> false + | v -> bad_config "has_runtime_lib" v + +let asm_supports_cfi = + match get_config "asm_supports_cfi" with + | "true" -> true + | "false" -> false + | v -> bad_config "asm_supports_cfi" v + +let version = get_config "version" |