Specifying potentially unreachable code in Boogie

May 18, 2010 at 10:09 AM

Hi all,

I recently started working on VCC, and I am implementing a transformation that may introduce dead code in the final Boogie program. However, at the point of insertion, I obviously have no way of knowing whether Boogie will be able to prove that the code is unreachable using /smoke (I could of course implement a separate analysis to infer this, but why do it if Boogie allows me not to?).
My question is, is there a mechanism in Boogie that would allow me to state that a certain program point *may be* unreachable (and if it is, we of course drop the soundness warnings), but may also *not be* unreachable, in which case we need the verification conditions to be generated as usual?

Cheers,
Francois

May 18, 2010 at 7:48 PM

There are two ways of doing that, one is asserting “$expect_unreachable()” which will prevent VCC from complaining about it. The other, better, way is asserting something with {:PossiblyUnreachable true} attribute, which will prevent Boogie from even checking it (see VC.ssc:421).

It might also disable testing the code *before* it, so it may be good to introduce a bogus control flow graph split for your stuff. In general it wasn’t tested very much, so it would be good if you experimented if the right smoke tests are disabled by it :-)

May 18, 2010 at 10:59 PM

Thanks Michal. I had seen the "$expect_unreachable()" in the VCC codebase but couldn't figure out if it was what I wanted.

I'll look into those two solutions and let you guys know if I find anything suspicious.

May 19, 2010 at 5:04 PM

So I had a quick look, and it looks like I am going to need to use "$expect_unreachable()" here (and even then, I'm not sure it will be sufficient). The thing is: the potentially dead code I introduce is not the innermost block, and is wrapped around code that should in fact be checked for logical inconsistencies.

To do things correctly, I need Boogie to report all potential unsoundness points, and then separately check them against the other ones that are reported (basically, I want to be able to report code Boogie proved unreachable, even if it is inside a block that is marked as potentially unreachable, on condition that the marked block was not proved to be actually unreachable...). This is, I think, not doable directly on Boogie, since the blocks are all flattened out for VC generation... Right now, I feel like an army of zombie code is going at my brain with wooden spoons.

Is there any order (e.g. innermost first) in which Boogie inserts the "assert false;" statements and reports the possible unreachable blocks? That would help greatly. Otherwise, I would also be happy with being able to get from a block A a collection containing all blocks Bi such that Bi strictly dominates A... It could also be useful to implement the smoke tests using such a device, to avoid reporting the same bit of unreachable code multiple times?

But in any case, it does look like the block-based attribute approach will not work for me, sorry I can't test it more extensively. I will of course keep an eye out for situations where it may become handy.

Thanks again for the pointers.
Francois

May 21, 2010 at 1:09 AM

Boogie sticks assert false at the end of a block, successor of which has more than one entry, i.e., just before joins in the CFG. It doesn’t check before forks, so indeed, if you have:

foo();

if (*) { bar() } else { baz() }

and foo() is already unreachable, you’ll get errors for bar() and baz().

The order in which it reports things is DFS, on the passive control flow graph.

If you want to play with that, you might want to get the passive CFG out of Boogie and generate the VCs yourself. I did that for VCC3.

Hope this helps somewhat,

Michal

May 21, 2010 at 1:08 PM

It does help a lot, thanks. Since this is a just a cosmetic aspect (unreachable code detection being incomplete anyway), I just quickly hacked together inside of VCC a mechanism to ignore the unreachable code reports I want to ignore, elaborating on the existing thing. I will look closer at this when I am done with the functional verification part of things.

Thanks again for your help,
Francois

May 24, 2010 at 7:01 PM

Sounds like a good plan!