isla 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications.
Documentation 
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

pc = "_PC"

ifetch = "Read_ifetch"

read_exclusives = []
write_exclusives = []

# The assembler is used for assembling the code in litmus tests. We
# assume it takes arguments like GNU as.
assembler = "aarch64-linux-gnu-as"
objdump = "aarch64-linux-gnu-objdump"
linker = "aarch64-linux-gnu-ld"

[mmu]
page_table_base = "0x300000"
page_size = "4096"
s2_page_table_base = "0x300000"
s2_page_size = "4096"

# This section contains the base address for loading the code for each
# thread in a litmus test, and the stride which is the distance
# between each thread in bytes. The overall range for thread memory is
# the half-open range [base,top)"
[threads]
base = "0x400000"
top = "0x500000"
stride = "0x10000"

[symbolic_addrs]
base = "0x600000"
stride = "0x10"

[registers]
ignore = []

[registers.defaults]

# A map from register names in the litmus to Sail register specifiers
# (roughtly corresponding to l-expressions in Sail, i.e. subscripting
# R[n] and field accesses R.field are allowed.)
[registers.renames]

[reads]

[writes]

[cache_ops]