[Soot-list] Intra-procedural Interval Analysis

[Elena Sherman]

Aleksandar,

Yes, the closest is soot.jimple.toolkits.annotation.parity.ParityAnalysis.
However, Parity analysis is somewhat different from Interval analysis
mainly because Parity analysis propagates abstract elements that create a
complete lattice, i.e, bot, even, odd, top. So, when two flows are merged
where one carrying even value and another carrying odd value, then the
resulting value (up the lattice) is top, which allows for analysis
termination.

But in case of Interval analysis at each merge of flows the interval might
increase just by a little bit, which not enough to reach fix point on its
own. For example, on the first loop iteration the flow with interval [0,1]
is merged with the flow with interval [0,2], which gives [0,3], on the next
one [0,3] is merged with [0,4], on the third [0,4] with [0,5] and so on.
Thus the analysis will not terminate. For this type of abstract domains
(numerical domains) one needs to introduce a widening operator which allows
for the interval to reach value, like [0, inifity) in our example, so the
analysis will terminate. These types of domains also have narrowing
operators that are used to gain some precision.

As you could see ForwardFlowAnalysis does not have abstract methods to
implement widening and narrowing operators, hence more likely not suitable
for numerical domains as is, and require some advanced work on your side if
you want to implement Interval analysis by extending ForwardFlowAnalysis. I
know that Jlint tool (written in C++) uses interval analysis in its
framework. You can look at their code and see how they've implemented it
there.

Hope it helps,
Elena Sherman





On Fri, Nov 20, 2015 at 2:26 AM, Aleksandar Dimovski <
aleks.dimovski at googlemail.com> wrote:

> Dear all,
>
>
> I would like to ask whether there exists an implementation for
> intra-procedural Interval analysis in SOOT framework, where for every
> variable a lower and an upper bound for its possible values are tracked. I
> cannot find it in soot.toolkits.scalar.ForwardFlowAnalysis. Maybe the
> closest to it is Parity Analysis.
>
>
> You can also refer to me some other similar intra-procedural analysis
> that tracks for each variable property from some very rich lattice (with
> large height).
>
>
> Thank you in advance,
>
> Aleksandar Dimovski
>
> _______________________________________________
> Soot-list mailing list
> Soot-list at CS.McGill.CA
> https://mailman.CS.McGill.CA/mailman/listinfo/soot-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://mailman.CS.McGill.CA/pipermail/soot-list/attachments/20151120/b5b70a06/attachment.html