1/* TODO: spec citations per structure */
2
3#include <drivers/iommu/vt_d.h>
4#include <drivers/verifier.h>
5
6#define DV_STRUCT vtd_regs
7dv_size(0xC0);
8dv_align(1);
9dv_field(uint32_t, version, 0x00);
10dv_field(uint32_t, _res0, 0x04);
11dv_field(uint64_t, capabilities, 0x08);
12dv_field(uint64_t, extended_capabilities, 0x10);
13dv_field(uint32_t, global_command, 0x18);
14dv_field(uint32_t, global_status, 0x1C);
15dv_field(uint64_t, root_table_addr, 0x20);
16dv_field(uint64_t, context_command, 0x28);
17dv_field(uint32_t, _res1, 0x30);
18dv_field(uint32_t, fault_status, 0x34);
19dv_field(uint32_t, fault_event_control, 0x38);
20dv_field(uint32_t, fault_event_data, 0x3C);
21dv_field(uint32_t, fault_event_addr, 0x40);
22dv_field(uint32_t, fault_event_addr_upper, 0x44);
23dv_field(uint64_t[2], _res2, 0x48);
24dv_field(uint64_t, advanced_fault_log, 0x58);
25dv_field(uint32_t, _res3, 0x60);
26dv_field(uint32_t, protected_memory_enable, 0x64);
27dv_field(uint32_t, protected_low_mem_base, 0x68);
28dv_field(uint32_t, protected_low_mem_limit, 0x6C);
29dv_field(uint64_t, protected_high_mem_base, 0x70);
30dv_field(uint64_t, protected_high_mem_limit, 0x78);
31dv_field(uint64_t, invalidation_queue_head, 0x80);
32dv_field(uint64_t, invalidation_queue_tail, 0x88);
33dv_field(uint64_t, invalidation_queue_addr, 0x90);
34dv_field(uint32_t, _res4, 0x98);
35dv_field(uint32_t, invalidation_comp_status, 0x9C);
36dv_field(uint32_t, invalidation_event_ctrl, 0xA0);
37dv_field(uint32_t, invalidation_event_data, 0xA4);
38dv_field(uint32_t, invalidation_event_addr, 0xA8);
39dv_field(uint32_t, invalidation_event_addr_upper, 0xAC);
40dv_field(uint64_t, invalidation_queue_error_record, 0xB0);
41dv_field(uint64_t, interrupt_remapping_table_addr, 0xB8);
42#undef DV_STRUCT
43
44#define DV_STRUCT vtd_root_entry
45dv_size(0x10);
46dv_align(1);
47dv_field(uint64_t, lo, 0x00);
48dv_field(uint64_t, hi, 0x08);
49#undef DV_STRUCT
50
51#define DV_STRUCT vtd_context_entry
52dv_size(0x10);
53dv_align(1);
54dv_field(uint64_t, lo, 0x00);
55dv_field(uint64_t, hi, 0x08);
56#undef DV_STRUCT
57
58#define DV_STRUCT vtd_inv_desc
59dv_size(0x10);
60dv_align(1);
61dv_field(uint64_t, lo, 0x00);
62dv_field(uint64_t, hi, 0x08);
63#undef DV_STRUCT
64