Peter Chang
2013-Nov-18 13:31 UTC
[LLVMdev] Finding tools to solve symbolic equation in llvm
Hello, I want to do points-to anlysis in llvm IR. I want it to be path sensitive, which means that when I print out the result, I need append the condition for the "May" Points-to. I plan to using symbolic execution to achieve this goal. Are there any tools in llvm, or stand-alone tools to solve the symbolic equation. Thank you! ----Peter Chang -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20131118/b588abc6/attachment.html>
Henrique Santos
2013-Nov-18 20:02 UTC
[LLVMdev] Finding tools to solve symbolic equation in llvm
I would suggest you take a look at KLEE, PAGAI and GiNaC. The first two are LLVM-based tools that do symbolic manipulation (of sorts) and the last is a C++ library for doing symbolic computation which is quite easy to use with an RTTI build of LLVM. If you can give us an example of what symbolic equation you might be trying to "solve", I'm sure we can narrow it down or suggest something new. Also, Ben Hardekopf & Calvin Lin have an article in CGO'11 about a flow-sensitive pointer analysis. You might take a look and see if they used something that might help you out. H. On Mon, Nov 18, 2013 at 11:31 AM, Peter Chang <blankboy2011 at gmail.com>wrote:> Hello, > > I want to do points-to anlysis in llvm IR. I want it to be path sensitive, > which means that when I print out the result, I need append the condition > for the "May" Points-to. > > I plan to using symbolic execution to achieve this goal. > > Are there any tools in llvm, or stand-alone tools to solve the symbolic > equation. > > Thank you! > > ----Peter Chang > > _______________________________________________ > LLVM Developers mailing list > LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev > >-------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20131118/61a0d480/attachment.html>
Daniel Berlin
2013-Nov-18 20:28 UTC
[LLVMdev] Finding tools to solve symbolic equation in llvm
Ben's LLVM based code is actually available. See: http://www.cs.ucsb.edu/~benh/research/downloads.html On Mon, Nov 18, 2013 at 12:02 PM, Henrique Santos <henrique.nazare.santos at gmail.com> wrote:> I would suggest you take a look at KLEE, PAGAI and GiNaC. > The first two are LLVM-based tools that do symbolic manipulation (of sorts) > and the last is a C++ library for doing symbolic computation which is quite > easy to use with an RTTI build of LLVM. > If you can give us an example of what symbolic equation you might be trying > to "solve", I'm sure we can narrow it down or suggest something new. > Also, Ben Hardekopf & Calvin Lin have an article in CGO'11 about a > flow-sensitive pointer analysis. You might take a look and see if they used > something that might help you out. > > H. > > > > On Mon, Nov 18, 2013 at 11:31 AM, Peter Chang <blankboy2011 at gmail.com> > wrote: >> >> Hello, >> >> I want to do points-to anlysis in llvm IR. I want it to be path sensitive, >> which means that when I print out the result, I need append the condition >> for the "May" Points-to. >> >> I plan to using symbolic execution to achieve this goal. >> >> Are there any tools in llvm, or stand-alone tools to solve the symbolic >> equation. >> >> Thank you! >> >> ----Peter Chang >> >> >> _______________________________________________ >> LLVM Developers mailing list >> LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu >> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev >> > > > _______________________________________________ > LLVM Developers mailing list > LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev >