wib

3 files changed, 25 insertions, 4 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 26f5f508..02e7d2e2 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -166,6 +166,8 @@ instance (Ord reg_name)
   let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
 end
 
+(** basic values *)
+
 type bit =
   | Bitc_zero
   | Bitc_one
@@ -184,7 +186,7 @@ type register_value = <| rv_bits: list bit_lifted; rv_dir: direction; rv_start:
 
 type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *)
 
-type instruction_field_value = list bit 
+type instruction_field_value = (*SHOULD BE JUST*)  list bit  (*register_value *)
 
 type byte = Byte of list bit (* of length 8 *)
 
@@ -200,6 +202,8 @@ type address = Address of list byte (* of length 8 *)
 
 type opcode = Opcode of list byte (* of length 4 *)
 
+(** typeclass instantiations *)
+
 instance (Ord register_value)
   let compare = defaultCompare
   let (<) = defaultLess
@@ -583,6 +587,14 @@ let address_of_register_value (rv:register_value) : maybe address =
       end
   end
 
+let address_of_memory_value (mv:memory_value) : maybe address = 
+  match byte_list_of_memory_value mv with
+  | Nothing -> Nothing
+  | Just bs -> 
+      if List.length bs <> 8 then Nothing else
+      Just (address_of_byte_list bs)
+  end 
+
 val byte_of_int : int -> byte
 let byte_of_int (i:int) : byte = 
   failwith "TODO"
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 7fc247a7..73feb8ac 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -67,7 +67,12 @@ let reg_value_to_string v =
   else (string_of_int l) ^ "_" ^ start ^ "'b" ^ 
     collapse_leading (List.fold_right (^) (List.map bit_lifted_to_string v.rv_bits) "")
 
-let mem_value_to_string v = bytes_to_string v
+
+let register_value_to_string rv = 
+  reg_value_to_string rv  
+
+let memory_value_to_string mv = 
+  bytes_to_string mv 
 
 (*let val_to_string v = match v with
   | Bitvector(bools, inc, fst)-> 
@@ -224,10 +229,10 @@ 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 " ^ (mem_value_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
+    "     Read_mem at " ^ (memory_value_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
     (format_events events)
   | (E_write_mem(write_kind,(Address_lifted location), length, tracking, value, v_tracking))::events ->
-    "     Write_mem at " ^ (mem_value_to_string location) ^ " writing " ^ (mem_value_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
+    "     Write_mem at " ^ (memory_value_to_string location) ^ " writing " ^ (memory_value_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
     (format_events events)
   | ((E_barrier b_kind)::events) ->
     "     Memory_barrier occurred\n" ^ 
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index c9d69eef..d668e912 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -56,3 +56,7 @@ val print_exp : (string-> unit) -> Interp.lenv -> 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
+
+
+val register_value_to_string : register_value -> string
+val memory_value_to_string : memory_value -> string