[Soot-list] Split units in Jimple / missing equals-implementation

[John Jorgensen]

>>>>> "eric.bodden" == Eric Bodden <eric.bodden at mail.mcgill.ca> writes:

    eric.bodden> This week I implemented a "must reaching
    eric.bodden> definitions" analysis, i.e. a definition os
    eric.bodden> reachable from a use when it is reachable on
    eric.bodden> *all* paths.  Strangely, this analysis missed
    eric.bodden> the following case:

    eric.bodden> 		int j;
    eric.bodden> 		try {
    eric.bodden> 			j=3;
    eric.bodden> 		} catch(Throwable t) {
    eric.bodden> 			j=4;
    eric.bodden> 		} finally {
    eric.bodden> 			j=5;
    eric.bodden> 		}
		
    eric.bodden> 		//why is j here not 5 FOR SURE?
    eric.bodden> 		System.out.println(j); //(1)
		

    eric.bodden> Actually, the definition for j has definetely
    eric.bodden> one unambigous reachable definition:
    eric.bodden> j=5. However, Soot splits this definition into
    eric.bodden> multiple ones in the exceptional unit
    eric.bodden> graph. Since AssignStmt also does not implement
    eric.bodden> hashcode/equals, the intersection at line (1)
    eric.bodden> fails, i.e. throws the information j=5 away.

    eric.bodden> So am I missing something or is there something wrong?

I think your diagnosis of when the introduction of multiple j=5
assignments occurs is incorrect, though it's been a while
since I worked on this, and I won't have a chance to refresh my
memory of ExceptionalUnitGraph for a couple of days.

There are two cases to consider, code generated by compilers that
work like javac did before version N (where I think N is 1.3, but I
could be wrong) and code generated by compilers that work like
javac has since version N.

Compilers that worked like Sun's pre-N javac implemented finally
by emitting jsr instructions that jumped to a single copy of the
finally code, with such a jsr appearing at the end of the try
block and at the end of all exception handlers covering the try
block.

It is difficult to analyze code including jsrs (some of the
original Soot papers discuss the difficulties; I forget the
details), which led to the decision early in the development of
Soot to replace the jsr constructs with multiple copies of the
finally block.  The replacement occurs very early in Soot's
processing, implemented in coffi.CFG if I recall correctly.  So
if you want to have a single copy of code to analyze, the scope
of the change involves much more than ExceptionalUnitGraph.

Apparently jsrs are problematic outside of Soot as well (I
believe, for example, that they complicate verification---see
section 4.9 of the VM spec) and Sun's compiler at version N
stopped using jsr, and started to implement finally with multiple
copies of the finally code, just like soot.  For example, javac
1.5.0_06 produces, for this variant of your illustration:

  int m(int j) {
    try {
      j=3;
    } catch(Throwable t) {
      j=4;
    } finally {
      j=5;
    }
    return j;
  }

this bytecode:

  int m(int);
    Code:
     0:   iconst_3
     1:   istore_1
     2:   iconst_5
     3:   istore_1
     4:   goto    20
     7:   astore_2
     8:   iconst_4
     9:   istore_1
     10:  iconst_5
     11:  istore_1
     12:  goto    20
     15:  astore_3
     16:  iconst_5
     17:  istore_1
     18:  aload_3
     19:  athrow
     20:  iload_1
     21:  ireturn
    Exception table:
     from   to  target type
       0     2     7   Class java/lang/Throwable

       0     2    15   any
       7    10    15   any
      15    16    15   any

which has 3 stores of 5 to i.

So recognizing that 5 is always stored to i requires
analyzing the CFG, and it is not the case that all the
assignments of 5 to i occur at a single definition.