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_interpreter_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_interpreter_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_interpreter_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 = Interp.detaint b 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_vector _ _ [Interp.V_lit (L_aux L_undef _)] -> Bitl_undef
    | Interp.V_unknown -> Bitl_unknown
    | _ -> Assert_extra.failwith ("bitls_from_ibits given unexpected " ^ (Interp.string_of_value b)) end) l

let bits_from_ibits l = List.map 
  (fun b -> 
    let b = Interp.detaint b 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
    | _ -> Assert_extra.failwith ("bits_from_ibits given unexpected " ^ (Interp.string_of_value b))
   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)
  | _ -> Assert_extra.failwith "to_bytes given list of bits not divisible by 8"
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))
  | _ -> Assert_extra.failwith "extern_reg given non-externable reg" 
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]
          | _ -> Assert_extra.failwith ("extern_reg_val given non externable value " ^ (Interp.string_of_value v)) 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
  let r_internal_start = if inc then start else (stop - start) + 1 in
  let r_start = if inc then r_internal_start else start in
  <| v with rv_bits = (Interp.from_n_to_n
                         (if inc then (start - v.rv_start_internal) else (v.rv_start_internal - start))
                         (if inc then (stop - v.rv_start_internal) else (v.rv_start_internal - stop)) v.rv_bits);
            rv_start = r_start;
            rv_start_internal = r_internal_start
  |> 

let update_reg_value_slice reg_name v start stop v2 =
  let v_internal = intern_reg_value v in
  let v2_internal = intern_reg_value v2 in
  extern_reg_value reg_name
    (if start = stop then
      (Interp.fupdate_vec v_internal start v2_internal)
    else
      (Interp.fupdate_vector_slice v_internal v2_internal start stop))

(*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


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_interpreter_mode true false) Interp.eenv (intern_reg_value arg) in [e]
    | args -> List.map fst (List.map (Interp.to_exp (make_interpreter_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

type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal
type interp_value_return =
  | Ivh_value of Interp.value
  | Ivh_value_after_exn of Interp.value
  | Ivh_error of decode_error

let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk =
  let errk_str = match ivh_mode with
    | Ivh_translate -> "translate"
    | Ivh_decode -> "decode"
    | Ivh_unsupported -> "supported_instructions"
    | Ivh_illegal -> "illegal instruction" end in
  let events_out = match events with [] -> Nothing | _ -> Just events end in
  let mode = (make_interpreter_mode true false) in
  match thunk() with
    | (Interp.Value value,_,_) ->
      if exn_seen
      then (Ivh_value_after_exn value, events_out)
      else
        (match ivh_mode with
         | Ivh_translate -> (Ivh_value value, events_out)
         | _ ->
           (match value with
            | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
            | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
              (match ivh_mode with
               | Ivh_decode -> (Ivh_error (Not_an_instruction_error arg), events_out)
               | Ivh_illegal -> (Ivh_error (Not_an_instruction_error arg), events_out)
               | Ivh_unsupported -> (Ivh_error (Unsupported_instruction_error instr), events_out)
               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end) end) end)
    | (Interp.Error l msg,_,_) -> (Ivh_error (Internal_error msg), events_out)
    | (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
      match List.lookup i (Interp_lib.library_functions direction) with
        | Nothing -> (Ivh_error (Internal_error ("External function not available " ^ i)), events_out)
        | Just f  -> 
          interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
                                 (fun _ -> Interp.resume mode stack (Just (f value)))
      end
    | (Interp.Action (Interp.Fail v) stack, _, _) ->
      match (Interp.detaint v) with
      | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) ->
        (Ivh_error (Internal_error ("Assert failed: " ^ s)), events_out)
      | _ -> (Ivh_error (Internal_error "Assert failed"), events_out) end
    | (Interp.Action (Interp.Exit exp) stack,_,_) ->
      interp_to_value_helper arg ivh_mode err_str instr direction registers events true
        (fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing)
    | (Interp.Action (Interp.Read_reg r slice) stack,_,_) ->
      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
        | _ -> Assert_extra.failwith "Reg not following expected structure" end in
      let err_value =
        (Ivh_error (Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)),
        events_out) in
      (match registers with
        | Nothing -> err_value
        | Just(regs) ->
          let reg = extern_reg r slice in
          match find_reg_name reg regs with
            | Nothing -> err_value
            | Just v ->
              let value = intern_reg_value v in
              interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
                (fun _ -> Interp.resume mode stack (Just value)) end end)      
    | (Interp.Action (Interp.Write_reg r slice value) stack,_,_) ->
      let ext_reg = extern_reg r slice in
      let reg_value = extern_reg_value ext_reg value in
      interp_to_value_helper arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events)
        exn_seen (fun _ -> Interp.resume mode stack Nothing)
    | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
      (Ivh_error (Internal_error ("Read memory request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
      (Ivh_error (Internal_error ("Write memory request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
      (Ivh_error (Internal_error ("Write ea request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Write_memv _ _) _,_,_) ->
      (Ivh_error (Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
    | _ -> (Ivh_error (Internal_error ("Non expected action in a " ^ errk_str)), events_out)
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 translate_address top_level end_flag thunk_name registers address =
  let (Address bytes i) = address in
  let mode = make_mode true false end_flag in
  let int_mode = mode.internal_mode in
  let (Context top_env direction _ _ _ _ _ _) = top_level in
  let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in
  let val_str = Interp.string_of_value intern_val in
  let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
  let (address_error,events) =
    interp_to_value_helper (Opcode bytes) Ivh_translate val_str ("",[],[]) internal_direction
      registers [] false
      (fun _ -> Interp.resume 
        int_mode 
        (Interp.Thunk_frame 
         (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown)
                   [arg;E_aux (E_lit (L_aux (L_num 0) Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)])
            (Interp_ast.Unknown, Nothing)) 
         top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in
  match (address_error) with
  | Ivh_value addr ->
    let (mem_v,_) = extern_mem_value mode addr in 
    ((address_of_memory_value end_flag mem_v), events)
  | Ivh_value_after_exn _ ->
    (Nothing, events)
  | Ivh_error err -> match err with
     | Internal_error msg -> Assert_extra.failwith msg
     | _ -> Assert_extra.failwith "Not an internal error either" end 
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 registers value = 
  let mode = make_interpreter_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,events) =
    interp_to_value_helper value Ivh_decode val_str ("",[],[]) internal_direction registers [] false
      (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
    | Ivh_value 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)
                | _ -> Assert_extra.failwith "decoded instruction doesn't match expectation"
              end
           | _ -> Assert_extra.failwith ("failed to find instruction " ^ i) end
        | _ -> Assert_extra.failwith "decoded instruction not a constructor" end in 
      let (arg,_) = Interp.to_exp mode Interp.eenv instr in
      let (instr_decoded_error,events) =
        interp_to_value_helper value Ivh_unsupported val_str instr_external internal_direction
          registers [] false
        (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
        | Ivh_value 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)
        | Ivh_value_after_exn v ->
          Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now"
        | Ivh_error err -> Decode_error err
        end
    | Ivh_value_after_exn _ -> Assert_extra.failwith "Decode called exit, so support will be needed for that now"
    | Ivh_error err -> Decode_error err
end


let decode_to_instruction (top_level:context) registers (value:opcode) : instruction_or_decode_error  = 
  match decode_to_istate top_level registers 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_interpreter_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 
      | _ -> Assert_extra.failwith "intern_ifield did not return vector"
    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 function " ^ i ^ " 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 function " ^ i ^ " 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 function " ^ i ^ " 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 function " ^ i ^ " 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.Fail value ->
           (match value with
            | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) -> (Fail (Just s),lm)
            | _ -> (Fail Nothing,lm) end)
         | 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)))
         | _ -> Assert_extra.failwith "Action not as expected: consider if a deiid could have appeared"
         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 


(*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))
    | (Fail _,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)
      | _ -> Assert_extra.failwith "interp_to_outcome may have produced a nondet action"
      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

(*This code is no longer uptodate. If no one is using it, then we don't need to fix it
If someone is using it, this will let me know*)
(*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)
*)