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

[Josh Branchaud]

Hi Sean,

If I understand correctly what you are asking, it seems that what you are
trying to do is state-space exploration (exploring the different possible
ways a program could execute). If all you want to do is aggregate the
conditions on each execution path of the program, this may not be too
difficult (depending on the allowed program constructs and your handling of
them).

Assuming you want to do more than just gather these conditions, it can get
a bit trickier depending on what you want to do. An analysis technique
known as symbolic execution does this gathering of conditions along the
execution paths, but as it adds new conditions, it checks for the
feasibility/truth of these conditions. For instance, if you have one
condition that says "x > 10" and another "x == 0" and both of these appear
in the same path, you would try to solve the expression (x > 10 && x == 0)
and find out that it can be solved. Because of this, the path is deemed
infeasible. Solving these expressions involves the use of a constraint
solver/decision procedure (the capabilities of which are limited at the
present).

Hopefully, Eric or someone else can speak to whether FBFA or something else
is what you are looking for.

On Sun, Jun 10, 2012 at 7:49 PM, 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
>
>


-- 
Josh Branchaud
Graduate Research Assistant, University of Nebraska-Lincoln
jbranchaud at gmail.com - (402) 660-1656
Website: cse.unl.edu/~jbrancha
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20120610/1808806e/attachment.html