Skip to content

Commit ac0a878

Browse files
Kswin01Kswin01
committed
domains: add sdf tests
Signed-off-by: Krishnan Winter <krishnan.winter@unsw.edu.au>
1 parent 8b3b6e6 commit ac0a878

13 files changed

Lines changed: 350 additions & 8 deletions

‎tool/microkit/src/sdf.rs‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -619,7 +619,7 @@ impl ProtectionDomain {
619619
if config.num_domain_schedules > 1 {
620620
return Err(format!("Protection domain {name} specifies a domain {domain} but system does not specify a domain schedule"));
621621
} else {
622-
return Err("Assigning PDs to domains is only supported built with a config that supports domains".to_string());
622+
return Err("Assigning PDs to domains is only supported when built with a config that supports domains".to_string());
623623
}
624624
}
625625
(_, _) => {}
@@ -1148,11 +1148,16 @@ impl DomainSchedule {
11481148
let child_name = child.tag_name().name();
11491149
match child_name {
11501150
"domain" => {
1151-
if schedule.len() == config.num_domain_schedules as usize {
1151+
if schedule.len() >= config.num_domain_schedules as usize {
11521152
return Err(format!(
1153-
"Error: length of domain schedule exceeds maximum of {}: {}",
1153+
"Error: length of domain schedule exceeds maximum of {}",
11541154
config.num_domain_schedules as usize,
1155-
loc_string(xml_sdf, pos)
1155+
));
1156+
}
1157+
if domain_ids.len() >= config.num_domains as usize {
1158+
return Err(format!(
1159+
"Error: number of domains exceeds maximum of {}",
1160+
config.num_domains as usize,
11561161
));
11571162
}
11581163

@@ -1161,9 +1166,8 @@ impl DomainSchedule {
11611166
let length = checked_lookup(xml_sdf, &child, "length")?.parse::<u64>();
11621167
if length.is_err() {
11631168
return Err(format!(
1164-
"Error: invalid domain timeslice length '{}': {}",
1169+
"Error: invalid domain timeslice for domain: {}",
11651170
name,
1166-
loc_string(xml_sdf, pos)
11671171
));
11681172
}
11691173

‎tool/microkit/tests/sdf/domain_assign_pd_to_invalid_domain.system‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="1000000" />
10+
</domain_schedule>
11+
12+
<protection_domain name="test1" domain="domain_2">
13+
<program_image path="test" />
14+
</protection_domain>
15+
</system>

‎tool/microkit/tests/sdf/domain_duplicate_index_shift.system‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="1000000" />
10+
<domain name="domain_2" length="1000000" />
11+
<domain_idx_shift shift="1" />
12+
<domain_idx_shift shift="2" />
13+
</domain_schedule>
14+
15+
<protection_domain name="test1" domain="domain_1">
16+
<program_image path="test" />
17+
</protection_domain>
18+
</system>

‎tool/microkit/tests/sdf/domain_duplicate_start_index.system‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="1000000" />
10+
<domain name="domain_2" length="1000000" />
11+
<domain_start index="1" />
12+
<domain_start index="2" />
13+
</domain_schedule>
14+
15+
<protection_domain name="test1" domain="domain_1">
16+
<program_image path="test" />
17+
</protection_domain>
18+
</system>

‎tool/microkit/tests/sdf/domain_exceed_max_domains.system‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="1000000" />
10+
<domain name="domain_2" length="1000000" />
11+
<domain name="domain_3" length="1000000" />
12+
<domain name="domain_4" length="1000000" />
13+
<domain name="domain_5" length="1000000" />
14+
<domain name="domain_6" length="1000000" />
15+
<domain name="domain_7" length="1000000" />
16+
<domain name="domain_8" length="1000000" />
17+
<domain name="domain_9" length="1000000" />
18+
<domain name="domain_10" length="1000000" />
19+
<domain name="domain_12" length="1000000" />
20+
<domain name="domain_13" length="1000000" />
21+
<domain name="domain_14" length="1000000" />
22+
<domain name="domain_15" length="1000000" />
23+
<domain name="domain_16" length="1000000" />
24+
<domain name="domain_17" length="1000000" />
25+
<domain name="domain_18" length="1000000" />
26+
<domain name="domain_19" length="1000000" />
27+
<domain name="domain_20" length="1000000" />
28+
<domain name="domain_22" length="1000000" />
29+
<domain name="domain_23" length="1000000" />
30+
<domain name="domain_24" length="1000000" />
31+
<domain name="domain_25" length="1000000" />
32+
<domain name="domain_26" length="1000000" />
33+
<domain name="domain_27" length="1000000" />
34+
<domain name="domain_28" length="1000000" />
35+
<domain name="domain_29" length="1000000" />
36+
<domain name="domain_30" length="1000000" />
37+
<domain name="domain_32" length="1000000" />
38+
<domain name="domain_33" length="1000000" />
39+
<domain name="domain_34" length="1000000" />
40+
<domain name="domain_35" length="1000000" />
41+
<domain name="domain_36" length="1000000" />
42+
<domain name="domain_37" length="1000000" />
43+
<domain name="domain_38" length="1000000" />
44+
<domain name="domain_39" length="1000000" />
45+
</domain_schedule>
46+
47+
<protection_domain name="test1" domain="domain_1">
48+
<program_image path="test" />
49+
</protection_domain>
50+
</system>

‎tool/microkit/tests/sdf/domain_invalid_shift.system‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="1000000" />
10+
<domain_idx_shift shift="zz" />
11+
</domain_schedule>
12+
13+
<protection_domain name="test1" domain="domain_1">
14+
<program_image path="test" />
15+
</protection_domain>
16+
</system>

‎tool/microkit/tests/sdf/domain_invalid_start_index.system‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="1000000" />
10+
<domain_start index="zz" />
11+
</domain_schedule>
12+
13+
<protection_domain name="test1" domain="domain_1">
14+
<program_image path="test" />
15+
</protection_domain>
16+
</system>

‎tool/microkit/tests/sdf/domain_invalid_timeslice.system‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="zz" />
10+
</domain_schedule>
11+
12+
<protection_domain name="test1" domain="domain_1">
13+
<program_image path="test" />
14+
</protection_domain>
15+
</system>

‎tool/microkit/tests/sdf/domain_no_schedule.system‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<protection_domain name="test1" domain="domain_1">
9+
<program_image path="test" />
10+
</protection_domain>
11+
</system>

‎tool/microkit/tests/sdf/domain_out_of_bounds_shift.system‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!--
3+
Copyright 2026, UNSW.
4+
5+
SPDX-License-Identifier: BSD-2-Clause
6+
-->
7+
<system>
8+
<domain_schedule>
9+
<domain name="domain_1" length="1000000" />
10+
<domain_idx_shift shift="1000" />
11+
</domain_schedule>
12+
13+
<protection_domain name="test1" domain="domain_1">
14+
<program_image path="test" />
15+
</protection_domain>
16+
</system>

0 commit comments

Comments
 (0)