blob: 136078aa92dd1ae180cdc22ea1c58b75a61816c5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
import Interp
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 reg_name =
| Reg of string (*Name of the register, accessing the entire register*)
| Reg_slice of string * integer * integer (*Name of the register, accessing from the first to second integer*)
| Reg_field of string * string * integer * integer (*Name of the register, name of the field of the register accessed, the index range of the field*)
| Reg_f_slice of string * string * integer * integer * integer * integer (* Same as above but only accessing from the third to the fourth integer of the field *)
type outcome =
| Read_mem of read_kind * value * (value -> instruction_state)
| Write_mem of write_kind * value * value * (bool -> instruction_state)
| Barrier of barrier_kind * instruction_state
| Read_reg of reg_name * (value -> instruction_state)
| Write_reg of reg_name * value * instruction_state
| Nondet_choice of list instruction_state
| Internal of instruction_state
| Done
| Error of string
type event =
| E_read_mem of read_kind * value
| E_write_mem of write_kind * value
| E_barrier of barrier_kind
| E_read_reg of reg_name
| E_write_reg of reg_name
(*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.defs Interp.tannot -> context
val initial_instruction_state : context -> string -> value -> instruction_state
type interp_mode = <| eager_eval : bool |>
val interp : interp_mode -> instruction_state -> outcome
val interp_exhaustive : instruction_state -> list event
|
