Merge branch 'master' into dwarf

3 files changed, 180 insertions, 189 deletions

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"
diff --git a/driver/Driver.ml b/driver/Driver.ml
index e943e6c9..d8b28285 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -20,17 +20,38 @@ open Timing
 
 let stdlib_path = ref Configuration.stdlib_path
 
-let command cmd =
+(* Invocation of external tools *)
+
+let command ?stdout args =
   if !option_v then begin
-    prerr_string "+ "; prerr_string cmd; prerr_endline ""
+    eprintf "+ %s" (String.concat " " args);
+    begin match stdout with
+    | None -> ()
+    | Some f -> eprintf " > %s" f
+    end;
+    prerr_endline ""
   end;
-  Sys.command cmd
-
-let quote_options opts =
-  String.concat " " (List.rev_map Filename.quote opts)
-
-let quote_arguments args =
-  String.concat " " (List.map Filename.quote args)
+  let argv = Array.of_list args in
+  assert (Array.length argv > 0);
+  try
+    let fd_out =
+      match stdout with
+      | None -> Unix.stdout
+      | Some f ->
+          Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
+    let pid =
+      Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
+    let (_, status) =
+      Unix.waitpid [] pid in
+    if stdout <> None then Unix.close fd_out;
+    match status with
+    | Unix.WEXITED rc -> rc
+    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
+  with Unix.Unix_error(err, fn, param) ->
+    eprintf "Error executing '%s': %s: %s %s\n"
+            argv.(0) fn (Unix.error_message err) param;
+    -1
 
 let safe_remove file =
   try Sys.remove file with Sys_error _ -> ()
@@ -68,16 +89,17 @@ let output_filename_default default_file =
 
 let preprocess ifile ofile =
   let output =
-    if ofile = "-" then "" else sprintf "> %s" ofile in
-  let cmd =
-    sprintf "%s -D__COMPCERT__ %s %s %s %s"
-      Configuration.prepro
-      (if Configuration.has_runtime_lib
-       then sprintf "-I%s" !stdlib_path
-       else "")
-      (quote_options !prepro_options)
-      ifile output in
-  if command cmd <> 0 then begin
+    if ofile = "-" then None else Some ofile in
+  let cmd = List.concat [
+    Configuration.prepro;
+    ["-D__COMPCERT__"];
+    (if Configuration.has_runtime_lib
+     then ["-I" ^ !stdlib_path]
+     else []);
+    List.rev !prepro_options;
+    [ifile]
+  ] in
+  if command ?stdout:output cmd <> 0 then begin
     if ofile <> "-" then safe_remove ofile;
     eprintf "Error during preprocessing.\n";
     exit 2
@@ -208,11 +230,13 @@ let compile_cminor_file ifile ofile =
 (* From asm to object file *)
 
 let assemble ifile ofile =
-  let cmd =
-    sprintf "%s -o %s %s %s"
-      Configuration.asm ofile (quote_options !assembler_options) ifile in
-  let retcode = command cmd in
-  if retcode <> 0 then begin
+  let cmd = List.concat [
+    Configuration.asm;
+    ["-o"; ofile];
+    List.rev !assembler_options;
+    [ifile]
+  ] in
+  if command cmd <> 0 then begin
     safe_remove ofile;
     eprintf "Error during assembling.\n";
     exit 2
@@ -221,14 +245,14 @@ let assemble ifile ofile =
 (* Linking *)
 
 let linker exe_name files =
-  let cmd =
-    sprintf "%s -o %s %s %s"
-      Configuration.linker
-      (Filename.quote exe_name)
-      (quote_arguments files)
-      (if Configuration.has_runtime_lib
-       then sprintf "-L%s -lcompcert" !stdlib_path
-       else "") in
+  let cmd = List.concat [
+    Configuration.linker;
+    ["-o"; exe_name];
+    files;
+    (if Configuration.has_runtime_lib
+     then ["-L" ^ !stdlib_path; "-lcompcert"]
+     else [])
+  ] in
   if command cmd <> 0 then exit 2
 
 (* Processing of a .c file *)
diff --git a/driver/Interp.ml b/driver/Interp.ml
index ab22cebb..2725dbfe 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -254,28 +254,14 @@ let compare_state s1 s2 =
       compare (rank_state s1) (rank_state s2)
   end
 
-(* Sets of states already explored *)
+(* Maps of states already explored. *)
 
-module StateSet =
-  Set.Make(struct
-             type t = state * Determinism.world
-             let compare (s1,w1) (s2,w2) = compare_state s1 s2
+module StateMap =
+  Map.Make(struct
+             type t = state
+             let compare = compare_state
            end)
 
-(* Purging states that will never be reached again based on their memory
-   next block.  All states with nextblock <= the given nextblock are
-   removed.  We take advantage of the fact that StateSets are sorted
-   by increasing nextblock, cf. the definition of compare_state above. *)
-
-let rec purge_seen nextblock seen =
-  let min = try Some(StateSet.min_elt seen) with Not_found -> None in
-  match min with
-  | None -> seen
-  | Some((s, w) as sw) ->
-      if P.le (mem_state s).Mem.nextblock nextblock
-      then purge_seen nextblock (StateSet.remove sw seen)
-      else seen
-
 (* Extract a string from a global pointer *)
 
 let extract_string m blk ofs =
@@ -435,7 +421,7 @@ and world_vstore ge m chunk id ofs ev =
 
 let do_event p ge time w ev =
   if !trace >= 1 then
-    fprintf p "@[<hov 2>Time %d: observable event:@ @[<hov 2>%a@]@]@."
+    fprintf p "@[<hov 2>Time %d: observable event:@ %a@]@."
               time print_event ev;
   (* Return new world after external action *)
   match ev with
@@ -497,11 +483,10 @@ let diagnose_stuck_state p ge w = function
   | ExprState(f,a,k,e,m) -> ignore(diagnose_stuck_expr p ge w f a k e m)
   | _ -> ()
 
-(* Exploration *)
+(* Execution of a single step.  Return list of triples
+   (reduction rule, next state, next world). *)
 
-let do_step p prog ge time (s, w) =
-  if !trace >= 2 then
-    fprintf p "@[<hov 2>Time %d: %a@]@." time print_state (prog, ge, s);
+let do_step p prog ge time s w =
   match Cexec.at_final_state s with
   | Some r ->
       if !trace >= 1 then
@@ -513,89 +498,71 @@ let do_step p prog ge time (s, w) =
       end
   | None ->
       let l = Cexec.do_step ge do_external_function do_inline_assembly w s in
-      if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin
+      if l = []
+      || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l
+      then begin
         pp_set_max_boxes p 1000;
         fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s);
         diagnose_stuck_state p ge w s;
         fprintf p "ERROR: Undefined behavior@.";
         exit 126
       end else begin
-        List.map (fun (t, s') -> (s', do_events p ge time w t)) l
+        List.map (fun (Cexec.TR(r, t, s')) -> (r, s', do_events p ge time w t)) l
       end
 
-let rec explore_one p prog ge time sw =
-  let succs = do_step p prog ge time sw in
+(* Exploration of a single execution. *)
+
+let rec explore_one p prog ge time s w =
+  if !trace >= 2 then
+    fprintf p "@[<hov 2>Time %d:@ %a@]@." time print_state (prog, ge, s);
+  let succs = do_step p prog ge time s w in
   if succs <> [] then begin
-    let sw' =
+    let (r, s', w') =
       match !mode with
       | First -> List.hd succs
       | Random -> List.nth succs (Random.int (List.length succs))
       | All -> assert false in
-    explore_one p prog ge (time + 1) sw'
+    if !trace >= 2 then
+      fprintf p "--[%s]-->@." (camlstring_of_coqstring r);
+    explore_one p prog ge (time + 1) s' w'
   end
 
-(* A priority queue structure where the priority is inversely proportional
-   to the memory nextblock. *)
-
-module PrioQueue = struct
-
-  type elt = int * StateSet.elt
-
-  type queue = Empty | Node of elt * queue * queue
-
-  let empty = Empty
-
-  let singleton elt = Node(elt, Empty, Empty)
-
-  let higher_prio (time1, (s1, w1)) (time2, (s2, w2)) =
-    P.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock
-
-  let rec insert queue elt =
-    match queue with
-    | Empty -> Node(elt, Empty, Empty)
-    | Node(e, left, right) ->
-        if higher_prio elt e
-        then Node(elt, insert right e, left)
-        else Node(e, insert right elt, left)
-
-  let rec remove_top = function
-  | Empty -> assert false
-  | Node(elt, left, Empty) -> left
-  | Node(elt, Empty, right) -> right
-  | Node(elt, (Node(lelt, _, _) as left),
-              (Node(relt, _, _) as right)) ->
-      if higher_prio lelt relt
-      then Node(lelt, remove_top left, right)
-      else Node(relt, left, remove_top right)
-
-  let extract = function
-  | Empty -> None
-  | Node(elt, _, _) as queue -> Some(elt, remove_top queue)
-
-  (* Return true if all elements of queue have strictly lower priority
-     than elt. *)
-  let dominate elt queue =
-    match queue with
-    | Empty -> true
-    | Node(e, _, _) -> higher_prio elt e
-end
-
-let rec explore_all p prog ge seen queue =
-  match PrioQueue.extract queue with
-  | None -> ()
-  | Some((time, sw) as tsw, queue') ->
-      if StateSet.mem sw seen then
-        explore_all p prog ge seen queue'
-      else
-        let succs = 
-          List.rev_map (fun sw -> (time + 1, sw)) (do_step p prog ge time sw) in
-        let queue'' = List.fold_left PrioQueue.insert queue' succs in
-        let seen' = StateSet.add sw seen in
-        let seen'' = 
-          if PrioQueue.dominate tsw queue''
-          then purge_seen (mem_state (fst sw)).Mem.nextblock seen'
-          else seen' in
-        explore_all p prog ge seen'' queue''
+(* Exploration of all possible executions. *)
+
+let rec explore_all p prog ge time states =
+  if !trace >= 2 then begin
+    List.iter
+      (fun (n, s, w) ->
+         fprintf p "@[<hov 2>State %d.%d: @ %a@]@."
+                   time n print_state (prog, ge, s))
+      states
+  end;
+  let rec explore_next nextstates seen numseen = function
+  | [] ->
+      List.rev nextstates
+  | (n, s, w) :: states ->
+      add_reducts nextstates seen numseen states n (do_step p prog ge time s w)
+
+  and add_reducts nextstates seen numseen states n = function
+  | [] ->
+      explore_next nextstates seen numseen states
+  | (r, s', w') :: reducts ->
+      let (n', nextstates', seen', numseen') =
+        try
+          (StateMap.find s' seen, nextstates, seen, numseen)
+        with Not_found ->
+          (numseen,
+           (numseen, s', w') :: nextstates,
+           StateMap.add s' numseen seen,
+           numseen + 1) in
+      if !trace >= 2 then begin
+        fprintf p "Transition state %d.%d --[%s]--> state %d.%d@."
+                  time n (camlstring_of_coqstring r) (time + 1) n'
+      end;
+      add_reducts nextstates' seen' numseen' states n reducts
+  in
+    let nextstates = explore_next [] StateMap.empty 1 states in
+    if nextstates <> [] then explore_all p prog ge (time + 1) nextstates
 
 (* The variant of the source program used to build the world for
    executing events.  
@@ -680,7 +647,6 @@ let execute prog =
       | Some(ge, s) ->
           match !mode with
           | First | Random ->
-              explore_one p prog1 ge 0 (s, world wge wm)
+              explore_one p prog1 ge 0 s (world wge wm)
           | All ->
-              explore_all p prog1 ge StateSet.empty 
-                                (PrioQueue.singleton (0, (s, world wge wm)))
+              explore_all p prog1 ge 0 [(1, s, world wge wm)]