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

arch = "RISCV"
name = "LB+data+ctrl"
hash = "a089d994113199f347ca5786ab3b2b59"
cycle = "Rfe DpDatadW Rfe DpCtrldW"
relax = ""
safe = "Rfe DpDatadW DpCtrldW"
generator = "diy7 (version 7.51+4(dev))"
prefetch = "0:x=F,0:y=W,1:y=F,1:x=W"
com = "Rf Rf"
orig = "DpDatadW Rfe DpCtrldW Rfe"
symbolic = ["x", "y"]

[thread.0]
init = { x8 = "y", x6 = "x" }
code = """
	lw x5,0(x6)
	xor x7,x5,x5
	ori x7,x7,1
	sw x7,0(x8)
"""

[thread.1]
init = { x8 = "x", x7 = "1", x6 = "y" }
code = """
	lw x5,0(x6)
	bne x5,x0,LC00
LC00:
	sw x7,0(x8)
"""

[final]
expect = "sat"
assertion = "0:x5 = 1 & 1:x5 = 1"