[Draft] Combine multiple range checks to handle noncontiguous ranges

[adpaco-aws]

I'd like to get feedback on this incomplete solution for the detection of invalid char values.

As far as I know this is the first time we need to check valid values using noncontiguous ranges. To this end, I've extended the current instrumentation to:

• Special-cased the return value of ty_validity_per_offset to return two ranges when we find a char value. The char value should be valid if it falls within any of these ranges.
• Tweaked the logic in build_limits so that the generated limits check more than one range. In other words, build_limits now accepts multiple reqs and builds a check that essentially does the following:

 req[0].valid_range.contains(value) ||  req[1].valid_range.contains(value) || ... ||  req[N].valid_range.contains(value)

In its current state, the solution is fundamentally wrong because we pass all the ranges to build_limits. However, if we collect all ranges that have the same offset, then passed that to build_limits for each offset value, I think the solution would be correct. That's the code that's missing, and because of that there's one regression failing.

Despite that, this prototype does work as expected on the example

#[kani::proof]
fn transmute_surrogate_ub() {
    unsafe {
        let val: u32 = kani::any();
        kani::assume(val < char::MAX.into());
        let c: char = std::mem::transmute::<u32, char>(val);
        match val {
            0..0xD800 | 0xE000..=0x11FFFF => assert!(char::from_u32(val).is_some()),
            _ => unreachable!(),
        }
    }
}

resulting in this:

SUMMARY:
 ** 1 of 20 failed
Failed Checks: Undefined Behavior: Invalid value of type `char`
 File: "src/main.rs", line 11, in transmute_surrogate_ub

VERIFICATION:- FAILED
Verification Time: 0.27028203s

And if we add kani::assume(!(0xD800..0xE000).contains(&val)); after the other kani::assume(...) instruction, we get a successful result because these checks are also successful:

Check 4: transmute_surrogate_ub.assertion.1
         - Status: SUCCESS
         - Description: "Undefined Behavior: Invalid value of type `char`"
         - Location: src/main.rs:11:23 in function transmute_surrogate_ub

Check 5: transmute_surrogate_ub.assertion.2
         - Status: SUCCESS
         - Description: "assertion failed: char::from_u32(val).is_some()"
         - Location: src/main.rs:13:46 in function transmute_surrogate_ub

Check 6: transmute_surrogate_ub.assertion.3
         - Status: SUCCESS
         - Description: "internal error: entered unreachable code: "
         - Location: src/main.rs:14:18 in function transmute_surrogate_ub

Would this solution be acceptable if we added what's missing?

Resolves #3241

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

@adpaco-aws is it OK if we close this for now since we don't have the bandwidth to iterate over the solution proposed here? Thanks!

[adpaco-aws]

@adpaco-aws is it OK if we close this for now since we don't have the bandwidth to iterate over the solution proposed here? Thanks!

Of course! Here, let me close it.