[Soot-list] toolkit for precondition inference

[Gianluca Amato]

On 08/28/2013 03:12 AM, Yongzhi Wang wrote:
> Dear All,
>
> I was wondering if Soot has some builtin tools that can perform
> precondition inference. If not, any other precondition inference tool
> that is suitable for java analysis is acceptable to me.
>
> The precondition inference means as follows.Suppose we have the
> following java method change(int i), we know after statement i = i-10, i
> will be (i>0). The precondition inference will figure out that before
> the statement, i should be i>10.
>
> change(int i){
>      // inferred precondition: i >10;
>      i = i-10;
>      // assert(i>0);
> }
>
> Thanks!

In Jandom [https://github.com/jandom-devel/Jandom] we implement 
POST-CONDITION inference:

change(int i) {
   // assert(i > 0)
   i = i - 10
   // inferred postcondition i > -10
}

We do this using the Parma Polyhedra Library 
[http://bugseng.com/products/ppl] to represent several different kind of 
invariants (intervals, general linear inequations, etc...). However, the 
software is still a work-in-progress.

I would be interested in implementing PRE-CONDITION inference. It should 
not be difficult, since all the required pieces are already in place.

--gianluca amato