llvm dev - Apr 2007 - [LLVMdev] New automated decision procedure for path-sensitive analysis

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

>
> 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.
>
> Thank you. I will try it.
But what I really mean is that array simulation is not an adequate solution
to pointer problems. :-)
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20070409/85530835/attachment.html>

Hi,

On 4/8/07, Zhongxing Xu <xuzhongxing at gmail.com>
wrote:
> Thank you. I will try it.
Np.
> But what I really mean is that array simulation is not an adequate solution
> to pointer problems. :-)
If you are only interested in a single abstract memory location per allocation
site, that can be handled efficiently. For structured graphs, symbolic
execution can be done very efficiently. I'd give you a reference, but
it's in submission
:-) . Once computed, definitions of abstract memory locations are bit-precise,
and you can pass such queries to Spear.

Proving properties for some more complex data structures than arrays can be
done, but I'm not an expert in that field, so can't give you good
references. The
best I can tell you is to google for shape analysis and separation logic.

Anyways, this is off-topic. If you have further questions/comments on
handling arrays/pointers/memory, please email me directly.

Domagoj Babic