Add support for irreducible CFG

[radumcostache]

This PR addresses Issue #921.

Added:

Conversion of irreducible flow graphs by Node Splitting (see Dragon book section 9.7.6). For every irreducible loop found, we duplicate one of the nodes (we first try to duplicate one that does not have invariants, if that exists) and all of the nodes that it dominates.

Tests:
The former Irreducible.bpl test from test0 has been dropped and a new dedicated directory has been created: irreduciblecfg. 6 other test-cases have been added:

• Canonical.bpl: similar to the previous Irreducible.bpl
• BackEdgeCounter.bpl: A test case provided by @gauravpartha on the corresponding issue to justify why Back Edge Elimination shouldn't be done directly on irreducible CFGs.
• CanonicalConditions.bpl: A simple canonical irreducible CFG with some conditions
• Tangled.bpl: A larger irreducible CFG that has to maintain an invariant
• Unsound.bpl: A while + goto example provided by @petemud on the corresponding issue. It previously gave a false positive with the /extractLoops option. With the current approach, the failing trace is successfully identified.
• Await.bpl: A simplified and slightly modified version of the example that we initially wanted to verify when we opened the issue.

[shazqadeer]

Thanks for putting up this PR.

Is it the case that with this change we will never see the IrreducibleLoopException?

[shazqadeer]

If you need to duplicate a node that has invariants, do you duplicate the invariants as well? I suppose yes and that this will happen naturally.

[radumcostache]

If you need to duplicate a node that has invariants, do you duplicate the invariants as well? I suppose yes and that this will happen naturally.

Yes, in this case the invariant gets copied too. However, we first attempt to duplicate a node that does not have invariants

[radumcostache]

Thanks for putting up this PR.

Is it the case that with this change we will never see the IrreducibleLoopException?

In the current form, I don't think it can be simply dropped. Actually, this is not the exception that was triggered before by a standard run of boogie on an Irreducible loop:

boogie/Source/VCGeneration/Transformations/RemoveBackEdges.cs

Line 94 in 996947e

throw new VCGenException("Irreducible flow graphs are unsupported.");

I managed to trigger it by using the /extractLoops attribute. Specifically, the part where it is thrown is the following:

boogie/Source/Core/AST/Program.cs

Line 558 in 996947e

throw new IrreducibleLoopException();

And caught here (resolved by loop extraction):

boogie/Source/VCGeneration/LoopExtractor.cs

Lines 13 to 31 in 996947e

	/// <summary>
	/// Used by Corral and Dafny.
	/// </summary>
	public static (Dictionary<string, Dictionary<string, Block>> loops, HashSet<Implementation> procsWithIrreducibleLoops)
	ExtractLoops(CoreOptions options, Program program)
	{
	var hasIrreducibleLoops = new HashSet<Implementation>();
	List<Implementation> loopImpls = new List<Implementation>();
	Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
	foreach (var impl in program.Implementations)
	{
	if (impl.Blocks != null && impl.Blocks.Count > 0)
	{
	try
	{
	Graph<Block> g = program.ProcessLoops(options, impl);
	CreateProceduresForLoops(options, impl, g, loopImpls, fullMap);
	}
	catch (Program.IrreducibleLoopException)

The part that I am mostly concerned about is the comment from above: Used by Corral and Dafny.. I believe that one option is to refactor Dafny and Corral to use our implementation of node splitting, but not sure if it's worth it.

[shazqadeer]

The part that I am mostly concerned about is the comment from above: Used by Corral and Dafny.. I believe that one option is to refactor Dafny and Corral to use our implementation of node splitting, but not sure if it's worth it.

ExtractLoops extracts reducible loops into recursive procedures and fails if an irreducible loop is discovered. Is it possible to invoke your new code for making loops reducible within ExtractLoops before doing the extraction into recursive procedures? If yes, then the IrreducibleLoopException should not be thrown.

[shazqadeer]

In general, I would like to take maximal advantage of your impressive PR in Boogie by eliminating all occurrences of

throw new VCGenException("Irreducible flow graphs are unsupported.");

and

throw new IrreducibleLoopException();

If you could do that as part of this PR, great! Otherwise, let us land this PR and hopefully somebody can pick up the remainder of the work later.

[radumcostache]

If you could do that as part of this PR, great! Otherwise, let us land this PR and hopefully somebody can pick up the remainder of the work later.

This shouldn't be a problem, I will do it in the coming days (shouldn't take long).

[radumcostache]

In general, I would like to take maximal advantage of your impressive PR in Boogie by eliminating all occurrences of

throw new VCGenException("Irreducible flow graphs are unsupported.");

and

throw new IrreducibleLoopException();

When I first checked the IrreducibleLoopException, I came across this one:

boogie/Source/Core/AST/Implementation.cs

Lines 634 to 640 in 35aebbe

	else // Proc is YieldProcedureDecl
	{
	graph.ComputeLoops();
	if (!graph.Reducible)
	{
	tc.Error(this, "irreducible control flow graph not allowed");
	}

From my understanding, this is part of the Civl infrastructure, thus I assume that in this case the program should be "natively" structured and this piece of code shouldn't be changed. Is this correct?

[shazqadeer]

When I first checked the IrreducibleLoopException, I came across this one:

boogie/Source/Core/AST/Implementation.cs

Lines 634 to 640 in 35aebbe

	else // Proc is YieldProcedureDecl
	{
	graph.ComputeLoops();
	if (!graph.Reducible)
	{
	tc.Error(this, "irreducible control flow graph not allowed");
	}

From my understanding, this is part of the Civl infrastructure, thus I assume that in this case the program should be "natively" structured and this piece of code shouldn't be changed. Is this correct?

Yes, this is part of Civl. But we can change it so that if we discover irreducible loop, we should apply your transformation to make it reducible and then invoke TypecheckLoopAnnotations(tc, graph).

[radumcostache]

@shazqadeer thank you for the review comments and approval. Would you like me to add/change anything else or shall we land it?

[shazqadeer]

Please go ahead and land the PR.

[radumcostache]

Unfortunately I don't have push rights on master :)