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
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
|
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(**************************************************************************)
open Printf ;;
open Big_int_Z ;;
open Sail_values;;
open Mips_extras_ml;;
let interact_print = ref true
let result_print = ref true
let error_print = ref true
let interactf : ('a, out_channel, unit) format -> 'a =
function f -> if !interact_print then printf f else ifprintf stderr f
let errorf : ('a, out_channel, unit) format -> 'a =
function f -> if !error_print then printf f else ifprintf stderr f
let resultf : ('a, out_channel, unit) format -> 'a =
function f -> if !result_print then printf f else ifprintf stderr f
let rec foldli f acc ?(i=0) = function
| [] -> acc
| x::xs -> foldli f (f i acc x) ~i:(i+1) xs;;
let big_int_to_hex i = Z.format "%x" i
let big_int_to_hex64 i = Z.format "%016x" i
let input_buf = (ref [] : int list ref);;
let max_cut_off = ref false
let max_instr = ref 0
let model_arg = ref "cheri"
let raw_list = ref []
let args = [
("--model", Arg.Set_string model_arg, "CPU model to use (mips, cheri, cheri128)");
("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop");
("--trace", Arg.Set trace_writes, "trace all register writes"); (* trace_writes is in sail_values.ml *)
("--quiet", Arg.Clear interact_print, "suppress trace of PC");
("--undef", Arg.String (fun s -> undef_val := bit_of_string s), "value to use for undef (u,0,1)");
]
module type ISA_model = sig
type ast
val init_model : unit -> unit
val inc_nextPC : unit -> unit
val get_pc : unit -> big_int
val translate_pc : unit -> big_int option
val get_opcode : big_int -> value
val decode : value -> ast option
val execute : ast -> unit
val is_halt : ast -> bool
val print_results : unit -> unit
end
let rec debug_print_gprs gprs start stop =
let gpr_val = vector_access gprs (big_int_of_int start) in
let gpr_str =
if has_undef gpr_val then
"uuuuuuuuuuuuuuuu"
else
big_int_to_hex64 (unsigned_big(gpr_val)) in
resultf "DEBUG MIPS REG %.2d 0x%s\n" start gpr_str;
if start < stop
then debug_print_gprs gprs (start + 1) stop
else ()
let cap_reg_to_string reg =
"0b" ^ (string_of_bit_array (get_barray reg))
let read_bit_reg = function
| Vregister (array,_,_,_,_) -> (!array).(0) = Vone
| _ -> failwith "read_bit_reg of non-reg"
let rec debug_print_caps capregs start stop =
let cap_val = vector_access capregs (big_int_of_int start) in
let cap_str = cap_reg_to_string cap_val in
resultf "DEBUG CAP REG %.2d %s\n" start cap_str;
if start < stop
then debug_print_caps capregs (start + 1) stop
else ()
let handle_uart uart_written uart_wdata uart_rdata uart_rvalid =
(try
let (pending, _, _) = Unix.select [Unix.stdin] [] [] 0.0 in
if pending != [] then
input_buf := (!input_buf) @ [(input_byte stdin)]
with _ -> ());
if (read_bit_reg uart_written) then
begin
let b = unsigned_int(uart_wdata) in
printf "%c" (Char.chr b);
printf "%!";
set_register uart_written (to_vec_dec_int (1,0))
end;
if not (read_bit_reg uart_rvalid) then
(match !input_buf with
| x :: xs ->
begin
set_register uart_rdata (to_vec_dec_int (8, x));
set_register uart_rvalid (to_vec_dec_int (1, 1));
input_buf := xs;
end
| _ -> ())
module MIPS_model : ISA_model = struct
type ast = Mips_embed._ast
let init_model () =
let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in
set_register Mips_embed._nextPC start_addr;
set_register_field_bit Mips_embed._CP0Status "BEV" Vone
let inc_nextPC () =
handle_uart Mips_embed._UART_WRITTEN Mips_embed._UART_WDATA Mips_embed._UART_RDATA Mips_embed._UART_RVALID;
set_register Mips_embed._inBranchDelay Mips_embed._branchPending;
set_register Mips_embed._branchPending (to_vec_dec_int (1, 0));
set_register Mips_embed._PC Mips_embed._nextPC;
let inBranchDelay = read_bit_reg Mips_embed._inBranchDelay in
if inBranchDelay then
set_register Mips_embed._nextPC Mips_embed._delayedPC
else
let pc_vaddr = unsigned_big(Mips_embed._PC) in
let npc_addr = add_int_big_int 4 pc_vaddr in
let npc_vec = to_vec_dec_big (bi64, npc_addr) in
set_register Mips_embed._nextPC npc_vec
let get_pc () = unsigned_big (Mips_embed._PC)
let translate_pc () =
try
Some (unsigned_big(Mips_embed._TranslatePC(Mips_embed._PC)))
with Sail_exit -> None
let get_opcode pc_a = Mips_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4))
let decode = Mips_embed._decode
let execute = Mips_embed._execute
let is_halt i = (i = Mips_embed.HCF)
let print_results () =
begin
resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Mips_embed._PC));
debug_print_gprs Mips_embed._GPR 0 31;
end
end
module CHERI_model : ISA_model = struct
type ast = Cheri_embed._ast
let init_model () =
let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in
set_register Cheri_embed._nextPC start_addr;
set_register_field_bit Cheri_embed._CP0Status "BEV" Vone;
let initial_cap_val_int = big_int_of_string "0x100000000fffffffe00000000000000000000000000000000ffffffffffffffff" in
let initial_cap_vec = to_vec_dec ((big_int_of_int 257), initial_cap_val_int) in
set_register Cheri_embed._PCC initial_cap_vec;
set_register Cheri_embed._nextPCC initial_cap_vec;
set_register Cheri_embed._delayedPCC initial_cap_vec;
for i = 0 to 31 do
set_register (vector_access_int Cheri_embed._CapRegs i) initial_cap_vec
done
let inc_nextPC () =
handle_uart Cheri_embed._UART_WRITTEN Cheri_embed._UART_WDATA Cheri_embed._UART_RDATA Cheri_embed._UART_RVALID;
set_register Cheri_embed._inBranchDelay Cheri_embed._branchPending;
set_register Cheri_embed._branchPending (to_vec_dec_int (1, 0));
set_register Cheri_embed._PC Cheri_embed._nextPC;
set_register Cheri_embed._PCC Cheri_embed._nextPCC;
let inBranchDelay = read_bit_reg Cheri_embed._inBranchDelay in
if inBranchDelay then
begin
set_register Cheri_embed._nextPC Cheri_embed._delayedPC;
set_register Cheri_embed._nextPCC Cheri_embed._delayedPCC;
end
else
let pc_vaddr = unsigned_big(Cheri_embed._PC) in
let npc_addr = add_int_big_int 4 pc_vaddr in
let npc_vec = to_vec_dec_big (bi64, npc_addr) in
set_register Cheri_embed._nextPC npc_vec
let get_pc () = unsigned_big (Cheri_embed._PC)
let translate_pc () =
try
Some (unsigned_big(Cheri_embed._TranslatePC(Cheri_embed._PC)))
with Sail_exit -> None
let get_opcode pc_a = Cheri_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4))
let decode = Cheri_embed._decode
let execute = Cheri_embed._execute
let is_halt i = (i = Cheri_embed.HCF)
let print_results () =
begin
resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Cheri_embed._PC));
debug_print_gprs Cheri_embed._GPR 0 31;
resultf "DEBUG CAP PCC %s\n" (cap_reg_to_string Cheri_embed._PCC);
debug_print_caps Cheri_embed._CapRegs 0 31;
end
end
module CHERI128_model : ISA_model = struct
type ast = Cheri128_embed._ast
let init_model () =
let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in
set_register Cheri128_embed._nextPC start_addr;
set_register_field_bit Cheri128_embed._CP0Status "BEV" Vone;
let initial_cap_val_int = big_int_of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *)
let initial_cap_vec = to_vec_dec ((bi129), initial_cap_val_int) in
set_register Cheri128_embed._PCC initial_cap_vec;
set_register Cheri128_embed._nextPCC initial_cap_vec;
set_register Cheri128_embed._delayedPCC initial_cap_vec;
for i = 0 to 31 do
set_register (vector_access_int Cheri128_embed._CapRegs i) initial_cap_vec
done
let inc_nextPC () =
handle_uart Cheri128_embed._UART_WRITTEN Cheri128_embed._UART_WDATA Cheri128_embed._UART_RDATA Cheri128_embed._UART_RVALID;
set_register Cheri128_embed._inBranchDelay Cheri128_embed._branchPending;
set_register Cheri128_embed._branchPending (to_vec_dec_int (1, 0));
set_register Cheri128_embed._PC Cheri128_embed._nextPC;
set_register Cheri128_embed._PCC Cheri128_embed._nextPCC;
let inBranchDelay = read_bit_reg Cheri128_embed._inBranchDelay in
if inBranchDelay then
begin
set_register Cheri128_embed._nextPC Cheri128_embed._delayedPC;
set_register Cheri128_embed._nextPCC Cheri128_embed._delayedPCC;
end
else
let pc_vaddr = unsigned_big(Cheri128_embed._PC) in
let npc_addr = add_int_big_int 4 pc_vaddr in
let npc_vec = to_vec_dec_big (bi64, npc_addr) in
set_register Cheri128_embed._nextPC npc_vec
let get_pc () = unsigned_big (Cheri128_embed._PC)
let translate_pc () =
try
Some (unsigned_big(Cheri128_embed._TranslatePC(Cheri128_embed._PC)))
with Sail_exit -> None
let get_opcode pc_a = Cheri128_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4))
let decode = Cheri128_embed._decode
let execute = Cheri128_embed._execute
let is_halt i = (i = Cheri128_embed.HCF)
let print_results () =
begin
resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Cheri128_embed._PC));
debug_print_gprs Cheri128_embed._GPR 0 31;
resultf "DEBUG CAP PCC %s\n" (cap_reg_to_string Cheri128_embed._PCC);
debug_print_caps Cheri128_embed._CapRegs 0 31;
end
end
let time_it action arg =
let start_time = Sys.time () in
let ret = action arg in
let finish_time = Sys.time () in
(finish_time -. start_time, ret)
let rec fde_loop (model, count) =
if !max_cut_off && count = !max_instr
then begin
resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count;
count
end
else
begin
let module Model = (val model : ISA_model) in
Model.inc_nextPC ();
if !interact_print then
interactf "\n**** instruction %d from address %s ****\n"
count (big_int_to_hex64 (Model.get_pc ()));
let m_paddr = Model.translate_pc () in
match m_paddr with
| Some pc ->
let opcode = Model.get_opcode pc in
if !interact_print then
interactf "decode: 0x%x\n" (unsigned_int(opcode));
let instruction = Model.decode opcode in
let i = match instruction with
| Some (i) -> i
| _ -> begin
errorf "\n**** Decode error ****\n";
exit 1;
end
in
if Model.is_halt i then
begin
Model.print_results ();
resultf "\nSUCCESS program terminated after %d instructions\n" count;
count
end
else
begin
(try
Model.execute(i)
with Sail_exit -> ()); (* exception during execute *)
fde_loop (model, count + 1)
end
| None -> (* Exception during PC translation *)
fde_loop (model, count + 1)
end
let rec load_raw_file buf addr len chan =
let to_read = min_int len page_size_bytes in
really_input chan buf 0 to_read;
add_mem_bytes addr buf 0 to_read;
if (len > to_read) then
load_raw_file buf (add_int_big_int to_read addr) (len - to_read) chan
let get_model = function
| "cheri128" -> (module CHERI128_model : ISA_model)
| "cheri" -> (module CHERI_model : ISA_model)
| "mips" -> (module MIPS_model : ISA_model)
| _ -> failwith "unknown model name"
let anon_raw s =
(* some input validation would be nice... *)
let len = String.length s in
let atidx = try
String.index s '@'
with Not_found -> raise (Arg.Bad "expected argument of form file@addr") in
let f = String.sub s 0 atidx in
let addr = String.sub s (atidx+1) (len - atidx -1) in
raw_list := (!raw_list) @ [(f, big_int_of_string addr)]
let load_raw_arg (f, a) =
let buf = Bytes.create page_size_bytes in
let chan = open_in_bin f in
let len = in_channel_length chan in
load_raw_file buf a len chan
let run () =
(* Turn off line-buffering of standard input to allow responsive console input *)
if Unix.isatty (Unix.stdin) then begin
let tattrs = Unix.tcgetattr (Unix.stdin) in
Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false})
end;
Arg.parse args anon_raw "" ;
List.iter load_raw_arg !raw_list;
let model = get_model !model_arg in
let module Model = (val model : ISA_model) in
Model.init_model ();
let (t, count) = time_it fde_loop (model, 0) in
resultf "Execution time: %f seconds %f IPS \n" t (float(count) /. t);;
run () ;;
|