Changing interface in step with Peter and ppcmem changes

5 files changed, 212 insertions, 141 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 31a75b73..c82e6da2 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -7,8 +7,10 @@ open import Pervasives
 open import Assert_extra
 
 
-val intern_value : value -> Interp.value
-val extern_value : interp_mode -> bool -> maybe integer -> Interp.value -> (value * maybe (list reg_name))
+val intern_reg_value : register_value -> Interp.value
+val intern_mem_value : memory_value -> Interp.value
+val extern_reg_value : maybe integer -> Interp.value -> register_value
+val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
 val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
 
 let build_context defs = match Interp.to_top_env defs with (_,context) -> context end
@@ -16,34 +18,56 @@ let build_context defs = match Interp.to_top_env defs with (_,context) -> contex
 let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
 let tracking_dependencies mode = mode.Interp.track_values
 
-let to_bits l = (List.map (fun b -> match b with
-                               | false -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
-			       | true ->  (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) end) l)
-let from_bits l = (List.map (fun b -> match b with
-                                 | Interp.V_lit (L_aux L_zero _) -> false
-				 | _ -> true end) l) 
+let to_bit = function 
+  | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
+  | Bitl_one ->  (Interp.V_lit (L_aux L_one Interp_ast.Unknown))
+  | Bitl_undef -> (Interp.V_lit (L_aux L_undef Interp_ast.Unknown))
+  | Bitl_unknown -> Interp.V_unknown 
+end
+
+let to_bool = function 
+  | Bitl_zero -> false
+  | Bitl_one ->  true
+  | Bitl_undef -> Assert_extra.failwith "to_bool given undef"
+  | Bitl_unknown -> Assert_extra.failwith "to_bool given unknown"
+end
+
+let is_bool = function 
+  | Bitl_zero -> true
+  | Bitl_one ->  true
+  | Bitl_undef -> false
+  | Bitl_unknown -> false
+end
+
+let to_bits l = List.map to_bit l
+let from_bits l = List.map 
+		     (fun b -> match b with
+                       | Interp.V_lit (L_aux L_zero _) -> Bitl_zero
+		       | Interp.V_lit (L_aux L_one _)  -> Bitl_one
+		       | Interp.V_lit (L_aux L_undef _) -> Bitl_undef
+		       | Interp.V_unknown -> Bitl_unknown end) l
+
 let rec to_bytes l = match l with
   | [] -> []
-  | (a::b::c::d::e::f::g::h::rest) ->
-    (natFromInteger(integerFromBoolList (false,(List.reverse([a;b;c;d;e;f;g;h])))))::(to_bytes rest)
-end
+  | (a::b::c::d::e::f::g::h::rest) -> (Byte_lifted[a;b;c;d;e;f;g;h])::(to_bytes rest)
+end 
+
+let all_known l = List.all is_bool l
+
+let bits_to_byte b = 
+  if ((List.length b) = 8) && (all_known b)
+  then natFromInteger (integerFromBoolList (false,(List.reverse (List.map to_bool b))))
+  else Assert_extra.failwith "bits_to_byte given a non-8 list or one containing ? and u"
 		   
-let intern_value v = match v with
-  | Bitvector [true] _ _ -> Interp.V_lit (L_aux L_one Interp_ast.Unknown)
-  | Bitvector [false] _ _ -> Interp.V_lit (L_aux L_zero Interp_ast.Unknown)
-  | Bitvector bs inc fst   -> Interp.V_vector fst inc  (to_bits bs)
-  | Bytevector bys -> Interp.V_vector 0 true 
-    (List.concat (List.map (fun by -> 
-      match Interp_lib.to_vec_inc (Interp.V_tuple([Interp.V_lit(L_aux (L_num 8) Interp_ast.Unknown);
-						   Interp.V_lit(L_aux (L_num (integerFromNat by)) Interp_ast.Unknown)]))
-      with
-	| Interp.V_vector _ _ bits -> bits 
-	| _ -> [] end) bys))
-  | Unknown -> Interp.V_unknown
-  | _ -> Interp.V_unknown
+let intern_reg_value v = match v with
+  | <| rv_bits=[b] |> -> to_bit b
+  | _ -> Interp.V_vector v.rv_start (v.rv_dir = D_increasing) (to_bits v.rv_bits)
 end
 
-let byte_list_of_integer size num = 
+let intern_mem_value v = 
+  Interp.V_vector 0 true (*get a default here*) (List.concatMap (fun (Byte_lifted bits) -> to_bits bits) v)
+
+(*let byte_list_of_integer size num = 
   if (num < 0)
   then failwith "signed integer given to byte_list_of_integer"
   else let internal_value = (Interp_lib.to_vec_inc 
@@ -71,63 +95,62 @@ let integer_of_byte_list bytes =
   match Interp_lib.to_num Interp_lib.Unsigned intv with
     | Interp.V_lit (L_aux (L_num n) _) -> n
   end
+*)
 
 let extern_reg r slice = match (r,slice) with
   | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x
   | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2)
-  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field y x (i,i)
-  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Nothing) -> Reg_field y x (i,j)
-  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Just(i1,j1)) -> Reg_f_slice y x (i,j) (i1,j1)
+  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> 
+    Reg_field y x (i,i)
+  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Nothing) -> 
+    Reg_field y x (i,j)
+  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Just(i1,j1)) ->
+    Reg_f_slice y x (i,j) (i1,j1)
 end
 
-let rec extern_value mode for_mem optional_start v = match v with
-  | Interp.V_track v regs -> 
-    let (external_v,_) = extern_value mode for_mem optional_start v in
-    (external_v,
-     if (for_mem && mode.Interp.track_values)
-     then (Just (List.map (fun r -> extern_reg r Nothing) regs))
-     else Nothing)
+let rec extern_reg_value optional_start v = match v with
+  | Interp.V_track v regs -> extern_reg_value optional_start v 
   | Interp.V_vector fst inc bits ->
-    if for_mem 
-    then (Bytevector (to_bytes (from_bits bits)), Nothing)
-    else (Bitvector (from_bits bits) inc fst, Nothing)
+    <| rv_bits=(from_bits bits); rv_dir=(if inc then D_increasing else D_decreasing); rv_start=fst|>
   | Interp.V_vector_sparse fst stop inc bits default ->
-    extern_value mode for_mem optional_start (Interp_lib.fill_in_sparse v)
+    extern_reg_value optional_start (Interp_lib.fill_in_sparse v)
   | Interp.V_lit (L_aux L_zero _) -> 
-    if for_mem
-    then (Bytevector [0],Nothing)
-    else let start = match optional_start with | Nothing -> 0 | Just i -> i end in
-    (Bitvector [false] true start, Nothing)
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
+    <| rv_bits=[Bitl_zero]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_lit (L_aux L_false _) ->
-    if for_mem
-    then (Bytevector [0],Nothing)
-    else let start = match optional_start with | Nothing -> 0 | Just i -> i end in
-      (Bitvector [false] true start, Nothing)
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
+    <| rv_bits=[Bitl_zero]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_lit (L_aux L_one _) -> 
-    if for_mem
-    then (Bytevector [1],Nothing)
-    else let start = match optional_start with | Nothing -> 0 | Just i -> i end in    
-    (Bitvector [true] true start, Nothing)
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
+    <| rv_bits=[Bitl_one]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_lit (L_aux L_true _) ->
-    if for_mem
-    then (Bytevector [1],Nothing)
-    else let start = match optional_start with | Nothing -> 0 | Just i -> i end in
-    (Bitvector [true] true start, Nothing)
-  | _ -> (Unknown,Nothing)
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
+    <| rv_bits=[Bitl_one]; rv_dir=D_increasing; rv_start=start |>
+  | Interp.V_lit (L_aux L_undef _) -> 
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
+    <| rv_bits=[Bitl_undef]; rv_dir=D_increasing; rv_start=start |>
+  | Interp.V_unknown -> 
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
+    <| rv_bits=[Bitl_unknown]; rv_dir=D_increasing; rv_start=start |>
 end 
 
-let rec slice_value bits start stop = 
-  match bits with
-    | Bitvector bools inc fst -> 
-      Bitvector (Interp.from_n_to_n (if inc then (start - fst) else (fst - start))
-                                    (if inc then (stop - fst) else (fst - stop)) bools)
-                 inc
-                 (if inc then start else ((stop - start) + 1))                
-    | Bytevector bytes -> 
-      Bytevector (Interp.from_n_to_n start stop bytes)
-    | Unknown -> Unknown
-end
+let rec extern_mem_value mode v = match v with
+  | Interp.V_track v regs -> 
+    let (external_v,_) = extern_mem_value mode v in
+    (external_v,
+     if mode.Interp.track_values then (Just (List.map (fun r -> extern_reg r Nothing) regs)) else Nothing)
+  | Interp.V_vector fst inc bits -> (to_bytes (from_bits bits), Nothing)
+  | Interp.V_vector_sparse fst stop inc bits default ->
+    extern_mem_value mode (Interp_lib.fill_in_sparse v)
+end 
+
+let rec slice_reg_value v start stop = 
+  let inc = v.rv_dir = D_increasing in
+  <| v with rv_bits = (Interp.from_n_to_n (if inc then (start - v.rv_start) else (v.rv_start - start))
+                                          (if inc then (stop - v.rv_start) else (v.rv_start - stop)) v.rv_bits);
+            rv_start = (if inc then start else ((stop - start) + 1)) |> 
 
+(*
 let append_value left right =
   match (left,right) with
     | (Bitvector bools1 inc fst, Bitvector bools2 _ _) -> Bitvector (bools1++bools2) inc fst
@@ -177,13 +200,14 @@ let coerce_Bitvector_of_Bytevector (v: value) : value =
         0
   | _ -> Assert_extra.failwith "coerce_Bitvector_of_Bitvector given non-Bytevector"
   end
+*)
 
 let initial_instruction_state top_level main args = 
   let e_args = match args with
     | [] -> [E_aux (E_lit (L_aux L_unit Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]
-    | [arg] -> let (e,_) = Interp.to_exp (make_mode true false) Interp.eenv (intern_value arg) in [e]
+    | [arg] -> let (e,_) = Interp.to_exp (make_mode true false) Interp.eenv (intern_reg_value arg) in [e]
     | args -> List.map fst (List.map (Interp.to_exp (make_mode true false) Interp.eenv)
-			      (List.map intern_value args)) end in
+			      (List.map intern_reg_value args)) end in
   Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) 
     top_level Interp.eenv Interp.emem Interp.Top
 
@@ -211,11 +235,11 @@ let power_externs = [
 ]
 
 (*All external functions*)
-let external_functions = 
-  Interp_lib.function_map ++ power_externs
+let external_functions = Interp_lib.function_map ++ power_externs
 
 type mem_function = (string * 
-                     (maybe read_kind * maybe write_kind * (interp_mode -> Interp.value -> (value * (maybe (list reg_name))))))
+                     (maybe read_kind * maybe write_kind * 
+			(interp_mode -> Interp.value -> (memory_value * (maybe (list reg_name))))))
 type barrier_function = (string * barrier_kind)
 
 (*List of memory functions; needs to be expanded with all of the memory functions needed for PPCMem.
@@ -227,10 +251,10 @@ let memory_functions =
 	       | Interp.V_tuple [location;length] ->
 		 match length with
 		   | Interp.V_lit (L_aux (L_num len) _) ->
-		     let (v,regs) = extern_value mode true Nothing location in
+		     let (v,regs) = extern_mem_value mode location in
 		     (v,len,regs) 
 		   | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-		     let (v,loc_regs) = extern_value mode true Nothing location in
+		     let (v,loc_regs) = extern_mem_value mode location in
 		     match loc_regs with
 		       | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
 		       | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
@@ -240,10 +264,10 @@ let memory_functions =
 			| Interp.V_tuple [location;length] ->
 			  match length with
 			    | Interp.V_lit (L_aux (L_num len) _) ->
-			      let (v,regs) = extern_value mode true Nothing location in
+			      let (v,regs) = extern_mem_value mode location in
 			      (v,len,regs) 
 			    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-			      let (v,loc_regs) = extern_value mode true Nothing location in
+			      let (v,loc_regs) = extern_mem_value mode location in
 			      match loc_regs with
 				| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
 				| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
@@ -253,10 +277,10 @@ let memory_functions =
 		| Interp.V_tuple [location;length] ->
 		  match length with
 		    | Interp.V_lit (L_aux (L_num len) _) ->
-		      let (v,regs) = extern_value mode true Nothing location in
+		      let (v,regs) = extern_mem_value mode location in
 		      (v,len,regs)
 		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-		      let (v,loc_regs) = extern_value mode true Nothing location in
+		      let (v,loc_regs) = extern_mem_value mode location in
 		      match loc_regs with
 			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
 			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
@@ -266,10 +290,10 @@ let memory_functions =
 		| Interp.V_tuple [location;length] ->
 		  match length with
 		    | Interp.V_lit (L_aux (L_num len) _) ->
-		      let (v,regs) = extern_value mode true Nothing location in
+		      let (v,regs) = extern_mem_value mode location in
 		      (v,len,regs)
 		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-		      let (v,loc_regs) = extern_value mode true Nothing location in
+		      let (v,loc_regs) = extern_mem_value mode location in
 		      match loc_regs with
 			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
 			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
@@ -318,7 +342,7 @@ end
 
 let decode_to_istate top_level value = 
   let mode = make_mode true false in
-  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_value value) in
+  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_reg_value value) in
   let (Interp.Env _ instructions _ _ _ _ _) = top_level in
   let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
     (fun _ -> Interp.resume 
@@ -334,9 +358,9 @@ let decode_to_istate top_level value =
 	    | Just(Instruction_extractor.Instr_form name parms effects) -> 
 	      match (parm,parms) with
 		| (Interp.V_lit (L_aux L_unit _),[]) -> (name, [], effects)
-		| (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),fst(extern_value mode false Nothing value))], effects)
+		| (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),(extern_reg_value Nothing value))], effects)
 		| (Interp.V_tuple vals,parms) -> 
-		  (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),fst(extern_value mode false Nothing value))) vals parms), effects)
+		  (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),(extern_reg_value Nothing value))) vals parms), effects)
           end end end in 
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
       let (instr_decoded,error) = interp_to_value_helper value instr_external
@@ -368,7 +392,7 @@ let decode_to_instruction top_level value =
 
 let instruction_to_istate top_level ((name, parms, _) as instr) = 
   let mode = make_mode true false in
-  let get_value (name,typ,v) = let (e,_) = Interp.to_exp mode Interp.eenv (intern_value v) in e in
+  let get_value (name,typ,v) = let (e,_) = Interp.to_exp mode Interp.eenv (intern_reg_value v) in e in
 (*  (Instr instr*)
     (Interp.Thunk_frame
        (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
@@ -386,25 +410,32 @@ let rec interp_to_outcome mode thunk =
     | Interp.Read_reg reg_form slice -> 
       Read_reg (extern_reg reg_form slice) 
                (fun v -> 
-                 let v = (intern_value v) in
+                 let v = (intern_reg_value v) in
                  let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
                  Interp.add_answer_to_stack next_state v)
     | Interp.Write_reg reg_form slice value ->
-      let optional_start = match slice with | Just (st1,st2) -> if (st1=st2) then Just st1 else Nothing | _ -> Nothing end in
-      let (v,_) = extern_value mode false optional_start value in Write_reg (extern_reg reg_form slice) v next_state
+      let optional_start = 
+	match slice with | Just (st1,st2) -> if (st1=st2) then Just st1 else Nothing | _ -> Nothing end in
+      Write_reg (extern_reg reg_form slice) (extern_reg_value optional_start value) next_state
     | Interp.Read_mem (Id_aux (Id i) _) value slice ->
       match List.lookup i memory_functions with
       | (Just (Just read_k,_,f)) -> 
-        let (location, length, tracking) = (f mode value) in
-        Read_mem read_k location length tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+        let (location, length, tracking) = (f mode value) in 
+	if (List.length location) = 8
+        then Read_mem read_k (Address_lifted location) length tracking 
+	  (fun v -> Interp.add_answer_to_stack next_state (intern_mem_value v))
+	else Error ("Memory address on read is not 64 bits")
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
     | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
       match List.lookup i memory_functions with
       | (Just (_,Just write_k,f)) -> 
         let (location, length, tracking) = (f mode loc_val) in
-        let (value, v_tracking) = (extern_value mode true Nothing write_val) in
-        Write_mem write_k location length tracking value v_tracking (fun b -> next_state) 
+        let (value, v_tracking) = (extern_mem_value mode write_val) in
+	if (List.length location) = 8
+        then Write_mem write_k (Address_lifted location) length tracking value v_tracking (fun b -> next_state) 
+	(*Note, does not pass boolean on conditional write, but we're not using that yet anyway*)
+	else Error "Memory address on write is not 64 bits"
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -441,12 +472,14 @@ let rec find_reg_name reg = function
   | (reg_name,v)::registers ->
     match (reg,reg_name) with
       | (Reg i, Reg n) -> if i = n then (Just v) else find_reg_name reg registers
-      | (Reg_slice i (p1,p2), Reg n) -> if i = n then (Just (slice_value v p1 p2)) else find_reg_name reg registers
-      | (Reg_field i f (p1,p2), Reg n) -> if i = n then (Just (slice_value v p1 p2)) else find_reg_name reg registers
+      | (Reg_slice i (p1,p2), Reg n) -> 
+	if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
+      | (Reg_field i f (p1,p2), Reg n) -> 
+	if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
       | (Reg_slice  i (p1,p2), Reg_slice n (p3,p4)) ->
 	if i=n 
 	then if p1=p3 && p2 = p4 then (Just v)
-	     else if p1>=p3 && p2<= p4 then (Just (slice_value v p1 p2))
+	     else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v p1 p2))
 	     else find_reg_name reg registers
 	  else find_reg_name reg registers
       | (Reg_field i f _,Reg_field n fn _) ->
@@ -457,20 +490,24 @@ let rec find_reg_name reg = function
 end end
 
 let rec ie_loop mode register_values i_state = 
+  let unknown_reg size =  
+    <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; rv_dir = D_increasing |> in
+  let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
   match (interp mode i_state) with
     | Done -> []
     | Error msg -> [E_error msg]
     | Read_reg reg i_state_fun -> 
       let v =  match register_values with
-	| Nothing -> Unknown
+	| Nothing -> unknown_reg 64
 	| Just(registers) -> match find_reg_name reg registers with
-	    | Nothing -> Unknown
+	    | Nothing -> unknown_reg 64 (*Wrong in some cases, need to look in reg and store full length of reg*)
 	    | Just v -> v end end in
       (E_read_reg reg)::(ie_loop mode register_values (i_state_fun v))
     | Write_reg reg value i_state->
       (E_write_reg reg value)::(ie_loop mode register_values i_state)
     | Read_mem read_k loc length tracking i_state_fun ->
-      (E_read_mem read_k loc length tracking)::(ie_loop mode register_values (i_state_fun Unknown))
+      (E_read_mem read_k loc length tracking)::
+	(ie_loop mode register_values (i_state_fun (unknown_mem (natFromInteger length))))
     | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
       (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode register_values (i_state_fun true))
     | Barrier barrier_k i_state ->
@@ -483,6 +520,9 @@ let interp_exhaustive register_values i_state =
   ie_loop mode register_values i_state
 
 let rec rr_ie_loop mode i_state = 
+  let unknown_reg size =  
+    <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; rv_dir = D_increasing |> in
+  let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
   match (interp mode i_state) with
     | Done -> ([],Done)
     | Error msg -> ([E_error msg], Error msg)
@@ -491,7 +531,7 @@ let rec rr_ie_loop mode i_state =
       let (events,outcome) = (rr_ie_loop mode i_state) in
       (((E_write_reg reg value)::events), outcome)
     | Read_mem read_k loc length tracking i_state_fun ->
-      let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in 
+      let (events,outcome) = (rr_ie_loop mode (i_state_fun (unknown_mem (natFromInteger length)))) in 
       (((E_read_mem read_k loc length tracking)::events),outcome)
     | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 834f3039..c4dc00f9 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -17,7 +17,7 @@ type read_kind = Read_plain | Read_reserve | Read_acquire
 type write_kind = Write_plain | Write_conditional | Write_release
 type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)
 
-type value = 
+(*type value = 
 | Bitvector of list bool  * bool * integer 
 (* In Bitvector bs b n:
    - the bs are the bits (true represents 1 and false represents 0)
@@ -72,7 +72,7 @@ instance  (Eq value)
   let (=) = valueEqual
   let (<>) x y = not (valueEqual x y)
 end
-
+*)
 type slice = (integer * integer)
 
 
@@ -136,20 +136,36 @@ instance (Ord reg_name)
   let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
 end
 
+type bit_lifted = 
+  | Bitl_zero
+  | Bitl_one
+  | Bitl_undef
+  | Bitl_unknown
+
+type direction = 
+  | D_increasing
+  | D_decreasing
+
+type register_value = <| rv_bits: list bit_lifted; rv_dir: direction; rv_start: integer |>
+
+type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *)
+
+type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*)
 
+type memory_value = list byte_lifted (* arbitrary length, > 1 *)
 
 type outcome =
 (* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
    integer is size to read, followed by registers that were used in computing that size *)
-| Read_mem of read_kind * value * integer * maybe (list reg_name) *  (value -> instruction_state)
+| Read_mem of read_kind * address_lifted * integer * maybe (list reg_name) *  (memory_value -> instruction_state)
 (* Request to write memory, first value and dependent registers is location, second is the value to write *)
-| Write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
-| Read_reg of reg_name * (value -> instruction_state) 
+| Read_reg of reg_name * (register_value -> instruction_state) 
 (* Request to write register *)
-| Write_reg of reg_name * value * instruction_state
+| Write_reg of reg_name * register_value * instruction_state
 (* List of instruciton states to be run in parrallel, any order permitted *)
 | Nondet_choice of list instruction_state * instruction_state
 (* Stop for incremental stepping, function can be used to display function call data *)
@@ -160,13 +176,13 @@ type outcome =
 | Error of string
 
 type event = 
-| E_read_mem of read_kind * value * integer * maybe (list reg_name)
-| E_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name)
+| E_read_mem of read_kind * address_lifted * integer * maybe (list reg_name)
+| E_write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_read_reg of reg_name
-| E_write_reg of reg_name * value
+| E_write_reg of reg_name * register_value
+| E_escape
 | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
-(*should there be a representation for escape down here?*)
 (*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
 
 
@@ -204,7 +220,7 @@ instance forall 'a. Ord 'a => (Ord (maybe 'a))
 end
 
 
-let eventCompare e1 e2 = 
+(*let eventCompare e1 e2 = 
   match (e1,e2) with
   | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
   | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
@@ -220,17 +236,17 @@ let eventCompare e1 e2 =
   | _ -> GT
   end
 
-
+*)
 
 instance (SetType event)
-  let setElemCompare = eventCompare
+  let setElemCompare = defaultCompare
 end
 
 
 
 (* Functions to build up the initial state for interpretation *)
 val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come from a .lem file generated by Sail*)
-val initial_instruction_state : context -> string -> list value -> instruction_state 
+val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
 (*Type representint the constructor parameters in instruction, other is a type not representable externally*)
@@ -254,7 +270,7 @@ end
 (*A representation of the AST node for each instruction in the spec, with concrete values from this call, and the potential static effects from the funcl clause for this instruction 
 Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
 *)
-type instruction = (string * list (string * instr_parm_typ * value) * list base_effect)
+type instruction = (string * list (string * instr_parm_typ * register_value) * list base_effect)
 
 let instructionEqual i1 i2 = match (i1,i2) with
   | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
@@ -264,7 +280,7 @@ type v_kind = Bitv | Bytev
 
 type decode_error = 
   | Unsupported_instruction_error of instruction
-  | Not_an_instruction_error of value
+  | Not_an_instruction_error of register_value
   | Internal_error of string
 
 type instruction_or_decode_error =
@@ -276,7 +292,10 @@ type i_state_or_error =
   | Instr of instruction * instruction_state
   | Decode_error of decode_error
 
-val num_to_bits : nat -> v_kind -> integer -> value
+(*val num_to_bits : nat -> v_kind -> integer -> value*)
+
+val byte_to_bits : word8 -> list bit_lifted
+val bits_to_byte : list bit_lifted -> word8
 
 val integer_of_byte_list : list word8 -> integer
 
@@ -284,45 +303,38 @@ val byte_list_of_integer : integer -> integer -> list word8
 
 
 (** propose to remove this: Function to decode an instruction and build the state to run it*)
-val decode_to_istate : context -> value -> i_state_or_error
+val decode_to_istate : context -> register_value -> i_state_or_error
 
 (** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*)
 (** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction.   This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *)
-val decode_to_instruction : context -> value -> instruction_or_decode_error
+val decode_to_instruction : context -> register_value -> instruction_or_decode_error
 
 (*Function to generate the state to run from an instruction form; is always an Instr*)
 val instruction_to_istate : context -> instruction -> i_state_or_error
 
 (* Augment an address by the given value *)
-val add_to_address : value -> integer -> value
+(*val add_to_address : value -> integer -> value
 
 (* Coerce a Bitvector value (presumed a multiple of 8 bits long) to a Bytevector value *)
 val coerce_Bytevector_of_Bitvector : value -> value
 
 (* Coerce a Bytevector value to a Bitvector value, increasing and starting at zero *)
-val coerce_Bitvector_of_Bytevector : value -> value
+val coerce_Bitvector_of_Bytevector : value -> value*)
 
-(* Slice a value into a smaller vector, starting at first number (wrt the indices of the bitvector value, not raw positions in its list of bits) and going to second (inclusive) according to order. 
-   For bytevectors, assumes you are slicing at the byte level, not the bit level *)
-val slice_value : value -> nat -> nat -> value
+(* Slice a register value into a smaller vector, starting at first number (wrt the indices of the register value, not raw positions in its list of bits) and going to second (inclusive) according to order. *)
+val slice_reg_value : register_value -> nat -> nat -> register_value
 
-(*append two vectors (bit x byte -> bit) *)
-val append_value : value -> value -> value 
+(*(*append two vectors (bit x byte -> bit) *)
+val append_value : value -> value -> value *)
 
 (* Big step of the interpreter, to the next request for an external action *)
 (* When interp_mode has eager_eval false, interpreter is (close to) small step *)
 val interp : interp_mode -> instruction_state -> outcome
 
 (* Run the interpreter without external interaction, feeding in Unknown on all reads except for those register values provided *)
-val interp_exhaustive : maybe (list (reg_name * value)) -> instruction_state -> list event
+val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event
 
 (* As above, but will request register reads: outcome will only be rreg, done, or error *)
 val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) 
 
 
-(*To discuss: Are these functions needed, since the memory requests carry the register dependencies for that request? *)
-val mem_read_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory reads to compute the addressses in is*)
-
-val mem_write_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory writes to compute the address (and value?, in a separate list?)*)
-
-
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 3fb85134..76e7dc54 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -49,9 +49,27 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 (* pp the bytes of a Bytevector as a hex value *)
 let bytes_to_string bytes = 
   (String.concat ""
-     (List.map (fun i -> let s = (Printf.sprintf "%x" i) in if (String.length s = 1) then "0"^s else s) bytes))
+     (List.map (fun i -> let s = (Printf.sprintf "%x" i) in if (String.length s = 1) then "0"^s else s) 
+	(List.map (fun (Byte_lifted bs) -> bits_to_byte bs) bytes)))
 
-let val_to_string v = match v with
+let bit_lifted_to_string = function
+  | Bitl_zero -> "0"
+  | Bitl_one ->  "1"
+  | Bitl_undef -> "u"
+  | Bitl_unknown -> "?"
+
+let reg_val_to_string v = 
+  let l = List.length v.rv_bits in
+  let start = (string_of_int (Big_int.int_of_big_int v.rv_start)) in
+  if List.mem l [8;16;32;64;128] then
+    let bytes = Interp_inter_imp.to_bytes v.rv_bits in
+    "0x" ^ "_" ^ start ^ "'" ^ bytes_to_string bytes
+  else (string_of_int l) ^ "_" ^ start ^ "'b" ^ 
+    collapse_leading (List.fold_right (^) (List.map bit_lifted_to_string v.rv_bits) "")
+
+let mem_val_to_string v = bytes_to_string v
+
+(*let val_to_string v = match v with
   | Bitvector(bools, inc, fst)-> 
       let l = List.length bools in
       if List.mem l [8;16;32;64;128] then 
@@ -67,7 +85,7 @@ let val_to_string v = match v with
     (*(string_of_int l) ^ " bytes -- " ^*) 
       "0x" ^
       bytes_to_string bytes
-  | Unknown0 -> "Unknown"
+  | Unknown0 -> "Unknown"*)
 
 let half_byte_to_hex v = 
   match v with
@@ -94,11 +112,11 @@ let rec bit_to_hex v =
     | a::b::c::d::vs -> half_byte_to_hex [a;b;c;d] ^ bit_to_hex vs
     | _ -> "bitstring given not divisible by 4"
 
-let val_to_hex_string v = match v with
+(*let val_to_hex_string v = match v with
   | Bitvector(bools, _, _) -> "0x" ^ bit_to_hex bools
   | Bytevector words -> val_to_string v
   | Unknown0 -> "Error: cannot turn Unknown into hex"
-;;
+;;*)
 
 let reg_name_to_string = function
   | Reg0 s -> s
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index ebb21152..c9d69eef 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -8,10 +8,11 @@ val loc_to_string : l -> string
 (*Returns the result of above for the exp's location *)
 val get_loc : tannot exp -> string
 (*interp_interface.value to string*)
-val val_to_string : value0 -> string
+val reg_value_to_string : register_value -> string
 val val_to_string_internal : Interp.lmem -> Interp.value -> string
-(*Force all representations to hex strings instead of a mixture of hex and binary strings*)
-val val_to_hex_string : value0 -> string
+
+(*(*Force all representations to hex strings instead of a mixture of hex and binary strings*)
+val val_to_hex_string : value0 -> string*)
 (* format one register *)
 val reg_name_to_string : reg_name -> string
 (* format the register dependencies *)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 1e74d3f0..2c705455 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -47,7 +47,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
   | _ -> assert false) l))
 ;;
 
-let val_to_string v = match v with
+(*let val_to_string v = match v with
   | Bitvector(bools, _, _) -> "0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
   | Bytevector words->
     "0x" ^ (String.concat ""
@@ -59,7 +59,7 @@ let val_to_string v = match v with
 	      | 14 -> "E"
 	      | 15 -> "F"
 	      | i  -> string_of_int i) words))		
-  | Unknown0 -> "Unknown"
+  | Unknown0 -> "Unknown"*)
 
 let reg_name_to_string = function
   | Reg0 s -> s