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.

Author: bschommer

.gitignore

@@ -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

Makefile

@@ -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

configure

@@ -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

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"