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

[Jan Beulich <jbeulich@xxxxxxxx>]

On 06.10.2026 15:06, Weiqi Wang wrote:
> 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>

Reviewed-by: Jan Beulich <jbeulich@xxxxxxxx>
with ...

> --- 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",

... this format string placed normally. We don't mind format strings going
past 80 columns. Possibly the word "region" could also be omitted. (Surely
this adjustment can be done while committing; no need to submit v4 just
for this.)

Jan