Unsoundness in Jimple Nullness Analysis

[svenkeidel]

@wouterraateland, I looked at your nullness analysis. First of all great work, it looks really good. However there is a small problem with unsoundness. Imagine the example jimple program 1 + "foo", your null analysis would produce NonNull, but the concrete interpreter would throw an exception. This is unsound. There are two solutions to this.

1. Approximate types more precisely:

   data Val
     = IntVal IsNull
     | LongVal IsNull
     | FloatVal IsNull
     | ...
     | Top
   

   This way the abstract interpreter can throw an exception whenever the concrete interpreter throws an exception.
2. Use an exception type, that does not approximate exceptions precisely. This is what the PropagateError type is for. The ordering of this type says that successful evaluations overapproximate exceptional evaluations: Fail <= Success. This means if the concrete interpreter fails, the abstract interpreter still can produce an successful result and it will be sound.

The first solution is more precise, but also more cumbersome to implement. Plus we are not interested in type errors when we approximate nullness of values.