Programming languages research · UChicago coursework · Spring 2019
Assay
Constructing the input that breaks a higher-order program — a study of relatively complete counterexamples.
Most of the term went into building interpreters — a ladder of small languages, each one adding a feature and a proof obligation. It ends somewhere else: with a PLDI paper, read closely enough to hand-trace its semantics, and an implementation we spent three weeks failing to run.
The paper is Nguyen and Van Horn on counterexamples for higher-order programs — given a program that can crash, construct an input that crashes it, soundly and completely. The difficulty is that the input may be a function, and functions can’t be filtered the way integers can. Their method sidesteps the search entirely: step through evaluation of a symbolic program, accumulate first-order constraints in a heap as you go, and when the program errors, hand what you’ve collected to an SMT solver. The counterexample falls out of the model.
What the write-up became, in the end, was as much about the gap between a published method and a runnable artifact — and what you learn by writing to the person who built it.
The instrument
The observation that makes it tractable
Searching the space of functions that might crash a program is hopeless — there are infinitely many. Nguyen and Van Horn's move is to note that if an unknown function can reach an error state at all, it can reach it by applying its input immediately, without loss of generality. What's left is first-order, and first-order constraints have solvers.
A heap that is also a path condition
Each evaluation step allocates a fresh location and records what must be true of the value there. By the time the program errors, the heap holds enough first-order constraints to reconstruct the input that got it there — handed to Z3, and read back as a concrete counterexample.
Three weeks against a published artifact
Every route to running their implementation was closed: the online evaluator's server was down, the VirtualBox image had expired, and building from source needed a Z3 version shipped only for Windows. Z3 worked fine in the terminal; their heap constructor still reported it missing. Their own CI was red at the time.
What the author told us
Email correspondence with Phuc Nguyen turned up work that isn't in any paper — an extension to mutable state that finds counterexamples a pure language forbids, and his own assessment that they weren't interesting enough to pursue.
The movement
The engineering underneath
A term of building interpreters ends by reading someone else's, closely enough to trace it by hand and then try to run it.
Why higher-order inputs resist the usual trick
For a first-order program you can filter candidate inputs directly — an integer either satisfies the constraint or it doesn't. A function argument has no such test; you cannot enumerate the functions that might break f. The paper's answer is not to search that space at all, but to assume the worst-case shape of the culprit and let the constraints accumulate.
let f (g : int -> int) (n : int) : int =
1 / (100 - (g n))
in (• f)Tracing the heap by hand
We worked the paper's example through step by step rather than taking the result on faith. Each reduction allocates a location — L1 for the unknown, L2 and L3 for the arguments it applies, L4 and L5 for the intermediate integers — and every entry added is first-order. At the point of division the semantics branch non-deterministically, and refining L5 to zero selects the error path.
Where it bottoms out
The residue is an ordinary SMT problem. Z3 returns a model, the model is plugged back into the heap, and out falls a concrete function that crashes the program. This is the whole payoff of the reduction: the hard, higher-order search has become five lines a solver can read.
(declare-const L3 Int)
(declare-const L4 Int)
(declare-const L5 Int)
(assert (= L5 (- 100 L4)))
(assert (= 0 L5))The artifact we could not run
Constructive engagement meant actually running their implementation, and we never managed it. Online evaluator down, VirtualBox image expired, and a source build that wanted a Windows-only Z3 build while our working Z3 went undetected. Three weeks, and the honest finding was about artifact rot rather than about the method — their continuous integration was failing at the same time we were.
Asking the author
We wrote to Phuc Nguyen about the build, and the correspondence outlasted the problem. He described the larger goal behind this line of work — making static analyzers less ad-hoc, since their soundness proofs tended to need fresh invention for every new language feature — and where counterexample generation had stalled. Extending it to mutable state does produce counterexamples, like the one below, that no pure function could give: g ignores its argument and returns zero the second time it's called. His verdict was that such examples are found but not interesting — not the kind of bug a programmer would care about.
(define h
(lambda f
(if (= 0 (f 1)) 0 (/ 1 (f 1)))))
(define g
(let ([counter 0])
(lambda _
(set! counter (+ 1 counter))
(if (= counter 2) 0 1))))
(h g)- Paper
- Nguyen & Van Horn, "Relatively Complete Counterexamples for Higher-Order Programs" (PLDI '15)
- Subject
- Symbolic execution · higher-order contract verification
- Tools
- Symbolic PCF · Racket · Z3
- Correspondence
- With the paper's first author, over the term
- Origin
- University of Chicago · CMSC 22100 (Programming Languages) · Spring 2019
- Team
- Partner project, completed with one collaborator