Taint printing changes: make it for debugging only, except when showing all events in exhaustive mode

2 files changed, 16 insertions, 4 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 7a9ae1cd..e0473707 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -58,6 +58,11 @@ type value =
  | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
  | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
+let rec {ocaml} string_of_reg_form r = match r with
+  | Reg id _ _ -> get_id id
+  | SubReg id reg_form _ -> (string_of_reg_form reg_form) ^ "." ^ (get_id id)
+end
+
 let rec {ocaml} string_of_value v = match v with
   | V_boxref nat t -> "$#" ^ (show nat) ^ "$"
   | V_lit (L_aux lit _) -> 
@@ -95,7 +100,7 @@ let rec {ocaml} string_of_value v = match v with
   | V_unknown -> "Unknown"
   | V_register _ -> "register_as_value"
   | V_register_alias _ _ -> "register_as_alias"
-  | V_track v _ -> "tainted " ^ (string_of_value v)
+  | V_track v rs -> (*"tainted by {" ^ (list_to_string string_of_reg_form "," rs) ^ "} --" ^*) (string_of_value v)
 end
 let ~{ocaml} string_of_value _ = ""
 
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 357cdc83..94a3f6a2 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -285,7 +285,7 @@ let rec val_to_string_internal ((Interp.LMem (_,memory)) as mem) = function
  | Interp.V_register _ | Interp.V_register_alias _ ->
      sprintf "reg-as-value" 
  | Interp.V_unknown -> "unknown"
- | Interp.V_track(v,_) -> (val_to_string_internal mem v)
+ | Interp.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v)
 ;;
 
 let rec top_frame_exp_state = function
@@ -347,6 +347,10 @@ let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
   (to_string x) (to_string y)
 ;;
 
+let format_tracking t = match t with
+  | Some rs -> "{ " ^ (dependencies_to_string rs) ^ "}"
+  | None -> "None"
+
 let rec format_events = function
   | [] -> 
     "     Done\n"
@@ -355,10 +359,13 @@ let rec format_events = function
   | (E_error s)::events ->
     "     Failed with message : " ^ s ^ " but continued on erroneously\n"
   | (E_read_mem(read_kind, (Address_lifted(location, _)), length, tracking))::events ->
-    "     Read_mem at " ^ (memory_value_to_string E_big_endian location) ^ " for " ^ (string_of_int length) ^ " bytes \n" ^
+    "     Read_mem at " ^ (memory_value_to_string E_big_endian location) ^ " based on registers " ^ 
+      format_tracking tracking ^  " for " ^ (string_of_int length) ^ " bytes \n" ^
     (format_events events)
   | (E_write_mem(write_kind,(Address_lifted (location,_)), length, tracking, value, v_tracking))::events ->
-    "     Write_mem at " ^ (memory_value_to_string E_big_endian location) ^ " writing " ^ (memory_value_to_string E_big_endian value) ^ " across " ^ (string_of_int length) ^ " bytes\n" ^
+    "     Write_mem at " ^ (memory_value_to_string E_big_endian location) ^ ", based on registers " ^ 
+      format_tracking tracking ^ ", writing " ^ (memory_value_to_string E_big_endian value) ^
+      ", based on " ^ format_tracking v_tracking ^ " across " ^ (string_of_int length) ^ " bytes\n" ^
     (format_events events)
   | ((E_barrier b_kind)::events) ->
     "     Memory_barrier occurred\n" ^