diff options
Diffstat (limited to 'src/lem_interp/run_interp_model.ml')
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 36 |
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) "" ""; |