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
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.
Ben's LLVM based code is actually available.
See:
http://www.cs.ucsb.edu/~benh/research/downloads.html