Preserve boolean expressions?

[Kelvin Ku <kelvin@cs.toronto.edu>]

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