Removing empty blocks before VC generation

Aug 11, 2009 at 1:32 AM

Hi everybody,

let's try using this discussion board instead of starting an email thread, other people might find this useful as well.

So, I was wondering recently whether Boogie cleans up (i.e. removes) empty blocks before doing VC generation. I found the /noRemoveEmptyBlocks switch in Boogie help, so my guess was that it is doing some empty block optimizations. I wanted to learn what exactly is going on, so I run Boogie on this simple bpl code:

procedure main()
{
start:
goto label1;

label1:
goto label2;

label2:
}

However, the generated VC still contains formulas for all of the blocks in this example, although they are empty.

Is generating error traces the only reason why these empty blocks are still part of the VC?

Is there a switch that would still remove them?

 

Thanks!

 

Cheers,

-- Zvonimir

Coordinator
Aug 13, 2009 at 6:43 PM

There were two reasons for the behavior you observed.

First, Boogie's inference adds assume statements to the beginning and end of every block.  This can make some otherwise empty block non-empty.  You can disable the inference with /noinfer, but then you also don't get the benefit of the inference.

Second, there was a bug in the remove-empty-block optimization where the optimized list of successors of the start block was never changed.  I fixed that (change set 31961).

You could change this further, if you want to, to consider a block to be empty if all it contains are "assert true" and "assume true" statements.  To do that, change the two occurrence of "b.Cmds.Length != 0" to something appropriate in method removeEmptyBlocksWorker in VC.ssc.

  Rustan