[LLVMdev] New automated decision procedure for path-sensitive analysis

[Domagoj Babic]

Hi Zhongxing,

On 4/8/07, Zhongxing Xu <xuzhongxing at gmail.com> wrote:
> I think the real difficult thing in path sensitive program analysis (or
> symbolic execution) is not the lack of decision procedures, but the
> translation of arbitrary pointer operations and library function calls in
> C/C++ program into the mathematics supported by the automated theorem
> prover.
> Almost every concept in the computer program except memory address has a
> counterpart in mathematics. I have tried to simulate memory by arrays in
> symbolic execution. But I found it is inadequate.

There has been some progress lately (see Rustan Leino's work on the weakest
precondition transformer) on handling arrays. Some automated theorem provers
even support the theories of arrays (like CVC, Simplify, Yices,...).
However, those
thm provers do not have a very good support for modular arithmetic. In fact,
they most often approximate bounded integers with rationals (reals), and that's
one of the reasons why they can't handle operators like MUL ( as they rely
on linear arithmetic solvers, like simplex ).

Spear takes a different approach - it is bit-precise, handles all operators, but
currently doesn't handle arrays directly. However, the other mentioned
thm provers
handle arrays by encoding them as UIFs + several axioms. As UIFs can be encoded
to SAT, I think that the theory of arrays could be as well. So, with a
bit of effort,
you should be able to use Spear for reasoning about arrays.

Cheers,
      Domagoj Babic