Adjust PropertyClass of assertions to identify UB

[tautschnig]

Anything listed as undefined behavior (UB) at
https://doc.rust-lang.org/reference/behavior-considered-undefined.html must also be considered UB by Kani and should not pass under should_fail. In preparation of this PR, all occurrences of PropertyClass in the code base were audited and, where necessary, adjusted.

Also, all uses of kani::assert were audited to confirm or adjust them. This resulted in first-time use of the UnsupportedCheck hook, which implied fixes to its implementation.

Resolves: #3571

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

[celinval]

What about value validity, memory initialization? I think they are all still using assertions.

[celinval]

sorry, wrong selection... 😳

[tautschnig]

What about value validity, memory initialization? I think they are all still using assertions.

Given how those were designed, is the only way to fix this to filter for their specific messages? My understanding is that those insert MIR-level assert calls, making them indistinguishable from user-provided assertions. Am I getting this wrong?

[celinval]

What about value validity, memory initialization? I think they are all still using assertions.

Given how those were designed, is the only way to fix this to filter for their specific messages? My understanding is that those insert MIR-level assert calls, making them indistinguishable from user-provided assertions. Am I getting this wrong?

Can we insert calls to kani::safety_check instead of kani::assert here?

I think we can just swap this code to retrieve kani::safety_check instead of kani::assert, but it's worth checking that all users of this code are adding safety properties. Otherwise, we can create a second variant to this enum, which allows instrumentation passes to use different checks.

By looking at this code, it reminded me that we also have an internal function named kani::check. I think that's also intended to check for safety.

[tautschnig]

Can we insert calls to kani::safety_check instead of kani::assert here?

@celinval If time permits, could you take a look at my proposed changes whether they match your expectations?

[carolynzech]

LGTM modulo these nits. Thanks!

Overridden by Carolyn's review per out-of-band communication.