Optimize blocks #919
Optimize blocks #919
Conversation
|
The block coalescing feature already exists in Boogie and appears to be on by default: |
Thanks. The coalescing I'm running happens for each split, after other optimizations which may enable more coalescing, so there is benefit in doing it again. However, I've removed the duplicate coalescing implementation that this PR adds. |
There was a problem hiding this comment.
This looks good. None of my comments are blocking.
I have slight worries about soundness when doing transformations like this, though I don't see anything suspicious right away. For the moment, I think I trust the test suite (plus the Dafny test suite, once it's being used there) to detect potential bugs.
Source/Core/AST/AbsyCmd.cs
Outdated
| @@ -3497,7 +3497,7 @@ void ObjectInvariant() | |||
| { | |||
| Contract.Invariant(labelNames == null || labelTargets == null || labelNames.Count == labelTargets.Count); | |||
| } | |||
|
|
|||
There was a problem hiding this comment.
You've added some trailing whitespace here. I find that Rider is very eager to do this!
| @@ -1,4 +1,4 @@ | |||
| using System.Collections.Generic; | |||
| using System.Collections.Generic; | |||
There was a problem hiding this comment.
What is this change? A change in line ending?
|
|
||
| namespace VCGeneration; | ||
|
|
||
| class OldBlockTransformations { |
| using System.Collections.Generic; | ||
| using System.Diagnostics.Contracts; | ||
| using System.Linq; | ||
| using System.Threading.Tasks.Dataflow; |
There was a problem hiding this comment.
This seems like a very relevant library for this kind of task, but I don't actually see how it's used. Is it?
Changes
Testing
AssumeFalseSplit.bplto take into account simplification (2)