Upgrade toolchain to nightly-2023-01-23

[celinval]

Description of changes:

Upgrade our toolchain to nightly-2023-01-23. The changes here are related to the following changes:

• Combine ty::Projection and ty::Opaque into ty::Alias rust-lang/rust#104986
• Guard ProjectionTy creation against passing the wrong number of substs rust-lang/rust#105657
• Harden the pre-tyctxt query system against accidental recomputation rust-lang/rust#105603
• Rename assert_uninit_valid intrinsic rust-lang/rust#105613
• Transform async ResumeTy in generator transform rust-lang/rust#105977
• Add log-backtrace option to show backtraces along with logging rust-lang/rust#104645

Resolved issues:

Resolves #2113

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

I initially upgraded the toolchain to nightly-2023-01-16 as planned in #2113. However, the AsyncAwait tests were failing due to wrong monomorphization. To fix that, I decided to upgrade to nightly-2023-01-23 instead to include the changes related to rust-lang/rust#105977. That fixed the regression.

Note: We should consider prioritizing #1365 to stop having to amend the function abi code.

I had to disable the rust logs temporarily after the merge. The issue was already fixed on newer versions of rustc (rust-lang/rust#107761). So I added a note to the next toolchain upgrade issue to re-enable this.

Testing:

• How is this change tested?

• Is this a refactor change?

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.

[zhassan-aws]

Weird: one s2n-quic perf harness is failing.

[celinval]

Weird: one s2n-quic perf harness is failing.

I'm trying to find out what's going on here. CBMC detects a non-existing loop inside Option<>::ok_or(). This is an example of test that is failing:

#[kani::proof]
#[kani::unwind(2)]
fn check_ok_or() {
    let opt : Option<bool> = kani::any();
    let val_or = opt.ok_or(());
    assert!(val_or.is_ok());
}

Without the changes from this PR, CBMC still detects a loop, but it only fails for --unwind 1.

[zhassan-aws]

This is an example of test that is failing:

Does it pass with a larger unwind value?

[celinval]

Does it pass with a larger unwind value?

Yes. It does. It also passes if I don't specify a bound. But why there is a loop here in the first place is a mystery. Let me see if I can reproduce this in C.

[celinval]

I did some digging and created a tiny C example that triggers the same issue: diffblue/cbmc#7506.

[tedinski]

Is the decision to block this, waiting on a CBMC fix and release? From that CBMC issue's discussion it wasn't clear this was going to be fixed soon...

[celinval]

Is the decision to block this, waiting on a CBMC fix and release? From that CBMC issue's discussion it wasn't clear this was going to be fixed soon...

That's a great question. I don't think we have decided it yet. I don't think this change is urgent, so I think we can wait a few more days to see if CBMC can scope out the fix. Once we have an idea of when this can be resolved, we can decide if a work around is granted. I rather delay this update for a week or two than push a work around to our users code.

Let me know if that makes sense or if you feel like we should just move ahead.

[tautschnig]

Is the decision to block this, waiting on a CBMC fix and release? From that CBMC issue's discussion it wasn't clear this was going to be fixed soon...

That's a great question. I don't think we have decided it yet. I don't think this change is urgent, so I think we can wait a few more days to see if CBMC can scope out the fix. Once we have an idea of when this can be resolved, we can decide if a work around is granted. I rather delay this update for a week or two than push a work around to our users code.

Let me know if that makes sense or if you feel like we should just move ahead.

Given the discussion we had in a meeting yesterday, a fix may be several weeks out. @martin-cs has a much more complete view of the concept of "loops" and their challenges, and tells me there are a lot of possible pitfalls. So I don't question that we need to find a way to address this for our customers, but it may well be worth upgrading with a workaround right now and then keeping open an issue to track reverting this workaround once a fix has been implemented.

[martin-cs]

On a previous project I learnt, to my cost, that there are a lot of weird loop configurations that turn up if you analyse a large enough code base. Either A. you play whack-a-mole and continuously tweak your loop handling or B. you need a dedicated loop normalisation pass. An A solution to this would be pretty quick but it will not be the last, a B solution to this will take longer but will benefit many other users ( @remi-delmas-3000 for one ).

At the moment I don't have the time allocation to solve the whole problem myself but am happy to meet with / share experience and benchmarks with anyone who does.

[celinval]

On a previous project I learnt, to my cost, that there are a lot of weird loop configurations that turn up if you analyse a large enough code base. Either A. you play whack-a-mole and continuously tweak your loop handling or B. you need a dedicated loop normalisation pass. An A solution to this would be pretty quick but it will not be the last, a B solution to this will take longer but will benefit many other users ( @remi-delmas-3000 for one ).

At the moment I don't have the time allocation to solve the whole problem myself but am happy to meet with / share experience and benchmarks with anyone who does.

I would love to hear more about it @martin-cs but in this case there is no loop. A simple DFS in the CFG should be enough to at least rule out false positives in the loop detection.

[martin-cs]

@celinval I completely agree with your point that it will solve this specific problem. My experience with this and other loop-related weirdness is that "We just need a small tweak to deal with this one" is a very long road of spiralling complexity and increasing fragility of the algorithms. Although it might be a little more work initially, I would strongly recommend a robust loop normalisation pass and robust loop detection algorithms because the list of "just one more tweak" seems to never end.

[celinval]

@celinval I completely agree with your point that it will solve this specific problem. My experience with this and other loop-related weirdness is that "We just need a small tweak to deal with this one" is a very long road of spiralling complexity and increasing fragility of the algorithms. Although it might be a little more work initially, I would strongly recommend a robust loop normalisation pass and robust loop detection algorithms because the list of "just one more tweak" seems to never end.

I get your point. We might try doing a topological sort on our side to see if we overcome the current issues we are facing.

Rust doesn't support goto statements, so I am hoping that the weird cases you are talking about won't be a problem here.

[celinval]

It looks like #2181 fixed the s2n-quic regression, but another performance test may be running out of memory. 🤦‍♀️

[martin-cs]

Rust doesn't support goto statements, so I am hoping that the weird cases you are talking about won't be a problem here.

Unfortunately ... you can still cause chaos without `goto`. Once you have inlining then returns start to behave a lot like localised gotos. Also sensible normalisations like "if you have a GOTO instruction who's target is an unconditional GOTO then you can jump directly to the second target" can create some surprisingly anomalous situations like loops with multiple back edges.

[celinval]

Rust doesn't support goto statements, so I am hoping that the weird cases you are talking about won't be a problem here.
Unfortunately ... you can still cause chaos without goto. Once you have inlining then returns start to behave a lot like localised gotos. Also sensible normalisations like "if you have a GOTO instruction who's target is an unconditional GOTO then you can jump directly to the second target" can create some surprisingly anomalous situations like loops with multiple back edges.

Interesting. Do you have any examples for these cases? Shouldn't the return statements behave like break statements at that point?

[celinval]

Running the failing test in my local machine with cargo kani, I got the following:

Configuration	Time	Memory
main (CBMC 5.75)	5.74s	165MB
this PR (CBMC 5.75)	206s	16GB
main (CBMC 5.70)	200.s	16GB

Note that the time in this PR is very similar to the one I obtained when running main with an older CBMC version (before diffblue/cbmc#7230).

I wonder if whatever has changed neutralized the optimization that @tautschnig introduced. 😕

[celinval]

I created #2191 to track the performance regression. This PR is blocked till we have a better picture of what's going on.

[celinval]

Since the fix has already been merged to CBMC and we should update the CBMC version before the release, we decided to mark the performance regression tests as ignored. In the mean time, the CBMC latest workflow will run the ignored tests.

I manually triggered the job in my fork to see if it works: https://github.com/celinval/kani-dev/actions/runs/4368456571