Make mips build again

Make quiet mode for sequential interpreter not print

4 files changed, 53 insertions, 35 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 1a70c6d7..b607afaa 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -688,6 +688,7 @@ let fupdate_vector_slice vec replace start stop =
 	(List.replicate (if is_inc(dir) then (stop-start) else (start-stop)) V_unknown) in
       (V_vector_sparse m n dir (replace_sparse (if is_inc(dir) then (<) else (>)) vals (List.reverse repsi)) d)
     | (V_unknown,_) -> V_unknown
+    | _ -> Assert_extra.failwith ("fupdate vector slice given " ^ (string_of_value vec) ^ " and " ^ (string_of_value replace))
      end) in
   binary_taint fupdate_vec_help vec replace
 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 8f9bc422..91a6c75d 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -234,7 +234,11 @@ let rec slice_reg_value v start stop =
 let update_reg_value_slice reg_name v start stop v2 =
   let v_internal = intern_reg_value v in
   let v2_internal = intern_reg_value v2 in
-  extern_reg_value reg_name (Interp.fupdate_vector_slice v_internal v2_internal start stop)
+  extern_reg_value reg_name
+    (if start = stop then
+      (Interp.fupdate_vec v_internal start v2_internal)
+    else
+      (Interp.fupdate_vector_slice v_internal v2_internal start stop))
 
 let initial_instruction_state top_level main args = 
   let e_args = match args with
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index f1310240..03ce132a 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -149,8 +149,15 @@ let rec perform_action ((reg, mem) as env) = function
  | _ -> (None, env)
 ;;
 
-let debug = ref true
-let debugf : ('a, out_channel, unit) format -> 'a = function f -> if !debug then eprintf f else ifprintf stderr f
+let interact_print = ref true
+let result_print = ref true
+let error_print = ref true
+let interactf : ('a, out_channel, unit) format -> 'a =
+  function f -> if !interact_print then eprintf f else ifprintf stderr f
+let errorf : ('a, out_channel, unit) format -> 'a =
+  function f -> if !error_print then eprintf f else ifprintf stderr f
+let resultf : ('a, out_channel, unit) format -> 'a =
+  function f -> if !result_print then eprintf f else ifprintf stderr f
 
 type interactive_mode = Step | Run | Next
 
@@ -188,22 +195,22 @@ let run
       | "n" | "next" -> Next
       | "r" | "run" -> Run
       | "rg" | "reg" | "registers" ->
-        Reg.iter (fun k v -> debugf "%s\n" (Reg.to_string k v)) reg;
+        Reg.iter (fun k v -> interactf "%s\n" (Reg.to_string k v)) reg;
         interact mode env stack
       | "m" | "mem" | "memory" ->
-        Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) mem;
+        Mem.iter (fun k v -> interactf "%s\n" (Mem.to_string k v)) mem;
         interact mode env stack
       | "bt" | "backtrace" | "stack" ->
-        print_backtrace_compact (fun s -> debugf "%s" s) stack;
+        print_backtrace_compact (fun s -> interactf "%s" s) stack;
         interact mode env stack
       | "e" | "exh" | "exhaust" ->
-        debugf "interpreting exhaustively from current state\n";
+        interactf "interpreting exhaustively from current state\n";
         let events = interp_exhaustive None stack in
-        debugf "%s" (format_events events);
+        interactf "%s" (format_events events);
         interact mode env stack
       | "c" | "cont" | "continuation" ->
         (* print not-compacted continuation *)
-        print_continuation (fun s -> debugf "%s" s) stack;
+        print_continuation (fun s -> interactf "%s" s) stack;
         interact mode env stack
       | "track" | "t" ->
         track_dependencies := not(!track_dependencies);
@@ -215,18 +222,18 @@ let run
         Pretty_interp.ignore_casts := true;
         interact mode env stack
       | "q" | "quit" | "exit" -> exit 0
-      | _ -> debugf "%s\n" usage; interact mode env stack
+      | _ -> interactf "%s\n" usage; interact mode env stack
     end
   in
-  let show act lhs arrow rhs = debugf "%s: %s %s %s\n"
+  let show act lhs arrow rhs = interactf "%s: %s %s %s\n"
       (green act) lhs (blue arrow) rhs in
   let left = "<-" and right = "->" in
   let rec loop mode env = function
     | Done ->
-      debugf "%s: %s\n" (grey name) (blue "done");
+      interactf "%s: %s\n" (grey name) (blue "done");
       (true, mode, !track_dependencies, env)
     | Error0 s -> 
-      debugf "%s: %s: %s\n" (grey name) (red "error") s;
+      errorf "%s: %s: %s\n" (grey name) (red "error") s;
       (false, mode, !track_dependencies, env) 
     | action ->
       let (return,env') = perform_action env action in
@@ -235,7 +242,7 @@ let run
         let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in
         let loc = get_loc (compact_exp top_exp) in
         if mode = Step || force then begin
-          debugf "%s\n" (Pretty_interp.pp_exp top_env Printing_functions.red top_exp);
+          interactf "%s\n" (Pretty_interp.pp_exp top_env Printing_functions.red top_exp);
           interact mode env' state
         end else
           mode in
@@ -282,16 +289,16 @@ let run
           show "mem_barrier" "" "" "";
           (step next, env, next)
         | Internal(None,None, next) ->
-          show "breakpoint" "" "" "";
+          show "stepped" "" "" "";
           (step ~force:true next,env',next)
         | Internal((Some fn),None,next) ->
-          show "breakpoint" fn "" "";
+          show "evaluated" fn "" "";
           (step ~force:true next, env',next)
         | Internal(None,Some vdisp,next) ->
-          show "breakpoint" (vdisp ()) "" "";
+          show "evaluated" (vdisp ()) "" "";
           (step ~force:true next,env', next)
         | Internal((Some fn),(Some vdisp),next) ->
-          show "breakpoint" (fn ^ " " ^ (vdisp ())) "" "";
+          show "evaluated" (fn ^ " " ^ (vdisp ())) "" "";
           (step ~force:true next, env', next)
         | Nondet_choice(nondets, next) ->
           let choose_order = List.sort (fun (_,i1) (_,i2) -> Pervasives.compare i1 i2) 
@@ -333,13 +340,13 @@ let run
   let imode = make_mode eager_eval !track_dependencies !default_endian in
   let (IState(instr_state,context)) = istate in
   let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in
-  debugf "%s: %s %s\n" (grey name) (blue "evaluate") 
+  interactf "%s: %s %s\n" (grey name) (blue "evaluate") 
     (Pretty_interp.pp_exp top_env Printing_functions.red top_exp);
   try
     Printexc.record_backtrace true;
     loop mode (reg, mem) (Interp_inter_imp.interp0 imode istate)
   with e ->
     let trace = Printexc.get_backtrace () in
-    debugf "%s: %s %s\n%s\n" (grey name) (red "interpretor error") (Printexc.to_string e) trace;
+    interactf "%s: %s %s\n%s\n" (grey name) (red "interpretor error") (Printexc.to_string e) trace;
     (false, mode, !track_dependencies, (reg, mem))
 ;;
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 58c24ab1..ea0c7f46 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -753,7 +753,12 @@ let break_instr = ref 0
 
 let args = [
   ("--file", Arg.Set_string file, "filename binary code to load in memory");
-  ("--quiet", Arg.Clear Run_interp_model.debug, "do not display interpreter actions");
+  ("--quiet", Arg.Clear Run_interp_model.interact_print, "do not display per-instruction actions");
+  ("--silent", Arg.Tuple [Arg.Clear Run_interp_model.error_print;
+                          Arg.Clear Run_interp_model.interact_print;
+                          Arg.Clear Run_interp_model.result_print],
+   "do not dispaly error messages, per-instruction actions, or results");
+  ("--no_result", Arg.Clear Run_interp_model.result_print, "do not display final register values");
   ("--interactive", Arg.Clear eager_eval , "interactive execution");
   ("--breakpoint", Arg.Int (fun i -> break_point := true; break_instr:= i), "run to instruction number i, then run interactively");
 ]
@@ -764,8 +769,9 @@ let time_it action arg =
   let finish_time = Sys.time () in
   finish_time -. start_time
 
+(*TODO MIPS specific, should print final register values under all models*)
 let rec debug_print_gprs start stop =
-  debugf "DEBUG MIPS REG %.2d %s\n" start (Printing_functions.logfile_register_value_to_string (Reg.find (Format.sprintf "GPR%02d" start) !reg));
+  resultf "DEBUG MIPS REG %.2d %s\n" start (Printing_functions.logfile_register_value_to_string (Reg.find (Format.sprintf "GPR%02d" start) !reg));
   if start < stop
   then debug_print_gprs (start + 1) stop
   else ()
@@ -782,7 +788,7 @@ let stop_condition_met model instr =
     | _ -> false)
   | MIPS -> (match instr with 
     | ("HCF", _, _) -> 
-      debugf "DEBUG MIPS PC %s\n"  (Printing_functions.logfile_register_value_to_string (Reg.find "PC" !reg));
+      resultf "DEBUG MIPS PC %s\n"  (Printing_functions.logfile_register_value_to_string (Reg.find "PC" !reg));
       debug_print_gprs 0 31;
       true
     | _ -> false)
@@ -845,7 +851,7 @@ let set_next_instruction_address model =
          reg := Reg.add "nextPC" (register_value_of_address delayedPC D_decreasing) !reg;
          reg := Reg.add "branchPending" (register_value_of_integer 1 1 Interp_interface.D_decreasing Nat_big_num.zero) !reg
        end
-     | (_, _, _) -> failwith "PC address contains unknown or undefined")
+     | (_, _, _) -> errorf "PC address contains unknown or undefined"; exit 1)
 
 let add1 = Nat_big_num.add (Nat_big_num.of_int 1)
 
@@ -904,33 +910,33 @@ let fetch_instruction_opcode_and_update_ia model =
         reg := Reg.add "PC" nextPC !reg;
         Opcode opcode
       end
-     | None -> failwith "nextPC contains unknown or undefined")
+     | None -> errorf "nextPC contains unknown or undefined"; exit 1)
   |  _ -> assert false
 
 let rec fde_loop count context model mode track_dependencies opcode =
-  debugf "\n**** instruction %d  ****\n" count;
+  interactf "\n**** instruction %d  ****\n" count;
   let (instruction,istate) = match Interp_inter_imp.decode_to_istate context opcode with
     | Instr(instruction,istate) ->
-      debugf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
+      interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
       (instruction,istate)
     | Decode_error d ->
       (match d with
        | Interp_interface.Unsupported_instruction_error instr ->
-         debugf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
+         errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
        | Interp_interface.Not_an_instruction_error op ->
          (match op with
           | Opcode bytes ->
-            debugf "\n**** Encountered non-decodeable opcode: %s ****\n" (Printing_functions.byte_list_to_string bytes))
-       | Internal_error s -> debugf "\n**** Internal error on decode: %s ****\n" s);
+            errorf "\n**** Encountered non-decodeable opcode: %s ****\n" (Printing_functions.byte_list_to_string bytes))
+       | Internal_error s -> errorf "\n**** Internal error on decode: %s ****\n" s);
       exit 1
   in
   if stop_condition_met model instruction
-  then eprintf "\nSUCCESS program terminated\n"
+  then resultf "\nSUCCESS program terminated\n"
   else
     begin
       set_next_instruction_address model;
       match Run_interp_model.run  istate !reg !prog_mem !eager_eval track_dependencies mode "execute" with
-      | false, _,_, _ -> eprintf "FAILURE\n"; exit 1
+      | false, _,_, _ -> errorf "FAILURE\n"; exit 1
       | true, mode, track_dependencies, (my_reg, my_mem) ->
         reg := my_reg;
         prog_mem := my_mem;
@@ -944,7 +950,7 @@ let run () =
     Arg.usage args "";
     exit 1;
   end;
-  if !eager_eval then Run_interp_model.debug := true;
+  (*if !eager_eval then Run_interp_model.debug := true;*)
 
   let ((isa_defs,
        (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4),
@@ -956,7 +962,7 @@ let run () =
 
   let initial_opcode = Opcode (List.map (fun b -> match b with
       | Some b -> b
-      | None -> failwith "A byte in opcode contained unknown or undef")
+      | None -> errorf "A byte in opcode contained unknown or undef"; exit 1)
       (List.map byte_of_memory_byte
          [Mem.find startaddr !prog_mem;
           Mem.find (add1 startaddr) !prog_mem;
@@ -968,6 +974,6 @@ let run () =
   (* entry point: unit -> unit fde *)
   let name = Filename.basename !file in
   let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false) initial_opcode) () in
-  Printf.eprintf "Execution time for file %s: %f seconds\n" name t;;
+  resultf "Execution time for file %s: %f seconds\n" name t;;
 
 run () ;;