[Soot-list] Condition propagation implemented in a ForwardBranchedFlowAnalysis?

[Sean Wedig]

Excellent, thanks, Josh and Eric.

Yeah, I figured that FBFA would be the best approach for pushing down the
path conditions.  I'm not too interested in noting the symbolic execution
piece to find inaccessible paths (at least, not yet)... but that's
something I hadn't considered before, either.  :)

I'll take a look at the NullnessAnalysis... I think what I'm getting most
stuck on is what to use for my abstraction type, and exactly what I need to
do in some of the operations. I remember flowThrough() confused me, since
it has outputs two Lists of <abstraction type>, which was different from
the flow analysis tutorial... but I'm sure more of it will become clear
once I look at an example.

Thanks for the rapid responses!
-Sean



On Mon, Jun 11, 2012 at 2:38 AM, Eric Bodden <eric.bodden at ec-spride.de>wrote:

> Hi Sean.
>
> What you are trying to compute are called path conditions. Many people
> have done this in the past, for instance for symbolic execution (as
> Josh mentioned already). I am not sure how many people have used Soot
> for this purpose (surely some).
>
> FBFA should be useful in that case, but obviously only on an
> intra-procedural level. You may want to look at existing subclasses,
> such as NullnessAnalysis:
>
> http://www.sable.mcgill.ca/soot/doc/soot/jimple/toolkits/annotation/nullcheck/NullnessAnalysis.html
>
> Doing this on the intra-procedural level is simple. Challenges, I
> believe, lie in loop conditions, in exceptions and in inter-procedural
> flows.
>
> Best wishes,
> Eric
>
> On 11 June 2012 07:49, Sean Wedig <sean.wedig at gmail.com> wrote:
> > Hello Soot list!
> >
> > I'm pretty new to Soot and program analysis in general, so please be
> gentle.
> >  :)
> >
> > I'd like to transform an application to insert dynamic observations about
> > the conditions under which code executes.  I'd like to be able to step
> > through a CFG and make simple assertions like "condition1 && condition2
> are
> > true when we got to this point in the program", where condition1 and
> > condition2 are based on the conditions from IfStmts.
> >
> > In the flow analysis tutorial, the flow analysis menagerie's JavaDoc,
> and in
> > Eric's post on intra-procedural analysis, I've seen indications that a
> > ForwardBranchedFlowAnalysis would be the way to do some of this - each of
> > those indicate that the FBFA is the best when we want to propogate, e.g.
> "p
> > != null" down one branch and "p == null" down the other.
> >
> > Is there a simple reference implementation of propagating if/then/else
> > conditions down the branches?  Has anyone implemented something like this
> > already?
> >
> > (I feel like it's a pretty simple thing to do, but I haven't quite
> gotten my
> > head around all the flow analysis methodology yet.)
> >
> > -Sean
> >
> > _______________________________________________
> > Soot-list mailing list
> > Soot-list at sable.mcgill.ca
> > http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
> >
>
>
>
> --
> Eric Bodden, Ph.D., http://bodden.de/
> Head of Secure Software Engineering Group at EC SPRIDE
> Principal Investigator in Secure Services at CASED
> Tel: +49 6151 16-75422    Fax: +49 6151 16-72051
> Room 3.2.14, Mornewegstr. 30, 64293 Darmstadt
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20120612/b248d3ab/attachment-0001.html