Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merge linear control-flow before reconstruction #346

Merged
merged 5 commits into from
Sep 5, 2024

Conversation

Nadrieril
Copy link
Member

@Nadrieril Nadrieril commented Sep 4, 2024

This PR does several cfg-related things:

  • Makes some ullbc terminators be statements instead; this reduces terminators to be the bare minimum needed for control flow: goto, switch, return and abort;
  • Adds a pass that merges linear goto chains into a single block. This happens particularly in bodies with lots of function calls; this lightens the work for the control-flow reconstruction pass;
  • These two transformations made the llbc output slightly worse, so this PR also adds a pass that improves the cfg.

@Nadrieril Nadrieril changed the title Linearize cfg before reconstruction Merge linear control-flow before reconstruction Sep 4, 2024
@@ -3,7 +3,7 @@ all: build

.PHONY: build
build: format
cargo build --release
CARGO_PROFILE_RELEASE_DEBUG=true cargo build --release
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does this do?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a drive-by change that keeps more debuginfo in release mode, so that we get useful backtraces and flamegraphs. Otherwise a lot of info is lost and the flamegraphs are useless

@Nadrieril
Copy link
Member Author

There's too high a risk of breaking libcrux because eurydice relies on specific control-flow shapes to detect loops. I'll remove the last pass added in this PR and keep it for when libcrux is fixed.

@sonmarcho
Copy link
Member

sonmarcho commented Sep 5, 2024

There's too high a risk of breaking libcrux because eurydice relies on specific control-flow shapes to detect loops. I'll remove the last pass added in this PR and keep it for when libcrux is fixed.

I guess we should open an issue for this, then?
For libcrux: you mean to generate for and while loops, right?

@Nadrieril
Copy link
Member Author

Nadrieril commented Sep 5, 2024

I guess we should open an issue for this, then?

I mean, I've got the branch ready for whenever it's fixed, no need

For libcrux: you mean to generate for and while loops, right?

yes

@Nadrieril Nadrieril merged commit 97ac430 into AeneasVerif:main Sep 5, 2024
5 of 6 checks passed
@Nadrieril Nadrieril deleted the linearize-calls branch September 5, 2024 15:32
@sonmarcho
Copy link
Member

I guess we should open an issue for this, then?

I mean, I've got the branch ready for whenever it's fixed, no need

As long as we don't forget it, I'm fine with that.

github-merge-queue bot pushed a commit to model-checking/kani that referenced this pull request Nov 6, 2024
This PR advances the Charon submodule commit from 2024-09-02 to
2024-11-04.

The main changes are due to:
- AeneasVerif/charon#346: This changed some
terminators into statements.
- AeneasVerif/charon#407: The removal of some
dependence on rustc code in the Charon library.

Towards: #3585 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants