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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
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 (* 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 (* For memory accesses *)
| 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,
integer is size to read, followed by registers that were used in computing that size *)
| Read_mem of read_kind * value * maybe (list reg_name) * 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 * maybe (list reg_name) * 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
(* 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 * value * maybe (list reg_name) * integer * maybe (list reg_name)
| E_write_mem of write_kind * value * maybe (list reg_name) * 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*)
(*should there be a representation for escape down here?*)
(*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 representint the constructor parameters in instruction_form, 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 integer (* A bitvector type, with length when statically known *)
(*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_form = (string * list (string * instr_parm_typ * value) * list base_effect)
type i_state_or_error =
| Instr of instruction_state * instruction_form
| Unsupported_instruction_error of instruction_form
| Not_an_instruction_error
| Internal_error of string
(*
type decode_error =
| Unsupported_instruction_error of instruction
| Not_an_instruction_error of value
| Internal_error of string
type i_state_or_error =
| Instr of instruction * instruction_state
| Decode_error of decode_error
*)
(*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?)*)
|
