Compiler intrinsics

[danielsn]

Rust has hundreds of compiler intrinsics. Unlike most other MIR features, which are represented in the IR using enum types, Rust intrinsics are identified using strings. This makes it difficult to know if we support all required Rust intrinsics.

Also, some instrinsics have complicated semantics, which is not always well documented. It is possible that implementations for these intrinsics may not correctly represent the Rust semantics.

Likelihood:

RMC currently only supports a small fraction of Rust intrinsics.

Mitigation:

• Raise a warning if RMC encounters code which uses unsupported intrinsics

Path to soundness:

Either document as as not supported, or add support.

Documentation:

[celinval]

@adpaco-aws, do you think we can close this issue? I believe we implement unsupported construct for any intrinsic that we don't support, right?

[adpaco-aws]

@adpaco-aws, do you think we can close this issue? I believe we implement unsupported construct for any intrinsic that we don't support, right?

Yes, it works the same way as with any other unsupported feature: If an unsupported intrinsic is within the reachable code for verification, it will raise a failure.

In addition to this mechanism, we also have documentation reflecting the current status for each intrinsic.

Currently, we support a significant amount of compiler intrinsics (see #727, #1163, and #1148 for an up-to-date status). The models for these intrinsics go through a code review process which guarantees they are as accurate as possible. The same process is followed to add support for new intrinsics. Therefore, I don't think we need to keep this issue open.