Add printing for instruction form

3 files changed, 27 insertions, 1 deletions

diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 1e3ed6da..8f9425e2 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -228,5 +228,26 @@ let instruction_state_to_string stack =
 
 let top_instruction_state_to_string stack = exp_to_string (top_frame_exp stack)
 
+let instr_parm_to_string (name, typ, value) = 
+  match (typ,value) with
+    | Bit, Bitvector ([true],_,_) -> "1"
+    | Bit, Bitvector ([false],_,_) -> "0"
+    | Other,_ -> "Unrepresentable external value"
+    | _, Unknown0 -> "Unknown"
+    | _, v -> let intern_v = (Interp_inter_imp.intern_value value) in
+	      match Interp_lib.to_num true intern_v with
+		| V_lit (L_aux(L_num n, _)) -> string_of_big_int n
+		| _ -> val_to_string value
+
+let rec instr_parms_to_string ps = 
+  match ps with
+    | [] -> ""
+    | [p] -> instr_parm_to_string p
+    | p::ps -> instr_parm_to_string p ^ ", " ^ instr_parms_to_string ps
+
+let instruction_to_string (name, parms, base_effects) = 
+  (String.lowercase name) ^ " " ^ instr_parms_to_string parms 
+
 let print_backtrace_compact printer stack = List.iter (print_exp printer) (compact_stack stack)
 let print_continuation printer stack = print_exp printer (top_frame_exp stack)
+let print_instruction printer instr = printer (instruction_to_string instr)
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index fab5f8ce..17cbbbeb 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -39,9 +39,10 @@ val instruction_state_to_string : instruction_state -> string
 (*format just the top of the call stack*)
 val top_instruction_state_to_string : instruction_state -> string
 
+val instruction_to_string : instruction -> string
 
 (*Functions to take a print function and cause a print event for the above functions *)
 val print_exp : (string-> unit) -> tannot exp -> unit 
 val print_backtrace_compact : (string -> unit) -> instruction_state -> unit
 val print_continuation : (string -> unit) -> instruction_state -> unit
-
+val print_instruction : (string -> unit) -> instruction -> unit
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 66d05e00..e6a13c50 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -101,6 +101,10 @@ let init_reg () =
       init "VRSAVE" zero_big_int 32;
       init "FPSCR" zero_big_int 64;
       init "VSCR" zero_big_int 32;
+      init "SPRG4" zero_big_int 64;
+      init "SPRG5" zero_big_int 64;
+      init "SPRG6" zero_big_int 64;
+      init "SPRG7" zero_big_int 64;
     ] @
     (* Commonly read before written general purpose register *)
       [init "GPR0" zero_big_int 64;