Scalable Typestate Analysis using Bit-Vector Machines

Static analyses based on typestates are important in certifying correctness of industrial code contracts. At their heart, such analyses rely on finite-state machines (FSMs) to specify important properties of an object. Unfortunately, many useful contracts are impractical to encode as FSMs and/or their associated FSMs have a prohibitively large number of states, which leads to sub-par performance for low-latency environments. To address this bottleneck, we present a lightweight typestate analyzer, based on a specification language that can succinctly specify code contracts with significant expressivity. A central idea in our analysis is that using a class of FSMs that can be expressed and analyzed as bit-vectors can unlock substantial performance improvements. We validate this idea by implementing our lightweight typestate analyzer in the industrial-strength static analyzer Infer. We show how our lightweight approach exhibits considerable performance and usability benefits when compared to existing techniques, including industrial-scale static analyzers.