[seL4] intel-vtd.c::vtd_get_n_paging looks so suspicious

9 Mar 2020

      Hello all,

kernel/src/plat/pc99/machine/intel-vtd.c::vtd_get_n_paging() confused me a
lot. Wish to get any help.

This func intends to calculate paging pages needed for all RMRRs. The
following code 'filter the identical regions by pci bus id', and use them to
figure out the final result.
```
    for (word_t i = 1; i < rmrr_list->num; i++) {
        if (vtd_get_root_index(rmrr_list->entries[i].device) !=
            vtd_get_root_index(filtered.entries[filtered.num - 1].device) &&
            rmrr_list->entries[i].base != filtered.entries[filtered.num - 1].base &&
            rmrr_list->entries[i].limit != filtered.entries[filtered.num - 1].limit) {
            filtered.entries[filtered.num] = rmrr_list->entries[i];
            filtered.num++;
        }
    }
```
But vtd_map_reserved_page() says, every different devices(with diff bus-dev-
func ID) have their own paging structures. Then why do filter here like this
, yet the logic looks so confusing.

And on line 313, it counts pages according to the specified level address
bits.
```
                size += get_n_paging(region, 32 - (VTD_PT_INDEX_BITS * i + seL4_PageBits));
```
So what does 32 mean? Maybe a typo?

Thanks,
laokz