Symbooglix resulting in ArgumentNullException due to Graph.cs

[liammachado]

For quite awhile now, Symbooglix has been throwing an ArgumentNullException when it is run on some cases. Consider the following example:

procedure fn1();
implementation fn1()
{
  anon0:
    goto $bb5;
  b4:
    goto $bb5;
  $bb5:
    goto $bb10;
  b9:
    goto $bb10;
  $bb10:
    return;
}
procedure main();
implementation main()
{
  anon0:
    return;
}

When I run "symbooglix example.bpl --entry-points=main" on the above example, it throws an ArgumentNullException with the following stack trace:

System.ArgumentNullException: Value cannot be null.
Parameter name: key
   at System.Collections.Generic.Dictionary.FindEntry(TKey key)
   at System.Collections.Generic.Dictionary.get_Item(TKey key)
   at Microsoft.Boogie.GraphUtil.Graph.Predecessors(Node n) in Boogie\Source\Graph\Graph.cs:line 483
   at Microsoft.Boogie.GraphUtil.DomRelation.NewComputeDominators() in Boogie\Source\Graph\Graph.cs:line 208
   at Microsoft.Boogie.GraphUtil.DomRelation..ctor(Graph g, Node source) in Boogie\Source\Graph\Graph.cs:line 87
   at Microsoft.Boogie.GraphUtil.Graph.get_DominatorMap() in Boogie\Source\Graph\Graph.cs:line 503
   at Microsoft.Boogie.GraphUtil.Graph.ComputeReducible(Graph g, Node source) in Boogie\Source\Graph\Graph.cs:line 703
   at Microsoft.Boogie.GraphUtil.Graph.ComputeLoops() in Boogie\Source\Graph\Graph.cs:line 838
   at Symbooglix.LoopEscapingScheduler.ReceiveExecutor(Executor executor) in Symbooglix\Executor\StateSchedulers\LoopEscapingScheduler.cs:line 114
   at Symbooglix.Executor.InternalRun(Implementation entryPoint, Int32 timeout) in Symbooglix\Executor\Executor.cs:line 670
   at Symbooglix.Executor.Run(Implementation entryPoint, Int32 timeout) in Symbooglix\Executor\Executor.cs:line 611
   at SymbooglixDriver.Driver.RealMain(String[] args) in SymbooglixDriver\Driver.cs:line 625
   at SymbooglixDriver.Driver.Main(String[] args) in SymbooglixDriver\Driver.cs:line 304
Exiting with EXCEPTION_RAISED

This issue was first raised last July:

boogie-org/symbooglix#32

When I pass the above file directly to Boogie, if I print the nodes of Graph g at this line:

https://github.com/boogie-org/boogie/blob/master/Source/Graph/Graph.cs#L82

It prints three nodes: one each for the anon0, $bb5, and $bb10 labels.

However, when I pass the above file to Symbooglix and print the nodes at that position, the Graph object contains five nodes: one for the above three labels, as well as one for b4 and one for b9. This presents a problem when this line is reached:

https://github.com/boogie-org/boogie/blob/master/Source/Graph/Graph.cs#L195

When the nodes are mapped to integers using this traversal of the Graph object, the traversal only hits the anon0, $bb5, and $bb10 labels. So the b4 and b9 labels are unreachable from the others. Which makes sense since anon0 is considered the "source" label, and we can see by looking at the .bpl file that the b4 and b9 labels are not "children" of the anon0 label. So this Graph does not have a single source node, but three source nodes, even though this traversal method (and I'm assuming many other parts of this class) assumes that whatever graph it is traversing has only a single source node.

This results in the postOrderNumberToNode map not being set for the b4 and b9 nodes, resulting in the variable at this line being set to null:

https://github.com/boogie-org/boogie/blob/master/Source/Graph/Graph.cs#L207

And the exception occurs at the very next line, as you can see from the above stack trace.

Note by the stack trace above the last place in Symbooglix code that is reached before Boogie code begins to be called:

https://github.com/symbooglix/symbooglix/blob/master/src/Symbooglix/Analysis/LoopInfo.cs#L58

Symbooglix is not calling impl.PruneUnreachableBlocks(), which would remove those b4 and b9 labels. I had already made a pull request (now closed) to Symbooglix making this change wherever impl.ComputeLoops() is called:

boogie-org/symbooglix#33

However, making this change resulted in another exception occurring in one of the regressions:

https://travis-ci.org/symbooglix/symbooglix/builds/336702517

Does anyone have any ideas for how to fix this issue? Should Boogie's Graph class be changed, or is there a way to fix this issue in Symbooglix?

[shazqadeer]

The Graph class in Boogie is meant for CFGs of the code of a Boogie procedure. These CFGs are single-entry. This issue is really a Symbooglix issue. I am closing it here and creating a new one with a link to this one in Symbooglix.