lib: sbi: Refresh the root memregion count after sanitize_domain()

[zeldovich]

Summary

This bug was found in the process of formally verifying the correctness of OpenSBI on top of the Sail RISC-V semantics using Lean.

root_add_memregion() computes root_memregs_count once, then loops sanitize_domain() + merge. sanitize_domain() can remove regions (any region covered by a superset region is dropped and the array shifted down), but the local count is never refreshed, so the merge step's sbi_memmove(nreg1, nreg1 + 1, sizeof(*nreg1) * (root_memregs_count - i1)) moves more entries than exist and runs past the array's terminating entry. Today this stays inside the allocation only because the array is allocated with ROOT_REGION_MAX + 1 slots and the stale count is bounded by ROOT_REGION_MAX. Recompute the count after each sanitize_domain().

An execution that triggers it

struct sbi_domain_memregion is 24 bytes (order, base, flags); the root array has 33 slots (sbi_calloc(…, ROOT_REGION_MAX + 1)), the last one the all-zero terminator (order == 0).

1. During sbi_domain_init() and the driver cold-inits, regions are added one at a time through sbi_domain_root_add_memregion(). Suppose N regions are registered so far (the virt platform registers 7 by the end of boot: firmware RW/RX, UART, CLINT MSWI, CLINT MTIMER, PLIC in two pieces, the all-RAM catch-all; N grows to 7).
2. A caller adds a region R that strictly covers an existing region S (same flags, S inside R). The ACLINT driver does this on virt: it registers the MSWI window 0x2000000/0x4000 and the MTIMER window 0x2004000/0xc000 separately, and sanitize_domain() merges them when a covering 2^16 CLINT region appears. On entry root_memregs_count = N (say 7) and root.regions[7] is the terminator.
3. root_add_memregion() appends R at index 7, increments the local count to 8 and writes the terminator at index 8.
4. sanitize_domain() sorts, then finds S covered by R and removes it: sbi_memmove(&regions[i], &regions[i+1], 24 * (count - i)) with its OWN recomputed count, shifting the tail (including the terminator) down by one. The array now holds 7 live regions and the terminator at index 7. root_add_memregion()'s local root_memregs_count is still 8.
5. The merge loop (sbi_domain_for_each_memregion, which stops at the terminator) finds two adjacent same-order same-flag regions at indices i1 - 1 and i1 and merges them: nreg->order++, then sbi_memmove(nreg1, nreg1 + 1, 24 * (root_memregs_count - i1)). With the stale 8 this copies 8 - i1 entries starting at index i1 + 1, i.e. up to and including index 8, while the live data plus terminator end at index 7. It reads one entry beyond the terminator (index 8, inside the 33-slot allocation, all zero after calloc) and writes it over index 7.
6. Result: nothing visibly wrong today, because the over-read lands on a zeroed slot inside the allocation and copying zeros over the terminator's position leaves a terminator there. Every extra removal widens the gap by one slot. Two conditions turn it into a real fault: (a) 32 registered regions, where index 32 is the terminator and the over-read reaches index 33, past the sbi_calloc block, pulling heap-neighbour bytes into the region table (a non-zero order there extends the table with a bogus region that lands in the PMP configuration of every hart); (b) a change that drops + 1 from the allocation or reuses the slot, which the current code silently depends on.

The fix recomputes the count from the array (sbi_domain_used_memregions) after every successful sanitize_domain() so the memmove covers exactly the remaining regions plus the terminator.

Verification

Proved: sbi_domain_root_add_memrange() on the virt platform's region sequence satisfies its contract against a model of the region array. The proof had to carry the out-of-range tail bytes explicitly to go through on the unfixed code; with the fix the memmove's range is the live array.