[LLVMdev] secure virtual architecture / safecode

[Vikram S. Adve]

SMT solvers seem more general-purpose than we need.  We just need an  
ILP solver of some kind (Omega, PIP, TaPAS, ...) for almost all uses I  
can think of.  Do you want to do more powerful symbolic analysis for  
some purpose?

--Vikram
Associate Professor, Computer Science
University of Illinois at Urbana-Champaign
http://llvm.org/~vadve



On Mar 27, 2009, at 12:08 PM, John Regehr wrote:

> On Wed, 25 Mar 2009, Vikram S. Adve wrote:
>
>> We do have a static array bounds checking algorithm based on the  
>> Omega
>> integer programming library, but it is not hugely effective.  I think
>> this can be strengthened a *lot*.
>
> I should add that I would be interested in helping with hooking a good
> decision procedure into LLVM.  This will be useful far beyond array  
> bounds
> check elimination.
>
> What is the current thinking?  SMT solver?
>
> John
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev