Correctly handle `assert_*` intrinsics #742

adpaco-aws · 2022-01-11T22:44:12Z

Description of changes:

Adds support for the assert_uninit and assert_zero intrinsics. Inserts the code for them and assert_inhabited into a single function.

Resolved issues:

Resolves #6
Resolves #7

Call-outs:

All backends check the condition for assert_inhabited first, then proceed to do the other ones. This proposal follows the same pattern.
The actual error for assert_inhabited (i.e., in src/test/rmc/Intrinsics/Assert/inhabited_panic.rs) is

[main.assertion.1] line 13 a panicking function std::mem::MaybeUninit::<T>::assume_init is invoked: FAILURE

This is due to the Nevers hook being applied instead of the Intrinsics one. I have tried doing some changes to the application condition (for example, return false if the instance is an intrinsic) to no success (ended up in some code that expected the Nevers hook to have applied).

Some reorganization in tests. The top level folder Assert now contains the multiple assertions test only, and another Assert folder has been created within Intrinsics to keep the tests related to the intrinsics in this PR.

Testing:

How is this change tested? Existing regression + 3 new tests + 1 removed test.
Is this a refactor change? No.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

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

adpaco-aws · 2022-01-12T14:15:23Z

@zhassan-aws brought #648 to my attention, thanks!!

Removing/Changing output_of_instance_is_never seems the way to go, but it appears that our backend relies on it in a few places so I do not think it will be trivial. I could create a tracking issue for the inhabited.rs test and come back to check once the change has taken place.

danielsn

The tests I see are for primitive types. Would it make sense to also ensure that we do the right thing for enums and structs?

danielsn · 2022-01-12T20:43:31Z

src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

@@ -567,6 +548,48 @@ impl<'tcx> GotocCtx<'tcx> {
        )
    }

+    /// Generates either a panic or no-op for `assert_*` intrinsics.
+    /// These are intrinsics that statically compile to panics if the type
+    /// layout is invalid so we get a message that mentions the offending type.


Reference to rust documentation here?

Added links to rust docs.

danielsn · 2022-01-12T20:50:41Z

src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

+            );
+        }
+
+        if intrinsic == "assert_uninit_valid" && !layout.might_permit_raw_init(self, false) {


Is there a spec we can point to here?

I was not able to find one as documentation regarding these intrinsics is quite hard to find.

The closest thing I could find is the actual implementation in rustc_codegen_ssa/src/mir/block.rs (codegen_panic_intrinsic) in addition to PR discussions. But if you know of one I will be happy to add it here.

FWIW, I think links directly to code serve as a reasonable reference, too. Maybe add that as a comment? (e.g. link directly to it on github?)

My main concern with that is that links to rustc code may become outdated pretty quickly. But even that is better that no links, so just added a note here linking to that function.

danielsn · 2022-01-12T20:50:44Z

src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

+
+        // Then we check if the type allows "raw" initialization for the cases
+        // where memory is zero-initialized or entirely uninitialized
+        if intrinsic == "assert_zero_valid" && !layout.might_permit_raw_init(self, true) {


Is there a spec we can point to here?

danielsn · 2022-01-12T20:51:22Z

src/test/rmc/Intrinsics/Assert/inhabited_panic.rs

+// The code below attempts to instantiate uninhabited type `!`.
+// This should cause the intrinsic `assert_inhabited` to generate a panic during
+// compilation, but at present it triggers the `Nevers` hook instead.


Do we have a tracking issue for this?

Created #751 which I linked here.

danielsn · 2022-01-12T20:52:33Z

src/test/rmc/Intrinsics/Assert/zero_valid_panic.rs

+
+// The code below attempts to zero-initialize type `&i32`, causing the intrinsic
+// `assert_zero_valid` to generate a panic during compilation.
+fn main() {


Should we also have a test with an expected pass (e.g. zero initializing a u8)?

The test in src/test/rmc/Intrinsics/Assert/zero_valid.rs (path updated in this PR) already does this for several types, including a user-defined struct.

tedinski · 2022-01-18T21:25:43Z

src/rmc-compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

+            );
+        }
+
+        if intrinsic == "assert_uninit_valid" && !layout.might_permit_raw_init(self, false) {


FWIW, I think links directly to code serve as a reasonable reference, too. Maybe add that as a comment? (e.g. link directly to it on github?)

adpaco-aws requested a review from a team as a code owner January 11, 2022 22:44

danielsn reviewed Jan 12, 2022

View reviewed changes

adpaco-aws mentioned this pull request Jan 13, 2022

Panic for assert_inhabited has no effect because of Nevers hook #751

Closed

tedinski approved these changes Jan 18, 2022

View reviewed changes

adpaco-aws force-pushed the assert-intrinsics branch from 5cc5515 to e20525f Compare January 18, 2022 22:32

Correctly handle assert_* intrinsics

797ecc3

adpaco-aws force-pushed the assert-intrinsics branch from e20525f to 797ecc3 Compare January 18, 2022 22:37

adpaco-aws merged commit b1396f2 into model-checking:main Jan 19, 2022

adpaco-aws mentioned this pull request Jan 19, 2022

Intrinsics Audit #727

Closed

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 22, 2022

Correctly handle assert_* intrinsics (model-checking#742)

53bc0e7

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 25, 2022

Correctly handle assert_* intrinsics (model-checking#742)

32380f9

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Correctly handle assert_* intrinsics (model-checking#742)

f8fe8c8

tedinski pushed a commit that referenced this pull request Apr 27, 2022

Correctly handle assert_* intrinsics (#742)

36e7d82

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Correctly handle `assert_*` intrinsics #742

Correctly handle `assert_*` intrinsics #742

adpaco-aws commented Jan 11, 2022

adpaco-aws commented Jan 12, 2022

danielsn left a comment

danielsn Jan 12, 2022

adpaco-aws Jan 13, 2022

danielsn Jan 12, 2022

adpaco-aws Jan 13, 2022

tedinski Jan 18, 2022

adpaco-aws Jan 18, 2022

danielsn Jan 12, 2022

adpaco-aws Jan 13, 2022

danielsn Jan 12, 2022

adpaco-aws Jan 13, 2022

danielsn Jan 12, 2022

adpaco-aws Jan 13, 2022

tedinski Jan 18, 2022

Correctly handle assert_* intrinsics #742

Correctly handle assert_* intrinsics #742

Conversation

adpaco-aws commented Jan 11, 2022

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

adpaco-aws commented Jan 12, 2022

danielsn left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Correctly handle `assert_*` intrinsics #742

Correctly handle `assert_*` intrinsics #742