Sun Jian <[email protected]> writes: > verifier_bounds.c already has 64-bit cross-sign-boundary bounds > deduction coverage. > > Recent 32-bit signed/unsigned intersection tests extended the refinement > coverage, but a corresponding negative case is still missing. > > Add a 32-bit selftest for that case and assert that the program is > rejected, confirming that verifier remains conservative there.
The "recent 32-bit signed/unsigned intersection tests" are Eduard's signed_unsigned_intersection32_case1/case2 (commit f81fdfd16771), which cover the two refinement branches added to deduce_bounds_32_from_32() in commit fbc7aef517d8. Your test claims to be a "negative case" for the two-overlap scenario where the verifier can't refine bounds. But tracing through the code, that's not what happens. After the two w0 conditionals you have u32=[0x80, 0xffffff80] and s32=[-128, 127]. In deduce_bounds_32_from_32(): - (u32)s32_min_value <= (u32)s32_max_value (0xffffff80 <= 0x7f) is false, so we enter the else branch - u32_max < (u32)s32_min (0xffffff80 < 0xffffff80) is false, skip - (u32)s32_max < u32_min (0x7f < 0x80) is true - the single-overlap else if fires, successfully narrowing the register to the constant 0xffffff80 So this isn't a "two overlaps / no refinement" case at all. The verifier resolves the value completely. This is the same else if branch that signed_unsigned_intersection32_case1 already exercises (with u32=[3, U32_MAX], s32=[S32_MIN, 1], where (u32)1 < 3 fires the same path). No new coverage is added.
