path: root/src/lem_interp/interp_interface.lem

(* PS NOTES FOR KATHY:

pls also change:  

  decode_to_istate
  decode_to_instruction 

to take an opcode as defined above, instead of a value 

and change 

  type instruction = (string * list (string * instr_parm_typ * value) * list base_effect)

to 

  type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
*)


import Interp
open import Interp_ast
open import Pervasives
open import Num

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

(* Abstract types, to be accessed only through this interface *)
type instruction_state = Interp.stack
type context = Interp.top_level
type interp_mode = Interp.interp_mode
val make_mode : bool -> bool -> interp_mode
val tracking_dependencies : interp_mode -> bool

(*Concrete types*)
type read_kind = Read_plain | Read_reserve | Read_acquire
type write_kind = Write_plain | Write_conditional | Write_release
type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)

(*type value = 
| Bitvector of list bool  * bool * integer 
(* In Bitvector bs b n:
   - the bs are the bits (true represents 1 and false represents 0)
   - the b specifies whether the indicies are increasing (true) or decreasing (false) along the list (for Power the Bitvector values are always increasing)    
   - the n is the index of the head of the list
*)
(*To discuss:  ARM8 uses at least one abstract record form for 
  some special registers, with no clear mapping to bits. Should
  we permit Record of (string * Bitvector) values as well?
*)
| Bytevector of list word8 (* For memory accesses *)
| Unknown
(*To add: an abstract value representing an unknown but named memory address?*)

instance (Ord bool)
  let compare = defaultCompare
  let (<) = defaultLess
  let (<=) = defaultLessEq
  let (>) = defaultGreater
  let (>=) = defaultGreaterEq
end

let valueCompare v1 v2 = 
  match (v1,v2) with
  | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) ->
    tripleCompare compare compare compare (bits1,inc1,start1) (bits2,inc2,start2)
  | (Bytevector words1, Bytevector words2) -> compare words1 words2
  | (Unknown,Unknown) -> EQ
  | (Bitvector _ _ _, _)  -> LT
  | (Bytevector _, _) -> LT
  | (_, _) -> GT
  end

instance (Ord value)
  let compare = valueCompare
  let (<) v1 v2 = (valueCompare v1 v2) = LT
  let (<=) v1 v2 = (valueCompare v1 v2) <> GT
  let (>) v1 v2 = (valueCompare v1 v2) = GT
  let (>=) v1 v2 = (valueCompare v1 v2) <> LT
end

let valueEqual v1 v2 =
  match (v1,v2) with
    | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) ->
      bits1 = bits2 && inc1 = inc2 && start1 = start2
    | (Bytevector words1, Bytevector words2) -> words1 = words2
    | (Unknown,Unknown) -> true
    | _ -> false
end 

instance  (Eq value)
  let (=) = valueEqual
  let (<>) x y = not (valueEqual x y)
end
*)
type slice = (integer * integer)


type reg_name = 
| Reg of string * integer
(*Name of the register, accessing the entire register, and the size of this register *)

| Reg_slice of string * slice 
(* Name of the register, accessing from the bit indexed by the first
to the bit indexed by the second integer of the slice, inclusive. For
Power the first will be a smaller number than or equal to the second;
for other architectures it might be the other way round.  *)

| Reg_field of string * string * slice 
(*Name of the register and name of the field of the register
accessed. The slice specifies where this field is in the register*)

| Reg_f_slice of string * string * slice * slice 
(* The first three components are as in Reg_field; the final slice
specifies a part of the field, indexed w.r.t. the register as a whole *)


(* because reg_name contains slice which currently contains Big_int.big_int, the default OCaml comparison is not sufficient and we need to define explicit type classes *)
let reg_nameEqual r1 r2 = 
  match (r1,r2) with
  | (Reg s1 l1, Reg s2 l2) -> s1=s2 && l1=l2
  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> s1=s2 && sl1=sl2
  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> s1=s2 && f1=f2 && sl1=sl2
  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> s1=s2 && f1=f2 && sl1=sl2 && sl1'=sl2'
  | _ -> false
  end

instance  (Eq reg_name)
  let (=) = reg_nameEqual
  let (<>) x y = not (reg_nameEqual x y)
end

let reg_nameCompare r1 r2 = 
  match (r1,r2) with
  | (Reg s1 l1, Reg s2 l2) -> pairCompare compare compare (s1,l1) (s2,l2)
  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> pairCompare compare compare (s1,sl1) (s2,sl2)
  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> 
      tripleCompare compare compare compare (s1,f1,sl1) (s2,f2,sl2)
  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> 
      pairCompare compare (tripleCompare compare compare compare) (s1,(f1,sl1,sl1')) (s2,(f2,sl2,sl2'))
  | (Reg _ _, _)  -> LT
  | (Reg_slice _ _, _) -> LT
  | (Reg_field _ _ _, _) -> LT
  | (_, _) -> GT
  end

instance (SetType reg_name)
  let setElemCompare = reg_nameCompare
end

instance (Ord reg_name)
  let compare = reg_nameCompare
  let (<)  r1 r2 = (reg_nameCompare r1 r2) = LT
  let (<=) r1 r2 = (reg_nameCompare r1 r2) <> GT
  let (>)  r1 r2 = (reg_nameCompare r1 r2) = GT
  let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
end

type bit =
  | Bitc_zero
  | Bitc_one

type bit_lifted = 
  | Bitl_zero
  | Bitl_one
  | Bitl_undef
  | Bitl_unknown

type direction = 
  | D_increasing
  | D_decreasing

type register_value = <| rv_bits: list bit_lifted; rv_dir: direction; rv_start: int |>  (* beter for this to be int, not integer *)

type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *)

type instruction_field_value = list bit 

type byte = Byte of list bit (* of length 8 *)

type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*)

type memory_byte = byte_lifted

type memory_value = list memory_byte (* the head of the list at the lowest address, of length >=1 *)

(* not sure which of these is more handy yet *)
type address = Address of list byte (* of length 8 *)

type opcode = Opcode of list byte (* of length 4 *)





type outcome =
(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
   integer is size to read, followed by registers that were used in computing that size *)
| Read_mem of read_kind * address_lifted * integer * maybe (list reg_name) *  (memory_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 * address_lifted * integer * maybe (list reg_name) * memory_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 * (register_value -> instruction_state) 
(* Request to write register *)
| Write_reg of reg_name * register_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 maybe string * maybe (unit -> string) * instruction_state
(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler *)
| Escape of maybe instruction_state
| Done
| Error of string

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



(* more explicit type classes to work around the occurrences of big_int in reg_name *)
instance (Ord read_kind)
  let compare = defaultCompare
  let (<) = defaultLess
  let (<=) = defaultLessEq
  let (>) = defaultGreater
  let (>=) = defaultGreaterEq
end
instance (Ord write_kind)
  let compare = defaultCompare
  let (<) = defaultLess
  let (<=) = defaultLessEq
  let (>) = defaultGreater
  let (>=) = defaultGreaterEq
end
instance (Ord barrier_kind)
  let compare = defaultCompare
  let (<) = defaultLess
  let (<=) = defaultLessEq
  let (>) = defaultGreater
  let (>=) = defaultGreaterEq
end

(* maybe isn't a member of type Ord - this should be in the Lem standard library*)
instance forall 'a. Ord 'a => (Ord (maybe 'a))
  let compare = maybeCompare compare
  let (<)  r1 r2 = (maybeCompare compare r1 r2) = LT
  let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT
  let (>)  r1 r2 = (maybeCompare compare r1 r2) = GT
  let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT
end


(*let eventCompare e1 e2 = 
  match (e1,e2) with
  | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
  | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
  | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
  | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
  | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)
  | (E_error s1, E_error s2) -> compare s1 s2
  | (E_read_mem _ _ _ _, _) -> LT
  | (E_write_mem _ _ _ _ _ _, _) -> LT
  | (E_barrier _, _) -> LT
  | (E_read_reg _, _) -> LT
  | (E_write_reg _ _, _) -> LT
  | _ -> GT
  end

*)

instance (SetType event)
  let setElemCompare = defaultCompare
end



(* Functions to build up the initial state for interpretation *)
val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come from a .lem file generated by Sail*)
val initial_instruction_state : context -> string -> list register_value -> instruction_state 
  (* string is a function name, list of value are the parameters to that function *)

(*Type representint the constructor parameters in instruction, other is a type not representable externally*)
type instr_parm_typ = 
  | Bit (*A single bit, represented as a one element Bitvector as a value*)
  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
  | Bvector of maybe int (* A bitvector type, with length when statically known *)

let instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
  | (Bit,Bit) -> true
  | (Other,Other) -> true
  | (Bvector i1,Bvector i2) -> i1 = i2
  | _ -> false
end 

instance (Eq instr_parm_typ) 
  let (=) = instr_parm_typEqual
  let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
end 

(*A representation of the AST node for each instruction in the spec, with concrete values from this call, and the potential static effects from the funcl clause for this instruction 
Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
*)
type instruction = (string * list (string * instr_parm_typ * register_value) * list base_effect)

let instructionEqual i1 i2 = match (i1,i2) with
  | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
end

type v_kind = Bitv | Bytev

type decode_error = 
  | Unsupported_instruction_error of instruction
  | Not_an_instruction_error of register_value
  | Internal_error of string

type instruction_or_decode_error =
  | IDE_instr of instruction
  | IDE_decode_error of decode_error

(** propose to remove the following type and use the above instead *)
type i_state_or_error =
  | Instr of instruction * instruction_state
  | Decode_error of decode_error


(** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*)
val decode_to_istate : context -> register_value -> i_state_or_error

(** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*)
(** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction.   This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *)
val decode_to_instruction : context -> register_value -> instruction_or_decode_error

(*Function to generate the state to run from an instruction form; is always an Instr*)
val instruction_to_istate : context -> instruction -> i_state_or_error

(* Augment an address by the given value *)
(*val add_to_address : value -> integer -> value

(* Coerce a Bitvector value (presumed a multiple of 8 bits long) to a Bytevector value *)
val coerce_Bytevector_of_Bitvector : value -> value

(* Coerce a Bytevector value to a Bitvector value, increasing and starting at zero *)
val coerce_Bitvector_of_Bytevector : value -> value*)

(* Slice a register value into a smaller vector, starting at first number (wrt the indices of the register value, not raw positions in its list of bits) and going to second (inclusive) according to order. *)
val slice_reg_value : register_value -> nat -> nat -> register_value

(*(*append two vectors (bit x byte -> bit) *)
val append_value : value -> value -> value *)

(* Big step of the interpreter, to the next request for an external action *)
(* When interp_mode has eager_eval false, interpreter is (close to) small step *)
val interp : interp_mode -> instruction_state -> outcome

(* Run the interpreter without external interaction, feeding in Unknown on all reads except for those register values provided *)
val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event

(* As above, but will request register reads: outcome will only be rreg, done, or error *)
val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) 


(** operations and coercions on basic values *)

(*val num_to_bits : nat -> v_kind -> integer -> value*)

val byte_to_bits : word8 -> list bit_lifted
val bits_to_byte : list bit_lifted -> word8

val integer_of_byte_list : list word8 -> integer

val byte_list_of_integer : integer -> integer -> list word8 


(* constructing values *)

val register_value : bit_lifted -> direction -> int -> int -> register_value
let register_value b dir width start_index = 
  <| rv_bits = List.replicate (natFromInt width) b;
     rv_dir = dir; (* D_increasing for Power *)
     rv_start = start_index; |>

val register_value_zeros : direction -> int -> int -> register_value
let register_value_zeros dir width start_index = 
  register_value Bitl_zero dir width start_index

val register_value_ones : direction -> int -> int -> register_value
let register_value_ones dir width start_index = 
  register_value Bitl_one dir width start_index

val memory_value_unknown : int (*the number of bytes*) -> memory_value
(*let memory_value_lifted_unknown (width:int) : memory_value_lifted = *)



val add_address_int : address -> int -> address 
(* let add_address_int (a:address) (i:int) : address = *)

val clear_low_order_bits_of_address : address -> address 



(* coercions *)
val integer_of_address : address -> integer 

val address_of_integer : integer -> address 

val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode
(*let opcode_of_bytes b0 b1 b2 b3 : maybe opcode = *)

val register_value_of_address : address -> register_value   

val address_lifted_of_register_value : register_value -> maybe address_lifted
(* returning Nothing iff the register value is not 64 bits wide, but allowing Bitl_undef and Bitl_unknown *)

val address_of_address_lifted : address_lifted -> maybe address
(* returning Nothing iff the address contains any Bitl_undef or Bitl_unknown *)