[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.