path: root/src/lem_interp/interp_inter_imp.lem

(*========================================================================*)
(*     Sail                                                               *)
(*                                                                        *)
(*  Copyright (c) 2013-2017                                               *)
(*    Kathyrn Gray                                                        *)
(*    Shaked Flur                                                         *)
(*    Stephen Kell                                                        *)
(*    Gabriel Kerneis                                                     *)
(*    Robert Norton-Wright                                                *)
(*    Christopher Pulte                                                   *)
(*    Peter Sewell                                                        *)
(*    Alasdair Armstrong                                                  *)
(*    Brian Campbell                                                      *)
(*    Thomas Bauereiss                                                    *)
(*    Anthony Fox                                                         *)
(*    Jon French                                                          *)
(*    Dominic Mulligan                                                    *)
(*    Stephen Kell                                                        *)
(*    Mark Wassell                                                        *)
(*                                                                        *)
(*  All rights reserved.                                                  *)
(*                                                                        *)
(*  This software was developed by the University of Cambridge Computer   *)
(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*     notice, this list of conditions and the following disclaimer.      *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*     notice, this list of conditions and the following disclaimer in    *)
(*     the documentation and/or other materials provided with the         *)
(*     distribution.                                                      *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
(*  SUCH DAMAGE.                                                          *)
(*========================================================================*)

open import Interp_ast
import Interp
import Interp_lib
import Instruction_extractor
import Set_extra
open import Pervasives
open import Assert_extra
open import Interp_ast
open import Interp_utilities
open import Sail_impl_base
open import Interp_interface

val intern_reg_value : register_value -> Interp_ast.value
val intern_mem_value : interp_mode -> direction -> memory_value -> Interp_ast.value
val extern_reg_value : reg_name -> Interp_ast.value -> register_value
val extern_with_track: forall 'a. interp_mode -> (Interp_ast.value -> 'a) -> Interp_ast.value -> ('a * maybe (list reg_name))
val extern_vector_value: Interp_ast.value -> list byte_lifted
val extern_mem_value :   Interp_ast.value -> memory_value
val extern_reg : Interp_ast.reg_form -> maybe (nat * nat) -> reg_name

let make_interpreter_mode eager_eval tracking_values debug =
  <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false; Interp.debug = debug; Interp.debug_indent = "" |>;;

let make_mode eager_eval tracking_values debug =
  <| internal_mode = make_interpreter_mode eager_eval tracking_values debug |>;;
let make_mode_exhaustive debug =
  <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true; Interp.debug = debug; Interp.debug_indent = "" |> |>;;
let tracking_dependencies mode = mode.internal_mode.Interp.track_values
let make_eager_mode mode = <| internal_mode = <| mode.internal_mode with Interp.eager_eval = true |> |>;;
let make_default_mode = fun () -> <| internal_mode = make_interpreter_mode false false false |>;;

let bitl_to_ibit = function 
  | Bitl_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown)) 
  | Bitl_one ->  (Interp_ast.V_lit (L_aux L_one Interp_ast.Unknown))
  | Bitl_undef -> (Interp_ast.V_lit (L_aux L_undef Interp_ast.Unknown))
  | Bitl_unknown -> Interp_ast.V_unknown
end

let bit_to_ibit = function
  | Bitc_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown))
  | Bitc_one -> (Interp_ast.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 bitl_from_ibit b = 
    let b = Interp.detaint b in
    match b with
    | Interp_ast.V_lit (L_aux L_zero _) -> Bitl_zero
    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitl_zero
    | Interp_ast.V_lit (L_aux L_one _)  -> Bitl_one
    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_one _)] -> Bitl_one
    | Interp_ast.V_lit (L_aux L_undef _) -> Bitl_undef
    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_undef _)] -> Bitl_undef
    | Interp_ast.V_unknown -> Bitl_unknown
    | _ -> Assert_extra.failwith ("bit_from_ibit given unexpected " ^ (Interp.string_of_value b)) 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 bitl_from_ibit l

let bits_from_ibits l = List.map 
  (fun b -> 
    let b = Interp.detaint b in
    match b with
    | Interp_ast.V_lit (L_aux L_zero _) -> Bitc_zero
    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitc_zero
    | Interp_ast.V_lit (L_aux L_one _)  -> Bitc_one
    | Interp_ast.V_vector _ _ [Interp_ast.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_ast.IInc
  | D_decreasing -> Interp_ast.IDec
end

let extern_direction = function
  | Interp_ast.IInc -> D_increasing
  | Interp_ast.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_ast.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_ast.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 =
  List.reverse v (* match little endian representation *)
  $> List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits)
  $> fun bits ->
  let direction = intern_direction direction in
  Interp_ast.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_ast.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits

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_ast.Form_Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> 
    Reg x (Interp.reg_start_pos r) (Interp.reg_size r) (extern_direction dir)
  | (Interp_ast.Form_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_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_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_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_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_ast.Form_SubReg (Id_aux (Id x) _) 
       ((Interp_ast.Form_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_ast.V_track v regs -> extern_reg_value reg_name v 
    | Interp_ast.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_ast.V_vector fst dir bits -> bitls_from_ibits bits
          | Interp_ast.V_lit (L_aux L_zero _) -> [Bitl_zero]
          | Interp_ast.V_lit (L_aux L_false _) -> [Bitl_zero]
          | Interp_ast.V_lit (L_aux L_one _) -> [Bitl_one]
          | Interp_ast.V_lit (L_aux L_true _) -> [Bitl_one]
          | Interp_ast.V_lit (L_aux L_undef _) -> [Bitl_undef]
          | Interp_ast.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 extern_with_track mode f = function
  | Interp_ast.V_track v regs ->
    (f v,
     if mode.internal_mode.Interp.track_values
     then (Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList regs)))
     else Nothing)
  | v -> (f v, Nothing)
  end

let rec extern_vector_value v = match v with
  | Interp_ast.V_vector _fst _inc bits ->
    bitls_from_ibits bits
    $> to_bytes
  | Interp_ast.V_vector_sparse _fst _stop _inc _bits _default ->
    Interp_lib.fill_in_sparse v
    $> extern_vector_value
  | Interp_ast.V_track v _ -> extern_vector_value v
  | _ -> Assert_extra.failwith ("extern_vector_value received non-externable value " ^ (Interp.string_of_value v))
end

let rec extern_mem_value v = List.reverse (extern_vector_value v)


let rec extern_ifield_value i_name field_name v ftyp = match (v,ftyp) with
  | (Interp_ast.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp
  | (Interp_ast.V_vector fst inc bits,_) -> bits_from_ibits bits
  | (Interp_ast.V_vector_sparse fst stop inc bits default,_) ->
    extern_ifield_value i_name field_name (Interp_lib.fill_in_sparse v) ftyp
  | (Interp_ast.V_lit (L_aux L_zero _),_) -> [Bitc_zero]
  | (Interp_ast.V_lit (L_aux L_false _),_) -> [Bitc_zero]
  | (Interp_ast.V_lit (L_aux L_one _),_) ->  [Bitc_one]
  | (Interp_ast.V_lit (L_aux L_true _),_) -> [Bitc_one]
  | (Interp_ast.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i
  | (Interp_ast.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i
  | (Interp_ast.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i
  | (Interp_ast.V_ctor _ _ (Interp_ast.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i)
  | (Interp_ast.V_ctor _ _ (Interp_ast.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 _ = Interp.debug_print ("slice_reg_value " ^ show v.rv_start_internal ^ " " ^ show v.rv_start ^ " " ^ show start ^ " " ^ show stop) in*)
  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
(*  let _ = Interp.debug_print (" " ^ " " ^ if inc then "Inc " else "dec " ^ show (List.length (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)) ^ " " ^ show (List.length v.rv_bits) ^ " " ^ show (v.rv_start_internal - start) ^ " " ^ show (v.rv_start_internal - stop) ^ "\n") in*)
  <| v with rv_bits = (Interp.from_n_to_n (start - v.rv_start) (stop - v.rv_start) v.rv_bits);
            rv_start = r_start;
            rv_start_internal = r_internal_start
  |> 

let lift_reg_name_to_whole reg_name size = match reg_name with
  | Reg _ _ _ _ -> reg_name
  | Reg_slice name start dir _ -> Reg name start size dir
  | Reg_field name start dir _ _ -> Reg name start size dir
  | Reg_f_slice name start dir _ _ _ -> Reg name start size dir
end

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 (lift_reg_name_to_whole reg_name 0)
        (if start = stop then
           (Interp.fupdate_vec v_internal start v2_internal)
         else
           (Interp.fupdate_vector_slice v_internal v2_internal start stop)))
      with rv_start = v.rv_start; rv_start_internal = v.rv_start_internal |>

(*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 _ _ _) ->
(*        let _ = Interp.debug_print ("find_reg_name " ^ i ^ " field case " ^ show p1 ^ " " ^ show p2 ^ "\n") in*)
        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 | Ivh_analysis
type interp_value_return =
  | Ivh_value of Interp_ast.value
  | Ivh_value_after_exn of Interp_ast.value
  | Ivh_error of decode_error

let rec interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen thunk =
  let errk_str = match ivh_mode with
    | Ivh_translate -> "translate"
    | Ivh_analysis -> "analysis"
    | 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 debug) 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)
         | Ivh_analysis -> (Ivh_value value, events_out)
         | _ ->
           (match value with
            | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
            | Interp_ast.V_ctor (Id_aux (Id "None") _) _ _ _ ->
              (match (ivh_mode,arg) with
               | (Ivh_decode, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out)
               | (Ivh_illegal, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out)
               | (Ivh_unsupported, _) -> (Ivh_error (Interp_interface.Unsupported_instruction_error instr), events_out)
               | _ -> Assert_extra.failwith "Reached unreachable pattern" end)
            | _ -> (Ivh_error (Interp_interface.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
    | (Interp.Error l msg,_,_) -> (Ivh_error (Interp_interface.Internal_error msg), events_out)
    | (Interp.Action (Interp.Return value) stack,_,_) ->
      interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen
        (fun _ -> Interp.resume mode stack (Just value))
    | (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
      match List.lookup i (Interp_lib.library_functions direction) with
        | Nothing -> (Ivh_error (Interp_interface.Internal_error ("External function not available " ^ i)), events_out)
        | Just f  ->
          interp_to_value_helper debug 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_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.V_lit (L_aux (L_string s) _)) ->
        (Ivh_error (Interp_interface.Internal_error ("Assert failed: " ^ s)), events_out)
      | _ -> (Ivh_error (Interp_interface.Internal_error "Assert failed"), events_out) end
    | (Interp.Action (Interp.Exit exp) stack,_,_) ->
      interp_to_value_helper debug 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_ast.Form_Reg (Id_aux (Id i) _) _ _ -> i
        | Interp_ast.Form_SubReg (Id_aux (Id i) _) (Interp_ast.Form_Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i
        | _ -> Assert_extra.failwith "Reg not following expected structure" end in
      let err_value =
        (Ivh_error (Interp_interface.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
(*              let _ = Interp.debug_print ("Register read of " ^ rname ^ " returning value " ^ (Interp.string_of_value value) ^ "\n") in *)
              interp_to_value_helper debug 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 debug 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 (Interp_interface.Internal_error ("Read memory request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Read_mem_tagged _ _ _) _,_,_) ->
      (Ivh_error (Interp_interface.Internal_error ("Read memory tagged request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
      (Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
      (Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Excl_res _) _,_,_) ->
      (Ivh_error (Interp_interface.Internal_error ("Exclusive result request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) ->
      (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
    | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) ->
      (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out)
    | (outcome, _, _) ->
       (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str ^ " " ^ Interp.string_of_outcome outcome)), 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 debug defs reads writes write_eas write_vals barriers excl_res externs =
  (*TODO add externs to to_top_env*)
  match Interp.to_top_env debug call_external_functions defs with 
    | (_,((Interp.Env _ _ dir _ _ _ _ _ debug) as context)) -> 
      Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing)
        reads writes write_eas write_vals barriers excl_res externs end


let translate_address top_level end_flag thunk_name registers address =
  let (Address bytes i) = address in
  let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in
  let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in
  let mode = make_mode true false debug in
  let int_mode = mode.internal_mode 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_ast.IInc else Interp_ast.IDec in
  let (address_error,events) =
    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str (V_list []) 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])
            (Interp_ast.Unknown, Nothing)) 
         top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in
  match (address_error) with
  | Ivh_value addr ->
    (address_of_byte_lifted_list (extern_vector_value addr), events)
  | Ivh_value_after_exn _ ->
    (Nothing, events)
  | Ivh_error err -> match err with
     | Interp_interface.Internal_error msg -> Assert_extra.failwith msg
     | _ -> Assert_extra.failwith "Not an internal error either" end 
end

let value_of_instruction_param direction (name,typ,v) = 
  let vec = intern_ifield_value direction v in
  let v = match vec with
    | Interp_ast.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 v

let intern_instruction direction (name,parms) =
  Interp_ast.V_ctor (Interp.id_of_string name) (mk_typ_id "ast") Interp_ast.C_Union
    (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms))

let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers (instruction : Interp_ast.value) =
  let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in
  let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in
  let mode = make_mode true false debug in
  let int_mode = mode.internal_mode in
  let val_str = Interp.string_of_value instruction in
  let (arg,_) = Interp.to_exp int_mode Interp.eenv instruction in
  let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
  let (analysis_or_error,events) =
    interp_to_value_helper debug Nothing Ivh_analysis val_str (V_list []) 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])
            (Interp_ast.Unknown, Nothing)) 
         top_env Interp.eenv (Interp.emem "instruction analysis top level") Interp.Top) Nothing) in
  match (analysis_or_error) with
  | Ivh_value analysis ->
    (match analysis with
     | Interp_ast.V_tuple [Interp_ast.V_list regs1;
                       Interp_ast.V_list regs2;
                       Interp_ast.V_list regs3;
                       Interp_ast.V_list nias;
                       dia;
                       ik] ->
       let reg_to_reg_name v = match v with
         | Interp_ast.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp_ast.V_lit (L_aux (L_string n) _)) ->
           let (start,length,direction,_) = regn_to_reg_details n Nothing in
           Reg n start length direction
         | Interp_ast.V_ctor (Id_aux (Id "RSlice") _) _ _
             (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _);
                              Interp_ast.V_lit (L_aux (L_num s1) _);
                              Interp_ast.V_lit (L_aux (L_num s2) _);]) ->
           let (start,length,direction,_) = regn_to_reg_details n Nothing in
           Reg_slice n start direction (extern_slice direction start (natFromInteger s1, natFromInteger s2))
                                       (*Note, this may need to change order depending on the direction*)
         | Interp_ast.V_ctor (Id_aux (Id "RSliceBit") _) _ _
             (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _);
                              Interp_ast.V_lit (L_aux (L_num s) _);]) ->
           let (start,length,direction,_) = regn_to_reg_details n Nothing in
           Reg_slice n start direction (extern_slice direction start (natFromInteger s,natFromInteger s))
         | Interp_ast.V_ctor (Id_aux (Id "RField") _) _ _
             (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _);
                              Interp_ast.V_lit (L_aux (L_string f) _);]) ->
           let (start,length,direction,span) = regn_to_reg_details n (Just f) in
           Reg_field n start direction f (extern_slice direction start span)             
         | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end
       in
       let get_addr v = match address_of_byte_lifted_list (extern_vector_value v) with
         | Just addr -> addr
         | Nothing -> failwith "get_nia encountered invalid address" end in
       let dia_to_dia = function
         | Interp_ast.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none
         | Interp_ast.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address ->
            DIA_concrete_address (get_addr address)
         | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) 
         | _ -> failwith "Register footprint analysis did not return dia of expected type" end in
       let nia_to_nia = function
         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _ -> NIA_successor
         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
            NIA_concrete_address (get_addr address)
         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ ->
            NIA_indirect_address
         | _ -> failwith "Register footprint analysis did not return nia of expected type" end in
       let (regs1,regs2,regs3,nias,dia,ik) =
         (List.map reg_to_reg_name regs1,
          List.map reg_to_reg_name regs2,
          List.map reg_to_reg_name regs3,
          List.map nia_to_nia nias,
          dia_to_dia dia,
          fromInterpValue ik) in
       ((regs1,regs2,regs3,nias,dia,ik), events)
     | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end)
  | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed"
  | Ivh_error err -> match err with
     | Interp_interface.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 interp_value_to_instr_external top_level instr = 
  let (Context (Interp.Env _ instructions _ _ _ _ _ _ debug) _ _ _ _ _ _ _ _ _ _) = top_level in
  match instr with
  | Interp_ast.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_ast.V_lit (L_aux L_unit _),[]) -> (name, [])
        | (value,[(p_name,ie_typ)]) -> 
           let t = migrate_typ ie_typ in
           (name, [(p_name,t, (extern_ifield_value name p_name value t))])
        | (Interp_ast.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))
        | _ -> 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


let decode_to_instruction top_level registers value : instruction_or_decode_error = 
  let (Context ((Interp.Env _ instructions _ _ _ _ _ _ debug) as top_env) direction _ _ _ _ _ _ _ _ _) = top_level in
  let mode = make_interpreter_mode true false debug 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_ast.IInc else Interp_ast.IDec in
  let (instr_decoded_error,events) =
    interp_to_value_helper debug (Just value) Ivh_decode val_str (V_list []) 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 = interp_value_to_instr_external top_level instr in*) 
      let (instr_decoded_error,events) =
        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr (*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 _ -> IDE_instr instr (*instr_external*)
        | Ivh_value_after_exn v ->
          Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now"
        | Ivh_error err -> IDE_decode_error err
        end
   | Ivh_value_after_exn _ ->
      Assert_extra.failwith ("Decode of " ^ val_str ^ " called exit.")
   | Ivh_error err -> IDE_decode_error err
end


let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = 
  let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
  match decode_to_instruction top_level registers value with
  | IDE_instr instr ->
     let mode = make_interpreter_mode true false in
     let (arg,_) = Interp.to_exp mode Interp.eenv instr in
     Instr instr
           (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)
  | IDE_decode_error de -> Decode_error de
  end


let instr_external_to_interp_value top_level instr =
  let (Context _ direction _ _ _ _ _ _ _ _ _) = top_level in
  let (name,parms) = instr in

  let get_value (_,typ,v) = 
    let vec = intern_ifield_value direction v in
    match vec with
      | Interp_ast.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 parmsV = match parms with
    | [] -> Interp_ast.V_lit (L_aux L_unit Unknown)
    | _  -> Interp_ast.V_tuple (List.map get_value parms)
    end in
  (*This type shouldn't be hard-coded*)
  Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) 
                (mk_typ_id "ast") Interp_ast.C_Union parmsV

val instruction_to_istate : context -> Interp_ast.value -> instruction_state 
let instruction_to_istate (top_level:context) (instr:Interp_ast.value) : instruction_state  = 
  let mode = make_interpreter_mode true false in
  let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
  let ast_node = fst (Interp.to_exp mode Interp.eenv instr) in
  (IState
     (Interp.Thunk_frame
        (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [ast_node])
               (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_reads_tagged mem_writes mem_write_eas mem_write_vals mem_write_vals_tagged barriers excl_res spec_externs) = context in
  let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.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_ast.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.Read_mem_tagged (Id_aux (Id i) _) value slice ->
        (match List.lookup i mem_reads_tagged with
          | (Just (MRT 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_tagged read_k (Address_lifted location address_int) length tracking 
                  (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp_ast.V_tuple ([(bitl_to_ibit tag);(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_with_track mode extern_mem_value 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.Excl_res (Id_aux (Id i) _) ->
        (match excl_res with
          | (Just (i', ER return)) ->
              Excl_res (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 ("Exclusive result function, not provided") end, lm)
      | Interp.Write_memv (Id_aux (Id i) _) address_val write_val ->
           (match List.lookup i mem_write_vals with
            | (Just (MV parmf return)) -> 
              let (value, v_tracking) = 
                match (Interp.detaint write_val) with
                  | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
                  | _ -> extern_with_track mode extern_mem_value write_val end in
               let location_opt = match parmf mode address_val with
                  | Nothing -> Nothing
                  | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with
                      | Just bs -> Just (integer_of_byte_list bs)
                      | _ -> Nothing end in Just (Address_lifted mv address_int) end
               in
               Write_memv location_opt 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.Write_memv_tagged (Id_aux (Id i) _) address_val tag_val write_val ->
           (match List.lookup i mem_write_vals_tagged with
            | (Just (MVT parmf return)) -> 
              let (value, v_tracking) = 
                match (Interp.detaint write_val) with
                  | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
                  | _ -> extern_with_track mode extern_mem_value write_val end in
               let location_opt = match parmf mode address_val with
                  | Nothing -> Nothing
                  | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with
                      | Just bs -> Just (integer_of_byte_list bs)
                      | _ -> Nothing end in Just (Address_lifted mv address_int) end
               in
               Write_memv_tagged location_opt ((bitl_from_ibit tag_val), 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.Return value ->
           interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode next_state (Just value))
         | 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_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.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



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


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 


(*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 reads_tagged writes write_eas write_vals write_vals_tagged barriers excl_res) = 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)
    | (Read_mem_tagged read_k loc length tracking i_state_fun, _) ->
      let (events,analysis_data) = ie_loop mode register_values (i_state_fun (Bitl_unknown, (unknown_mem length))) in
      ((E_read_memt 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)
    | (Excl_res 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_excl_res :: (events ++ events'), analysis_data)
    | (Write_memv opt_address 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 opt_address value tracking)::(events++events'),analysis_data)
    | (Write_memv_tagged opt_address 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_memvt opt_address 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 ;;
  
val interp_exhaustive : bool -> maybe (list (reg_name * register_value)) -> instruction_state -> list event
let interp_exhaustive debug register_values i_state =
  let mode = make_mode_exhaustive debug in
  match ie_loop mode register_values i_state with
    | (events,_) -> events
end


val state_to_outcome_s : 
  (instruction_state -> unit -> (string * string)) -> 
  interp_mode -> instruction_state -> Sail_impl_base.outcome_s unit
val outcome_to_outcome : 
  (instruction_state -> unit -> (string * string)) -> 
  interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome unit

let rec outcome_to_outcome pp_instruction_state mode = 
  let state_to_outcome_s = 
    state_to_outcome_s pp_instruction_state in
  function
  | Interp_interface.Read_mem rk addr size _ k ->
     Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v))
  | Interp_interface.Write_mem rk addr size _ mv _ k ->
     failwith "Write_mem not supported anymore"
  | Interp_interface.Write_ea wk addr size _ state ->
     Sail_impl_base.Write_ea (wk,addr,size) (state_to_outcome_s mode state)
  | Interp_interface.Excl_res k ->
     Sail_impl_base.Excl_res (fun v -> state_to_outcome_s mode (k v))
  | Interp_interface.Write_memv _ mv _ k ->
     Sail_impl_base.Write_memv mv (fun v -> state_to_outcome_s mode (k v))
  | Interp_interface.Barrier bk state ->
     Sail_impl_base.Barrier bk (state_to_outcome_s mode state)
  | Interp_interface.Footprint state ->
     Sail_impl_base.Footprint (state_to_outcome_s mode state)
  | Interp_interface.Read_reg r k ->
     Sail_impl_base.Read_reg r (fun v -> state_to_outcome_s mode (k v))
  | Interp_interface.Write_reg r rv state ->
     Sail_impl_base.Write_reg (r,rv) (state_to_outcome_s mode state)
  | Interp_interface.Nondet_choice _ _ ->
     failwith "Nondet_choice not supported yet"
  | Interp_interface.Escape _ _ ->
     Sail_impl_base.Escape Nothing
  | Interp_interface.Fail maybestring ->
     Sail_impl_base.Fail maybestring
  | Interp_interface.Internal maybestring maybeprint state ->
     Sail_impl_base.Internal (maybestring,maybeprint) (state_to_outcome_s mode state)
  | Interp_interface.Analysis_non_det _ _ ->
     failwith "Analysis_non_det outcome returned"
  | Interp_interface.Done ->
     Sail_impl_base.Done ()
  | Interp_interface.Error message ->
     failwith ("Interpreter error: " ^ message)
end

and state_to_outcome_s pp_instruction_state mode state = 
  let next_outcome' = interp mode state in
  let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in
  (next_outcome, 
   Just ((pp_instruction_state state), 
         (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state))
  )

val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> Interp_ast.value -> Sail_impl_base.outcome_s unit
let initial_outcome_s_of_instruction pp_instruction_state context mode instruction =
  let state = instruction_to_istate context instruction in
  state_to_outcome_s pp_instruction_state mode state


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


let instruction_kind_of_event nia_reg : event -> maybe instruction_kind = function
  (* this is a hack to avoid adding special events for AArch64 transactional-memory *)
  | E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start)
  | E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort)
  | E_barrier Barrier_TM_COMMIT -> Just (IK_trans Transaction_commit)

  | E_read_mem rk _ _ _ -> Just (IK_mem_read rk)
  | E_read_memt rk _ _ _ -> Just (IK_mem_read rk)
  | E_write_mem wk _ _ _ _ _  -> Just (IK_mem_write wk)
  | E_write_ea wk _ _ _ -> Just (IK_mem_write wk)
  | E_excl_res -> Nothing
  | E_write_memv _ _ _ -> Nothing
  | E_write_memvt _ _ _ -> Nothing
  | E_barrier bk -> Just (IK_barrier bk)
  | E_footprint -> Nothing
  | E_read_reg _ -> Nothing
  | E_write_reg reg _ ->
      if register_base_name reg = register_base_name nia_reg then Just IK_branch
      else Nothing
  | E_error s -> failwith ("instruction_kind_of_event error: "^s)
  | E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*)
 end
(* TODO: how can we decide, looking only at the output of interp_exhaustive,
   that an instruction is a conditional branch? *)

let regs_in_of_event : event -> list reg_name = function
  | E_read_mem _ _ _ _ -> []
  | E_read_memt _ _ _ _ -> []
  | E_write_mem _ _ _ _ _ _  -> []
  | E_write_ea _ _ _ _ -> []
  | E_excl_res -> []
  | E_write_memv _ _ _ -> []
  | E_write_memvt _ _ _ -> []
  | E_barrier _ -> []
  | E_footprint -> []
  | E_read_reg r -> [r]
  | E_write_reg _ _ -> []
  | E_error s -> failwith ("regs_in_of_event "^s)
  | E_escape -> [] (*failwith ("regs_in_of_event escape")*)
  end

let regs_out_of_event : event -> list reg_name = function
  | E_read_mem _ _ _ _ -> []
  | E_read_memt _ _ _ _ -> []
  | E_write_mem _ _ _ _ _ _  -> []
  | E_write_ea _ _ _ _ -> []
  | E_excl_res -> []
  | E_write_memv _ _ _ -> []
  | E_write_memvt _ _ _ -> []
  | E_barrier _ -> []
  | E_footprint -> []
  | E_read_reg _ -> []
  | E_write_reg r _ -> [r]
  | E_error s -> failwith ("regs_out_of_event "^s)
  | E_escape -> [] (*failwith ("regs_out_of_event escape")*)
  end


let regs_feeding_memory_access_address_of_event : event -> list reg_name = function
  | E_read_mem _ _ _ (Just rs)       -> rs
  | E_read_mem _ _ _ None            -> []
  | E_read_memt _ _ _ (Just rs)       -> rs
  | E_read_memt _ _ _ None            -> []
  | E_write_mem _ _ _ (Just rs) _ _  -> rs
  | E_write_mem _ _ _ None _ _       -> []
  | E_write_ea wk _ _ (Just rs)      -> rs
  | E_write_ea wk _ _ None           -> []
  | E_excl_res                       -> []
  | E_write_memv _ _ _               -> []
  | E_write_memvt _ _ _               -> []
  | E_barrier bk                     -> []
  | E_footprint                      -> []
  | E_read_reg _                     -> []
  | E_write_reg _ _                  -> []
  | E_error s -> failwith ("regs_feeding_memory_access_address_of_event " ^ s)
  | E_escape -> [] (*failwith ("regs_feeding_memory_access_address_of_event escape")*)
end

let nia_address_of_event nia_reg (event: event) : maybe (maybe address) = 
   (* return Nothing for unknown/undef *)
  match event with
  | E_write_reg reg reg_value ->
     if register_base_name reg = register_base_name nia_reg then
       let al = match address_lifted_of_register_value reg_value with
         | Just al -> al
         | Nothing -> failwith "nia_register_of_event: NIA read not 64 bits" 
       end in
       Just (address_of_address_lifted al)
     else Nothing
  | _ -> Nothing
  end

let interp_instruction_analysis 
      top_level
      (interp_exhaustive : ((list (reg_name * register_value)) -> list event))
      instruction 
      nia_reg 
      (nias_function : (list (maybe address) -> list nia))
      ism environment =
    
    let es = interp_exhaustive environment in

    let regs_in = List.concatMap regs_in_of_event es in
    let regs_out = List.concatMap regs_out_of_event es in

    let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in

    let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in
    let nias = nias_function nia_address in

    let dia = DIA_none in (* FIX THIS! *)

    let inst_kind =
      match List.mapMaybe (instruction_kind_of_event nia_reg) es with
      | [] -> IK_simple
      | inst_kind :: [] -> inst_kind
      | inst_kind :: inst_kinds ->
          if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
            inst_kind

          else if
            (forall (inst_kind' MEM (inst_kind :: inst_kinds)).
                match inst_kind' with
                | IK_mem_read _  -> true
                | IK_mem_write _ -> true
                | IK_mem_rmw _   -> false
                | IK_barrier _   -> false
                | IK_branch      -> false
                | IK_trans _     -> false
                | IK_simple      -> false
                end)
          then
            match
              List.partition
                (function IK_mem_read _ -> true | _ -> false end)
                (inst_kind :: inst_kinds)
            with
            | ((IK_mem_read r) :: rs, (IK_mem_write w) :: ws) ->
                let () = ensure (forall (r' MEM rs). r' = IK_mem_read r) "more than one kind of read" in
                let () = ensure (forall (w' MEM ws). w' = IK_mem_write w) "more than one kind of write" in
                IK_mem_rmw (r, w)
            | _ -> fail
            end

          (* the TSTART instruction can also be aborted so it will have two kinds of events *)
          else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
                        inst_kind' = IK_trans Transaction_start) &&
                  (forall (inst_kind' MEM (inst_kind :: inst_kinds)).
                        inst_kind' = IK_trans Transaction_start
                        || inst_kind' = IK_trans Transaction_abort)
          then
            IK_trans Transaction_start

          else
            failwith "multiple instruction kinds"
    end in

  (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)

let interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment =
  fst (instruction_analysis context endianness analysis_function
                            reg_info (Just environment) instruction)



val print_and_fail_of_inequal : forall 'a. Show 'a => 
                                  (string -> unit) -> 
                                (instruction -> string) ->
                                (string * 'a) -> (string * 'a) -> unit
let print_and_fail_if_inequal 
      (print_endline,instruction)
      (name1,xs1) (name2,xs2) =
  if xs1 = xs2 then ()
  else 
    let () = print_endline (name1^": "^show xs1) in
    let () = print_endline (name2^": "^show xs2) in
    failwith (name1^" and "^ name2^" inequal for instruction: \n" ^ Interp.string_of_value instruction)

let interp_compare_analyses 
      print_endline
      (non_pseudo_registers : set reg_name -> set reg_name)
      context
      endianness
      interp_exhaustive
      (instruction : Interp_ast.value)
      nia_reg
      (nias_function : (list (maybe address) -> list nia))
      ism
      environment
      analysis_function
      reg_info = 
  let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = 
    interp_instruction_analysis context interp_exhaustive instruction nia_reg nias_function ism 
                                environment in
  let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) =
    (Set.fromList regs_in1,
     Set.fromList regs_out1,
     Set.fromList regs_feeding_address1,
     Set.fromList nias1) in
  let (regs_in1S,regs_out1S,regs_feeding_addres1S) = 
    (non_pseudo_registers regs_in1S,
     non_pseudo_registers regs_out1S,
     non_pseudo_registers regs_feeding_address1S) in

  let (regs_in2,regs_out2,regs_feeding_address2,nias2,dia2,inst_kind2) = 
    interp_handwritten_instruction_analysis 
      context endianness instruction analysis_function reg_info environment in
  let (regs_in2S,regs_out2S,regs_feeding_address2S,nias2S) =
    (Set.fromList regs_in2,
     Set.fromList regs_out2,
     Set.fromList regs_feeding_address2,
     Set.fromList nias2) in
  let (regs_in2S,regs_out2S,regs_feeding_addres2S) = 
    (non_pseudo_registers regs_in2S,
     non_pseudo_registers regs_out2S,
     non_pseudo_registers regs_feeding_address2S) in

  let aux = (print_endline,instruction) in
  let () = (print_and_fail_if_inequal aux)
             ("regs_in exhaustive",regs_in1S) 
             ("regs_in hand",regs_in2S) in
  let () = (print_and_fail_if_inequal aux) 
             ("regs_out exhaustive",regs_out1S)
             ("regs_out hand",regs_out2S) in
  let () = (print_and_fail_if_inequal aux) 
             ("regs_feeding_address exhaustive",regs_feeding_address1S)
             ("regs_feeding_address hand",regs_feeding_address2S) in
  let () = (print_and_fail_if_inequal aux) 
             ("nias exhaustive",nias1S)
             ("nias hand",nias2S) in
  let () = (print_and_fail_if_inequal aux) 
             ("dia exhaustive",dia1)
             ("dia hand",dia2) in
  let () = (print_and_fail_if_inequal aux) 
             ("inst_kind exhaustive",inst_kind1)
             ("inst_kind hand",inst_kind2) in

  (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1)