[Checkers] Question about the flow algorithm

[Adam Warski]

Hello,

to reply to the first post, checking the code:

  String s = null;
  try {
    methodThrowingAnException();
    s = "m";  // assignment never happens
  } finally {
    // what's the type of 's' here?
    s.toString(); // throw NullPointerException;
  }

with the current algorithm works - the NPE is detected, because  
finally has an annotation set which is a conjunction of the  
annotations before, after and in the points where a method throwing  
exceptions is invoked. This has the downside that the set of  
annotations after the finally block is the same one - which can be  
quite restricted, because of the possible exceptions. What I'm trying  
to achieve is something less restrictive, as if all catches are not- 
alive, then the annotation set after finally shouldn't be additionally  
restricted at all.

> Now that I have read your code more thoroughly, I think the proposed  
> algorithm has one bug.  It assumes that catches never throw an  
> exception implicitly.  Here is an example:
>
>  String s = null;
>  try {
>    methodThrowingException();
>    s = "m";
>    // annosAfterNormal = {NonNull={s}}
>    // annosBeforeCatch = {NonNull={}}
>  } catch (Exception e) {
>    methodThrowingException();
>    s = "m"; // <-- basically dead-code
>    // annosAfterCatch = {NonNull={s}}, alive == true
>  } catch(Error e) {
>    s = "m";
>    return;
>    // annosAfterCatch = {NonNull={s}}, alive == false;
>  } finally {
>    // what's the type of 's' here?
>    s.toString();
>  }
>
> annosAfterNormal and annosAfterCatch for all catches has 's' as  
> NonNull.  However, 's' is null because s is never assigned.

As for your example - you're right, but that's because I didn't  
rewrite my notes exactly enough ;)
The finally block should be evaluated twice with annotations sets  
which are a conjunction of:
(1) all alive-catch after-annotations, and before-annotations
(2) all non-alive catches after-annotations, and before-annotations

(then the (1)+finally is used as the starting point for evaluating the  
rest of the code).

The important part is that you take a conjunction of the before- and  
after-catch annotations. The before-catch annotations are again a  
conjunction of begin-of-try annotations, end-of-try annotations and  
exception-throwing-statements annotations. This again can be relaxed  
by only taking a conjunction of exception-throwing annotations and end- 
of-try annos.

There is another problem, however. If you have:

String s = "s"
try {
    methodThrowingException();
} catch (Exception e) {
    s = null;
    methodThrowingException();
    s = "s";
} finally {
    s.toString();
}

the NPE will be missed by both current and my implementation. The  
reason is that while in a catch, the annotations aren't &&-ed with the  
annotations for finally (only with the annos for the surrounding try,  
if any). So the solution would be to introduce an additional in-catch  
annotations (similar to tryBits), which would be &&-ed on any  
exception-throwing statements.

>> Then we come to evaluating the finally block; it is evaluated twice,
>> with initial annotation sets:
>> (1) conjunction of all annosAfterCatch where catchAlive == true and
>> the "annosAfterNormal" set
>> (2) conjunction of all annosAfterCatch where catchAlive == false
>>
>> The annotation set after the whole try-catch-construct should be the
>> annotation set after evaluating finally (1).
>
> I assume that your algorithm here assumes the presence of catches  
> for all possible throwables.  Otherwise, we would need another  
> evaluation with annosBeforeCatch as initial set for the case where  
> an exception is not caught.

Yes, you are right.

Also, here's another problem.
Imagine you have two nested try-s. If the exception is not caught in  
the first try, then it could get caught in the second. So the  
annotations in the second try's catches and finally block should  
really cover the fact that the exception can be thrown at the point of  
execution inside the first try. So when invoking a method, not only  
the top annos from tryBits stack should be &&-ed with the current  
annos (like it is in the current algorithm), but possibly more. The  
conservative solution is to &&-ed them with the whole stack.

Adam