From c130f4936bad11fd6dab3a5d142b870d2a5f650c Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 29 Dec 2014 11:15:29 +0100
Subject: Use Unix.create_process instead of Sys.command (continued).

---
 driver/Configuration.ml | 125 ++++++++++++++++++++++++------------------------
 1 file changed, 63 insertions(+), 62 deletions(-)

(limited to 'driver/Configuration.ml')

diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index e73125f7..0012dc0c 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -10,86 +10,87 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open Printf
 
-let config_vars: (string, string) Hashtbl.t = Hashtbl.create 10
+(* Locate the .ini file, which is either in the same directory as
+  the executable or in the directory ../share *)
 
+let ini_file_name =
+  try
+    Sys.getenv "COMPCERT_CONFIG"
+  with Not_found ->
+    let exe_dir = Filename.dirname Sys.executable_name in
+    let exe_ini = Filename.concat exe_dir "compcert.ini" in
+    let share_dir =
+      Filename.concat (Filename.concat exe_dir Filename.parent_dir_name)
+                      "share" in
+    let share_ini = Filename.concat share_dir "compcert.ini" in
+    if Sys.file_exists exe_ini then exe_ini
+    else if Sys.file_exists share_ini then share_ini
+    else begin 
+      eprintf "Cannot find compcert.ini configuration file.\n";
+      exit 2
+    end
+
+(* Read in the .ini file *)
 
-(* Read in the .ini file, which is either in the same directory or in the directory ../share *)
 let _ =
   try
-    let file = 
-      try
-        let env_file = Sys.getenv "COMPCERT_CONFIG" in
-        open_in env_file
-      with Not_found ->
-        let dir = Sys.getcwd () 
-        and name = Sys.executable_name 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"
+    Readconfig.read_config_file ini_file_name
+  with
+  | Readconfig.Error(file, lineno, msg) ->
+      eprintf "Error reading configuration file %s.\n" ini_file_name;
+      eprintf "%s:%d:%s\n" file lineno msg;
+      exit 2
+  | Sys_error msg ->
+      eprintf "Error reading configuration file %s.\n" ini_file_name;
+      eprintf "%s\n" msg;
+      exit 2
 
 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
+  match Readconfig.key_val key with
+  | Some v -> v
+  | None -> 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 bad_config key vl =
+  eprintf "Invalid value `%s' for configuration option `%s'\n"
+          (String.concat " " vl) key;
+  exit 2
 
-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 get_config_string key =
+  match get_config key with
+  | [v] -> v
+  | vl -> bad_config key vl
 
-let model = get_config "model"
-let abi = get_config "abi"
-let system = get_config "system"
+let get_config_list key =
+  match get_config key with
+  | [] -> bad_config key []
+  | vl -> vl
+
+let prepro = get_config_list "prepro"
+let asm = get_config_list "asm"
+let linker = get_config_list "linker"
+let arch = 
+  match get_config_string "arch" with
+  | "powerpc"|"arm"|"ia32" as a -> a
+  | v -> bad_config "arch" [v]
+let model = get_config_string "model"
+let abi = get_config_string "abi"
+let system = get_config_string "system"
 let has_runtime_lib = 
-  match get_config "has_runtime_lib" with
+  match get_config_string "has_runtime_lib" with
   | "true" -> true
   | "false" -> false
-  | v -> bad_config "has_runtime_lib" v
-
-
+  | v -> bad_config "has_runtime_lib" [v]
 let stdlib_path =
   if has_runtime_lib then
-    get_config "stdlib_path"
+    get_config_string "stdlib_path"
   else
     ""
-
 let asm_supports_cfi = 
-  match get_config "asm_supports_cfi" with
+  match get_config_string "asm_supports_cfi" with
   | "true" -> true
   | "false" -> false
-  | v -> bad_config "asm_supports_cfi" v
+  | v -> bad_config "asm_supports_cfi" [v]
 
-let version = get_config "version"
+let version = get_config_string "version"
-- 
cgit