Separate out printing facility from model driver into printing_functions interface

5 files changed, 227 insertions, 188 deletions

diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib
index ebca3114..e77b22a8 100644
--- a/src/lem_interp/extract.mllib
+++ b/src/lem_interp/extract.mllib
@@ -8,4 +8,5 @@ Interp_inter_imp
 
 Pretty_interp
 Run_interp
+Printing_functions
 Run_interp_model
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
new file mode 100644
index 00000000..4cc02074
--- /dev/null
+++ b/src/lem_interp/printing_functions.ml
@@ -0,0 +1,196 @@
+open Printf ;;
+open Interp_ast ;;
+open Interp_utilities ;;
+open Interp_interface ;;
+open Interp_inter_imp ;;
+
+open Big_int ;;
+
+let lit_to_string = function
+ | L_unit -> "unit"
+ | L_zero -> "0b0"
+ | L_one -> "0b1"
+ | L_true -> "true"
+ | L_false -> "false"
+ | L_num n -> string_of_big_int n
+ | L_hex s -> "0x"^s
+ | L_bin s -> "0b"^s
+ | L_undef -> "undefined"
+ | L_string s -> "\"" ^ s ^ "\""
+;;
+
+let id_to_string = function
+  | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s
+;;
+
+let loc_to_string = function
+  | Unknown -> "location unknown"
+  | Int(s,_) -> s
+  | Range(s,fline,fchar,tline,tchar) -> 
+      if fline = tline
+      then sprintf "%s:%d:%d" s fline fchar
+      else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar
+;;
+
+let collapse_leading s =
+  if String.length s <= 8 then s else
+  let first_bit = s.[0] in
+  let templ = sprintf "%c...%c" first_bit first_bit in
+  let regexp = Str.regexp "^\\(000000*\\|111111*\\)" in
+  Str.replace_first regexp templ s
+;;
+
+let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function
+  | Interp.V_lit(L_aux(L_zero, _)) -> "0"
+  | Interp.V_lit(L_aux(L_one, _)) -> "1"
+  | _ -> assert false) l))
+;;
+
+let val_to_string v = match v with
+  | Bitvector(bools, inc, fst)-> let l = List.length bools in
+    (string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
+  | Bytevector words ->
+    let l = List.length words in
+    (string_of_int l) ^ " bytes --" ^
+      (String.concat ""
+	 (List.map (fun i -> (Printf.sprintf "0x%x " i)) words))
+  | Unknown0 -> "Unknown"
+
+let reg_name_to_string = function
+  | Reg0 s -> s
+  | Reg_slice(s,(first,second)) -> 
+    s ^ "[" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
+  | Reg_field(s,f,_) -> s ^ "." ^ f
+  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f ^ "]" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
+
+let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
+
+let rec val_to_string_internal = function
+ | Interp.V_boxref(n, t) -> sprintf "boxref %d" n
+ | Interp.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
+ | Interp.V_tuple l ->
+     let repr = String.concat ", " (List.map val_to_string_internal l) in
+     sprintf "(%s)" repr
+ | Interp.V_list l ->
+     let repr = String.concat "; " (List.map val_to_string_internal l) in
+     sprintf "[||%s||]" repr
+ | Interp.V_vector (first_index, inc, l) ->
+     let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index  in
+     let repr =
+       try bitvec_to_string (* (if inc then l else List.rev l)*) l
+       with Failure _ ->
+         sprintf "[%s]" (String.concat "; " (List.map val_to_string_internal l)) in
+     sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
+ | Interp.V_record(_, l) ->
+     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal value) in
+     let repr = String.concat "; " (List.map  pp l) in
+     sprintf "{%s}" repr
+ | Interp.V_ctor (id,_, value) ->
+     sprintf "%s %s" (id_to_string id) (val_to_string_internal value)
+ | Interp.V_register r ->
+     sprintf "reg-as-value" 
+ | Interp.V_unknown -> "unknown"
+;;
+
+let rec top_frame_exp = function
+  | Interp.Top -> raise (Invalid_argument "top_frame_exp")
+  | Interp.Hole_frame(_, e, _, _, _, Top)
+  | Interp.Thunk_frame(e, _, _, _, Top) -> e
+  | Interp.Thunk_frame(_, _, _, _, s)
+  | Interp.Hole_frame(_, _, _, _, _, s) -> top_frame_exp s
+
+let tunk = Unknown, None
+let ldots = E_aux(E_id (Id_aux (Id "...", Unknown)), tunk)
+let rec compact_exp (E_aux (e, l)) =
+  let wrap e = E_aux (e, l) in
+  match e with
+ | E_block (e :: _) -> compact_exp e
+ | E_nondet (e :: _) -> compact_exp e
+ | E_if (e, _, _) ->
+     wrap(E_if(compact_exp e, ldots, E_aux(E_block [], tunk)))
+ | E_for (i, e1, e2, e3, o, e4) ->
+    wrap(E_for(i, compact_exp e1, compact_exp e2, compact_exp e3, o, ldots))
+ | E_case (e, _) ->
+     wrap(E_case(compact_exp e, []))
+ | E_let (bind, _) -> wrap(E_let(bind, ldots))
+ | E_app (f, args) -> wrap(E_app(f, List.map compact_exp args))
+ | E_app_infix (l, op, r) -> wrap(E_app_infix(compact_exp l, op, compact_exp r))
+ | E_tuple exps -> wrap(E_tuple(List.map compact_exp exps))
+ | E_vector exps -> wrap(E_vector(List.map compact_exp exps))
+ | E_vector_access (e1, e2) ->
+     wrap(E_vector_access(compact_exp e1, compact_exp e2))
+ | E_vector_subrange (e1, e2, e3) ->
+     wrap(E_vector_subrange(compact_exp e1, compact_exp e2, compact_exp e3))
+ | E_vector_update (e1, e2, e3) ->
+     wrap(E_vector_update(compact_exp e1, compact_exp e2, compact_exp e3))
+ | E_vector_update_subrange (e1, e2, e3, e4) ->
+     wrap(E_vector_update_subrange(compact_exp e1, compact_exp e2, compact_exp e3, compact_exp e4))
+ | E_vector_append (e1, e2) ->
+     wrap(E_vector_append(compact_exp e1, compact_exp e2))
+ | E_list exps -> wrap(E_list(List.map compact_exp exps))
+ | E_cons (e1, e2) ->
+     wrap(E_cons(compact_exp e1, compact_exp e2))
+ | E_record_update (e, fexps) ->
+     wrap(E_record_update (compact_exp e, fexps))
+ | E_field (e, id) ->
+     wrap(E_field(compact_exp e, id))
+ | E_assign (lexp, e) -> wrap(E_assign(lexp, compact_exp e))
+ | E_block [] | E_nondet [] | E_cast (_, _) | E_internal_cast (_, _)
+ | E_id _|E_lit _|E_vector_indexed (_, _)|E_record _|E_internal_exp _ | E_exit _->
+     wrap e
+
+(* extract, compact and reverse expressions on the stack;
+ * the top of the stack is the head of the returned list. *)
+let rec compact_stack ?(acc=[]) = function
+  | Interp.Top -> acc
+  | Interp.Hole_frame(_,e,_,_,_,s)
+  | Interp.Thunk_frame(e,_,_,_,s) -> compact_stack ~acc:((compact_exp e) :: acc) s
+;;  
+
+let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
+  (string_of_big_int x) (string_of_big_int y)
+;;
+
+let rec format_events = function
+  | [] -> 
+    "     Done\n"
+  | [E_error s] -> 
+    "     Failed with message : " ^ s ^ "\n"
+  | (E_error s)::events ->
+    "     Failed with message : " ^ s ^ " but continued on erroneously\n"
+  | (E_read_mem(read_kind, location, length, tracking))::events ->
+    "     Read_mem at " ^ (val_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
+    (format_events events)
+  | (E_write_mem(write_kind,location, length, tracking, value, v_tracking))::events ->
+    "     Write_mem at " ^ (val_to_string location) ^ " writing " ^ (val_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
+    (format_events events)
+  | ((E_barrier b_kind)::events) ->
+    "     Memory_barrier occurred\n" ^ 
+    (format_events events)
+  | (E_read_reg reg_name)::events ->
+    "     Read_reg of " ^ (reg_name_to_string reg_name) ^ "\n" ^
+    (format_events events)
+  | (E_write_reg(reg_name, value))::events ->
+    "     Write_reg of " ^ (reg_name_to_string reg_name) ^ " writing " ^ (val_to_string value) ^ "\n" ^
+    (format_events events)
+;;
+
+(* ANSI/VT100 colors *)
+let disable_color = ref false
+let color bright code s =
+  if !disable_color then s
+  else sprintf "\x1b[%s3%dm%s\x1b[m" (if bright then "1;" else "") code s
+let red = color true 1
+let green = color false 2
+let yellow = color true 3
+let blue = color true 4
+let grey = color false 7
+
+let exp_to_string e = Pretty_interp.pp_exp e
+
+let get_loc (E_aux(_, (l, (_ : tannot)))) = loc_to_string l
+let print_exp printer e =
+  printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp e) ^ "\n")
+
+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)
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
new file mode 100644
index 00000000..24c80359
--- /dev/null
+++ b/src/lem_interp/printing_functions.mli
@@ -0,0 +1,24 @@
+open Interp_utilities;;
+open Interp_ast ;;
+open Interp_interface ;;
+
+val loc_to_string : l -> string
+val top_frame_exp : instruction_state -> tannot exp
+val get_loc : tannot exp -> string
+val compact_exp : tannot exp -> tannot exp
+val val_to_string : value0 -> string
+val dependencies_to_string : reg_name list -> string
+val reg_name_to_string : reg_name -> string
+
+val format_events : event list -> string
+
+val exp_to_string : tannot exp -> string
+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 red : string -> string
+val blue : string -> string
+val green : string -> string
+val yellow : string -> string
+val grey : string -> string
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 04b7eecc..a90dffc2 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -1,156 +1,10 @@
 open Printf ;;
 open Interp_ast ;;
-(*open Interp ;;
-open Interp_lib ;;*)
 open Interp_interface ;;
 open Interp_inter_imp ;;
 
 open Big_int ;;
-
-let lit_to_string = function
- | L_unit -> "unit"
- | L_zero -> "0b0"
- | L_one -> "0b1"
- | L_true -> "true"
- | L_false -> "false"
- | L_num n -> string_of_big_int n
- | L_hex s -> "0x"^s
- | L_bin s -> "0b"^s
- | L_undef -> "undefined"
- | L_string s -> "\"" ^ s ^ "\""
-;;
-
-let id_to_string = function
-  | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s
-;;
-
-let loc_to_string = function
-  | Unknown -> "location unknown"
-  | Int(s,_) -> s
-  | Range(s,fline,fchar,tline,tchar) -> 
-      if fline = tline
-      then sprintf "%s:%d:%d" s fline fchar
-      else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar
-;;
-
-let collapse_leading s =
-  if String.length s <= 8 then s else
-  let first_bit = s.[0] in
-  let templ = sprintf "%c...%c" first_bit first_bit in
-  let regexp = Str.regexp "^\\(000000*\\|111111*\\)" in
-  Str.replace_first regexp templ s
-;;
-
-let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function
-  | Interp.V_lit(L_aux(L_zero, _)) -> "0"
-  | Interp.V_lit(L_aux(L_one, _)) -> "1"
-  | _ -> assert false) l))
-;;
-
-let val_to_string v = match v with
-  | Bitvector(bools, inc, fst)-> let l = List.length bools in
-    (string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
-  | Bytevector words ->
-    let l = List.length words in
-    (string_of_int l) ^ " bytes --" ^
-      (String.concat ""
-	 (List.map (fun i -> (Printf.sprintf "0x%x " i)) words))
-  | Unknown0 -> "Unknown"
-
-let reg_name_to_string = function
-  | Reg0 s -> s
-  | Reg_slice(s,(first,second)) -> 
-    s ^ "[" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
-  | Reg_field(s,f,_) -> s ^ "." ^ f
-  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f ^ "]" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
-
-let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
-
-let rec val_to_string_internal = function
- | Interp.V_boxref(n, t) -> sprintf "boxref %d" n
- | Interp.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | Interp.V_tuple l ->
-     let repr = String.concat ", " (List.map val_to_string_internal l) in
-     sprintf "(%s)" repr
- | Interp.V_list l ->
-     let repr = String.concat "; " (List.map val_to_string_internal l) in
-     sprintf "[||%s||]" repr
- | Interp.V_vector (first_index, inc, l) ->
-     let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index  in
-     let repr =
-       try bitvec_to_string (* (if inc then l else List.rev l)*) l
-       with Failure _ ->
-         sprintf "[%s]" (String.concat "; " (List.map val_to_string_internal l)) in
-     sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
- | Interp.V_record(_, l) ->
-     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal value) in
-     let repr = String.concat "; " (List.map  pp l) in
-     sprintf "{%s}" repr
- | Interp.V_ctor (id,_, value) ->
-     sprintf "%s %s" (id_to_string id) (val_to_string_internal value)
- | Interp.V_register r ->
-     sprintf "reg-as-value" 
- | Interp.V_unknown -> "unknown"
-;;
-
-let rec top_frame_exp = function
-  | Interp.Top -> raise (Invalid_argument "top_frame_exp")
-  | Interp.Hole_frame(_, e, _, _, _, Top)
-  | Interp.Thunk_frame(e, _, _, _, Top) -> e
-  | Interp.Thunk_frame(_, _, _, _, s)
-  | Interp.Hole_frame(_, _, _, _, _, s) -> top_frame_exp s
-
-let tunk = Unknown, None
-let ldots = E_aux(E_id (Id_aux (Id "...", Unknown)), tunk)
-let rec compact_exp (E_aux (e, l)) =
-  let wrap e = E_aux (e, l) in
-  match e with
- | E_block (e :: _) -> compact_exp e
- | E_nondet (e :: _) -> compact_exp e
- | E_if (e, _, _) ->
-     wrap(E_if(compact_exp e, ldots, E_aux(E_block [], tunk)))
- | E_for (i, e1, e2, e3, o, e4) ->
-    wrap(E_for(i, compact_exp e1, compact_exp e2, compact_exp e3, o, ldots))
- | E_case (e, _) ->
-     wrap(E_case(compact_exp e, []))
- | E_let (bind, _) -> wrap(E_let(bind, ldots))
- | E_app (f, args) -> wrap(E_app(f, List.map compact_exp args))
- | E_app_infix (l, op, r) -> wrap(E_app_infix(compact_exp l, op, compact_exp r))
- | E_tuple exps -> wrap(E_tuple(List.map compact_exp exps))
- | E_vector exps -> wrap(E_vector(List.map compact_exp exps))
- | E_vector_access (e1, e2) ->
-     wrap(E_vector_access(compact_exp e1, compact_exp e2))
- | E_vector_subrange (e1, e2, e3) ->
-     wrap(E_vector_subrange(compact_exp e1, compact_exp e2, compact_exp e3))
- | E_vector_update (e1, e2, e3) ->
-     wrap(E_vector_update(compact_exp e1, compact_exp e2, compact_exp e3))
- | E_vector_update_subrange (e1, e2, e3, e4) ->
-     wrap(E_vector_update_subrange(compact_exp e1, compact_exp e2, compact_exp e3, compact_exp e4))
- | E_vector_append (e1, e2) ->
-     wrap(E_vector_append(compact_exp e1, compact_exp e2))
- | E_list exps -> wrap(E_list(List.map compact_exp exps))
- | E_cons (e1, e2) ->
-     wrap(E_cons(compact_exp e1, compact_exp e2))
- | E_record_update (e, fexps) ->
-     wrap(E_record_update (compact_exp e, fexps))
- | E_field (e, id) ->
-     wrap(E_field(compact_exp e, id))
- | E_assign (lexp, e) -> wrap(E_assign(lexp, compact_exp e))
- | E_block [] | E_nondet [] | E_cast (_, _) | E_internal_cast (_, _)
- | E_id _|E_lit _|E_vector_indexed (_, _)|E_record _|E_internal_exp _ | E_exit _->
-     wrap e
-
-(* extract, compact and reverse expressions on the stack;
- * the top of the stack is the head of the returned list. *)
-let rec compact_stack ?(acc=[]) = function
-  | Interp.Top -> acc
-  | Interp.Hole_frame(_,e,_,_,_,s)
-  | Interp.Thunk_frame(e,_,_,_,s) -> compact_stack ~acc:((compact_exp e) :: acc) s
-;;  
-
-let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
-  (string_of_big_int x) (string_of_big_int y)
-;;
+open Printing_functions ;;
 
 module Reg = struct
   include Map.Make(struct type t = string let compare = compare end)
@@ -265,29 +119,7 @@ let increment bytes =
 ;;
 let unit_lit = (L_aux(L_unit,Interp_ast.Unknown))
 
-let rec format_events = function
-  | [] -> 
-    "     Done\n"
-  | [E_error s] -> 
-    "     Failed with message : " ^ s ^ "\n"
-  | (E_error s)::events ->
-    "     Failed with message : " ^ s ^ " but continued on erroneously\n"
-  | (E_read_mem(read_kind, location, length, tracking))::events ->
-    "     Read_mem at " ^ (val_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
-    (format_events events)
-  | (E_write_mem(write_kind,location, length, tracking, value, v_tracking))::events ->
-    "     Write_mem at " ^ (val_to_string location) ^ " writing " ^ (val_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
-    (format_events events)
-  | ((E_barrier b_kind)::events) ->
-    "     Memory_barrier occurred\n" ^ 
-    (format_events events)
-  | (E_read_reg reg_name)::events ->
-    "     Read_reg of " ^ (reg_name_to_string reg_name) ^ "\n" ^
-    (format_events events)
-  | (E_write_reg(reg_name, value))::events ->
-    "     Write_reg of " ^ (reg_name_to_string reg_name) ^ " writing " ^ (val_to_string value) ^ "\n" ^
-    (format_events events)
-;;
+
 
 let rec perform_action ((reg, mem) as env) = function
  (* registers *)
@@ -334,17 +166,6 @@ let mode_to_string = function
   | Run -> "run"
   | Next -> "next"
 
-(* ANSI/VT100 colors *)
-let disable_color = ref false
-let color bright code s =
-  if !disable_color then s
-  else sprintf "\x1b[%s3%dm%s\x1b[m" (if bright then "1;" else "") code s
-let red = color true 1
-let green = color false 2
-let yellow = color true 3
-let blue = color true 4
-let grey = color false 7
-
 let run
   ?(main_func = "main")
   ?(parameters = [])
@@ -354,9 +175,6 @@ let run
   ?(track_dependencies= ref false)
   ?mode
   (name, spec) =
-  let get_loc (E_aux(_, (l, _))) = loc_to_string l in
-  let print_exp  e =
-    debugf "%s: %s\n" (get_loc e) (Pretty_interp.pp_exp e) in
   (* interactive loop for step-by-step execution *)
   let usage = "Usage:
     step    go to next action [default]
@@ -384,8 +202,8 @@ let run
         Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) mem;
         interact mode env stack
     | "bt" | "backtrace" | "stack" ->
-        List.iter print_exp (compact_stack stack);
-        interact mode env stack
+      print_backtrace_compact (fun s -> debugf "%s" s) stack;
+      interact mode env stack
     | "e" | "exh" | "exhaust" ->
       debugf "interpreting exhaustively from current state\n";
       let events = interp_exhaustive stack in
@@ -393,7 +211,7 @@ let run
       interact mode env stack
     | "c" | "cont" | "continuation" ->
         (* print not-compacted continuation *)
-        print_exp (top_frame_exp stack);
+        print_continuation (fun s -> debugf "%s" s) stack;
         interact mode env stack
     | "track" | "t" ->
       track_dependencies := not(!track_dependencies);
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index dfb618a4..76a8292d 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -152,7 +152,7 @@ let rec fde_loop count main_func parameters mem reg ?mode track_dependencies pro
   | true, mode, track_dependencies, (reg, mem) ->
       if eq_zero (get_reg reg "CIA") then
         eprintf "\nSUCCESS: returned with value %s\n"
-          (Run_interp_model.val_to_string (get_reg reg "GPR3"))
+          (Printing_functions.val_to_string (get_reg reg "GPR3"))
       else
         fde_loop (count+1) main_func parameters mem reg ~mode:mode track_dependencies prog
 ;;