arch = "AArch64"
name = "SB+dmb.sy+rfi-pos-ctrl"
hash = "782aa43579d102a40a34046d76d3ebbf"
cycle = "Rfi PosRR DpCtrldR Fre DMB.SYdWR Fre"
relax = ""
safe = "Rfi Fre PosRR DMB.SYdWR DpCtrldR"
prefetch = "0:x=F,0:y=T,1:y=F,1:x=T"
com = "Fr Fr"
orig = "DMB.SYdWR Fre Rfi PosRR DpCtrldR Fre"
symbolic = ["x", "y"]
[thread.0]
init = { X3 = "y", X1 = "x" }
code = """
MOV W0,#1
STR W0,[X1]
DMB SY
LDR W2,[X3]
"""
[thread.1]
init = { X5 = "x", X1 = "y" }
code = """
MOV W0,#1
STR W0,[X1]
LDR W2,[X1]
LDR W3,[X1]
CBNZ W3,LC00
LC00:
LDR W4,[X5]
"""
[final]
expect = "sat"
assertion = "(and (and (and (and (and (= (last_write_to x) 1) (= (last_write_to y) 1)) (= (register X2 0) 0)) (= (register X2 1) 1)) (= (register X3 1) 1)) (= (register X4 1) 0))"
