Skip to content

Commit

Permalink
(examples) more ASID/VMID examples
Browse files Browse the repository at this point in the history
  • Loading branch information
@bensimner
bensimner committed Feb 4, 2025
1 parent 9bca38a commit 990c567
Show file tree
Hide file tree
Showing 24 changed files with 316 additions and 81 deletions.
5 changes: 5 additions & 0 deletions examples/.gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,3 +24,8 @@
/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
5 changes: 5 additions & 0 deletions examples/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,11 @@ build-objs += bad_race
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)
Expand Down
4 changes: 4 additions & 0 deletions examples/common.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,10 @@ int recv(void);
#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)); \
Expand Down
6 changes: 6 additions & 0 deletions examples/expected/bad_EL2_ASID.log
View file
Original file line number Diff line number Diff line change
@@ -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
28 changes: 14 additions & 14 deletions examples/expected/bad_bbm_by_wrong_VMID.log
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,23 @@
(mem-init (id 0) (tid 0) (address 0xaaaac5764000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:26"))
(mem-init (id 1) (tid 0) (address 0xaaaac5765000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:27"))
(mem-init (id 2) (tid 0) (address 0xaaaac5766000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:28"))
(mem-init (id 3) (tid 0) (address 0xaaaac5767000) (size 0x1000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:29"))
(hint (id 4) (tid 0) (kind set_root_lock) (location 0xaaaac5764000) (value 0xaaaac5768000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:30"))
(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaac5765000) (value 0xaaaac5764000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:31"))
(hint (id 6) (tid 0) (kind set_owner_root) (location 0xaaaac5766000) (value 0xaaaac5764000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:32"))
(mem-write (id 7) (tid 0) (mem-order plain) (address 0xaaaac5764000) (value 0xaaaac5765003) (src "examples/tests/bad_bbm_by_wrong_VMID.c:35"))
(sysreg-write (id 8) (tid 0) (sysreg vttbr_el2) (value 0xaaaac5764000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:38"))
(lock (id 9) (tid 0) (address 0xaaaac5768000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:40"))
(mem-write (id 10) (tid 0) (mem-order plain) (address 0xaaaac5764000) (value 0x0) (src "examples/tests/bad_bbm_by_wrong_VMID.c:41"))
(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 0x1aaaac5767000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:45"))
(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 0xaaaac5764000) (src "examples/tests/bad_bbm_by_wrong_VMID.c:54"))
(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 0xaaaac5764000) (value 0xaaaac5766003) (src "examples/tests/bad_bbm_by_wrong_VMID.c:57"))
(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
22 changes: 11 additions & 11 deletions examples/expected/bad_bbm_missing_tlbi.log
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
(mem-init (id 0) (tid 0) (address 0xaaaab2d74000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:25"))
(mem-init (id 1) (tid 0) (address 0xaaaab2d75000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:26"))
(mem-init (id 2) (tid 0) (address 0xaaaab2d76000) (size 0x1000) (src "examples/tests/bad_bbm_missing_tlbi.c:27"))
(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaab2d74000) (value 0xaaaab2d77000) (src "examples/tests/bad_bbm_missing_tlbi.c:28"))
(hint (id 4) (tid 0) (kind set_owner_root) (location 0xaaaab2d75000) (value 0xaaaab2d74000) (src "examples/tests/bad_bbm_missing_tlbi.c:29"))
(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaab2d76000) (value 0xaaaab2d74000) (src "examples/tests/bad_bbm_missing_tlbi.c:30"))
(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaab2d74000) (value 0xaaaab2d75003) (src "examples/tests/bad_bbm_missing_tlbi.c:33"))
(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaab2d74000) (src "examples/tests/bad_bbm_missing_tlbi.c:36"))
(lock (id 8) (tid 0) (address 0xaaaab2d77000) (src "examples/tests/bad_bbm_missing_tlbi.c:38"))
(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaab2d74000) (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 0xaaaab2d74000) (value 0xaaaab2d76003) (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
6 changes: 3 additions & 3 deletions examples/expected/bad_no_assoc_lock.log
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(mem-init (id 0) (tid 0) (address 0xaaaab0104000) (size 0x1000) (src "examples/tests/bad_no_assoc_lock.c:17"))
(sysreg-write (id 1) (tid 0) (sysreg vttbr_el2) (value 0xaaaab0104000) (src "examples/tests/bad_no_assoc_lock.c:18"))
(mem-write (id 2) (tid 0) (mem-order plain) (address 0xaaaab0104000) (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
16 changes: 8 additions & 8 deletions examples/expected/bad_no_bbm.log
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
(mem-init (id 0) (tid 0) (address 0xaaaad4944000) (size 0x1000) (src "examples/tests/bad_no_bbm.c:24"))
(mem-init (id 1) (tid 0) (address 0xaaaad4945000) (size 0x1000) (src "examples/tests/bad_no_bbm.c:25"))
(hint (id 2) (tid 0) (kind set_root_lock) (location 0xaaaad4944000) (value 0xaaaad4946000) (src "examples/tests/bad_no_bbm.c:26"))
(hint (id 3) (tid 0) (kind set_owner_root) (location 0xaaaad4945000) (value 0xaaaad4944000) (src "examples/tests/bad_no_bbm.c:27"))
(mem-write (id 4) (tid 0) (mem-order plain) (address 0xaaaad4944000) (value 0xaaaad4945003) (src "examples/tests/bad_no_bbm.c:30"))
(sysreg-write (id 5) (tid 0) (sysreg vttbr_el2) (value 0xaaaad4944000) (src "examples/tests/bad_no_bbm.c:33"))
(lock (id 6) (tid 0) (address 0xaaaad4946000) (src "examples/tests/bad_no_bbm.c:35"))
(mem-write (id 7) (tid 0) (mem-order plain) (address 0xaaaad4944000) (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
11 changes: 11 additions & 0 deletions examples/expected/bad_no_bbm_stage1.log
View file
Original file line number Diff line number Diff line change
@@ -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
9 changes: 9 additions & 0 deletions examples/expected/bad_overlap_ASID.log
View file
Original file line number Diff line number Diff line change
@@ -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
9 changes: 9 additions & 0 deletions examples/expected/bad_overlap_VMID.log
View file
Original file line number Diff line number Diff line change
@@ -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
8 changes: 4 additions & 4 deletions examples/expected/bad_race.log
View file
Original file line number Diff line number Diff line change
@@ -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
8 changes: 4 additions & 4 deletions examples/expected/bad_switch_wrong_vmid.log
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(mem-init (id 0) (tid 0) (address 0xaaaab3b24000) (size 0x1000) (src "examples/tests/bad_switch_wrong_vmid.c:23"))
(hint (id 1) (tid 0) (kind set_root_lock) (location 0xaaaab3b24000) (value 0xaaaab3b25000) (src "examples/tests/bad_switch_wrong_vmid.c:24"))
(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0xaaaab3b24000) (src "examples/tests/bad_switch_wrong_vmid.c:27"))
(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 0x1aaaab3b24000) (src "examples/tests/bad_switch_wrong_vmid.c:32"))
(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
8 changes: 4 additions & 4 deletions examples/expected/bad_unlocked_write.log
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(mem-init (id 0) (tid 0) (address 0xaaaae4e94000) (size 0x1000) (src "examples/tests/bad_unlocked_write.c:18"))
(hint (id 1) (tid 0) (kind set_root_lock) (location 0xaaaae4e94000) (value 0xaaaae4e95000) (src "examples/tests/bad_unlocked_write.c:19"))
(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0xaaaae4e94000) (src "examples/tests/bad_unlocked_write.c:20"))
(mem-write (id 3) (tid 0) (mem-order plain) (address 0xaaaae4e94000) (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
Loading

0 comments on commit 990c567

Please sign in to comment.