An automated theorem prover and a language model generate conformance tests from one specification.

What is it about?

Conformance testing asks whether an implementation agrees with its specification. When the specification is expressed in prose, one established approach is to mechanize it as an executable specification. This executable then serves as the oracle, and an input on which an implementation disagrees is a potential bug, either in the implementation or in the mechanized specification itself. How those inputs are obtained matters, because an oracle can only adjudicate the inputs it receives. Inputs can be derived from the specification itself, and coverage-guided generators can drive aggregate coverage high. But aggregate coverage does not provide a way to target a specific condition in the specification and generate an input that reaches it. This matters particularly for error conditions, where implementations are known to diverge and where the code is empirically under-tested. RuSMT is a framework that generates inputs for exactly those conditions. The specification is written in a small language embedded in Rust, whose types and operations correspond to those of Z3, an automated theorem prover. Each error condition the specification states carries a marker. The same program is then used in two ways. Compiled, it runs as the conformance oracle. Translated to SMT-LIB, Z3's input language, it becomes one question per marker: is there an input that reaches it? Z3 and a language model work together to answer. If Z3 finds an input, it becomes a test. If Z3 proves there is none, the marker is unreachable. If Z3 gives no answer in time, the language model proposes an input, and Z3 checks it. A rejected proposal goes back to the model with Z3's verdict, and the model tries again. The result is a conformance test suite with one test for each marker reached.

Featured Image

Photo by Rahul Mishra on Unsplash

Photo by Rahul Mishra on Unsplash

Why is it important?

RuSMT aims each test at one condition, the specification marks. This enables us to generate test cases for empirically under-tested error cases. Moreover, the oracle and the test suite come from the same program, so there is no second artifact to keep in step with the specification. The method is also not tied to one language: adding a language means writing its specification in the DSL. We evaluated the framework on two case studies. For IMP, a small textbook imperative language, Z3 alone generated tests for both markers. For a TOML 1.1.0 parser with 183 markers, Z3 alone generated none within our budget because lowering the entire recursive parser to SMT makes the formula grow quickly. With the language model proposing inputs, RuSMT generated tests for 146 of the 183. We ran these tests against four independent TOML parsers, in Rust, Python, Go, and JavaScript. On 12 inputs, at least one parser disagreed with the oracle. Nine involve behaviour the standard leaves open, such as integer size. Three are implementation bugs, and one was previously unreported: smol-toml accepts the array-of-tables header [[a], which needs two closing brackets. We reported it upstream.

Perspectives