blob: 1422635be4f2de72a47d5501093b92a2ba9f224e (
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
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
|
/*=======================================================================================*/
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/
// When the symbolic execution is running a litmus test, it sets a
// different entry point for each thread in the compiled litmus test.
val get_entry_point : unit -> xlenbits
$ifdef SYMBOLIC
$include <elf.sail>
function get_entry_point() = to_bits(sizeof(xlen), elf_entry())
$else
function get_entry_point() = zero_extend(0x1000)
$endif
function main() : unit -> unit = {
// initialize extensions
ext_init();
PC = get_entry_point();
print_bits("PC = ", PC);
try {
init_model();
sail_end_cycle();
loop()
} catch {
Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
Error_internal_error() => print("Error: internal error")
}
}
// For symbolic execution using Isla, we need an entry point that
// allows us to execute a single instruction.
$ifdef SYMBOLIC
$include <isla.sail>
val isla_footprint_no_init : forall 'n, 'n in {16, 32}. bits('n) -> bool
function isla_footprint_no_init(opcode) = {
try {
isla_reset_registers();
sail_end_cycle();
let instr = if length(opcode) == 16 then {
ext_decode_compressed(opcode)
} else {
ext_decode(opcode)
};
let _ = execute(instr);
true
} catch {
_ => false
}
}
val isla_footprint : forall 'n, 'n in {16, 32}. bits('n) -> bool
function isla_footprint(opcode) = {
try {
init_model();
isla_footprint_no_init(opcode)
} catch {
_ => false
}
}
$endif
|
