Add option to enable layout randomization

[giltho]

Description of changes:

Randomize layouts by default, but adds a flag to disable that feature.

Resolved issues:

Resolves #1622 (if accepted)

Call-outs:

None that I know of

Testing:

Regression test suite seems to still be working The feature itself is kind of untestable. I could write a test that depends on the current rustc layout procedure and check that it passes with the flag but doesn't without it (and that's how I tested the change locally). However, that test could break on any sync with rustc

Checklist

• [x] Each commit message has a non-empty body, explaining why the change was made
• [x] Methods or procedures are documented
• [x] Regression or unit tests are included, or existing tests cover the modified code
• [x] 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.

[danielsn]

On the one hand, I want a test, on the other hand, its randomization and so would fail sometimes.

Anyone got a suggestion?

Have n copies of the struct, transmute between them, and check that the value never changes. Should fail with prob -> 100%

[danielsn]

// Or use macros to make this cleaner
struct Foo1 {
  a: u16;
  b: u32;
}

struct Foo2 {
  a: u16;
  b: u32;
}

struct Foo3 {
  a: u16;
  b: u32;
}

pub fn check() {
  a: u32 = kani::any();
  b: u32 = kani::any();
  foo : struct Foo1 {a,b};
  bar : struct Foo2 = transmute(foo);
  assert_eq!(bar.a, a);
  assert_eq!(bar.b, b);

[celinval]

The test above would still fail in 50% of the cases. I don't think we should add a test that might fail randomly, even if the test fails in 1% of the cases. Is there a way to control the randomization seed so we can guarantee that the test always fail?

[danielsn]

If we do n steps, it will fail in 2^(-n) times. if we set n == 64, we get an erroneous failure probability less than that of the computer being hit by a cosmic ray and giving the wrong result

[giltho]

Can you please explain why that should be the default? I'm not convinced that's the case.

Writing code that depends on the memory layout should be considered a developer error. The Rust documentation repeatedly says that the code developer should never rely on the structure layout (except if specified using repr(C)). If Kani fails with randomize_layout but not without, it means that the code depends on something it shouldn't depend on. It could break on the next release of Rustc without any warnings.

Another example would be the layout of pointers. Although it is defined internally, the stdlib explicitely mentions that nobody except std should rely on its layout as it could change without warning at any moment:

[celinval]

Can you please explain why that should be the default? I'm not convinced that's the case.

Writing code that depends on the memory layout should be considered a developer error. The Rust documentation repeatedly says that the code developer should never rely on the structure layout (except if specified using repr(C)). If Kani fails with randomize_layout but not without, it means that the code depends on something it shouldn't depend on. It could break on the next release of Rustc without any warnings.

Another example would be the layout of pointers. Although it is defined internally, the stdlib explicitely mentions that nobody except std should rely on its layout as it could change without warning at any moment:

I totally agree that we should provide an option to validate that the code depends on the structure layout, but this change is not necessarily doing this.

This change is randomizing whether the verification might fail or not if the user depends on the structure layout. This change could cause inconsistent results that are hard to reproduce and hard to debug. I think that we should figure out a way to reproduce the failure before turning this on by default.

[celinval]

Here is an example of a bad user experience in my mind.

User runs cargo kani and gets an assertion failure. Now the user runs cargo kani --visualize or cargo kani --enable-unstable --concrete-playback to figure out why there was a failure in the first place. The second run doesn't fail and leave the user without any clue what went wrong.

[zhassan-aws]

For the record, there is a layout_seed debug option that allows one to fix the random seed for reproducibility purposes: https://github.com/rust-lang/rust/blob/2e35f954ada0f0c777844dc4fa66684efe90a035/compiler/rustc_session/src/options.rs#L1497

[giltho]

Here is an example of a bad user experience in my mind

Very good point, it's very dangerous for tests to be non-reproducible.

For the record, there is a layout_seeddebug option that allows one to fix the random seed for reproducibility purposes

That's great news! It does mean that we either have to choose a fix one, or keep track of the seed we chose on every run if we want to rerun with the same seed for concrete playback for example. Second option seems unmaintainable. Should I just set layout_seed = 42?

[celinval]

Wouldn't always running with a fixed seed defeat the purpose of randomizing though?

My suggestion is that we have the randomization off by default. We add an option to randomize the layout with an optional argument that is the seed value. If no seed value is provided, you can use a fixed one

[giltho]

There's an argument for a fixed seed which is "yes it's fixed, but it's possibly different from the standard compiler choice". Also, note that in general, even without any randomization, there's no guarantees that between two runs the compiler is going to choose the same layout.

So here are the two choices I believe:

• 1. What you proposed: randomization is off by default + an option to randomize the layout with an optional seed argument.
• 2. Randomization with a fix seed by default + an option to set the seed or make it random + an option to disable the randomization

I do agree that on paper, the first one makes more sense, but I also believe that making it optional makes it quite probable that it will never be used, so I still think there's an argument to be made for the second one.

I entirely trust your judgement on that so tell me what option you prefer and I'll implement it

[celinval]

One more question about this one. What about the std library? I'm assuming this option wouldn't randomize the std library structures, right? Or are we planning to rebuild std?

I rather keep it simple and consistent with the compiler by default. This will also ensure that the concrete playback also works well by default.

For the concrete playback, when user turns randomization on, we should probably emit a warning or even a comment as part of the test that tells the user which seed was used.

[giltho]

One more question about this one. What about the std library? I'm assuming this option wouldn't randomize the std library structures, right? Or are we planning to rebuild std?

That is not an issue at all, because metadata files keep track of all the information necessary to recompute the layout. So if std was already compiled, its layout shouldn't be randomized at all. If std was compiled with randomized layouts, the information would also be kept and that wouldn't change anything.

I rather keep it simple and consistent with the compiler by default. This will also ensure that the concrete playback also works well by default.

I think I agree with you. Although in theory the second solution would work with concrete playback, it also adds up to the list of things the Kani team has to document and remember when adding new features, and that's a pain for maintainability.

For the concrete playback, when user turns randomization on, we should probably emit a warning or even a comment as part of the test that tells the user which seed was used.

Agreed!

[giltho]

I looked into how to get the seed, and actually... It looks like the randomization is already deterministic 😆

-Zrandomize-layout isn't really random at all, but allows you to change the seed. That means it's not necessary to emit a warning with the layout seed because if the layout seed is set, the user will have set it themselves

[celinval]

1. For the concrete playback, we should still mention that the user have to compile their code with -Zrandomize-layout, right?

2. Sorry if I wasn't clear. My point about the std is that the randomization will not be applied to structures that came from the std, unless if we recompile that too.

[giltho]

1. True! It's a bit annoying that the user will not be able to use the LSP interface to rerun the tests, since it wouldn't set that param correctly :(
2. Ah yes true. I guess that's ok

[giltho]

Fixed according to discussion and rebased on main

[danielsn]

I'm not sure we need --enable-unstable. What would our criteria be for marking it more stable than it is now?

Thank you for the changes!

I'm debating about one thing, should we bother adding the --enable-unstable for now? @danielsn?

[giltho]

I think this is ready to be merged!

[giltho]

I think this is ready to be merged

[giltho]

Ah, this went out of sync :/