path: root/src/lem_interp/interp_inter_imp.lem

import Interp
import Interp_lib
import Instruction_extractor
open import Interp_ast
open import Interp_interface
open import Pervasives
open import Assert_extra


val intern_reg_value : register_value -> Interp.value
val intern_mem_value : direction -> memory_value -> Interp.value
val extern_reg_value : maybe nat -> 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 (nat * nat) -> reg_name


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 bitl_to_ibit = 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 bit_to_ibit = function
  | Bitc_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown))
  | Bitc_one -> (Interp.V_lit (L_aux L_one Interp_ast.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 bits_to_ibits l = List.map bit_to_ibit l
let bitls_to_ibits l = List.map bitl_to_ibit l
let bitls_from_ibits l = List.map 
  (fun b -> 
    let b = (match b with | Interp.V_track v _ -> v | _ -> b end) in
    match b with
    | Interp.V_lit (L_aux L_zero _) -> Bitl_zero
    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitl_zero
    | Interp.V_lit (L_aux L_one _)  -> Bitl_one
    | Interp.V_vector _ _ [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 bits_from_ibits l = List.map 
  (fun b -> 
    let b = (match b with | Interp.V_track v _ -> v | _ -> b end) in
    match b with
    | Interp.V_lit (L_aux L_zero _) -> Bitc_zero
    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitc_zero
    | Interp.V_lit (L_aux L_one _)  -> Bitc_one
    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitc_one
   end) l

let rec to_bytes l = match l with
  | [] -> []
  | (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 all_known_bytes l = List.all (fun (Byte_lifted bs) -> List.all is_bool bs) l

let bits_to_word8 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_word8 given a non-8 list or one containing ? and u"

let intern_direction = function
  | D_increasing -> Interp.IInc
  | D_decreasing -> Interp.IDec
end

let intern_opcode direction (Opcode v) =
  let bits = List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v in
  let direction = intern_direction direction in
  Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits
		   
let intern_reg_value v = match v with
  | <| rv_bits=[b] |> -> bitl_to_ibit b
  | _ -> Interp.V_vector v.rv_start (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
end

let intern_mem_value direction v = 
  let bits = (List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) v) in
  let direction = intern_direction direction in
  Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) -1)) direction bits

let intern_ifield_value direction v =
  let bits = bits_to_ibits v in
  let direction = intern_direction direction in
  Interp.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits

(*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 
			       (Interp.V_tuple([Interp.V_lit(L_aux (L_num (size * 8)) Interp_ast.Unknown);
						Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) in
       let num_check = Interp_lib.to_num Interp_lib.Unsigned internal_value in
       match (num_check,internal_value) with
	 | (Interp.V_lit (L_aux (L_num n) _), Interp.V_vector _ _ bits) ->
	   if num = n
	   then (to_bytes (from_bits bits))
	   else failwith "byte_list_of_integer given an integer larger than given size"
       end
*)

let num_to_bits size kind num =
(* num_to_bits needed in src_power_get/trans_sail.gen - rather than reengineer the generation, we include a wrapper here *) 
  Interp_interface.bit_list_of_integer size num


(*
  match kind with
    | Bitv -> Bitvector (match (Interp_lib.to_vec_inc 
				  (Interp.V_tuple([Interp.V_lit(L_aux (L_num (integerFromNat size)) Interp_ast.Unknown);
						   Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) with
	| Interp.V_vector _ _ bits -> from_bits bits end) true 0
    | Bytev -> Bytevector (byte_list_of_integer (integerFromNat (size/8)) num)
end 

let integer_of_byte_list bytes =
  let intv = intern_value (Bytevector bytes) in
  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) _) (Just(t,_,_,_)),Nothing) -> 
    Reg x (Interp.reg_size r)
  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Just(i1,i2)) -> Reg_slice x (intFromNat i1, intFromNat i2)
  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> 
    let i = intFromInteger i in
    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 (intFromInteger i,intFromInteger 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 (intFromInteger i,intFromInteger j) (intFromNat i1, intFromNat j1)
end

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 dir bits ->
    <| rv_bits=(bitls_from_ibits bits); 
       rv_dir=(if Interp.is_inc(dir) then D_increasing else D_decreasing);
       rv_start=fst|>
  | Interp.V_vector_sparse fst stop inc bits default ->
    extern_reg_value optional_start (Interp_lib.fill_in_sparse v)
  | Interp.V_lit (L_aux L_zero _) -> 
    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 _) ->
    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 _) -> 
    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 _) ->
    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 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 (bitls_from_ibits bits), Nothing)
  | Interp.V_vector_sparse fst stop inc bits default ->
    extern_mem_value mode (Interp_lib.fill_in_sparse v)
  | _ -> Assert_extra.failwith ("extern_mem_value received non-externable value " ^ (Interp.string_of_value v))
end 

let rec extern_ifield_value v = match v with
  | Interp.V_track v regs -> extern_ifield_value v 
  | Interp.V_vector fst inc bits -> bits_from_ibits bits
  | Interp.V_vector_sparse fst stop inc bits default ->
    extern_ifield_value (Interp_lib.fill_in_sparse v)
  | Interp.V_lit (L_aux L_zero _) -> [Bitc_zero]
  | Interp.V_lit (L_aux L_false _) -> [Bitc_zero]
  | Interp.V_lit (L_aux L_one _) ->  [Bitc_one]
  | Interp.V_lit (L_aux L_true _) -> [Bitc_one]
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
    | (Bytevector bytes1, Bytevector bytes2) -> Bytevector (bytes1++bytes2)
    | ((Bitvector _ _ _ as bit),(Bytevector _ as byte)) ->
      (match (intern_value bit,intern_value byte) with
	| (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) -> 
	  (fst (extern_value (make_mode true false) false Nothing (Interp.V_vector a b (bits1++bits2))))
	| _ -> Unknown end)
    | ((Bytevector _ as byte),(Bitvector _ _ _ as bit)) ->
      (match (intern_value byte,intern_value bit) with
	| (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) -> 
	  (fst (extern_value (make_mode true false) true Nothing (Interp.V_vector a b (bits1++bits2))))
	| _ -> Unknown end)
    | _ -> Unknown 
end

let add_to_address value num =
  match value with
    | Unknown -> Unknown
    | Bitvector _ _ _ -> 
      fst(extern_value (make_mode true false) false Nothing
	             (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1 
			(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
    | Bytevector _ ->
      fst(extern_value (make_mode true false) true Nothing
	             (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1 
			(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
end


let coerce_Bytevector_of_Bitvector (v: value) : value =
  match v with
  | Bitvector bs b i -> Bytevector (to_bytes bs)
  | _ -> Assert_extra.failwith "coerce_Bytevector_of_Bitvector given non-Bitvector"
  end

let coerce_Bitvector_of_Bytevector (v: value) : value =
  match v with
  | Bytevector ws -> Bitvector 
        (List.concatMap 
           (fun w -> 
             List.reverse 
               (boolListFrombitSeq 8 (bitSeqFromNat w)))
            ws)
        true
        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_reg_value arg) in [e]
    | args -> List.map fst (List.map (Interp.to_exp (make_mode true false) Interp.eenv)
			      (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


let rec interp_to_value_helper arg instr direction thunk = 
  match thunk() with
    | Interp.Value value -> (Just value,Nothing)
    | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
    | Interp.Action (Interp.Call_extern i value) stack ->
      match List.lookup i (Interp_lib.library_functions direction) with
	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
	| Just f  -> 
          interp_to_value_helper arg instr direction (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
      end 
    | Interp.Action (Interp.Exit (E_aux e _)) _ ->
      match e with
	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
      end 
    | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
end

let call_external_functions direction outcome = 
  match outcome with
    | Interp.Action (Interp.Call_extern i value) stack ->
      match List.lookup i (Interp_lib.library_functions direction) with
	| Nothing -> Nothing
	| Just f -> Just (f value) end
    | _ -> Nothing end

let build_context defs reads writes barriers externs = 
  (*TODO add externs to to_top_env*)
  match Interp.to_top_env call_external_functions defs with 
    | (_,((Interp.Env _ _ dir _ _ _ _ _) as context)) -> 
      Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes barriers externs end


let rec find_instruction i = function
  | [] -> Nothing
  | Instruction_extractor.Skipped::instrs -> find_instruction i instrs
  | ((Instruction_extractor.Instr_form name parms effects) as instr)::instrs ->
      if i = name
      then Just instr
      else find_instruction i instrs
end

let migrate_typ = function
  | Instruction_extractor.IBit -> Bit
  | Instruction_extractor.IBitvector len ->
    Bvector (match len with Nothing -> Nothing | Just i -> Just (natFromInteger i) end) 
  | Instruction_extractor.IOther -> Other
end

let decode_to_istate top_level value = 
  let mode = make_mode true false in
  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _) = top_level in
  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_opcode direction value) in
  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
  let (instr_decoded,error) = interp_to_value_helper value ("",[],[]) internal_direction
    (fun _ -> Interp.resume 
      (make_mode true false) 
      (Interp.Thunk_frame 
	 (E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) 
	 top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
  match (instr_decoded,error) with
    | (Just instr, _) -> 
      let instr_external = match instr with
	| Interp.V_ctor (Id_aux (Id i) _) _ _ parm ->
	  match (find_instruction i instructions) with
	    | 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), (extern_ifield_value value))], effects)
		| (Interp.V_tuple vals,parms) -> 
		  (name, 
		   (Interp.map2 (fun value (p_name,ie_typ) -> 
		     (p_name,(migrate_typ ie_typ),(extern_ifield_value 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 internal_direction
	(fun _ -> Interp.resume 
	 (make_mode true false) 
	 (Interp.Thunk_frame 
	 (E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) 
	    (Interp_ast.Unknown, Nothing)) 
	 top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
      match (instr_decoded,error) with
	| (Just instr,_) ->
	  let (arg,_) = Interp.to_exp mode Interp.eenv instr in
	  Instr instr_external
	    (IState (Interp.Thunk_frame
		       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
		       top_env Interp.eenv Interp.emem Interp.Top)
	       top_level)
	| (Nothing, Just err) -> Decode_error err
      end 
    | (Nothing, Just err) -> Decode_error err
end


let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_decode_error  = 
  match decode_to_istate top_level value with
  | Instr inst is -> IDE_instr inst
  | Decode_error de -> IDE_decode_error de
  end

val instruction_to_istate : context -> instruction -> instruction_state 
let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instruction) : instruction_state  = 
  let mode = make_mode true false in
  let (Context top_env direction _ _ _ _) = top_level in
  let get_value (name,typ,v) = 
    let vec = intern_ifield_value direction v in
    let v = match vec with
      | Interp.V_vector start dir bits ->
	match typ with
	  | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end
	  | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec
	  | _ -> vec
       end 
    end in
    let (e,_) = Interp.to_exp mode Interp.eenv v in e 
  in
  (IState
     (Interp.Thunk_frame
	(E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
		  [(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms))
		      (Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))])
	   (Interp_ast.Unknown,Nothing))
	top_env Interp.eenv Interp.emem Interp.Top)
     top_level)

let rec interp_to_outcome mode context thunk = 
  let (Context _ direction mem_reads mem_writes barriers spec_externs) = context in
  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
  match thunk () with
  | Interp.Value _ -> Done
  | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
  | Interp.Action a next_state ->
    match a with
    | Interp.Read_reg reg_form slice -> 
      Read_reg (extern_reg reg_form slice) 
               (fun v -> 
                 let v = (intern_reg_value v) in
                 let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
                 IState (Interp.add_answer_to_stack next_state v) context)
    | 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
      Write_reg (extern_reg reg_form slice) (extern_reg_value optional_start value) (IState next_state context)
    | Interp.Read_mem (Id_aux (Id i) _) value slice ->
      match List.lookup i mem_reads with
      | (Just (MR read_k f)) -> 
        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 -> IState (Interp.add_answer_to_stack next_state (intern_mem_value direction v)) context)
	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 mem_writes with
      | (Just (MW write_k f return)) -> 
        let (location, length, tracking) = (f mode loc_val) in
        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 -> 
	    match return with 
	      | Nothing -> (IState next_state context)
	      | Just return_bool -> return_bool (IState next_state context) b end)
	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 ->
      match List.lookup i barriers with
	| Just barrier -> 
	  Barrier barrier (IState next_state context)
	| _ -> Error ("Barrier " ^ i ^ " function not found") end
    | Interp.Nondet exps -> 
      let nondet_states = List.map (Interp.set_in_context next_state) exps in
      Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context)
    | Interp.Call_extern i value -> 
      match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with
      | Nothing -> Error ("External function not available " ^ i)
      | Just f  -> 
        if (mode.Interp.eager_eval)
        then interp_to_outcome mode context (fun _ -> Interp.resume mode next_state (Just (f value))) 
        else let new_v = f value in
             Internal (Just i) 
                      (Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v)))
                      (IState (Interp.add_answer_to_stack next_state new_v) context)
      end
    | Interp.Step l Nothing Nothing -> Internal Nothing Nothing (IState next_state context)
    | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing (IState next_state context)
    | Interp.Step l (Just name) (Just value) ->
      Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context)
    end 
  end 

let interp mode (IState interp_state context) = 
  interp_to_outcome mode context (fun _ -> Interp.resume mode interp_state Nothing)

(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
let rec find_reg_name reg = function
  | [] -> Nothing
  | (reg_name,v)::registers ->
    match (reg,reg_name) with
      | (Reg i size, Reg n size2) -> if i = n && size = size2 then (Just v) else find_reg_name reg registers
      | (Reg_slice i (p1,p2), Reg n _) -> 
	if i = n then (Just (slice_reg_value v (natFromInt p1) (natFromInt p2))) else find_reg_name reg registers
      | (Reg_field i f (p1,p2), Reg n _) -> 
	if i = n then (Just (slice_reg_value v (natFromInt p1) (natFromInt 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_reg_value v (natFromInt p1) (natFromInt p2)))
	     else find_reg_name reg registers
	  else find_reg_name reg registers
      | (Reg_field i f _,Reg_field n fn _) ->
	if i=n && f = fn then (Just v) else find_reg_name reg registers
      | (Reg_f_slice i f _ (p1,p2), Reg_f_slice n fn _ (p3,p4)) ->
	if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers
      | _ -> find_reg_name reg registers
end end

let reg_size = function
  | Reg i size -> size
  | Reg_slice i (p1,p2) -> natFromInt (if p1 < p2 then (p2-p1 +1) else (p1-p2 +1))
  | Reg_field i f (p1,p2) -> natFromInt (if p1 < p2 then (p2-p1 +1) else (p1-p2 +1))
  | Reg_f_slice i f _ (p1,p2) -> natFromInt (if p1 < p2 then p2-p1 +1 else p1-p2+1)
end

let rec ie_loop mode register_values (IState interp_state context) = 
  let (Context _ direction externs reads writes barriers) = context in
  let unknown_reg size =  
    <| rv_bits = (List.replicate size Bitl_unknown);
       rv_start = (if direction = D_increasing then 0 else (size-1));
       rv_dir = direction |> in
  let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
  match interp mode (IState interp_state context) with
    | Done -> []
    | Error msg -> [E_error msg]
    | Read_reg reg i_state_fun -> 
      let v =  match register_values with
	| Nothing -> unknown_reg (reg_size reg)
	| Just(registers) -> match find_reg_name reg registers with
	    | Nothing -> unknown_reg (reg_size 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_mem 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 ->
      (E_barrier barrier_k)::(ie_loop mode register_values i_state)
    | Internal _ _ next -> (ie_loop mode register_values next)
     end ;;
  
let interp_exhaustive register_values i_state = 
  let mode = make_mode true true in
  ie_loop mode register_values i_state

let rec rr_ie_loop mode i_state = 
  let (IState _ (Context _ direction _ _ _ _)) = i_state in
  let unknown_reg size =  
    <| rv_bits = (List.replicate size Bitl_unknown); 
       rv_start = (if direction=D_increasing then 0 else (size-1));
       rv_dir = direction |> 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)
    | Read_reg reg i_state_fun -> ([], Read_reg reg i_state_fun)
    | Write_reg reg value 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_mem 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
      (((E_write_mem write_k loc length tracking value v_tracking)::events),outcome)
    | Barrier barrier_k i_state ->
      let (events,outcome) = (rr_ie_loop mode i_state) in
      (((E_barrier barrier_k)::events),outcome)
    | Internal _ _ next -> (rr_ie_loop mode next)
     end ;;

let rr_interp_exhaustive mode i_state events = 
  let (events',outcome) = rr_ie_loop mode i_state in ((events ++ events'),outcome)