| Page table setup | Code |
|---|---|
physical pa1;
intermediate ipa1;
assert pa1 == ipa1;
ipa1 |-> pa1;
s1table new_table 0x280000 {
x |-> invalid;
x ?-> ipa1;
};
identity 0x283000 with default;
x |-> invalid at level 2;
x ?-> table(0x283000) at level 2;
identity 0x1000 with code;
|
|
| Thread 0 | |
{R0=mkdesc3(oa=ipa1), R1=pte3(x, new_table), R2=mkdesc2(table=extz(0x283000, 64)), R3=pte2(x, page_table_base), PSTATE.EL=0b01}
|
|
STR X0,[X1]
DMB ST
STR X2,[X3]
|
|
| Thread 1 | |
{R1=x, VBAR_EL1=extz(0x1000, 64)}
|
|
LDR X0,[X1]
|
|
| thread_1_el1_handler | |
MRS x14,esr_el1
AND X14,X14,#0b111
CMP x14,#0b111
MOV X17,#1
MOV X18,#2
// if ESR_EL1.ISS.DFSC == Translation Level 3 then x2 = 1 else x2 = 2
CSEL x0,x17,x18,eq
|
|
| Final State | |
1:X0=1 |
|
| ETS | ROT.inv+dmbst forbidden (0 of 3) 3919ms |
| strong | ROT.inv+dmbst forbidden (0 of 3) 3998ms |
isla-axiomatic
--arch=/path/to/rems-project/isla-snapshots/aarch64.ir
--config=/path/to/rems-project/isla/configs/aarch64_mmu_on.toml
--footprint-config=/path/to/rems-project/isla/configs/aarch64.toml
--model=/path/to/rems-project/systems-isla-tests/models/aarch64_mmu_strong_ETS.cat
--armv8-page-tables
--check-sat-using "(then dt2bv qe simplify solve-eqs bv)"
--remove-uninteresting safe
--dot .
-t /path/to/litmus-tests/litmus-tests-armv8a-system-vmsa/tests/pgtable/HAND/ROT.inv+dmbst.litmus.toml
To generate diagrams we use model aarch64_mmu_no_axioms.cat to get diagrams of forbidden executions.
To generate LaTeX sources of each test, pass --latex=.