Enforcing Object Protocols by Combining Static and Dynamic Analysis

In this paper, we consider object protocols that constrain interactions between objects in a program. Several such protocols have been proposed in the literature [3, 9, 6, 5]. For many APIs (such as JDOM [23], JDBC [22]), API designers constrain how API clients interact with API objects. In practice, API clients violate such constraints, as evidenced by postings in discussion forums for these APIs. Thus, it is important that API designers specify constraints using appropriate object protocols and enforce them. The goal of an object protocol is expressed as a protocol in variant. Fundamental properties such as ownership can be expressed as protocol invariants. We present a language, PROLANG, to specify object protocols along with their protocol invariants, and a tool, INVCOP++, to check if a program satisfies a protocol invariant. INVCOP++ separates the problem of checking if a protocol satisfies its protocol invariant (called protocol correctness), from the problem of checking if a program conforms to a protocol (called program conformance). The former is solved using static analysis, and the latter using runtime analysis. Due to this separation (1) errors made in protocol design are detected at a higher level of abstraction, independent of the program’s source code, and (2) performance of conformance checking is improved as protocol correctness has been verified statically. We present theoretical guarantees about the way we combine static and runtime analysis, and empirical evidence that our tool INVCOP++ finds usage errors in widely used APIs. We also show that statically checking protocol correctness greatly optimizes the overhead of checking program conformance, thus enabling API clients to test whether their programs use the API as intended by the API designer.