RuSMT: An Executable Semantics as Conformance Oracle and Test Suite Synthesizer

Abstract

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 with it 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. This paper presents RuSMT, a framework for encoding prose specifications as executable oracles using a domain-specific language embedded in Rust. Its DSL provides types denoting Z3 sorts and primitives corresponding to Z3's operations. Concretely, the author writes the specification and marks a branch with a named marker, which identifies a path condition for the backend test synthesizer. In this paper, markers always identify error conditions. The same program is therefore used in two ways: compiled by rustc, it executes as the conformance oracle; lowered to SMT-LIB it yields one reachability query per marker. Z3 then solves each query: a sat model is rendered by a printer into a test program in the specified language, while unsat indicates that the marker is unreachable. If Z3 returns unknown or times out, RuSMT invokes a language model to propose a concrete candidate based on the emitted SMT-LIB and Z3's previous verdicts. The candidate is added to the original query as a single equality, thus constraining the search. If the candidate is rejected, its result is fed back to the language model to propose a new candidate. The process repeats until the fixed budget is exhausted. We write two executable specifications in the DSL: IMP, Winskel's canonical small imperative language as a small end-to-end demonstration, and a TOML 1.1.0 parser, implemented from the published specification. We mark 2 branches in the IMP program and 183 in the TOML parser. Z3 alone solves both IMP queries. It solves none of the 183 TOML queries within our available computational budget: lowering the recursive parser as a whole effectively turns the problem into bounded model checking, whose formula-size blowup is well known. With the language model in the loop, RuSMT reaches 146 of the 183. We ran the TOML-generated test suite against four independent TOML parsers and found divergences on 12 inputs. Of these, 9 test behaviour the specification leaves open, such as integer width and float exponent range, so they are not conformance obligations. The remaining three are implementation defects, 1 of which was previously unreported. The unreported defect was found in smol-toml, which accepts an array-of-tables header closed by a single bracket; we have reported this issue upstream.