Merge.

1 files changed, 18 insertions, 18 deletions

diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index fbb06eed..f8c05085 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -50,7 +50,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 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, inc, fst)->
+  | Bytevector words ->
     let l = List.length words in
     (string_of_int l) ^ " bytes --" ^
       (String.concat ""
@@ -191,7 +191,7 @@ module Mem = struct
     add key valu m
 
   let to_string loc v =
-    sprintf "[%s] -> %x" (val_to_string (Bytevector(loc, true, zero_big_int))) v
+    sprintf "[%s] -> %x" (val_to_string (Bytevector loc)) v
 end ;;
 
 let rec slice bitvector (start,stop) = 
@@ -202,8 +202,8 @@ let rec slice bitvector (start,stop) =
                  inc,
                  (if inc then zero_big_int else (add_big_int (sub_big_int stop start) unit_big_int)))
                 
-    | Bytevector(bytes, inc, fst) -> 
-      Bytevector((Interp.from_n_to_n start stop bytes),inc,fst) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
+    | Bytevector bytes -> 
+      Bytevector((Interp.from_n_to_n start stop bytes)) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
     | Unknown0 -> Unknown0
 ;;
 
@@ -245,12 +245,12 @@ let fupdate_slice original e (start,stop) =
                                     (if inc then (sub_big_int start fst) else (sub_big_int fst start))
                                     (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bs bools), inc, fst)
       | _ -> Unknown0)
-    | Bytevector(bytes,inc,fst) -> (*Can this happen?*)
+    | Bytevector bytes -> (*Can this happen?*)
       (match e with
-      | Bytevector([byte],_,_) -> 
-        Bytevector((list_update zero_big_int start stop byte bytes),inc,fst)
-      | Bytevector(bs,_,_) ->
-        Bytevector((list_update_list zero_big_int start stop bs bytes),inc,fst)
+      | Bytevector [byte] -> 
+        Bytevector (list_update zero_big_int start stop byte bytes)
+      | Bytevector bs ->
+        Bytevector (list_update_list zero_big_int start stop bs bytes)
       | _ -> Unknown0)
     | Unknown0 -> Unknown0
 ;;
@@ -272,10 +272,10 @@ let rec format_events = function
     "     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, dep))::events ->
+  | (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, dep, value, vdep))::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) ->
@@ -306,13 +306,13 @@ let rec perform_action ((reg, mem) as env) = function
    let old_val = Reg.find id reg in
    let new_val = fupdate_slice old_val value (combine_slices range mini_range) in
    (None,(Reg.add id new_val reg,mem))
- | Read_mem0(_,Bytevector(location,_,_), length, _,_) ->
+ | Read_mem0(_,(Bytevector location), length, _,_) ->
    let rec reading location length = 
      if eq_big_int length zero_big_int 
      then []
      else (Mem.find location mem)::(reading (increment location) (sub_big_int length unit_big_int)) in
-   (Some (Bytevector((List.rev (reading location length)), true, zero_big_int)), env) (*TODO: how to get order back here? *)
- | Write_mem0(_,(Bytevector(location,_,_)), length, _, (Bytevector(bytes,_,_)),_,_) ->
+   (Some (Bytevector((List.rev (reading location length)))), env)
+ | Write_mem0(_,(Bytevector location), length, _, (Bytevector bytes),_,_) ->
    let rec writing location length bytes mem = 
      if eq_big_int length zero_big_int
      then mem
@@ -440,20 +440,20 @@ let run
 	| Write_reg0(reg,value,next) ->
 	  show "write_reg" (reg_name_to_string reg) left (val_to_string value);
 	  (step next, env', next)
-	| Read_mem0(kind, location, length, dependencies, next_thunk) ->
+	| Read_mem0(kind, location, length, tracking, next_thunk) ->
 	  (match return with
 	    | Some(value) -> 
 	      show "read_mem" (val_to_string location) right (val_to_string value);
-              (match dependencies with
+              (match tracking with
               | None -> ()
               | Some(deps) ->
                 show "read_mem address depended on" (dependencies_to_string deps) "" "");
 	      let next = next_thunk value in
 	      (step next, env', next)
 	    | None -> assert false)
-	| Write_mem0(kind,location, length, dependencies, value, val_dependencies, next_thunk) ->
+	| Write_mem0(kind,location, length, tracking, value, v_tracking, next_thunk) ->
 	  show "write_mem" (val_to_string location) left (val_to_string value);
-          (match (dependencies,val_dependencies) with
+          (match (tracking,v_tracking) with
           | (None,None) -> ();
           | (Some(deps),None) ->
             show "write_mem address depended on" (dependencies_to_string deps) "" "";