Tracking issue: common unsupported features

[tedinski]

Our current top-100 data set for unsupported features looks like this:

Assessed 82 successfully, with 18 failures.
======================================================
 Unsupported feature           |   Crates | Instances 
                               | impacted |    of use 
-------------------------------+----------+-----------
 caller_location               |       75 |       218 
 simd_bitmask                  |       33 |       111 
 try                           |       26 |       667 
 Projection mismatch           |       20 |        38 
 TerminatorKind::InlineAsm     |        8 |        19 
 PointerCast::ClosureFnPointer |        6 |        31 
 'sqrtf64' intrinsic           |        2 |         2 
 float_to_int_unchecked        |        1 |        24 
 'expf64' intrinsic            |        1 |         1 
 'fmaf32' intrinsic            |        1 |         1 
 'fmaf64' intrinsic            |        1 |         1 
 'log10f32' intrinsic          |        1 |         1 
 'log10f64' intrinsic          |        1 |         1 
 'log2f32' intrinsic           |        1 |         1 
 'log2f64' intrinsic           |        1 |         1 
 'logf64' intrinsic            |        1 |         1 
 'powf64' intrinsic            |        1 |         1 
 'powif32' intrinsic           |        1 |         1 
======================================================

From analyzing some other "real-world" data sets, we see similar data:

======================================================
 Unsupported feature           |   Crates | Instances 
                               | impacted |    of use 
-------------------------------+----------+-----------
 caller_location               |       48 |        58 
 simd_bitmask                  |       24 |        35 
 try                           |       14 |        75 
 Projection mismatch           |       11 |        11 
 TerminatorKind::InlineAsm     |        4 |         7 
 PointerCast::ClosureFnPointer |        2 |        85 
======================================================

This is a tracking issue for the top issues we see above.

caller_location

• Handle new caller_location intrinsic the right way #374
• Warning about unsupported caller_location intrinsic #2010
• This intrinsic may be part of the "bloat" that we're seeing with Investigate assess performance regression with MIR linker #1828. From PR2032: "This macro ends up calling panic!, which calls panic_fmt, which calls std::panic::Location::caller which in turn calls std::intrinsics::caller_location."
• Other than the performance issue, this is likely a low priority: there isn't likely a lot of code we actually want to verify that needs it. It appears common, but for reasons related to e.g. panic macros.

simd_bitmask

• Add support to simd_bitmask intrinsic #2131
• Appears commonly used, but we haven't investigated if it's impacting customers... yet.

try

• Unimplemented: catch_unwind intrinsic #267
• Add support to stack unwind panic strategy #692
• Not yet clear if it's impacting customers, it's prevalence may be the result of test code.

Projection mismatch

• Not clear there's one issue here
• Invalid projection on firecracker regression with the 2022-11-20 rust toolchain #1926
• Handle Variant check in projection assertion #448

TerminatorKind::InlineAsm

• Something of a research project, but cheap hacks (e.g. only supporting a few common instructions) might be hugely beneficial.
• Add support for inline ASM #2

PointerCast::ClosureFnPointer

• PointerCast::ClosureFnPointer is unimplemented #274

[tedinski]

A short summary of these top-6 features:

1. ClousreFnPointer should be supported in the next release.
2. InlineAsm and try will not be supported soon: both require pretty extensive work.
3. simd_bitmask should be relatively easy to support, as soon as we know customers are actually hitting it, we'd prioritize it quickly.
4. "Projection mismatch" may be more than one issue, and we'll need to investigate them more to decide what to do. If you have a proof harness hitting this, please let us know.
5. caller_location is unlikely to have any impact.

[celinval]

I did some digging and I have a feeling that the projection mismatch and the simd_bitmask likely have the same cause. I believe they are both triggered by str::contains. I'll post more information in the related issues (#1926).

[celinval]

On a different note, the issue #448 is not related to any of the projection mismatch that we are seeing. This issue is in fact asking to add a new check that could potentially detect further projection mismatch.