Assignment Abstract Interpretation

Introduction

In this assignment you will implement an intra-procedural typestate propagation strategy for a subset of Java, which generalizes the flow-sensitive data-flow transformations from the previous assignments to propagation of properties. Your strategy should be extensible such that it can deal with typestates for different types.

Unitialized Variables

The basic example you should implement is checking that local variables are initialized before being used.

Null Pointers

Next example is tracking of variables that possibly contain null pointers. The following examples illustrate some typical situations.

1

void foo() {
  List l;
  l.bar(); 
}

l is null here

2

void foo() {
  List l;
  if(whatever)
    l = new ArrayList();
}

l may be null after this point

3

void foo(List l2) {
  List l1;
  l1 = l2; 
}

nullness of l1 depends on l2

4

void bar(String arg) {
  if (arg == null) {
    return;
  }
  ...
}

After this point, up to the next assignment to arg we know that arg is not null.

5

void bar(A arg) {
  if (arg != null) {
    arg.foo();
  }
}

Access to arg is safe.

6

In the next examples, the boolean operators play an important role. Depending on the location of the null pointer check, we might know whether the variable is null or not. So, the access to arg is not necessarily safe.

void bar(A arg) {
  if (whatever || arg != null) {
    arg.foo();
  }
}

void bar(A arg) {
  if (whatever && blaat || arg != null) {
    arg.foo();
  }
}

However, in the next case the null check is first, so we know now that arg can never be null in the then branch of the if.

void bar(A arg) {
  if (arg != null && whatever) {
    arg.foo();
  }
}

7

void process(String s)
{
  int len = s.length();
}

Here s may be null; should be guarded

void process(String s)
{
  if (s != null)
    {
      int len = s.length();
      ...
    }
  else
    ...
}

8

Note that you need information about methods that are invoked from your program. In the next example you need to know if the substring method will return null or not, depending on its inputs. For this assignment, we assume that you have knowledge about the behaviour of these methods, so you can define the nullness of the methods that are used in your testcases.

void process(String s1)
{
  String s2 = s1.substring(1);
}

Remarks

Consider lazy logical operators (and, or), control-flow, conditional returns and throws.

Always Unlock

Further extend your typestate checker to check proper use of the Lock interface; locks should be unlocked in the lexical scope of the lock.

Lock l = ...; 
l.lock();
try {
  // access the resource protected by this lock
} finally {
  l.unlock();
}