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 : 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 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"

(*All but reg_value should take a mode to get direction and start correct*)
let intern_opcode (Opcode v) =
  Interp.V_vector 0 true
    (List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v)
		   
let intern_reg_value v = match v with
  | <| rv_bits=[b] |> -> bitl_to_ibit b
  | _ -> Interp.V_vector (integerFromInt v.rv_start) (v.rv_dir = D_increasing) (bitls_to_ibits v.rv_bits)
end

let intern_mem_value v = 
  Interp.V_vector 0 true (List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) v)

let intern_ifield_value v =
  Interp.V_vector 0 true (bits_to_ibits 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 
			       (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 (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)
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 inc bits ->
    <| rv_bits=(bitls_from_ibits bits); 
       rv_dir=(if inc then D_increasing else D_decreasing);
       rv_start=(intFromInteger 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 -> (intFromInteger 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 -> (intFromInteger 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 -> (intFromInteger 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 -> (intFromInteger 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 -> (intFromInteger 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 -> (intFromInteger 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
  let start = intFromInteger start in
  let stop = intFromInteger stop in
  <| v with rv_bits = (Interp.from_n_to_n (integerFromInt (if inc then (start - v.rv_start) else (v.rv_start - start)))
                                          (integerFromInt (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 countLeadingZeros_helper bits =
  match bits with
    | (Interp.V_lit (L_aux L_zero _))::bits -> 
      let (Interp.V_lit (L_aux (L_num n) loc)) = countLeadingZeros_helper bits in
      Interp.V_lit (L_aux (L_num (n+1)) loc)
    | _ -> Interp.V_lit (L_aux (L_num 0) Interp_ast.Unknown)
end
let rec countLeadingZeros (Interp.V_tuple v) = match v with
  | [Interp.V_track v r;Interp.V_track v2 r2] -> 
    Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) (r++r2)
  | [Interp.V_track v r;v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
  | [v;Interp.V_track v2 r2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
  | [Interp.V_unknown;_] -> Interp.V_unknown
  | [_;Interp.V_unknown] -> Interp.V_unknown
  | [Interp.V_vector _ _ bits;Interp.V_lit (L_aux (L_num n) _)] -> 
    countLeadingZeros_helper (snd (List.splitAt (natFromInteger n) bits))
end

(*Power specific external functions*)
let power_externs = [
  ("countLeadingZeroes", countLeadingZeros);
]

(*All external functions*)
let external_functions = Interp_lib.function_map ++ power_externs

type mem_function = (string * 
                     (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.
  Should probably be expanded into a parameter to mode as with above
*)
let memory_functions =
  [ ("MEMr", (Just(Read_plain), Nothing, 
	     (fun mode v -> match v with
	       | Interp.V_tuple [location;length] ->
		 match length with
		   | Interp.V_lit (L_aux (L_num len) _) ->
		     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_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)))
	      end end end)));
    ("MEMr_reserve", (Just(Read_reserve),Nothing,
		      (fun mode v -> match v with
			| Interp.V_tuple [location;length] ->
			  match length with
			    | Interp.V_lit (L_aux (L_num len) _) ->
			      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_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)))
		       end end end)));		      
    ("MEMw", (Nothing, Just(Write_plain), 
	      (fun mode v -> match v with
		| Interp.V_tuple [location;length] ->
		  match length with
		    | Interp.V_lit (L_aux (L_num len) _) ->
		      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_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)))
	       end end end)));
    ("MEMw_conditional", (Nothing, Just(Write_conditional), 
	      (fun mode v -> match v with
		| Interp.V_tuple [location;length] ->
		  match length with
		    | Interp.V_lit (L_aux (L_num len) _) ->
		      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_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)))
	      end end end)));
  ]

let barrier_functions = [
  ("I_Sync", Isync);
  ("H_Sync", Sync);
  ("LW_Sync", LwSync);
  ("EIEIO", Eieio);
]

let rec interp_to_value_helper arg instr 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 external_functions with
	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
	| Just f  -> 
          interp_to_value_helper arg instr (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 outcome = 
  match outcome with
    | Interp.Action (Interp.Call_extern i value) stack ->
      match List.lookup i external_functions with
	| Nothing -> Nothing
	| Just f -> Just (f value) end
    | _ -> Nothing end

let build_context defs = match Interp.to_top_env call_external_functions defs with (_,context) -> context 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 (intFromInteger i) end) 
  | Instruction_extractor.IOther -> Other
end

let decode_to_istate top_level value = 
  let mode = make_mode true false in
  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_opcode value) in
  let (Interp.Env _ instructions _ _ _ _ _) = top_level in
  let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
    (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_level 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
	(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_level 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
	    (Interp.Thunk_frame
		   (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
		   top_level Interp.eenv Interp.emem Interp.Top)
	| (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 get_value (name,typ,v) = 
    let (e,_) = Interp.to_exp mode Interp.eenv (intern_ifield_value v) in e in
    (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_level Interp.eenv Interp.emem Interp.Top) 

let rec interp_to_outcome mode thunk = 
  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 
                 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
      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 
	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_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 ->
      match List.lookup i barrier_functions with
	| Just barrier -> 
	  Barrier barrier next_state
	| _ -> 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 nondet_states next_state      
    | Interp.Call_extern i value -> 
      match List.lookup i external_functions with
      | Nothing -> Error ("External function not available " ^ i)
      | Just f  -> 
        if (mode.Interp.eager_eval)
        then interp_to_outcome mode (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)))
                      (Interp.add_answer_to_stack next_state new_v)
      end
    | Interp.Step l Nothing Nothing -> Internal Nothing Nothing next_state 
    | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing next_state
    | Interp.Step l (Just name) (Just value) ->
      Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) next_state
    end 
  end 

let interp mode i_state = interp_to_outcome mode (fun _ -> Interp.resume mode i_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 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

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

let rec ie_loop mode register_values i_state = 
  let unknown_reg size =  
    <| rv_bits = (List.replicate (natFromInteger size) Bitl_unknown); rv_start = 0; rv_dir = D_increasing |> in
  let unknown_mem size = List.replicate (natFromInteger 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_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 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)
    | 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 (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
      (((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)