Update the rust toolchain to `nightly-2022-05-03` #1181

celinval · 2022-05-10T03:54:56Z

Description of changes:

Update the rust toolchain to nightly-2022-05-03. There were many issues that had to be fixed to upgrade the toolchain. I split the changes into the following commits:

Fix compilation (usually due to API changes).
Fix handling of Box due to changes in its internal representation (Implement core::ptr::Unique on top of NonNull rust-lang/rust#96010).
Implement new statement kind (Deinit).
Fix discriminant handling. The constant conversion to i64 was panicking and the niche_value conversion was also triggering an overflow error. I disabled the conversion checks for now and simplified the entire logic.

Resolved issues:

Resolves #1162

Call-outs:

This change disables conversion checks. I am open to discussion, but I think this check is too strict and it was rather complicating our codegen logic. I propose to instrument casting later based on user configuration.

Testing:

How is this change tested? Old tests
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.

tedinski

Other than the subtleties of the discriminant change it looks good, should get a second approval from someone on that.

danielsn · 2022-05-10T19:00:21Z

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

-                        wrapping_sub(&niche_val, *niche_start)
-                    };
+
+                    // Compute relative discriminant value (`niche_val - niche_start`).


Is there Rust documentation to point to here?

Nope... I can point to the code where I derived this comment from though.

danielsn · 2022-05-10T19:03:52Z

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

+        // No need to subtract.
+        expr.clone()
+    } else {
+        let unsigned = Type::unsigned_int(expr.typ().width().unwrap());


Make this a helper function on the type?

Also, this will turn ssize_t into uint64_t instead of size_t. It would be nice to handle the CInt types specially here

ok... let me create a helper function in the bindings crate to deal with different types.

danielsn · 2022-05-10T19:05:06Z

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

+                let layout = self.layout_of(dst_mir_ty);
+                if layout.is_zst() || self.ignore_var_ty(dst_mir_ty) {
+                    // We ignore assignment for all zero size types
+                    // Ignore generators too for now:


Why do we need to ignore generators?

Because we don't codegen them and they end up with size 0 despite what their layout says.

BTW, I changed the check to see if the size of the destination is 0, which today will exclude generators. The first check might be redundant now, but I guess it doesn't hurt for now.

danielsn · 2022-05-10T19:05:25Z

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

+                    // We ignore assignment for all zero size types
+                    // Ignore generators too for now:
+                    // https://github.com/model-checking/kani/issues/416
+                    Stmt::skip(Location::none())


No location available?

I can probably fix that. Let me see. I just took this code from the way we handle assignment.

danielsn · 2022-05-10T19:06:26Z

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -1263,7 +1263,7 @@ impl<'tcx> GotocCtx<'tcx> {
            _ => unreachable!(),
        };

-        let rustc_target::abi::Scalar { value: prim_type, .. } = element;
+        let prim_type = element.primitive();


That's cleaner :)

danielsn · 2022-05-10T19:07:15Z

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

 impl<'tcx> GotocCtx<'tcx> {
    /// Dereference a boxed type `std::boxed::Box<T>` to get a `*T`.
    ///
    /// WARNING: This is based on a manual inspection of how boxed types are currently
    /// a) implemented by the rust standard library
    /// b) codegenned by Kani.
    /// If either of those change, this will almost certainly stop working.
-    pub fn deref_box(&self, e: Expr) -> Expr {
+    pub fn deref_box(&self, box_expr: Expr) -> Expr {


Does the comment below need to be updated?

danielsn · 2022-05-10T19:08:43Z

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -102,14 +102,17 @@ impl<'tcx> GotocCtx<'tcx> {
    }
 }

+/// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer).
+const RAW_PTR_FROM_BOX: [&str; 3] = ["0", "pointer", "pointer"];


zhassan-aws · 2022-05-10T19:53:44Z

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

+        expr.clone()
+    } else {
+        let unsigned = Type::unsigned_int(expr.typ().width().unwrap());
+        let constant = Expr::int_constant(constant as i64, unsigned.clone());


Why is there a cast to i64?

this might be leftover from previous attempts... :)

zhassan-aws · 2022-05-10T20:12:11Z

tests/kani/Enum/discriminant_128bits.rs

+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check niche optimization for mix of option, tuple and nonnull.


This comment doesn't seem accurate (don't see a tuple, and nonnull should perhaps be nonzero).

yes, it is outdated

celinval · 2022-05-11T17:04:10Z

@zhassan-aws @danielsn would you like to take a look at the new revision? Cheers!

zhassan-aws · 2022-05-11T17:23:14Z

cprover_bindings/src/goto_program/typ.rs

+    /// Convert type to its unsigned counterpart if possible.
+    /// For types that are already unsigned, this will return self.
+    /// Note: This will expand any typedef.
+    pub fn to_unsigned(&self) -> Option<Self> {


This compiles but regression is failing due to unimplemented statement.

Box<T> now users NonNull<T> instead of raw pointer.

We codegen an assignment to non-det value per documentation. See more information here: - rust-lang/rust#95125

After the merge, the previous wrapping sub logic was triggering a panic due to u128 -> i64 conversion. There were also other overflow issues when trying to convert the `niche_value` to unsigned. For now, I'm disabling the coversion check which I believe is too strict. We should consider implementing a more flexible check later that can be controlled by the user without affecting the internal compiler codegen.

- Improve comments. - Remove wrong cast to i64. - Fix statement location. - Create util function to create unsigned type.

danielsn · 2022-05-11T21:25:57Z

cprover_bindings/src/goto_program/typ.rs

+    pub fn to_unsigned(&self) -> Option<Self> {
+        let concrete = self.unwrap_typedef();
+        match concrete {
+            CInteger(CIntType::SSizeT) => Some(CInteger(CIntType::SizeT)),


Aren't there some other types that could go here too?

I could include Bool which would be a no-op and I could handle CBitField but I noticed that we don't handle that in neither signed() or unsigned() so we should probably add some logic there too. For us to add support to Char we would need access to the machine model. Is there any other type you would like to see?

Let me know what you prefer and I can add that as a follow up PR.

danielsn

I had one comment but it is a minor one.

celinval requested a review from a team as a code owner May 10, 2022 03:54

tedinski approved these changes May 10, 2022

View reviewed changes

danielsn reviewed May 10, 2022

View reviewed changes

zhassan-aws reviewed May 10, 2022

View reviewed changes

zhassan-aws approved these changes May 11, 2022

View reviewed changes

celinval added 5 commits May 11, 2022 14:09

Update rust toolchain to nightly-2022-05-03

1443181

This compiles but regression is failing due to unimplemented statement.

Handle change to Box<T> structure

ddd6005

Box<T> now users NonNull<T> instead of raw pointer.

Handle new statement kind Deinit

b378f72

We codegen an assignment to non-det value per documentation. See more information here: - rust-lang/rust#95125

Address PR comments:

dbec9fc

- Improve comments. - Remove wrong cast to i64. - Fix statement location. - Create util function to create unsigned type.

celinval force-pushed the issue-1162-toolchain branch from 5deac08 to dbec9fc Compare May 11, 2022 21:10

danielsn approved these changes May 11, 2022

View reviewed changes

Merge branch 'main' into issue-1162-toolchain

12cf423

celinval merged commit d0b74ca into model-checking:main May 12, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update the rust toolchain to `nightly-2022-05-03` #1181

Update the rust toolchain to `nightly-2022-05-03` #1181

celinval commented May 10, 2022

tedinski left a comment

danielsn May 10, 2022

celinval May 10, 2022

danielsn May 10, 2022

danielsn May 10, 2022

celinval May 10, 2022

danielsn May 10, 2022

celinval May 10, 2022

celinval May 11, 2022

danielsn May 10, 2022

celinval May 10, 2022

danielsn May 10, 2022

danielsn May 10, 2022

celinval May 10, 2022

danielsn May 10, 2022

zhassan-aws May 10, 2022

celinval May 10, 2022

zhassan-aws May 10, 2022

celinval May 10, 2022

celinval commented May 11, 2022

zhassan-aws May 11, 2022

danielsn May 11, 2022

celinval May 11, 2022

danielsn left a comment

Update the rust toolchain to nightly-2022-05-03 #1181

Update the rust toolchain to nightly-2022-05-03 #1181

Conversation

celinval commented May 10, 2022

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

tedinski 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

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

celinval commented May 11, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danielsn left a comment

Choose a reason for hiding this comment

Update the rust toolchain to `nightly-2022-05-03` #1181

Update the rust toolchain to `nightly-2022-05-03` #1181