import Interp
open import Pervasives
open import Num

type read_kind = Interp.read_kind
type write_kind = Interp.write_kind
type barrier_kind = Interp.barrier_kind

type word8 = nat (* bounded at a byte, for when lem supports it*)

type value = 
| Bitvector of list bool (* For register accesses *)
| Bytevector of list word8 (* For memory accesses *)
| Unknown

type instruction_state = Interp.stack
type context = Interp.top_level

type slice = (integer * integer)

type reg_name = 
| Reg of string (*Name of the register, accessing the entire register*)
| Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*)
| Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*)
| Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)

type outcome =
(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *)
| Read_mem of read_kind * value * maybe (list reg_name) *  (value -> instruction_state)
(* Request to write memory, first value and dependent registers is location, second is the value to write *)
| Write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
(* Request a memory barrier *)
| Barrier of barrier_kind * instruction_state
(* Request to read register, will track dependency when mode.track_values *)
| Read_reg of reg_name * (value -> instruction_state) 
(* Request to write register *)
| Write_reg of reg_name * value * instruction_state
(* List of instruciton states to be run in parrallel, any order permitted *)
| Nondet_choice of list instruction_state * instruction_state
(* Stop for incremental stepping, function can be used to display function call data *)
| Internal of (unit -> string) * instruction_state
| Done
| Error of string

type event = 
| E_read_mem of read_kind * value * maybe (list reg_name) 
| E_write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name)
| E_barrier of barrier_kind
| E_read_reg of reg_name
| E_write_reg of reg_name * value
| E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)


val build_context : Interp_ast.defs Interp.tannot -> context
val initial_instruction_state : context -> string -> value -> instruction_state

type interp_mode = Interp.interp_mode 
val interp : interp_mode -> instruction_state -> outcome

val interp_exhaustive : instruction_state -> list event

val rr_interp_exhaustive : instruction_state -> list event -> (outcome * (list event)) (* Like interp_exhaustive but will read registers; the outcome will only ever be a rreg request, done, or error *)

val mem_read_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory reads to compute the addressses in is*)

val mem_write_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory writes to compute the address (and value?, in a separate list?)*)