path: root/src/lem_interp/interp_inter_imp.lem

import Interp
import Interp_lib
import Instruction_extractor
import Set_extra
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 : interp_mode -> direction -> memory_value -> Interp.value
val extern_reg_value : reg_name -> 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_interp_mode eager_eval tracking_values = 
  <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;;

let make_mode eager_eval tracking_values endian = 
  <|internal_mode = make_interp_mode eager_eval tracking_values;
    endian = endian|>;;
let make_mode_exhaustive endian = 
  <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true|>;
     endian = endian |>;;
let tracking_dependencies mode = mode.internal_mode.Interp.track_values
let make_eager_mode mode = <| mode with internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;;
let make_default_mode _ = <|internal_mode = make_interp_mode false false; endian = E_big_endian|>;;

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 extern_direction = function
  | Interp.IInc -> D_increasing
  | Interp.IDec -> D_decreasing
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_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
end

let intern_mem_value mode direction v = 
  let v = if mode.endian = E_big_endian then v else List.reverse v in
  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 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

let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
  match d with
    | D_increasing -> (i,j) (*This is the case the thread/concurrecny model expects, so no change needed*)
    | D_decreasing -> 
      let slice_i = start - i in 
      let slice_j = (i - j) + slice_i in
      (slice_i,slice_j)
   end 

let extern_reg r slice = match (r,slice) with
  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> 
    Reg x (Interp.reg_start_pos r) (Interp.reg_size r) (extern_direction dir)
  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Just(i1,i2)) -> 
    let start = Interp.reg_start_pos r in
    let edir = extern_direction dir in
    Reg_slice x start edir (extern_slice edir start (i1, i2))
  | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _),Nothing) -> 
    let i = natFromInteger i in
    let start = Interp.reg_start_pos main_r in
    let edir = extern_direction dir in
    Reg_field y start edir x (extern_slice edir start (i,i))
  | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Nothing) -> 
    let start = Interp.reg_start_pos main_r in
    let edir = extern_direction dir in
    Reg_field y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j))
  | (Interp.SubReg (Id_aux (Id x) _) 
       ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) ->
    let start = Interp.reg_start_pos main_r in
    let edir = extern_direction dir in
    Reg_f_slice y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j)) 
                               (extern_slice edir start (i1, j1))
end

let rec extern_reg_value reg_name v = 
  match v with
    | Interp.V_track v regs -> extern_reg_value reg_name v 
    | Interp.V_vector_sparse fst stop inc bits default ->
      extern_reg_value reg_name (Interp_lib.fill_in_sparse v)
    | _ ->
      let (internal_start, external_start, direction) =
	(match reg_name with 
	  | Reg _ start size dir ->
	    (start, (if dir = D_increasing then start else (start - (size +1))), dir)
	  | Reg_slice _ reg_start dir (slice_start, slice_end) ->
	    ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
	     slice_start, dir)
	  | Reg_field _ reg_start dir _ (slice_start, slice_end) ->
	    ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
	     slice_start, dir)
	  | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) ->
	    ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
	     slice_start, dir) end) in
      let bit_list = 
	(match v with 
	  | Interp.V_vector fst dir bits -> bitls_from_ibits bits
	  | Interp.V_lit (L_aux L_zero _) -> [Bitl_zero]
	  | Interp.V_lit (L_aux L_false _) -> [Bitl_zero]
	  | Interp.V_lit (L_aux L_one _) -> [Bitl_one]
	  | Interp.V_lit (L_aux L_true _) -> [Bitl_one]
	  | Interp.V_lit (L_aux L_undef _) -> [Bitl_undef]
	  | Interp.V_unknown -> [Bitl_unknown] end) in
      <| rv_bits=bit_list; 
         rv_dir=direction;
	 rv_start=external_start;
	 rv_start_internal = internal_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.internal_mode.Interp.track_values 
     then (Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList regs)))
     else Nothing)
  | Interp.V_vector fst inc bits -> 
    let bytes = to_bytes (bitls_from_ibits bits) in 
    if mode.endian = E_big_endian 
    then (bytes, Nothing)
    else (List.reverse bytes, 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 i_name field_name v ftyp = match (v,ftyp) with
  | (Interp.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp
  | (Interp.V_vector fst inc bits,_) -> bits_from_ibits bits
  | (Interp.V_vector_sparse fst stop inc bits default,_) ->
    extern_ifield_value i_name field_name (Interp_lib.fill_in_sparse v) ftyp
  | (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]
  | (Interp.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i
  | (Interp.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i
  | (Interp.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i
  | (Interp.V_ctor _ _ (Interp.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i)
  | (Interp.V_ctor _ _ (Interp.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i)
  | _ -> Assert_extra.failwith ("extern_ifield_value of " ^ i_name ^ " for field " ^ field_name ^ " given non-externable " ^ (Interp.string_of_value v) ^ " ftyp is " ^ show ftyp)
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 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_interp_mode true false) Interp.eenv (intern_reg_value arg) in [e]
    | args -> List.map fst (List.map (Interp.to_exp (make_interp_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 "istate top level") Interp.Top


let rec interp_to_value_helper arg err_str 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 err_str instr direction 
	    (fun _ -> Interp.resume (make_interp_mode true false) stack (Just (f value)))
      end 
    | (Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack,_,_) ->
      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))
	| E_lit (L_aux (L_string str) _) -> (Nothing, Just (Internal_error ("Exit called with message: " ^ str)))
	| E_id (Id_aux (Id i) _) -> 
	  (match (Interp.resume (make_interp_mode true false) (Interp.set_in_context stack exp) Nothing) with
	    | (Interp.Value (Interp.V_lit (L_aux (L_string str) _)),_,_) ->
	      (Nothing, Just (Internal_error ("Exit called when decoding "^err_str ^" with message: " ^ str)))
	    | _ -> (Nothing, Just (Internal_error ("Exit called with unrecognized expression bound to an id " ^ i))) end)
	| _ -> (Nothing, Just (Internal_error "Exit called with unrecognized expression"))
      end 
    | (Interp.Action (Interp.Read_reg r _) _,_,_) ->
      let rname = match r with 
	| Interp.Reg (Id_aux (Id i) _) _ _ -> i
	| Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i end in
      (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a decode of " ^ err_str)))
    | (Interp.Action (Interp.Write_reg _ _ _) _,_,_) ->
      (Nothing, Just (Internal_error "Register write request in a decode"))
    | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
      (Nothing, Just (Internal_error "Read memory request in a decode"))
    | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
      (Nothing, Just (Internal_error "Write memory request in a decode"))
    | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
      (Nothing, Just (Internal_error "Write ea request in a decode"))
    | (Interp.Action (Interp.Write_memv _ _) _,_,_) ->
      (Nothing, Just (Internal_error "Write memory value request in a decode"))
    | _ -> (Nothing, Just (Internal_error "Non expected action in a 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 write_eas write_vals 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 write_eas write_vals 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 len  
  | Instruction_extractor.IRange len -> Range len
  | Instruction_extractor.IEnum s max -> Enum s max
  | Instruction_extractor.IOther -> Other
end

let decode_to_istate top_level value = 
  let mode = make_interp_mode true false in
  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in
  let intern_val = intern_opcode direction value in
  let val_str = Interp.string_of_value intern_val in
  let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
  let (instr_decoded,error) = interp_to_value_helper value val_str ("",[],[]) internal_direction
    (fun _ -> Interp.resume 
      mode 
      (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 "decode top level") 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)]) -> 
		  let t = migrate_typ ie_typ in
		  (name, [(p_name,t, (extern_ifield_value name p_name value t))], effects)
		| (Interp.V_tuple vals,parms) -> 
		  (name, 
		   (Interp_utilities.map2 (fun value (p_name,ie_typ) -> 
		     let t = migrate_typ ie_typ in
		     (p_name,t,(extern_ifield_value name p_name value t))) 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 val_str instr_external internal_direction
	(fun _ -> Interp.resume 
	 mode
	  (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 "decode second top level") 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 "execute") 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_interp_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
	  | Enum _ _ -> 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 "execute") Interp.Top)
     top_level)

let rec interp_to_outcome mode context thunk = 
  let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in
  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
  match thunk () with
  | (Interp.Value _,lm,le) -> (Done,lm)
  | (Interp.Error l msg,lm,le) -> (Error msg,lm)
  | (Interp.Action a next_state,lm,le) ->
    (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.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in 
            IState (Interp.add_answer_to_stack next_state v) context), lm)
      | Interp.Write_reg reg_form slice value ->
	let reg_name = extern_reg reg_form slice in
	(Write_reg reg_name (extern_reg_value reg_name value) (IState next_state context),lm)
      | 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 let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with
	      | Just bs -> Just (integer_of_byte_list bs)
	      | _ -> Nothing end in
                Read_mem read_k (Address_lifted location address_int) length tracking 
		  (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value mode direction v)) context)
	    else Error ("Memory address on read is not 64 bits")
          | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
        end  , lm)
      | 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 let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with
	      | Just bs -> Just (integer_of_byte_list bs)
	      | _ -> Nothing end in
             Write_mem write_k (Address_lifted location address_int) 
	       length tracking value v_tracking 
	       (fun b -> 
		 match return with 
		   | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) 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 , lm)
      | Interp.Write_ea (Id_aux (Id i) _) loc_val ->
	(match List.lookup i mem_write_eas with
	  | (Just (MEA write_k f)) ->
	    let (location, length, tracking) = (f mode loc_val) in
	    if (List.length location) = 8
	    then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with
	      | Just bs -> Just (integer_of_byte_list bs)
	      | _ -> Nothing end in
              Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context)
            else Error "Memory address for write is not 64 bits"
          | _ -> Error ("Memory " ^ i ^ " function to signal impending write, not found") end, lm)
        | Interp.Write_memv (Id_aux (Id i) _) write_val ->
	  (match List.lookup i mem_write_vals with
	    | (Just (MV return)) -> 
	      let (value, v_tracking) = 
		match (Interp.detaint write_val) with
		  | Interp.V_tuple[_;v] -> (extern_mem_value mode (Interp.retaint write_val v))
		  | _ -> (extern_mem_value mode write_val) end in
              Write_memv value v_tracking 
		(fun b -> 
		  match return with
		    | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
		    | Just return_bool -> return_bool (IState next_state context) b end)
            | _ -> Error ("Memory " ^ i ^ " function with write value kind not found") end, lm)
         | 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, lm)
         | Interp.Footprint (Id_aux (Id i) _) lval ->
	   (Footprint (IState next_state context), lm)
	 | Interp.Nondet exps tag ->
	   (match tag with
	     | Tag_unknown _ ->
	       let possible_states = List.map (Interp.set_in_context next_state) exps in
	       let cleared_possibles = List.map Interp.clear_stack_state possible_states in
	       Analysis_non_det (List.map (fun i -> IState i context) cleared_possibles) (IState next_state context)   
	     | _ -> 
	       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) end, lm)
         | 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), lm)
	     | Just f  -> 
               if (mode.internal_mode.Interp.eager_eval)
               then interp_to_outcome mode context 
		    (fun _ -> Interp.resume mode.internal_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), lm)
            end)
         | Interp.Step l Nothing Nothing -> (Internal Nothing Nothing (IState next_state context), lm)
	 | Interp.Step l (Just name) Nothing -> (Internal (Just name) Nothing (IState next_state context), lm)
	 | Interp.Step l (Just name) (Just value) ->
	   (Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context), lm)
	 | Interp.Exit e -> 
	   (Escape (match e with
	     | E_aux (E_lit (L_aux L_unit _)) _ -> Nothing
	     | _ -> Just (IState (Interp.set_in_context next_state e) context) end)  (IState next_state context),
	    (snd (Interp.get_stack_state next_state)))
         end )  
        end

let interp mode (IState interp_state context) = 
  match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with
    | (o,_) -> o
end 

(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
(*TODO immediate: this will be impacted by need to change slicing *)
let rec find_reg_name reg = function
  | [] -> Nothing
  | (reg_name,v)::registers ->
    match (reg,reg_name) with
      | (Reg i start size dir, Reg n start2 size2 dir2) -> 
	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 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_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 _) ->
	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

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

(*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*)
let rec ie_loop mode register_values (IState interp_state context) = 
  let (Context _ direction externs reads writes write_eas write_vals barriers) = context in
  let unknown_reg size =  
    <| rv_bits = (List.replicate size Bitl_unknown);
       rv_start = 0;
       rv_start_internal = (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_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with
    | (Done,lm) -> ([],(lm,true))
    | (Error msg,lm) -> ([E_error msg],(lm,false))
    | (Escape Nothing i_state,lm) -> ([E_escape],(lm,false))
    (*Do we want to record anything about the escape expression, which may be a function call*)
    | (Escape _ i_state,lm) -> ([E_escape],(lm,false))
    | (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
      let (events,analysis_data) = ie_loop mode register_values (i_state_fun v) in
      ((E_read_reg reg)::events,analysis_data)
    | (Write_reg reg value i_state, _)->
      let (events,analysis_data) = ie_loop mode register_values i_state in
      ((E_write_reg reg value)::events,analysis_data)
    | (Read_mem read_k loc length tracking i_state_fun, _) ->
      let (events,analysis_data) = ie_loop mode register_values (i_state_fun (unknown_mem length)) in
      ((E_read_mem read_k loc length tracking)::events,analysis_data)
    | (Write_mem write_k loc length tracking value v_tracking i_state_fun, _) ->
      let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
      let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
      (*TODO: consider if lm and lm should be distinct and merged*)
      ((E_write_mem write_k loc length tracking value v_tracking)::(events++events'),analysis_data)
    | (Write_ea write_k loc length tracking i_state, _) ->
      let (events,analysis_data) = ie_loop mode register_values i_state in
      ((E_write_ea write_k loc length tracking)::events,analysis_data)
    | (Write_memv value tracking i_state_fun, _) ->
      let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
      let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
      (*TODO: consider if lm and lm should be merged*)
      ((E_write_memv value tracking)::(events++events'),analysis_data)
    | (Barrier barrier_k i_state, _) ->
      let (events,analysis_data) = ie_loop mode register_values i_state in
      ((E_barrier barrier_k)::events,analysis_data)
    | (Footprint i_state, _) ->
      let (events,analysis_data) = ie_loop mode register_values i_state in
      (E_footprint::events,analysis_data)
    | (Internal _ _ next, _) -> (ie_loop mode register_values next)
    | (Analysis_non_det possible_istates i_state,_) ->
      if possible_istates = []
      then ie_loop mode register_values i_state
      else 
	let (possible_events,possible_states) = List.unzip(List.map (ie_loop mode register_values) possible_istates) in
	let (unified_mem,update_mem) = List.foldr 
	  (fun (lm,terminated_normally) (mem,update_mem) -> 
	    if terminated_normally && update_mem
	    then (Interp.merge_lmems lm mem, true)
	    else if terminated_normally 
	    then (lm, true)
	    else (mem, false))	  
	  (List_extra.head possible_states) (List_extra.tail possible_states) in
	let updated_i_state = 
	  if update_mem
	  then match i_state with 
	    | (IState interp_state context) -> IState (Interp.update_stack_state interp_state unified_mem) context end
	  else i_state in
        let (events,analysis_data) = ie_loop mode register_values updated_i_state in
        ((List.concat possible_events)++events, analysis_data)
     end ;;
  
let interp_exhaustive register_values i_state = 
  let mode = make_mode_exhaustive E_big_endian in
  match ie_loop mode register_values i_state with
    | (events,_) -> events
end

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 = 0;
       rv_start_internal = (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)