Merge VMIDs

doc/asciidoc/sections/intro.adoc

@@ -28,4 +28,6 @@ Casemate currently supports Arm-A, and the following page table protocols:
 
 * Context switching between different page tables.
 
+* Invalidation-by-VMID and re-use of VMIDs.
+
 * Thread-local address spaces.

doc/asciidoc/sections/trace-format.adoc

@@ -135,8 +135,7 @@ TLBI-OP-ADDR-KIND =
 
 TLBI-OP-ADDR =
     TLBI-OP-ADDR-KIND,
-      "(", "addr", u64, ")",
-      "(", "level", u64, ")"
+      "(", "value", u64, ")"
   ;
 ----
 

examples/.gitignore

@@ -26,3 +26,11 @@
 /good_free_page
 /good_free_tree
 /good_write_child
+/bad_switch_wrong_vmid
+/good_bbm_by_VMID
+/bad_bbm_by_wrong_VMID
+/good_bbm_stage1
+/bad_no_bbm_stage1
+/bad_overlap_ASID
+/bad_overlap_VMID
+/bad_EL2_ASID

examples/Makefile

@@ -1,4 +1,4 @@
-.PHONY: build clean logs
+.PHONY: build clean logs list-build-objs
 
 build-objs += simple
 build-objs += good_write
@@ -13,6 +13,17 @@ build-objs += bad_free_page_without_clean
 build-objs += good_free_page
 build-objs += good_free_tree
 build-objs += good_write_child
+build-objs += bad_switch_wrong_vmid
+build-objs += good_bbm_by_VMID
+build-objs += bad_bbm_by_wrong_VMID
+build-objs += bad_overlap_VMID
+build-objs += good_bbm_stage1
+build-objs += bad_no_bbm_stage1
+build-objs += bad_overlap_ASID
+build-objs += bad_EL2_ASID
+
+list-build-objs:
+	@echo $(build-objs)
 
 build: $(addprefix $(src)/,$(build-objs)) $(src)/compile_commands.json
 

examples/common.h

@@ -16,6 +16,21 @@ void join(void);
 void send(tid_t to, int v);
 int recv(void);
 
+/*
+ * Macros that require input of a maximum size
+ *
+ * TODO: make compiler check
+ */
+#define REQ_U8_AS_U64(X) ((u64)(X))
+#define REQ_U64(X) ((u64)(X))
+
+#define MAKE_TTBR(BADDR,ID) \
+	((BADDR) | ((ID) << 48ULL))
+
+#define ID0 0ULL
+#define ID1 1ULL
+#define ID2 2ULL
+
 #define WRITE_ONCE(VAR, VAL) \
 	({	\
 		casemate_model_step_write(WMO_plain, (u64)&VAR, (VAL)); \
@@ -42,10 +57,10 @@ int recv(void);
 	casemate_model_step_isb()
 
 #define TLBI_ALL(OP) \
-	casemate_model_step_tlbi1(TLBI_##OP)
+	casemate_model_step_tlbi(TLBI_##OP)
 
 #define TLBI_ADDR(OP, ADDR, LEVEL) \
-	casemate_model_step_tlbi3(TLBI_##OP, ADDR, LEVEL)
+	casemate_model_step_tlbi_reg(TLBI_##OP, REQ_U64(ADDR) | (REQ_U8_AS_U64(LEVEL) << 44ULL))
 
 #define LOCK(L) \
 	casemate_model_step_lock((u64)&(L))

examples/expected/bad_EL2_ASID.log

@@ -0,0 +1,6 @@
+(mem-init (id 0) (tid 0) (address 0xaaaac1ab4000) (size 0x1000) (src "examples/tests/bad_EL2_ASID.c:19"))
+(mem-init (id 1) (tid 0) (address 0xaaaac1ab5000) (size 0x1000) (src "examples/tests/bad_EL2_ASID.c:20"))
+(hint (id 2) (tid 0) (kind set_root_lock) (location 0xaaaac1ab4000) (value 0xaaaac1ab6000) (src "examples/tests/bad_EL2_ASID.c:22"))
+(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaac1ab5000) (value 0xaaaac1ab6008) (src "examples/tests/bad_EL2_ASID.c:23"))
+(sysreg-write (id 4) (tid 0) (sysreg ttbr0_el2) (value 0x1aaaac1ab4000) (src "examples/tests/bad_EL2_ASID.c:26"))
+! TTBR0_EL2 ASID is reserved 0

examples/expected/bad_bbm_by_wrong_VMID.log

@@ -0,0 +1,23 @@
+(mem-init (id 0) (tid 0) (address 0xaaaab9385000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:26"))
+(mem-init (id 1) (tid 0) (address 0xaaaab9386000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:27"))
+(mem-init (id 2) (tid 0) (address 0xaaaab9387000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:28"))
+(mem-init (id 3) (tid 0) (address 0xaaaab9388000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:29"))
+(hint (id 4) (tid 0) (kind set_root_lock) (location 0xaaaab9385000) (value 0xaaaab9389000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:30"))
+(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaab9386000) (value 0xaaaab9385000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:31"))
+(hint (id 6) (tid 0) (kind set_owner_root) (location 0xaaaab9387000) (value 0xaaaab9385000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:32"))
+(mem-write (id 7) (tid 0) (mem-order plain) (address 0xaaaab9385000) (value 0xaaaab9386003) (src "examples/tests/bad_bbm_by_wrong_VMID.c:35"))
+(sysreg-write (id 8) (tid 0) (sysreg vttbr_el2) (value 0xaaaab9385000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:38"))
+(lock (id 9) (tid 0) (address 0xaaaab9389000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:40"))
+(mem-write (id 10) (tid 0) (mem-order plain) (address 0xaaaab9385000) (value 0x0) (src "examples/tests/bad_bbm_by_wrong_VMID.c:41"))
+(barrier (id 11) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_by_wrong_VMID.c:44"))
+(sysreg-write (id 12) (tid 0) (sysreg vttbr_el2) (value 0x1aaaab9388000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:45"))
+(barrier (id 13) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_by_wrong_VMID.c:46"))
+(tlbi (id 14) (tid 0) ipas2e1is (value 0x300000000000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:47"))
+(barrier (id 15) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_by_wrong_VMID.c:48"))
+(tlbi (id 16) (tid 0) vmalle1is (src "examples/tests/bad_bbm_by_wrong_VMID.c:49"))
+(barrier (id 17) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_by_wrong_VMID.c:50"))
+(barrier (id 18) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_by_wrong_VMID.c:52"))
+(sysreg-write (id 19) (tid 0) (sysreg vttbr_el2) (value 0xaaaab9385000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:54"))
+(barrier (id 20) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_by_wrong_VMID.c:55"))
+(mem-write (id 21) (tid 0) (mem-order plain) (address 0xaaaab9385000) (value 0xaaaab9387003) (src "examples/tests/bad_bbm_by_wrong_VMID.c:57"))
+! BBM invalid unclean->valid

examples/expected/bad_bbm_missing_tlbi.log

@@ -1,14 +1,14 @@
-(mem-init (id 0) (tid 0) (address 0xaaaad0563000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:25"))
-(mem-init (id 1) (tid 0) (address 0xaaaad0564000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:26"))
-(mem-init (id 2) (tid 0) (address 0xaaaad0565000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:27"))
-(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaad0563000) (value 0xaaaad0566000) (src "examples/tests/bad_bbm_missing_tlbi.c:28"))
-(hint (id 4) (tid 0) (kind set_owner_root) (location 0xaaaad0564000) (value 0xaaaad0563000) (src "examples/tests/bad_bbm_missing_tlbi.c:29"))
-(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaad0565000) (value 0xaaaad0563000) (src "examples/tests/bad_bbm_missing_tlbi.c:30"))
-(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaad0563000) (value 0xaaaad0564003) (src "examples/tests/bad_bbm_missing_tlbi.c:33"))
-(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaad0563000) (src "examples/tests/bad_bbm_missing_tlbi.c:36"))
-(lock (id 8) (tid 0) (address 0xaaaad0566000) (src "examples/tests/bad_bbm_missing_tlbi.c:38"))
-(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaad0563000) (value 0x0) (src "examples/tests/bad_bbm_missing_tlbi.c:39"))
+(mem-init (id 0) (tid 0) (address 0xaaaadccc5000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:25"))
+(mem-init (id 1) (tid 0) (address 0xaaaadccc6000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:26"))
+(mem-init (id 2) (tid 0) (address 0xaaaadccc7000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:27"))
+(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaadccc5000) (value 0xaaaadccc8000) (src "examples/tests/bad_bbm_missing_tlbi.c:28"))
+(hint (id 4) (tid 0) (kind set_owner_root) (location 0xaaaadccc6000) (value 0xaaaadccc5000) (src "examples/tests/bad_bbm_missing_tlbi.c:29"))
+(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaadccc7000) (value 0xaaaadccc5000) (src "examples/tests/bad_bbm_missing_tlbi.c:30"))
+(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaadccc5000) (value 0xaaaadccc6003) (src "examples/tests/bad_bbm_missing_tlbi.c:33"))
+(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaadccc5000) (src "examples/tests/bad_bbm_missing_tlbi.c:36"))
+(lock (id 8) (tid 0) (address 0xaaaadccc8000) (src "examples/tests/bad_bbm_missing_tlbi.c:38"))
+(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaadccc5000) (value 0x0) (src "examples/tests/bad_bbm_missing_tlbi.c:39"))
 (barrier (id 10) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_missing_tlbi.c:40"))
 (barrier (id 11) (tid 0) dsb (kind ish) (src "examples/tests/bad_bbm_missing_tlbi.c:41"))
-(mem-write (id 12) (tid 0) (mem-order plain) (address 0xaaaad0563000) (value 0xaaaad0565003) (src "examples/tests/bad_bbm_missing_tlbi.c:42"))
+(mem-write (id 12) (tid 0) (mem-order plain) (address 0xaaaadccc5000) (value 0xaaaadccc7003) (src "examples/tests/bad_bbm_missing_tlbi.c:42"))
 ! BBM invalid unclean->valid

examples/expected/bad_no_assoc_lock.log

@@ -1,4 +1,4 @@
-(mem-init (id 0) (tid 0) (address 0x55fce57ad000) (size 0x1000) (src "examples/tests/bad_no_assoc_lock.c:17"))
-(sysreg-write (id 1) (tid 0) (sysreg vttbr_el2) (value 0x55fce57ad000) (src "examples/tests/bad_no_assoc_lock.c:18"))
-(mem-write (id 2) (tid 0) (mem-order plain) (address 0x55fce57ad000) (value 0x0) (src "examples/tests/bad_no_assoc_lock.c:19"))
+(mem-init (id 0) (tid 0) (address 0xaaaacbf54000) (size 0x1000) (src "examples/tests/bad_no_assoc_lock.c:17"))
+(sysreg-write (id 1) (tid 0) (sysreg vttbr_el2) (value 0xaaaacbf54000) (src "examples/tests/bad_no_assoc_lock.c:18"))
+(mem-write (id 2) (tid 0) (mem-order plain) (address 0xaaaacbf54000) (value 0x0) (src "examples/tests/bad_no_assoc_lock.c:19"))
 ! must have associated owner with a root

examples/expected/bad_no_bbm.log

@@ -1,9 +1,9 @@
-(mem-init (id 0) (tid 0) (address 0xaaaaccbb3000) (size 0x1000) (src "examples/tests/bad_no_bbm.c:24"))
-(mem-init (id 1) (tid 0) (address 0xaaaaccbb4000) (size 0x1000) (src "examples/tests/bad_no_bbm.c:25"))
-(hint (id 2) (tid 0) (kind set_root_lock) (location 0xaaaaccbb3000) (value 0xaaaaccbb5000) (src "examples/tests/bad_no_bbm.c:26"))
-(hint (id 3) (tid 0) (kind set_owner_root) (location 0xaaaaccbb4000) (value 0xaaaaccbb3000) (src "examples/tests/bad_no_bbm.c:27"))
-(mem-write (id 4) (tid 0) (mem-order plain) (address 0xaaaaccbb3000) (value 0xaaaaccbb4003) (src "examples/tests/bad_no_bbm.c:30"))
-(sysreg-write (id 5) (tid 0) (sysreg vttbr_el2) (value 0xaaaaccbb3000) (src "examples/tests/bad_no_bbm.c:33"))
-(lock (id 6) (tid 0) (address 0xaaaaccbb5000) (src "examples/tests/bad_no_bbm.c:35"))
-(mem-write (id 7) (tid 0) (mem-order plain) (address 0xaaaaccbb3000) (value 0x3) (src "examples/tests/bad_no_bbm.c:36"))
+(mem-init (id 0) (tid 0) (address 0xaaaabad05000) (size 0x1000) (src "examples/tests/bad_no_bbm.c:24"))
+(mem-init (id 1) (tid 0) (address 0xaaaabad06000) (size 0x1000) (src "examples/tests/bad_no_bbm.c:25"))
+(hint (id 2) (tid 0) (kind set_root_lock) (location 0xaaaabad05000) (value 0xaaaabad07000) (src "examples/tests/bad_no_bbm.c:26"))
+(hint (id 3) (tid 0) (kind set_owner_root) (location 0xaaaabad06000) (value 0xaaaabad05000) (src "examples/tests/bad_no_bbm.c:27"))
+(mem-write (id 4) (tid 0) (mem-order plain) (address 0xaaaabad05000) (value 0xaaaabad06003) (src "examples/tests/bad_no_bbm.c:30"))
+(sysreg-write (id 5) (tid 0) (sysreg vttbr_el2) (value 0xaaaabad05000) (src "examples/tests/bad_no_bbm.c:33"))
+(lock (id 6) (tid 0) (address 0xaaaabad07000) (src "examples/tests/bad_no_bbm.c:35"))
+(mem-write (id 7) (tid 0) (mem-order plain) (address 0xaaaabad05000) (value 0x3) (src "examples/tests/bad_no_bbm.c:36"))
 ! BBM valid->valid

examples/expected/bad_no_bbm_stage1.log

@@ -0,0 +1,11 @@
+(mem-init (id 0) (tid 0) (address 0xaaaae87e5000) (size 0x1000) (src "examples/tests/bad_no_bbm_stage1.c:21"))
+(mem-init (id 1) (tid 0) (address 0xaaaae87e6000) (size 0x1000) (src "examples/tests/bad_no_bbm_stage1.c:22"))
+(mem-init (id 2) (tid 0) (address 0xaaaae87e7000) (size 0x1000) (src "examples/tests/bad_no_bbm_stage1.c:23"))
+(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaae87e5000) (value 0xaaaae87e8000) (src "examples/tests/bad_no_bbm_stage1.c:24"))
+(hint (id 4) (tid 0) (kind set_owner_root) (location 0xaaaae87e6000) (value 0xaaaae87e5000) (src "examples/tests/bad_no_bbm_stage1.c:25"))
+(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaae87e7000) (value 0xaaaae87e5000) (src "examples/tests/bad_no_bbm_stage1.c:26"))
+(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaae87e5000) (value 0xaaaae87e6003) (src "examples/tests/bad_no_bbm_stage1.c:29"))
+(sysreg-write (id 7) (tid 0) (sysreg ttbr0_el2) (value 0xaaaae87e5000) (src "examples/tests/bad_no_bbm_stage1.c:32"))
+(lock (id 8) (tid 0) (address 0xaaaae87e8000) (src "examples/tests/bad_no_bbm_stage1.c:34"))
+(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaae87e5000) (value 0xaaaae87e7003) (src "examples/tests/bad_no_bbm_stage1.c:35"))
+! BBM valid->valid

examples/expected/bad_overlap_ASID.log

@@ -0,0 +1,9 @@
+(mem-init (id 0) (tid 0) (address 0xaaaac51f5000) (size 0x1000) (src "examples/tests/bad_overlap_ASID.c:19"))
+(mem-init (id 1) (tid 0) (address 0xaaaac51f6000) (size 0x1000) (src "examples/tests/bad_overlap_ASID.c:20"))
+(hint (id 2) (tid 0) (kind set_root_lock) (location 0xaaaac51f5000) (value 0xaaaac51f7000) (src "examples/tests/bad_overlap_ASID.c:22"))
+(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaac51f6000) (value 0xaaaac51f7008) (src "examples/tests/bad_overlap_ASID.c:23"))
+(sysreg-write (id 4) (tid 0) (sysreg ttbr0_el2) (value 0xaaaac51f5000) (src "examples/tests/bad_overlap_ASID.c:25"))
+(barrier (id 5) (tid 0) dsb (kind ish) (src "examples/tests/bad_overlap_ASID.c:26"))
+(barrier (id 6) (tid 0) isb (src "examples/tests/bad_overlap_ASID.c:27"))
+(sysreg-write (id 7) (tid 0) (sysreg ttbr0_el2) (value 0xaaaac51f6000) (src "examples/tests/bad_overlap_ASID.c:30"))
+! duplicate (VM/AS)ID

examples/expected/bad_overlap_VMID.log

@@ -0,0 +1,9 @@
+(mem-init (id 0) (tid 0) (address 0xaaaaad1e5000) (size 0x1000) (src "examples/tests/bad_overlap_VMID.c:19"))
+(mem-init (id 1) (tid 0) (address 0xaaaaad1e6000) (size 0x1000) (src "examples/tests/bad_overlap_VMID.c:20"))
+(hint (id 2) (tid 0) (kind set_root_lock) (location 0xaaaaad1e5000) (value 0xaaaaad1e7000) (src "examples/tests/bad_overlap_VMID.c:22"))
+(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaaad1e6000) (value 0xaaaaad1e7008) (src "examples/tests/bad_overlap_VMID.c:23"))
+(sysreg-write (id 4) (tid 0) (sysreg vttbr_el2) (value 0xaaaaad1e5000) (src "examples/tests/bad_overlap_VMID.c:25"))
+(barrier (id 5) (tid 0) dsb (kind ish) (src "examples/tests/bad_overlap_VMID.c:26"))
+(barrier (id 6) (tid 0) isb (src "examples/tests/bad_overlap_VMID.c:27"))
+(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaaad1e6000) (src "examples/tests/bad_overlap_VMID.c:30"))
+! duplicate (VM/AS)ID

examples/expected/bad_race.log

@@ -1,5 +1,5 @@
-(mem-init (id 0) (tid 0) (address 0xaaaac73b4000) (size 0x1000) (src "examples/tests/bad_race.c:42"))
-(hint (id 1) (tid 0) (kind set_root_lock) (location 0xaaaac73b4000) (value 0xaaaac73b5000) (src "examples/tests/bad_race.c:43"))
-(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0xaaaac73b4000) (src "examples/tests/bad_race.c:46"))
-(mem-write (id 3) (tid 1) (mem-order release) (address 0xaaaac73b4008) (value 0x1) (src "examples/tests/bad_race.c:24"))
+(mem-init (id 0) (tid 0) (address 0xaaaad1f75000) (size 0x1000) (src "examples/tests/bad_race.c:42"))
+(hint (id 1) (tid 0) (kind set_root_lock) (location 0xaaaad1f75000) (value 0xaaaad1f76000) (src "examples/tests/bad_race.c:43"))
+(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0xaaaad1f75000) (src "examples/tests/bad_race.c:46"))
+(mem-write (id 3) (tid 1) (mem-order release) (address 0xaaaad1f75008) (value 0x1) (src "examples/tests/bad_race.c:24"))
 ! must write to pte while holding owner lock

examples/expected/bad_reuse_page.log

@@ -1,15 +1,15 @@
-(mem-init (id 0) (tid 0) (address 0xaaaadee24000) (size 0x1000) (src "examples/tests/bad_reuse_page.c:23"))
-(mem-init (id 1) (tid 0) (address 0xaaaadee25000) (size 0x1000) (src "examples/tests/bad_reuse_page.c:24"))
-(mem-init (id 2) (tid 0) (address 0xaaaadee26000) (size 0x1000) (src "examples/tests/bad_reuse_page.c:25"))
-(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaadee24000) (value 0xaaaadee27000) (src "examples/tests/bad_reuse_page.c:26"))
-(hint (id 4) (tid 0) (kind set_root_lock) (location 0xaaaadee26000) (value 0xaaaadee27008) (src "examples/tests/bad_reuse_page.c:27"))
-(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaadee25000) (value 0xaaaadee24000) (src "examples/tests/bad_reuse_page.c:28"))
-(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaadee24000) (value 0xaaaadee25003) (src "examples/tests/bad_reuse_page.c:29"))
-(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaadee24000) (src "examples/tests/bad_reuse_page.c:31"))
-(lock (id 8) (tid 0) (address 0xaaaadee27000) (src "examples/tests/bad_reuse_page.c:33"))
-(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaadee24000) (value 0x0) (src "examples/tests/bad_reuse_page.c:34"))
-(unlock (id 10) (tid 0) (address 0xaaaadee27000) (src "examples/tests/bad_reuse_page.c:35"))
-(sysreg-write (id 11) (tid 0) (sysreg vttbr_el2) (value 0xaaaadee26000) (src "examples/tests/bad_reuse_page.c:38"))
-(lock (id 12) (tid 0) (address 0xaaaadee27008) (src "examples/tests/bad_reuse_page.c:39"))
-(mem-write (id 13) (tid 0) (mem-order plain) (address 0xaaaadee26000) (value 0xaaaadee25003) (src "examples/tests/bad_reuse_page.c:40"))
+(mem-init (id 0) (tid 0) (address 0xaaaac6c45000) (size 0x1000) (src "examples/tests/bad_reuse_page.c:23"))
+(mem-init (id 1) (tid 0) (address 0xaaaac6c46000) (size 0x1000) (src "examples/tests/bad_reuse_page.c:24"))
+(mem-init (id 2) (tid 0) (address 0xaaaac6c47000) (size 0x1000) (src "examples/tests/bad_reuse_page.c:25"))
+(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaac6c45000) (value 0xaaaac6c48000) (src "examples/tests/bad_reuse_page.c:26"))
+(hint (id 4) (tid 0) (kind set_root_lock) (location 0xaaaac6c47000) (value 0xaaaac6c48008) (src "examples/tests/bad_reuse_page.c:27"))
+(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaac6c46000) (value 0xaaaac6c45000) (src "examples/tests/bad_reuse_page.c:28"))
+(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaac6c45000) (value 0xaaaac6c46003) (src "examples/tests/bad_reuse_page.c:29"))
+(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaac6c45000) (src "examples/tests/bad_reuse_page.c:31"))
+(lock (id 8) (tid 0) (address 0xaaaac6c48000) (src "examples/tests/bad_reuse_page.c:33"))
+(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaac6c45000) (value 0x0) (src "examples/tests/bad_reuse_page.c:34"))
+(unlock (id 10) (tid 0) (address 0xaaaac6c48000) (src "examples/tests/bad_reuse_page.c:35"))
+(sysreg-write (id 11) (tid 0) (sysreg vttbr_el2) (value 0x1aaaac6c47000) (src "examples/tests/bad_reuse_page.c:38"))
+(lock (id 12) (tid 0) (address 0xaaaac6c48008) (src "examples/tests/bad_reuse_page.c:39"))
+(mem-write (id 13) (tid 0) (mem-order plain) (address 0xaaaac6c47000) (value 0xaaaac6c46003) (src "examples/tests/bad_reuse_page.c:40"))
 ! double-use pte

examples/expected/bad_switch_wrong_vmid.log

@@ -0,0 +1,7 @@
+(mem-init (id 0) (tid 0) (address 0xaaaab4134000) (size 0x1000) (src "examples/tests/bad_switch_wrong_vmid.c:23"))
+(hint (id 1) (tid 0) (kind set_root_lock) (location 0xaaaab4134000) (value 0xaaaab4135000) (src "examples/tests/bad_switch_wrong_vmid.c:24"))
+(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0xaaaab4134000) (src "examples/tests/bad_switch_wrong_vmid.c:27"))
+(barrier (id 3) (tid 0) dsb (kind ish) (src "examples/tests/bad_switch_wrong_vmid.c:28"))
+(barrier (id 4) (tid 0) isb (src "examples/tests/bad_switch_wrong_vmid.c:29"))
+(sysreg-write (id 5) (tid 0) (sysreg vttbr_el2) (value 0x1aaaab4134000) (src "examples/tests/bad_switch_wrong_vmid.c:32"))
+! root already associated with an (VM/AS)ID

examples/expected/bad_unlocked_write.log

@@ -1,5 +1,5 @@
-(mem-init (id 0) (tid 0) (address 0x55c4e6f25000) (size 0x1000) (src "examples/tests/bad_unlocked_write.c:18"))
-(hint (id 1) (tid 0) (kind set_root_lock) (location 0x55c4e6f25000) (value 0x55c4e6f26000) (src "examples/tests/bad_unlocked_write.c:19"))
-(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0x55c4e6f25000) (src "examples/tests/bad_unlocked_write.c:20"))
-(mem-write (id 3) (tid 0) (mem-order plain) (address 0x55c4e6f25000) (value 0x0) (src "examples/tests/bad_unlocked_write.c:21"))
+(mem-init (id 0) (tid 0) (address 0xaaaad2224000) (size 0x1000) (src "examples/tests/bad_unlocked_write.c:18"))
+(hint (id 1) (tid 0) (kind set_root_lock) (location 0xaaaad2224000) (value 0xaaaad2225000) (src "examples/tests/bad_unlocked_write.c:19"))
+(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0xaaaad2224000) (src "examples/tests/bad_unlocked_write.c:20"))
+(mem-write (id 3) (tid 0) (mem-order plain) (address 0xaaaad2224000) (value 0x0) (src "examples/tests/bad_unlocked_write.c:21"))
 ! must write to pte while holding owner lock