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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
|
(* 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
*)
open import Sail_impl_base
import Interp
open import Interp_ast
open import Pervasives
open import Num
open import Assert_extra
type interpreter_state = Interp.stack (*Deem abstract*)
(* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *)
type specification = Interp_ast.defs Interp.tannot (*Deem abstract*)
type interpreter_mode = Interp.interp_mode (*Deem abstract*)
type interp_mode = <| internal_mode: interpreter_mode; endian: end_flag |>
val make_mode : (*eager*) bool -> (*tracking*) bool -> end_flag -> interp_mode
val tracking_dependencies : interp_mode -> bool
(*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
type external_functions = list (string * (Interp.value -> Interp.value))
(*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*)
type barriers = list (string * barrier_kind)
type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name))
type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value
type memory_read = MR of read_kind * memory_parameter_transformer
type memory_reads = list (string * memory_read)
type memory_write_ea = MEA of write_kind * memory_parameter_transformer
type memory_write_eas = list (string * memory_write_ea)
type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
and memory_writes = list (string * memory_write)
and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
and memory_write_vals = list (string * memory_write_val)
(* Definition information needed to run an instruction *)
and context =
Context of Interp.top_level * direction *
memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions
(* An instruction in flight *)
and instruction_state = IState of interpreter_state * context
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 * nat * 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 * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
(* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
| Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state
(* Request to write memory at last signaled address. Memory value should be 8* the size given in ea signal *)
| Write_memv of maybe address_lifted * memory_value * maybe (list reg_name) * (bool -> instruction_state)
(* Request a memory barrier *)
| Barrier of barrier_kind * instruction_state
(* Tell the system to dynamically recalculate dependency footprint *)
| Footprint of 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
(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler
The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp *)
| Escape of maybe instruction_state * instruction_state
(*Result of a failed assert with possible error message to report*)
| Fail of maybe string
(* Stop for incremental stepping, function can be used to display function call data *)
| Internal of maybe string * maybe (unit -> string) * instruction_state
(* Analysis can lead to non_deterministic evaluation, represented with this outcome *)
(*Note: this should not be externally visible *)
| Analysis_non_det of list instruction_state * instruction_state
(*Completed interpreter*)
| Done
(*Interpreter error*)
| Error of string
type event =
| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
| E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
| E_barrier of barrier_kind
| E_footprint
| E_read_reg of reg_name
| E_write_reg of reg_name * register_value
| E_escape
| E_error of string
let ~{ocaml} 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_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
| (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,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_escape,E_escape) -> EQ
| (E_read_mem _ _ _ _, _) -> LT
| (E_write_mem _ _ _ _ _ _, _) -> LT
| (E_write_ea _ _ _ _, _) -> LT
| (E_write_memv _ _ _, _) -> LT
| (E_barrier _, _) -> LT
| (E_read_reg _, _) -> LT
| (E_write_reg _ _, _) -> LT
| _ -> GT
end
let inline {ocaml} eventCompare = defaultCompare
let ~{ocaml} eventLess b1 b2 = eventCompare b1 b2 = LT
let ~{ocaml} eventLessEq b1 b2 = eventCompare b1 b2 <> GT
let ~{ocaml} eventGreater b1 b2 = eventCompare b1 b2 = GT
let ~{ocaml} eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT
let inline {ocaml} eventLess = defaultLess
let inline {ocaml} eventLessEq = defaultLessEq
let inline {ocaml} eventGreater = defaultGreater
let inline {ocaml} eventGreaterEq = defaultGreaterEq
instance (Ord event)
let compare = eventCompare
let (<) = eventLess
let (<=) = eventLessEq
let (>) = eventGreater
let (>=) = eventGreaterEq
end
instance (SetType event)
let setElemCompare = compare
end
(* Functions to build up the initial state for interpretation *)
val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context
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 instruction_or_decode_error =
| IDE_instr of instruction * Interp.value
| 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 -> maybe (list (reg_name * register_value)) -> opcode -> 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 -> maybe (list (reg_name * register_value))-> opcode -> 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 -> instruction_state (*i_state_or_error*)
(* 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
(*Create a new register value where the contents of nat to nat are replaced by the second register_value *)
val update_reg_value_slice : reg_name -> register_value -> nat -> nat -> register_value -> register_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))
val translate_address :
context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address
-> maybe address * maybe (list event)
val instruction_analysis :
context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat)))
-> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind)
val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state unit
|
