Re: Preserve boolean expressions?

[Jennifer LHOTAK <jlhotak@sable.mcgill.ca>]

The code where Soot creates a condAnd(&&) and a condOr(||) in the case
where you start from a java source is found in
soot/javaToJimple/JimpleBodyBuilder.java in two methods createCondAnd and
createCondOr. They are mostly undocumented, but if you are familiar with
Jimple they should be straight forward.

Jennifer

On Fri, 28 May 2004, Kelvin Ku wrote:

> It seems that Soot unrolls boolean expressions into a sequence of "if
> var = true/false goto label" statements in a lazy-evaluation way. e.g. the
> statement
>
> if a && b ...
>
> in the original Java source, where a and b are boolean variables, becomes
>
> if a == 0 goto labelx;
>
> if b == 0 goto labelx;
>
> in the Jimple representation. Soot also does this to a boolean expression
> that is not the condition of an if statement, for example, a boolean
> expression which is the right-hand-side of an assignment statement. And
> while Grimple aggregates arithmetic expressions, it doesn't seem to do so
> for boolean expressions.
>
> We would like to use the original expression in order to do a type of
> reachability analysis, e.g. in the code fragment
>
> if (a && !a)
>   b = true;
> else
>   b = false;
>
> the fact that the condition "a && !a" is unsatisfiable implies that the
> statement "b = true" is unreachable. However, the unrolled form
>
>         if a == 0 goto label0;
>
>         if a != 0 goto label0;
>
>         b = 1;
>         goto label1;
>
>      label0:
>         b = 0;
>
>      label1:
>         return;
>
> cannot be analyzed in the same manner. To determine the reachability of "b
> = 1", we have to walk the control-flow graph and collect condition
> information. This is effectively the same as finding the satisfying
> variable assignments for the formula "a && !a", but in a less efficient
> manner than, say, a SAT solver might use.
>
> Could someone either:
>
> (1) Point me to the parts of Soot's internal code which unroll boolean
> expressions (I imagine javac already does so for the sake of generating
> efficient code, but this unrolling happens even when I start with a Java
> source file as input to Soot). If I can understand the mechanism I might
> be able to reconstruct the original boolean expression from the if/goto
> statements.
>
> or (2) Tell me how to preserve or refer to the original boolean
> expression.
>
> Thanks,
> Kelvin Ku
>