[PATCH v3 2/2] xen/pdx: reject regions crossing a lookup table index

[Weiqi Wang <coolhaoyt@xxxxxxxxx>]

From: Weiqi Wang <weiqi.wang-2@xxxxxxxxxxxxxxxxxxxxxxxxx>

pdx_is_region_compressible() only looks up the table entry of the first
page, and checks the region against [pfn_base, pfn_base +
pdx_region_size).  pfn_base need not be aligned to the table index
granularity, so that window can extend into the next index, which belongs
to a different range with a different offset.  A region whose tail lies
there is reported compressible, yet its last page on its own is not, and
translates through the wrong offset.

Require the first and last page of the region to use the same table
index.

This can be reached from the coverage check in srat_parse_regions() when an
e820 RAM range is not covered by the SRAT ranges, which is the case that
check is meant to catch.

Add a test case that fails without this change.

Found with the ESBMC bounded model checker, and confirmed by running the
failing case natively against the unmodified code.

Fixes: c5c45bcbd6a1 ("pdx: introduce a new compression algorithm based on 
region offsets")
Assisted-by: Claude Code:claude-opus-5-5 # finding the issue with ESBMC, patch 
creation
Signed-off-by: Weiqi Wang <weiqi.wang-2@xxxxxxxxxxxxxxxxxxxxxxxxx>
---

Notes:
    Changes in v3:
    - reword the second paragraph to start with "Require" (Roger)
    - reword the ESBMC line so it no longer names a counterexample that is
      not part of the commit log (Roger)
    - add the reproduction as a test case in tools/tests/pdx (Roger)
    
    Changes in v2:
    - the issue is not tied to huge addresses (Jan): replaced the example
      with a ~5 GB reproduction and dropped the 2^51 remark
    
    This was discussed when the offset compression was reviewed.  In the v2
    thread [1] Jan asked whether pdx_is_region_compressible() is correct when
    a region crosses a lookup table slot boundary.  The thread concluded it
    was not an issue, on the basis that pages contiguous in MFN space are also
    contiguous in PDX space.  The case below is one where that does not hold
    for the code as merged: the region is reported compressible, its last page
    on its own is not, and that page round-trips to a different PFN.
    
    The ranges are as srat_parse_regions() would see them.  The RAM range is
    not covered by either SRAT range, which is the situation the coverage
    check in srat_parse_regions() is meant to detect.  On staging plus the
    first patch of this series, before this patch:
    
      region [0x4ca9b, 0x12982e) compressible: 1
      last page: pfn 0x12982d -> pdx 0xa982d -> pfn 0xe982d
    
    With this patch the region is reported not compressible, and
    srat_parse_regions() disables compression.  The test case added here is
    this same ~5 GB layout, checked through pdx_is_region_compressible()
    directly; it fails before the change and passes after.  The existing
    tests in tools/tests/pdx continue to pass in both mask and offset mode.
    
    Other callers that rely on the same answer are mem_hotadd_check() and the
    EFI ram_range_valid() check.  I have not run those paths.
    
    One behavioural change to check: with npages == 0 the new condition
    compares against pfn - 1.  The callers I looked at never pass 0.
    
    Model checking (ESBMC, 2 SRAT ranges and 2 e820 RAM ranges, all free
    within a bounded address range, the srat_parse_regions() coverage check
    modelled) finds no accepted RAM page that fails to round-trip with both
    patches applied.  It also finds no layout where the coverage check now
    rejects what setup accepted, with RAM equal to the SRAT ranges.  This is
    bounded to 2 ranges.
    
    [1] 
https://www.mail-archive.com/xen-devel@xxxxxxxxxxxxxxxxxxxx/msg194095.html

 tools/tests/pdx/test-pdx.c | 33 +++++++++++++++++++++++++++++++++
 xen/common/pdx.c           |  3 ++-
 2 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/tools/tests/pdx/test-pdx.c b/tools/tests/pdx/test-pdx.c
index 6728ffc7a5..10c659b775 100644
--- a/tools/tests/pdx/test-pdx.c
+++ b/tools/tests/pdx/test-pdx.c
@@ -288,6 +288,39 @@ int main(int argc, char **argv)
         }
     }
 
+#ifdef CONFIG_PDX_OFFSET_COMPRESSION
+    /*
+     * srat_parse_regions() passes e820 RAM ranges to
+     * pdx_is_region_compressible(), and these can be wider than any single
+     * SRAT range.  A region must be rejected when its first and last page
+     * resolve through different lookup table indices, even if it fits within
+     * pdx_region_size.  The values are PFNs from a ~5 GiB layout.
+     */
+    {
+        unsigned long ram_start = 0x4ca9bUL, ram_end = 0x12982eUL;
+
+        pfn_pdx_compression_reset();
+        pfn_pdx_add_region(pfn_to_paddr(0x5bbd3UL),
+                           pfn_to_paddr(0xf18f2UL - 0x5bbd3UL));
+        pfn_pdx_add_region(pfn_to_paddr(0x1869bdUL),
+                           pfn_to_paddr(0x189f58UL - 0x1869bdUL));
+
+        if ( !pfn_pdx_compression_setup(0) )
+        {
+            printf("table-index crossing test: compression disabled\n");
+            ret_code = EXIT_FAILURE;
+        }
+        else if ( pdx_is_region_compressible(pfn_to_paddr(ram_start),
+                                             ram_end - ram_start) )
+        {
+            printf(
+    "region [%#lx, %#lx) crosses a table index but was accepted\n",
+                   ram_start, ram_end);
+            ret_code = EXIT_FAILURE;
+        }
+    }
+#endif
+
     return ret_code;
 }
 
diff --git a/xen/common/pdx.c b/xen/common/pdx.c
index 23655ef3bd..52928faa15 100644
--- a/xen/common/pdx.c
+++ b/xen/common/pdx.c
@@ -324,7 +324,8 @@ bool pdx_is_region_compressible(paddr_t base, unsigned long 
npages)
     unsigned long pfn_base = pfn_bases[PFN_TBL_IDX(pfn)];
 
     return pfn >= pfn_base &&
-           pfn + npages <= pfn_base + pdx_region_size;
+           pfn + npages <= pfn_base + pdx_region_size &&
+           PFN_TBL_IDX(pfn) == PFN_TBL_IDX(pfn + npages - 1);
 }
 
 static int __init cf_check cmp_node(const void *a, const void *b)
-- 
2.34.1