diff options
| -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" |