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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
import Interp
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 (* For register accesses : in conformance with Sail, tracks order and starting lsb number*)
(*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 * bool * integer (* For memory accesses : see above *)
| Unknown
(*To add: an abstract value representing an unknown but named memory address?*)
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 * integer * 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 * integer * 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 maybe string * maybe (unit -> string) * instruction_state
| Done
| Error of string
type event =
| E_read_mem of read_kind * value * integer * maybe (list reg_name)
| E_write_mem of write_kind * value * integer * 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*)
(*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*)
(* 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 value -> instruction_state
(* string is a function name, list of value are the parameters to that function *)
type i_state_or_error =
| Instr of instruction_state
| Unsupported_instruction_error
| Not_an_instruction_error
| Internal_error of string
(*Function to decode an instruction and build the state to run it*)
val decode_to_istate : context -> value -> i_state_or_error
(* 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 *)
val interp_exhaustive : 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))
(*To discuss: Are these functions needed, since the memory requests carry the register dependencies for that request? *)
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?)*)
|
