Merge branch 'master' into no-shell

4 files changed, 113 insertions, 137 deletions

diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index bc095af6..0a2c8fca 100644
--- a/driver/Commandline.ml
+++ b/driver/Commandline.ml
@@ -52,7 +52,7 @@ let rec find_action text = function
   | (pat, act) :: rem ->
       if match_pattern text pat then Some act else find_action text rem
 
-let parse_array spec usage argv first last =
+let parse_array spec argv first last =
   (* Split the spec into Exact patterns (in a hashtable) and other patterns *)
   let exact_cases = (Hashtbl.create 29 : (string, action) Hashtbl.t) in
   let rec split_spec = function
@@ -69,10 +69,7 @@ let parse_array spec usage argv first last =
         with Not_found -> find_action s inexact_cases in
       match optact with
       | None ->
-          if s <> "-help" && s <> "--help" 
-          then eprintf "Unknown argument `%s'\n" s
-          else printf "%s" usage;
-          exit 2
+          eprintf "Unknown argument `%s'\n" s; exit 2
       | Some(Set r) ->
           r := true; parse (i+1)
       | Some(Unset r) ->
@@ -101,5 +98,5 @@ let parse_array spec usage argv first last =
     end
   in parse first
 
-let parse_cmdline spec usage =
-  parse_array spec usage Sys.argv 1 (Array.length Sys.argv - 1)
+let parse_cmdline spec =
+  parse_array spec Sys.argv 1 (Array.length Sys.argv - 1)
diff --git a/driver/Commandline.mli b/driver/Commandline.mli
index 7a18905f..79786678 100644
--- a/driver/Commandline.mli
+++ b/driver/Commandline.mli
@@ -34,8 +34,7 @@ type action =
   | String of (string -> unit)  (** read next arg as a string, call function *)
   | Integer of (int -> unit)    (** read next arg as an int, call function *)
 
-val parse_cmdline:
-  (pattern * action) list -> string (* usage string *) -> unit
+val parse_cmdline: (pattern * action) list -> unit
 
 (* Note on precedence: [Exact] patterns are tried first, then the other
    patterns are tried in the order in which they appear in the list. *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 14ce11f4..d22dd77c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -130,7 +130,7 @@ let parse_c_file sourcename ifile =
   end;
   (* Conversion to Csyntax *)
   let csyntax =
-    match C2C.convertProgram ast with
+    match Timing.time "CompCert C generation" C2C.convertProgram ast with
     | None -> exit 2
     | Some p -> p in
   flush stderr;
@@ -466,6 +466,9 @@ Interpreter mode:
   -all           Simulate all possible execution orders
 "
 
+let print_usage_and_exit _ =
+  printf "%s" usage_string; exit 0
+
 let language_support_options = [
   option_fbitfields; option_flongdouble;
   option_fstruct_return; option_fvararg_calls; option_funprototyped;
@@ -485,26 +488,9 @@ let cmdline_actions =
   let f_opt name ref =
     [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
   [
-(* File arguments *)
-  Suffix ".c", Self (fun s ->
-      push_action process_c_file s; incr num_source_files);
-  Suffix ".i", Self (fun s ->
-      push_action process_i_file s; incr num_source_files);
-  Suffix ".p", Self (fun s ->
-      push_action process_i_file s; incr num_source_files);
-  Suffix ".cm", Self (fun s ->
-      push_action process_cminor_file s; incr num_source_files);
-  Suffix ".s", Self (fun s ->
-      push_action process_s_file s; incr num_source_files);
-  Suffix ".S", Self (fun s ->
-      push_action process_S_file s; incr num_source_files);
-  Suffix ".o", Self push_linker_arg;
-  Suffix ".a", Self push_linker_arg;
-  (* GCC compatibility: .o.ext files are also object files *)
-  _Regexp ".*\\.o\\.", Self push_linker_arg;
-  (* GCC compatibility: .h files can be preprocessed with -E *)
-  Suffix ".h", Self (fun s ->
-      push_action process_h_file s; incr num_source_files);
+(* Getting help *)
+  Exact "-help", Self print_usage_and_exit;
+  Exact "--help", Self print_usage_and_exit;
 (* Processing options *)
   Exact "-c", Set option_c;
   Exact "-E", Set option_E;
@@ -583,6 +569,32 @@ let cmdline_actions =
 (* Code generation options *)
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
+  @ [
+(* Catch options that are not handled *)
+  Prefix "-", Self (fun s ->
+      eprintf "Unknown option `%s'\n" s; exit 2);
+(* File arguments *)
+  Suffix ".c", Self (fun s ->
+      push_action process_c_file s; incr num_source_files);
+  Suffix ".i", Self (fun s ->
+      push_action process_i_file s; incr num_source_files);
+  Suffix ".p", Self (fun s ->
+      push_action process_i_file s; incr num_source_files);
+  Suffix ".cm", Self (fun s ->
+      push_action process_cminor_file s; incr num_source_files);
+  Suffix ".s", Self (fun s ->
+      push_action process_s_file s; incr num_source_files);
+  Suffix ".S", Self (fun s ->
+      push_action process_S_file s; incr num_source_files);
+  Suffix ".o", Self push_linker_arg;
+  Suffix ".a", Self push_linker_arg;
+  (* GCC compatibility: .o.ext files and .so files are also object files *)
+  _Regexp ".*\\.o\\.", Self push_linker_arg;
+  Suffix ".so", Self push_linker_arg;
+  (* GCC compatibility: .h files can be preprocessed with -E *)
+  Suffix ".h", Self (fun s ->
+      push_action process_h_file s; incr num_source_files);
+  ]
 
 let _ =
   try
@@ -600,7 +612,7 @@ let _ =
       end;
     Builtins.set C2C.builtins;
     CPragmas.initialize();
-    parse_cmdline cmdline_actions usage_string;
+    parse_cmdline cmdline_actions;
     let nolink = !option_c || !option_S || !option_E || !option_interp in
     if nolink && !option_o <> None && !num_source_files >= 2 then begin
       eprintf "Ambiguous '-o' option (multiple source files)\n";
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 9bb9d237..2725dbfe 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -122,22 +122,22 @@ let print_val_list p vl =
 let print_state p (prog, ge, s) =
   match s with
   | State(f, s, k, e, m) ->
-      PrintCsyntax.print_pointer_hook := print_pointer ge e;
+      PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "in function %s, statement@ @[<hv 0>%a@]"
               (name_of_function prog f)
               PrintCsyntax.print_stmt s
   | ExprState(f, r, k, e, m) ->
-      PrintCsyntax.print_pointer_hook := print_pointer ge e;
+      PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "in function %s, expression@ @[<hv 0>%a@]"
               (name_of_function prog f)
               PrintCsyntax.print_expr r
   | Callstate(fd, args, k, m) ->
-      PrintCsyntax.print_pointer_hook := print_pointer ge Maps.PTree.empty;
+      PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty;
       fprintf p "calling@ @[<hov 2>%s(%a)@]"
               (name_of_fundef prog fd)
               print_val_list args
   | Returnstate(res, k, m) ->
-      PrintCsyntax.print_pointer_hook := print_pointer ge Maps.PTree.empty;
+      PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty;
       fprintf p "returning@ %a"
               print_val res
   | Stuckstate ->
@@ -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 =
@@ -389,7 +375,7 @@ let convert_external_arg ge v t =
   | Vsingle f, AST.Tsingle -> Some (EVsingle f)
   | Vlong n, AST.Tlong -> Some (EVlong n)
   | Vptr(b, ofs), AST.Tint -> 
-      Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs))
+      Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs))
   | _, _ -> None
 
 let rec convert_external_args ge vl tl =
@@ -422,20 +408,20 @@ and world_io ge m id args =
   None
 
 and world_vload ge m chunk id ofs =
-  Genv.find_symbol ge id >>= fun b ->
+  Genv.find_symbol ge.genv_genv id >>= fun b ->
   Mem.load chunk m b ofs >>= fun v ->
   Cexec.eventval_of_val ge v (type_of_chunk chunk) >>= fun ev ->
   Some(ev, world ge m)
 
 and world_vstore ge m chunk id ofs ev =
-  Genv.find_symbol ge id >>= fun b ->
+  Genv.find_symbol ge.genv_genv id >>= fun b ->
   Cexec.val_of_eventval ge ev (type_of_chunk chunk) >>= fun v ->
   Mem.store chunk m b ofs v >>= fun m' ->
   Some(world ge m')
 
 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
@@ -479,7 +465,7 @@ let diagnose_stuck_expr p ge w f a kont e m =
   if found then true else begin
     let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in
     if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin
-      PrintCsyntax.print_pointer_hook := print_pointer ge e;
+      PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e;
       fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@."
               PrintCsyntax.print_expr a;
       true
@@ -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.  
@@ -633,7 +600,9 @@ let change_main_function p old_main old_main_ty =
   let new_main_id = intern_string "___main" in
   { prog_main = new_main_id;
     prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs;
-    prog_public = p.prog_public }
+    prog_public = p.prog_public;
+    prog_types = p.prog_types;
+    prog_comp_env = p.prog_comp_env }
 
 let rec find_main_function name = function
   | [] -> None
@@ -667,8 +636,8 @@ let execute prog =
   | None -> exit 126
   | Some prog1 ->
       let wprog = world_program prog1 in
-      let wge = Genv.globalenv wprog in
-      match Genv.init_mem wprog with
+      let wge = globalenv wprog in
+      match Genv.init_mem (program_of_program wprog) with
       | None ->
           fprintf p "ERROR: World memory state undefined@."; exit 126
       | Some wm ->
@@ -678,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)]