error traces in inlined programs

Developer
Feb 25, 2010 at 7:32 AM

Hi,

I have a program with multiple procedures that have a {:inline 1} attribute. Any error trace that is generated for this program is on the inlined version of the program: It has labels like $inline$foo$0$lab1, which do not exist in the input program. Is there a way to map this error trace back onto the input program?

Thanks,

Akash

 

Coordinator
Feb 25, 2010 at 4:06 PM

I think it should be possible to undo the additions to the labels that are done during inlining, but I don’t have in my head what prefixes/suffixes are added.  Boogie also performs various peephole optimizations, like empty-block elimination and block coalescing.  For these, Boogie tries to keep relevant labels (that is, when it eliminates a block, it tries to throw away labels that were introduced in some translation phase).  But this is not always possible, for example, if both blocks to be coalesced have relevant labels.  An alternative implementation, which you're welcome to consider, would be to keep track of sets of labels for each block.  Then, all blocks could be reported back, and after an inlining-label-undoing step, you'd get back the labels of the original Boogie program.

Is that along the lines of what you'd want to see?

Developer
Feb 26, 2010 at 3:01 AM

Yes, that helps.

One follow-up question: Where do I look to find all the peephole optimizations performed by Boogie? (I call VC.ConditionGeneration.VerifyImplementation.) I already know that "\noRemoveEmptyBlocks" turns off one optimization. I would also like to turn off the other optimization just to make error trace mapping simpler (and possibly do the optimizations myself).

Thanks,

Akash

Coordinator
Feb 26, 2010 at 4:54 AM

The other flag is /coalesceBlocks.  I think those are the two peep-hole optimizations that are performed.  To search the code for where this is done, a good place to start is found by searching for "peep-hole" (which will take you to the source file VC.ssc).

You can also see the effect of the various stages of the Boogie pipeline by using the /traceverify flag.