[LLVMdev] PredicateSimplifier questions

[John Regehr]

Thanks for the answers Nick!

> I wrote predsimplify as I was learning about compiler theory. It's
> pretty dumb in the sense that it spends lots of time analysing things
> that will never be used, and despite being the slowest pass in LLVM I
> haven't seen it improve run-times in a nightly test.

Interesting.  The application I have in mind here is some TinyOS code 
where we've added lots of array bounds checks.  The vast majority of these 
in fact cannot fail but LLVM and GCC are not smart enough to see this. 
It seemed like predsimplify was probably the right pass for this, but I 
haven't studied its success rate yet.

The problem isn't execution cost but rather code size.  This is for the 
msp430 platform which has too little flash memory.  The code bloat really 
is a showstopper here: a number of existing applications overflow the 
available memory when we add checking, and cannot be run!  (This is using 
gcc, we do not yet have an LLVM port to msp430.)

So the "pluggable domain" thing (an idea we had good luck with at the 
source level using CIL) is not just for compiler class, but also for 
solving this real problem.  In addition to calling out to standard 
abstract domains I want to for example play with shelling out to a 
heavyweight decision procedure.  This should make many spurious bounds 
checks go away.  Greg Morrisett reports good success with this approach in 
the Cyclone compiler.  Inspection of embedded codes shows that most array 
accesses can be proved to be in bounds pretty easily-- though these proofs 
are apparently out of reach of -O2 type optimizers.

> Predsimplify is believed to have bugs (it results in miscompiled
> programs) and certainly isn't efficient (it was written before much of
> include/ADT). Finally, predsimplify is likely to go away once I or
> someone else writes a proper VRP pass.

Well I do have a good way to find integer miscompilations... but don't 
want to waste everyone's time if this pass is on the way out.

John Regehr