Skip to content

Example: Typestate Analysis with Heros

The problem

Many APIs have an unwritten rule about the order in which their methods may be called. A file handle must be opened before it is written to. An Iterator must not be advanced after the collection was modified. A Cipher must be initialised before it encrypts. The Java type system does not express any of this: every one of those calls compiles.

A typestate is the missing piece of information — not "what type is this object?" but "what state is this object in, right now, at this program point?". A typestate analysis attaches a small finite automaton to an API class, and then checks that every object of that class only ever sees call sequences the automaton accepts.

Two things make this harder than the analyses in Live Variable Analysis and Constant Propagation:

  • The object usually travels across method boundaries, so the analysis has to be interprocedural.
  • The analysis has to track which objects exist and, for each of them, which state it is in. That is two different kinds of information at once.

IDE — the framework Heros implements and SootUp binds to — is built exactly for that shape of problem. This page configures it step by step. Every snippet is taken from sootup.examples/src/test/java/sootup/examples/typestate, which is compiled and run by CI, so what you read here is what actually executes.

Step 1 — The target program

The API whose protocol we want to enforce:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
/**
 * A tiny API with a usage protocol: a handle must be opened before it is written to,
 * and it must be closed afterwards.
 *
 * <p>Nothing in the Java type system enforces that order. The typestate analysis in
 * {@code sootup.examples.typestate} does.
 */
public class FileHandle {

    /** Moves the handle from CLOSED to OPEN. */
    public void open() {
        // no-op: only the call sequence matters for the analysis
    }

    /** Legal only while the handle is OPEN. */
    public void write(String data) {
        // no-op
    }

    /** Moves the handle from OPEN back to CLOSED. */
    public void close() {
        // no-op
    }
}

And the program using it:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
/**
 * Two uses of the {@link FileHandle} protocol: one that respects it and one that does not.
 *
 * <p>{@code correctUsage} additionally performs the {@code write} inside a second method,
 * so the analysis only reaches the right answer if it follows the call.
 */
public class Example {

    public static void correctUsage() {
        FileHandle handle = new FileHandle();   // state: CLOSED
        handle.open();                          // state: OPEN
        writeGreeting(handle);                  // state: OPEN  (write happens in the callee)
        handle.close();                         // state: CLOSED
    }

    public static void protocolViolation() {
        FileHandle handle = new FileHandle();   // state: CLOSED
        handle.write("nothing is open yet");    // no CLOSED --write--> transition: ERROR
        handle.close();                         // still ERROR
    }

    private static void writeGreeting(FileHandle handle) {
        handle.write("hello");
    }
}

Note that correctUsage performs the write inside a second method. An intraprocedural analysis would simply not see it.

Step 2 — The protocol as an automaton

The rule "open, then write as often as you like, then close" is a two-state automaton:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
                      open
           ┌─────────────────────────┐
           │                         ▼
    ╔═════════════╗            ┌───────────┐ ──┐
    ║   CLOSED    ║            │   OPEN    │   │ write
    ╚═════════════╝            └───────────┘ ◄─┘
           ▲                         │
           └─────────────────────────┘
                      close

    ╔═╗  initial state, and the only accepting state
From Event To
CLOSED open OPEN
OPEN write OPEN
OPEN close CLOSED

Every transition not in that table is a violation. CLOSED --write--> ? has no entry, so calling write on a closed handle is an error.

Written with the small Typestate helper from the example:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
/** CLOSED --open--> OPEN --write--> OPEN --close--> CLOSED */
static Typestate fileHandleProtocol() {
  Typestate.Builder builder = Typestate.builder();
  int closed = builder.addState("CLOSED");
  int open = builder.addState("OPEN");

  builder.setInitialState(closed);
  builder.addTransition(closed, "open", open);
  builder.addTransition(open, "write", open);
  builder.addTransition(open, "close", closed);
  builder.setAccepting(closed, true);

  return builder.build();
}

States are plain ints on purpose — a state has to fit inside the value the solver propagates, and it has to be cheap to compare:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
public int getStateCount() {
  return names.length;
}

public String getStateName(int state) {
  return names[state];
}

public int getInitialState() {
  return initialState;
}

/**
 * Applies {@code event} — the name of the method that was just called — to {@code state}.
 *
 * @return the successor state, or {@link #INVALID_STATE} if the call is not allowed here.
 */
public int trigger(int state, String event) {
  if (state < 0 || state >= transitions.size()) {
    return INVALID_STATE;
  }
  Integer target = transitions.get(state).get(event);
  return target == null ? INVALID_STATE : target;
}

public boolean isAccepting(int state) {
  return state >= 0 && state < accepting.length && accepting[state];
}

Step 3 — Why IFDS is not enough, and what IDE adds

IFDS turns an interprocedural analysis into a graph reachability problem over an exploded supergraph. Each node of that graph is a pair (statement, fact), and the analysis question becomes: which pairs are reachable from the starting pair?

That answers "is this local one of the handles I care about?" — a yes/no question. It cannot answer "and which state is it in?", because the only thing IFDS computes is reachability.

IDE adds a second dimension. Every edge of the exploded supergraph additionally carries an edge function: a function that transforms a value as the fact flows along that edge. So the analysis now computes two things at every program point — the set of facts that reach it, and for each fact a value.

For a typestate analysis the split is natural:

IDE element Our choice Meaning
Facts D Jimple Value the locals that currently point at a tracked object
Values V TypestateFact the automaton state that object is in
Zero fact an artificial local <<zero>> always reachable; new facts are generated out of it
Flow functions four methods which locals to track across a statement
Edge functions four methods how the state changes along that same step
Meet lattice TOP / states / ERROR / BOTTOM how to combine values where paths join

The one sentence to remember

Flow functions decide which facts survive a statement. Edge functions decide what value each surviving fact carries. Both are asked for every statement, and for the same four kinds of edge.

Step 4 — Dependencies

The Heros binding lives in its own module.

1
2
3
4
5
<dependency>
    <groupId>org.soot-oss</groupId>
    <artifactId>sootup.analysis.interprocedural</artifactId>
    <version>2.0.0</version>
</dependency>

1
implementation "org.soot-oss:sootup.analysis.interprocedural:2.0.0"

It brings Heros itself in transitively. The two classes you will subclass or instantiate are DefaultJimpleIDETabulationProblem (your problem description) and JimpleIDESolver (the solver that runs it).

Step 5 — The value type

TypestateFact is the V of the problem. Besides the automaton's own states it needs three special values, and Heros gives each of them a specific job:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
public final class TypestateFact {

  static final int CODE_ERROR = -1;
  static final int CODE_TOP = -2;
  static final int CODE_BOTTOM = -3;

  /** No information yet. The IDE solver starts every value at top. */
  public static final TypestateFact TOP = new TypestateFact(null, CODE_TOP);

  /** Two execution paths reach this point in different states. */
  public static final TypestateFact BOTTOM = new TypestateFact(null, CODE_BOTTOM);

  /** A call was made that the automaton does not allow — the protocol was violated. */
  public static final TypestateFact ERROR = new TypestateFact(null, CODE_ERROR);

  private final Typestate automaton;
  private final int code;

  private TypestateFact(Typestate automaton, int code) {
    this.automaton = automaton;
    this.code = code;
  }

  /** Wraps a state of {@code automaton}; invalid states collapse to {@link #ERROR}. */
  public static TypestateFact of(Typestate automaton, int code) {
    switch (code) {
      case CODE_TOP:
        return TOP;
      case CODE_BOTTOM:
        return BOTTOM;
      case CODE_ERROR:
        return ERROR;
      default:
        return new TypestateFact(automaton, code);
    }
  }
  • TOP is the neutral element of the meet. The solver starts every value at top and never stores it, so "top" and "no entry in the result map" are the same thing.
  • BOTTOM is the absorbing element: two paths reach this point with the object in different states and the analysis cannot commit to either.
  • ERROR is ours, not something Heros requires. It records that a call happened for which the automaton has no transition — that is the bug we are looking for.

Step 6 — The problem class

Everything else is one class. It extends the SootUp template, which fixes the node type to Stmt and the method type to SootMethod for you:

1
2
3
public class TypestateProblem
    extends DefaultJimpleIDETabulationProblem<
        Value, TypestateFact, InterproceduralCFG<Stmt, SootMethod>> {

The template asks for six things: a zero value, the initial seeds, an all-top function, a meet lattice, a flow function factory and an edge function factory. The next steps fill them in one by one.

Step 7 — The zero fact and the seeds

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
/**
 * The artificial "zero" fact. It is always reachable, so it is the fact that other facts are
 * generated out of — see {@link #getNormalFlow} below, where the tracked local is generated from
 * the zero fact at the {@code new} statement.
 */
@Override
protected Value createZeroValue() {
  return new Local("<<zero>>", NullType.getInstance());
}

/** Where the analysis starts: the zero fact, at the first statement of the entry method. */
@Override
public Map<Stmt, Set<Value>> initialSeeds() {
  return DefaultSeeds.make(
      Collections.singleton(entryMethod.getBody().getControlFlowGraph().getStartingStmt()),
      zeroValue());
}

The zero fact is a fact that is reachable at every statement by construction. It is not a variable of the program; it is a placeholder that means "control flow gets here". It matters because IFDS and IDE can only ever propagate facts, never invent them: a new fact has to be generated from a fact that already holds — and the zero fact is the one that always holds.

The seeds say where analysis begins: here, the zero fact at the first statement of the entry method. DefaultSeeds.make is a Heros convenience for the common "one fact, a set of start statements" case.

The zero fact does not carry top

The solver sets the value of the zero fact at a seed to the lattice's bottom element, not top. That is why the edge function that creates an object (Step 10) must be a constant function — it has to produce the initial state no matter what came in. Deriving the state from the incoming value would produce BOTTOM for every object.

Step 8 — The meet lattice

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
/** Before anything is known, every value is top. */
@Override
protected EdgeFunction<TypestateFact> createAllTopFunction() {
  return new AllTop<>(TypestateFact.TOP);
}

@Override
protected MeetLattice<TypestateFact> createMeetLattice() {
  return new MeetLattice<TypestateFact>() {

    @Override
    public TypestateFact topElement() {
      return TypestateFact.TOP;
    }

    @Override
    public TypestateFact bottomElement() {
      return TypestateFact.BOTTOM;
    }

    @Override
    public TypestateFact meet(TypestateFact left, TypestateFact right) {
      if (left.equals(right)) {
        return left;
      }
      if (left == TypestateFact.TOP) {
        return right;
      }
      if (right == TypestateFact.TOP) {
        return left;
      }
      // a violation on one path is a violation, even if another path is fine
      if (left == TypestateFact.ERROR || right == TypestateFact.ERROR) {
        return TypestateFact.ERROR;
      }
      // two different states: the analysis cannot say which one holds here
      return TypestateFact.BOTTOM;
    }
  };
}

meet is applied wherever paths join. Two paths that agree keep their state; if one of them says nothing (TOP) the other one wins; if one of them found a violation the violation wins, because a bug on one path is still a bug; and if two paths genuinely disagree — say one leaves the handle OPEN and the other CLOSED — the result is BOTTOM, meaning "no single state describes this point".

createAllTopFunction returns the function that maps everything to TOP. Heros uses it to initialise its jump function table, i.e. as the value of an edge nothing is known about yet.

Step 9 — Flow functions: which locals to track

Heros asks for four flow functions, one per kind of edge in the exploded supergraph:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
@Override
protected FlowFunctions<Stmt, Value, SootMethod> createFlowFunctionsFactory() {
  return new FlowFunctions<Stmt, Value, SootMethod>() {

    @Override
    public FlowFunction<Value> getNormalFlowFunction(Stmt curr, Stmt succ) {
      return getNormalFlow(curr);
    }

    @Override
    public FlowFunction<Value> getCallFlowFunction(Stmt callStmt, SootMethod destinationMethod) {
      return getCallFlow(callStmt, destinationMethod);
    }

    @Override
    public FlowFunction<Value> getReturnFlowFunction(
        Stmt callSite, SootMethod calleeMethod, Stmt exitStmt, Stmt returnSite) {
      return getReturnFlow(callSite, calleeMethod, exitStmt);
    }

    @Override
    public FlowFunction<Value> getCallToReturnFlowFunction(Stmt callSite, Stmt returnSite) {
      return getCallToReturnFlow(callSite);
    }
  };
}

Normal flow — inside a method body

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
/**
 * Inside a method body. A tracked object is born at {@code l = new C()}; an assignment between
 * locals makes the analysis follow the new name as well.
 */
FlowFunction<Value> getNormalFlow(Stmt curr) {
  if (!(curr instanceof JAssignStmt)) {
    return Identity.v();
  }
  JAssignStmt assign = (JAssignStmt) curr;
  Value leftOp = assign.getLeftOp();
  Value rightOp = assign.getRightOp();

  if (rightOp instanceof JNewExpr && rules.containsKey(rightOp.getType())) {
    // generate the fact out of the zero fact; the edge function supplies the initial state
    return new Gen<>(leftOp, zeroValue());
  }
  if (rightOp instanceof Local) {
    return new AliasFlowFunction(leftOp, rightOp);
  }
  if (rightOp instanceof JCastExpr) {
    return new AliasFlowFunction(leftOp, ((JCastExpr) rightOp).getOp());
  }
  // anything else overwrites the left-hand side with a value we do not track
  return new AliasFlowFunction(leftOp, null);
}

new C() for a class we have a rule for is where a tracked object comes into existence: Gen takes the zero fact and returns both it and the new fact, so the local becomes tracked from here on. An assignment between locals adds the new name; anything else overwrites the left-hand side and therefore kills whatever was tracked under that name:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
public final class AliasFlowFunction implements FlowFunction<Value> {

  private final Value target;
  private final Value rightHandSide;

  public AliasFlowFunction(Value target, Value rightHandSide) {
    this.target = target;
    this.rightHandSide = rightHandSide;
  }

  @Override
  public Set<Value> computeTargets(Value source) {
    Set<Value> result = new HashSet<>();
    if (!source.equals(target)) {
      result.add(source);
    }
    if (rightHandSide != null && source.equals(rightHandSide)) {
      result.add(target);
    }
    return result.isEmpty() ? Collections.emptySet() : result;
  }
}

Call flow — entering a callee

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
/**
 * Entering a callee. Arguments are renamed to the callee's parameter locals so that the tracked
 * object keeps being followed inside. Calls to the API itself are not entered at all — they are
 * summarised on the call-to-return edge instead, which is where the protocol step happens.
 */
FlowFunction<Value> getCallFlow(Stmt callStmt, SootMethod destinationMethod) {
  if (rules.containsKey(destinationMethod.getDeclaringClassType())
      || !destinationMethod.hasBody()) {
    return KillAll.v();
  }
  AbstractInvokeExpr invokeExpr = callStmt.asInvokableStmt().getInvokeExpr().get();
  List<Immediate> args = invokeExpr.getArgs();
  List<Value> parameterLocals = parameterLocalsOf(destinationMethod);

  return source -> {
    Set<Value> result = new HashSet<>();
    for (int i = 0; i < args.size() && i < parameterLocals.size(); i++) {
      if (args.get(i).equals(source)) {
        result.add(parameterLocals.get(i));
      }
    }
    return result;
  };
}

Facts are renamed: the fact for an argument at the call site becomes the fact for the corresponding parameter local in the callee. Nothing else is passed in, so the callee only sees what it was actually given.

Calls into the API itself are deliberately not entered. FileHandle.open() has a body, but analysing that body would tell us nothing — the protocol step is the call, and it is modelled on the call-to-return edge instead. Returning KillAll here is how you say "summarise this call, do not descend into it".

Return flow — leaving a callee

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
/**
 * Leaving a callee. Everything local to the callee is killed; only the parameters — mapped back
 * onto the caller's arguments — and the returned value survive. Because the edge function on this
 * edge is the identity, the state the object reached inside the callee travels back with it.
 */
FlowFunction<Value> getReturnFlow(Stmt callSite, SootMethod calleeMethod, Stmt exitStmt) {
  AbstractInvokeExpr invokeExpr = callSite.asInvokableStmt().getInvokeExpr().get();
  List<Immediate> args = invokeExpr.getArgs();
  List<Value> parameterLocals = parameterLocalsOf(calleeMethod);
  Value returnedOp = exitStmt instanceof JReturnStmt ? ((JReturnStmt) exitStmt).getOp() : null;
  Value assignedTo =
      callSite instanceof JAssignStmt ? ((JAssignStmt) callSite).getLeftOp() : null;

  return source -> {
    Set<Value> result = new HashSet<>();
    for (int i = 0; i < args.size() && i < parameterLocals.size(); i++) {
      if (parameterLocals.get(i).equals(source)) {
        result.add(args.get(i));
      }
    }
    if (returnedOp != null && assignedTo != null && returnedOp.equals(source)) {
      result.add(assignedTo);
    }
    return result;
  };
}

The mirror image: parameters are mapped back onto the caller's arguments and the returned value onto the assignment target; everything else dies with the callee's frame. Because the edge function on this edge is the identity (Step 10), the state the object reached inside the callee travels back out with it. This is the step that makes the analysis interprocedural — remove it and correctUsage would never see its write.

Call-to-return flow — flowing around a call

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
/**
 * Flowing around a call. For an API call the receiver has to survive, because the edge function
 * on this very edge performs the protocol step. For any other call the facts that were handed to
 * the callee are killed here — they come back through the return edge, and keeping both copies
 * would hide the effect the callee had on them.
 */
FlowFunction<Value> getCallToReturnFlow(Stmt callSite) {
  if (ruleFor(callSite) != null || icfg.getCalleesOfCallAt(callSite).isEmpty()) {
    return Identity.v();
  }
  List<Immediate> args = callSite.asInvokableStmt().getInvokeExpr().get().getArgs();
  return source -> {
    for (Immediate arg : args) {
      if (arg.equals(source)) {
        return Collections.emptySet();
      }
    }
    return Collections.singleton(source);
  };
}

This edge exists for the facts that are not affected by the call. For an API call the receiver has to travel along it, because this is where the protocol step is applied. For any other call the arguments must not travel along it: they went into the callee and come back through the return edge, and keeping a second, unchanged copy here would meet with the updated one and lose the effect of the call.

Step 10 — Edge functions: where the state actually changes

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
@Override
protected EdgeFunctions<Stmt, Value, SootMethod, TypestateFact> createEdgeFunctionsFactory() {
  return new EdgeFunctions<Stmt, Value, SootMethod, TypestateFact>() {

    /** {@code l = new C()} starts the automaton for the new object. */
    @Override
    public EdgeFunction<TypestateFact> getNormalEdgeFunction(
        Stmt curr, Value currNode, Stmt succ, Value succNode) {
      if (curr instanceof JAssignStmt) {
        JAssignStmt assign = (JAssignStmt) curr;
        Typestate automaton = rules.get(assign.getRightOp().getType());
        if (assign.getRightOp() instanceof JNewExpr
            && automaton != null
            && currNode.equals(zeroValue())
            && succNode.equals(assign.getLeftOp())) {
          return TypestateEdgeFunction.generating(automaton);
        }
      }
      return EdgeIdentity.v();
    }

    /** {@code receiver.m()} on a tracked class is one step of the protocol. */
    @Override
    public EdgeFunction<TypestateFact> getCallToReturnEdgeFunction(
        Stmt callSite, Value callNode, Stmt returnSite, Value returnSideNode) {
      Typestate automaton = ruleFor(callSite);
      if (automaton == null) {
        return EdgeIdentity.v();
      }
      AbstractInvokeExpr invokeExpr = callSite.asInvokableStmt().getInvokeExpr().get();
      String methodName = invokeExpr.getMethodSignature().getName();
      if ("<init>".equals(methodName) || !(invokeExpr instanceof AbstractInstanceInvokeExpr)) {
        // the constructor creates the object, it is not a step of the protocol
        return EdgeIdentity.v();
      }
      Local receiver = ((AbstractInstanceInvokeExpr) invokeExpr).getBase();
      if (!receiver.equals(callNode) || !receiver.equals(returnSideNode)) {
        // some other tracked object flows past this call untouched
        return EdgeIdentity.v();
      }
      return TypestateEdgeFunction.transition(automaton, methodName);
    }

    /** Call and return edges only rename facts; the state travels along unchanged. */
    @Override
    public EdgeFunction<TypestateFact> getCallEdgeFunction(
        Stmt callStmt, Value srcNode, SootMethod destinationMethod, Value destNode) {
      return EdgeIdentity.v();
    }

    @Override
    public EdgeFunction<TypestateFact> getReturnEdgeFunction(
        Stmt callSite,
        SootMethod calleeMethod,
        Stmt exitStmt,
        Value exitNode,
        Stmt returnSite,
        Value retNode) {
      return EdgeIdentity.v();
    }
  };
}

Only two of the four ever do anything, and both of them have to be careful about which fact they were asked about:

  • l = new C() starts the automaton. The generated fact gets the constant function "initial state", regardless of the incoming value.
  • receiver.m() on a tracked class is a protocol step, provided the fact being asked about really is the receiver. The same call also carries other tracked objects past it; for those, the edge function must be the identity, or their state would change too.
  • The constructor is filtered out: <init> creates the object, it is not a step of the protocol.
  • Call and return edges are the identity — they only rename facts.

Step 11 — Writing an edge function

An edge function has to support four operations: computeTarget (apply it), composeWith (do this one, then that one), meetWith (combine two of them) and equalTo. Heros composes edge functions over and over while it builds method summaries, so the representation matters:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
/** Table slots for the three values that are not automaton states. */
private static final int SLOT_TOP = 0;

private static final int SLOT_BOTTOM = 1;
private static final int SLOT_ERROR = 2;
private static final int SLOT_COUNT = 3;

private final Typestate automaton;

/** {@code table[slotOf(code)]} is the result for an incoming value encoded as {@code code}. */
private final int[] table;

private static int slotOf(int code) {
  switch (code) {
    case TypestateFact.CODE_TOP:
      return SLOT_TOP;
    case TypestateFact.CODE_BOTTOM:
      return SLOT_BOTTOM;
    case TypestateFact.CODE_ERROR:
      return SLOT_ERROR;
    default:
      return SLOT_COUNT + code;
  }
}

/** The value a given slot stands for — the inverse of {@link #slotOf}. */
private static int codeOf(int slot) {
  switch (slot) {
    case SLOT_TOP:
      return TypestateFact.CODE_TOP;
    case SLOT_BOTTOM:
      return TypestateFact.CODE_BOTTOM;
    case SLOT_ERROR:
      return TypestateFact.CODE_ERROR;
    default:
      return slot - SLOT_COUNT;
  }
}

private int apply(int incomingCode) {
  return table[slotOf(incomingCode)];
}

Representing a function as "apply this list of events" would grow without bound inside a loop and the solver would never reach a fixed point. Because the automaton is finite, every function from value to value can be written down as a table instead: one slot per state, plus one slot for each special value. Composition and meet then work slot by slot, equalTo is a table comparison, and only finitely many distinct edge functions exist — so the solver terminates.

The two functions the analysis actually builds:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
/**
 * The constant function returning the automaton's initial state, used where a tracked object is
 * created. It has to be constant: the fact is generated out of the zero fact, and the zero fact
 * carries the bottom value — "reachable", not "in some state".
 */
public static TypestateEdgeFunction generating(Typestate automaton) {
  int[] table = new int[SLOT_COUNT + automaton.getStateCount()];
  Arrays.fill(table, automaton.getInitialState());
  return new TypestateEdgeFunction(automaton, table);
}

/**
 * The function performing one protocol step. A state that has no transition for {@code event}
 * maps to {@link TypestateFact#ERROR}; the three special values map to themselves.
 */
public static TypestateEdgeFunction transition(Typestate automaton, String event) {
  int[] table = new int[SLOT_COUNT + automaton.getStateCount()];
  table[SLOT_TOP] = TypestateFact.CODE_TOP;
  table[SLOT_BOTTOM] = TypestateFact.CODE_BOTTOM;
  // once the protocol is broken it stays broken
  table[SLOT_ERROR] = TypestateFact.CODE_ERROR;
  for (int state = 0; state < automaton.getStateCount(); state++) {
    table[SLOT_COUNT + state] = automaton.trigger(state, event);
  }
  return new TypestateEdgeFunction(automaton, table);
}

And the four operations, all of them entry-by-entry over the table:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
@Override
public TypestateFact computeTarget(TypestateFact source) {
  return TypestateFact.of(automaton, apply(source.code()));
}

/** Apply {@code this} first, then {@code secondFunction} — entry by entry. */
@Override
public EdgeFunction<TypestateFact> composeWith(EdgeFunction<TypestateFact> secondFunction) {
  if (secondFunction instanceof EdgeIdentity) {
    return this;
  }
  if (secondFunction instanceof TypestateEdgeFunction) {
    TypestateEdgeFunction second = (TypestateEdgeFunction) secondFunction;
    if (second.automaton == automaton) {
      int[] composed = new int[table.length];
      for (int slot = 0; slot < table.length; slot++) {
        composed[slot] = second.apply(table[slot]);
      }
      return new TypestateEdgeFunction(automaton, composed);
    }
  }
  return secondFunction;
}

@Override
public EdgeFunction<TypestateFact> meetWith(EdgeFunction<TypestateFact> otherFunction) {
  if (otherFunction == this || equalTo(otherFunction)) {
    return this;
  }
  if (otherFunction instanceof AllTop) {
    return this;
  }
  int[] met = new int[table.length];
  if (otherFunction instanceof EdgeIdentity) {
    // the identity maps every value to itself, so meet it slot by slot
    for (int slot = 0; slot < table.length; slot++) {
      met[slot] = meetCode(codeOf(slot), table[slot]);
    }
    return new TypestateEdgeFunction(automaton, met);
  }
  if (otherFunction instanceof TypestateEdgeFunction) {
    TypestateEdgeFunction other = (TypestateEdgeFunction) otherFunction;
    if (other.automaton == automaton) {
      for (int slot = 0; slot < table.length; slot++) {
        met[slot] = meetCode(table[slot], other.table[slot]);
      }
      return new TypestateEdgeFunction(automaton, met);
    }
  }
  return otherFunction;
}

@Override
public boolean equalTo(EdgeFunction<TypestateFact> other) {
  if (!(other instanceof TypestateEdgeFunction)) {
    return false;
  }
  TypestateEdgeFunction that = (TypestateEdgeFunction) other;
  return automaton == that.automaton && Arrays.equals(table, that.table);
}

Composition order

f.composeWith(g) means apply f first, then g — not the mathematical g ∘ f reading of "compose with". Getting this backwards is the single most common mistake when writing an IDE problem, and it produces plausible-looking but wrong states rather than a crash.

Step 12 — Building the ICFG and solving

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
/** Loads the target program, builds the ICFG and solves the IDE problem for one entry method. */
static Map<Value, TypestateFact> analyze(String entryMethodName) {
  AnalysisInputLocation inputLocation =
      new JavaClassPathAnalysisInputLocation(
          "src/test/resources/Typestate/binary", SourceType.Application, Collections.emptyList());
  JavaView view = new JavaView(Collections.singletonList(inputLocation));

  ClassType exampleType = view.getIdentifierFactory().getClassType("Example");
  SootClass exampleClass = view.getClass(exampleType).get();
  SootMethod entryMethod =
      exampleClass.getMethods().stream()
          .filter(m -> m.getName().equals(entryMethodName))
          .findFirst()
          .get();

  // the ICFG builds a class-hierarchy call graph from the given entry points
  JimpleBasedInterproceduralCFG icfg =
      new JimpleBasedInterproceduralCFG(
          view, Collections.singletonList(entryMethod.getSignature()), false, false);

  Map<ClassType, Typestate> rules = new HashMap<>();
  rules.put(view.getIdentifierFactory().getClassType("FileHandle"), fileHandleProtocol());

  TypestateProblem problem = new TypestateProblem(icfg, entryMethod, rules);
  JimpleIDESolver<Value, TypestateFact, InterproceduralCFG<Stmt, SootMethod>> solver =
      new JimpleIDESolver<>(problem);
  solver.solve();

  List<Stmt> stmts = entryMethod.getBody().getStmts();
  return solver.resultsAt(stmts.get(stmts.size() - 1));
}

JimpleBasedInterproceduralCFG is SootUp's implementation of the Heros ICFG interface. Given a View and a list of entry points it builds a call graph with class hierarchy analysis and stitches the per-method CFGs together at call sites. The two booleans switch on exceptional control flow and reflective call resolution; both are off here.

Then it is three lines: construct the problem, hand it to JimpleIDESolver, call solve(). Results are read per statement with resultsAt, which returns Map<D, V> — here, a map from local to automaton state — with the zero fact and all top values already filtered out.

Step 13 — The result

For correctUsage, the analysis computes this (the values shown are the ones holding before each statement executes):

1
2
3
4
5
6
7
$stack1 = new FileHandle                                     {}
specialinvoke $stack1.<FileHandle: void <init>()>()          {$stack1=CLOSED}
l0 = $stack1                                                 {$stack1=CLOSED}
virtualinvoke l0.<FileHandle: void open()>()                 {$stack1=CLOSED, l0=CLOSED}
staticinvoke <Example: void writeGreeting(FileHandle)>(l0)   {$stack1=CLOSED, l0=OPEN}
virtualinvoke l0.<FileHandle: void close()>()                {$stack1=CLOSED, l0=OPEN}
return                                                       {$stack1=CLOSED, l0=CLOSED}

l0 is OPEN across the call to writeGreeting and CLOSED again at the end — the write inside the callee did not break anything. For protocolViolation the same run ends with l0=ERROR: CLOSED has no write transition, and ERROR is sticky.

Step 14 — Verifying the result

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
/** The value the analysis computed for the local with the given name. */
static TypestateFact factFor(Map<Value, TypestateFact> results, String localName) {
  return results.entrySet().stream()
      .filter(e -> e.getKey().toString().equals(localName))
      .map(Map.Entry::getValue)
      .findFirst()
      .orElseThrow(() -> new AssertionError(localName + " was not tracked; got " + results));
}

@Test
public void correctUsageEndsInAnAcceptingState() {
  Map<Value, TypestateFact> results = analyze("correctUsage");

  // l0 is the local holding the handle; write() happens inside writeGreeting(), so this only
  // works because the analysis follows the call
  TypestateFact handle = factFor(results, "l0");
  assertEquals("CLOSED", handle.toString());
  assertTrue(handle.isAccepting(), "the handle should end in a final state");
  assertFalse(results.containsValue(TypestateFact.ERROR), "no violation expected: " + results);
}

@Test
public void violationIsReported() {
  Map<Value, TypestateFact> results = analyze("protocolViolation");

  // CLOSED has no write transition, so the call folds the value to ERROR and keeps it there
  assertEquals(TypestateFact.ERROR, factFor(results, "l0"));
}

@Test
public void aliasesAreTrackedByName() {
  // $stack1 and l0 are the same object, but the analysis tracks names, not objects: it never
  // learns that a call on l0 also changes the state of $stack1. Removing this limitation needs
  // a pointer analysis.
  Map<Value, TypestateFact> results = analyze("protocolViolation");
  assertEquals("CLOSED", factFor(results, "$stack1").toString());
}

CI runs these on every pull request, so a SootUp API change that breaks the analysis fails the build before it can silently invalidate this page.

The third test is the honest one. $stack1 and l0 are the same object, yet $stack1 stays CLOSED even in protocolViolation: the analysis tracks names, not objects, and it never learns that a call on l0 also changes the state of $stack1. Fixing that needs a pointer analysis to supply the alias set of each tracked object — which is exactly what production typestate tools such as Boomerang do on top of an IDE solver.

Common pitfalls

  • The zero fact carries bottom, not top. Generating edge functions must be constant. See Step 7.
  • composeWith applies this first. See Step 11.
  • Constructors are not protocol steps. <init> shows up as an ordinary call on the receiver and will trigger a transition unless you filter it out.
  • An edge function is asked for every pair of facts, not just the interesting one. Always check that the fact you were handed is the receiver before transitioning, and return EdgeIdentity.v() otherwise.
  • API calls surface on the call-to-return edge. If the ICFG has a body for the API method, the call edge fires too; return KillAll there unless you really want to analyse the API's implementation.
  • solve() before resultsAt(). resultsAt on an unsolved solver returns an empty map rather than failing.
  • No aliasing. Without a pointer analysis the results hold for the local, not for the object.

What to try next