COVERAGE.md

Coverage

Which rung of checking exists for which language, and who runs it. A claim in policy/upheld.toml names a rule and the seam it runs at; this page is the same claim one level up: for a language, at a rung, what enforces it and where.

Every cell holds exactly one of four states:

• native: this binary evaluates it.
• published toolchain id: the consumer's own compiler or linter, run by a language: system id in .pre-commit-hooks.yaml that is named in the cell. uphold publishes only the command line. The tool, its version and its configuration stay the consumer's. A fleet that pins uphold would otherwise keep one copy of the command per repository, and the id is the one copy. The cost is coupling: a change to an id's entry or its defaults reaches every consumer at its next pin bump. So an entry carries only what makes it a check, and a consumer's args: carries the rest.
• consumer-owned external gate: the compiler, linter or verifier the consumer wires into its own hook config, named in the cell. uphold ships nothing that runs the tool; its part is the pointer on this page.
• not covered: nothing here and no named tool. A cell whose state is planned but not yet true carries the issue that plans it, and nothing more.

Rungs

rung	what	ladder
text	regex over bytes: regexp, comment_regexp, prose_regexp, require_regexp	commit
syntax	an ast-grep rule over the parse tree	commit
semantic	compiler and linter	push for a whole-program build and lint; commit for a per-file linter
proof	a verifier over a stated core	push, or manual where a run is longer than minutes

The ladder column is checked against lefthook.yml and .pre-commit-config.yaml for the rungs this repository runs on itself, and the two files agree with each other on each:

• text: uphold scan (content-policy) is a pre-commit hook in both.
• syntax: ast-grep scan (ast-grep) and ast-grep test (ast-grep-rule-tests) are pre-commit hooks in both, over the rules under ast-grep/rules. Each reads one tree per file and needs no build.
• semantic: cargo clippy --all-targets (engine-clippy) is a pre-push hook in both, because it compiles the whole crate and its tests. ruff check and shellcheck are pre-commit hooks in both, because each reads only the files staged. The rung is split by cost class, not by name: a linter that reads one file at a time sits at commit, and one that needs the whole program built sits at push.
• proof: cargo kani (kani) is a manual hook in both, and CI runs it as a job of its own, because the harnesses take minutes of solver time.

Records by rung

The same ladder, read from the catalog side: which records say a gate at each rung can see them, and which state no rung and are held by a reviewer alone. That list is generated from each record's enforcement.rung into QUICK_REFERENCE.md, under the same staleness gate as the rest of that page, so it is not repeated here. What this repository actually claims against those records is uphold check --coverage, whose last line counts the claimable records a rule here claims.

What a gate at each rung reads

These are what a consumer imports into its own hook config and claims a record for in policy/upheld.toml; uphold ships the pointer, not the tool. None of them is a record: a record is what is upheld, and these are how a gate observes it.

text

concept	what it gives a check	example tools
Lexical analysis (tokens)	the source as a stream of tokens, so a match can tell a keyword from the same word in a string or comment	flex, ANTLR lexer grammars

syntax

concept	what it gives a check	example tools
Concrete syntax tree	every token in the grammar's shape, layout and comments kept, so a finding can print the exact span	tree-sitter, ANTLR
Abstract syntax tree	the program's structure without layout, so a rule matches a construct however it is spelled	Clang AST, ast-grep

semantic

concept	what it gives a check	example tools
High-level intermediate representation	names resolved and types assigned, so a check sees what an identifier refers to	rustc HIR, MLIR, LLVM IR
Control-flow graph	every path a function can take, so a check can ask whether one statement is reached before another	LLVM, Soot
Data-flow graph	which value flows into which operation	Joern, LLVM
Program dependence graph	data and control dependences in one graph, so a program can be sliced to what affects one statement	Joern, WALA
Static single-assignment form	each variable assigned once, so a value's definition is its name	LLVM, GCC
Call graph	which function can call which, the ground of every interprocedural question	Soot, WALA, SVF
Def-use chains	each definition linked to every use it reaches, and back	LLVM, GCC
Dominator tree	which statement runs before another on every path, so "checked before used" is decidable	LLVM, GCC
Data-flow analysis	facts propagated over the control-flow graph to a fixed point; reaching definitions, liveness and constant propagation are instances	CodeQL, Soot
Range analysis	the interval each integer can hold, so an index or an overflow can be shown in bounds	Frama-C, GCC
Nullness analysis	whether a reference can be null where it is dereferenced	NullAway, Infer
Pointer and alias analysis	which memory a pointer may refer to, so two accesses can be told apart	SVF, WALA
Escape analysis	whether a reference outlives its scope or its thread	Go compiler
Shape analysis	the form a heap structure keeps, such as an acyclic list, across every operation on it	Infer
Taint analysis	whether data from an untrusted source reaches a sink without passing a sanitizer	CodeQL, Semgrep, Joern
Information-flow analysis	whether a secret can influence a public output, implicit flows through branches included	JOANA
Dependency analysis	which statements must stay in order, the ground of loop transformation and slicing	Polly, isl
Precision: interprocedural, flow-, context- and path-sensitive	how much of the program an answer accounts for: across calls, in statement order, per call site, per branch; each costs time and removes false positives	Infer, Clang Static Analyzer, SVF
Abstract interpretation	a sound over-approximation of every run in a chosen domain, so an absent alarm is a proof over that domain	Astree, Frama-C, APRON
Interval, octagon and polyhedral domains	bounds per variable; bounds on sums and differences of pairs; any linear relation: each more precise and more costly than the last	APRON, Astree, Polly/isl

proof

concept	what it gives a check	example tools
Operational semantics and abstract machines	an executable definition of what a language means, against which programs and tools are checked	K Framework
Predicate abstraction	a finite abstraction by the truth of chosen predicates, which a model checker can explore	CPAchecker
Hoare logic	pre- and postconditions a proof carries across each statement	Dafny, Why3, SPARK
Weakest preconditions	the least a state must satisfy before a statement for its postcondition to hold after it	Why3, Boogie
Verification-condition generation	each annotated routine turned into formulas a solver discharges	Boogie, Why3
Separation logic	reasoning about one heap region with the rest framed off, so pointer programs can be proved	VeriFast, Infer
Concurrent separation logic	heap ownership divided between threads, so each is proved alone	Iris, VeriFast
Rely-guarantee	each thread proved against what the others may do and what it promises them	Iris
Refinement types	types carrying predicates a solver checks, such as a non-empty list or an in-bounds index	Liquid Haskell, F*
Dependent types	types that mention values, so a specification is a type and a proof is a program	Lean, Agda, Idris
Contract verification	each routine's pre- and postconditions proved for every input rather than checked on some	SPARK, Frama-C, Dafny
Invariant checking	a property shown to hold at every loop iteration or every reachable state	Dafny, Kind 2
Termination analysis	a ranking function that decreases on every loop and call, so the program halts	AProVE, Ultimate Automizer
Refinement checking	an implementation's behaviors shown to be among its specification's	FDR, mCRL2
Relational verification	a property relating two runs or two programs, proved together	EasyCrypt
Noninterference	secret inputs shown not to affect public outputs, over every pair of runs	EasyCrypt, F*
Translation validation	each compilation checked to preserve meaning, instead of the compiler proved once	Alive2
Equivalence checking	two programs shown to compute the same function	Alive2
Bisimulation	two transition systems shown to match each other step for step	mCRL2
Symbolic execution	each path's condition as a formula, so a solver finds an input that reaches it or shows none does	KLEE, angr
Concolic execution	concrete runs that record their path conditions and negate them to reach new paths	SymCC
Bounded model checking	every execution up to a bound encoded for a SAT or SMT solver; this repository proves its own verdict path this way with Kani	CBMC, Kani
Explicit-state model checking	every reachable state enumerated and stored	SPIN
Symbolic model checking	sets of states held as decision diagrams or formulas, so large spaces are explored without listing them	nuXmv
Unbounded model checking	a property proved for runs of any length, by induction or interpolation	nuXmv, Kind 2
Software model checking	model checking over source code rather than a hand-written model	CPAchecker, Ultimate Automizer
CEGAR	a coarse abstraction refined wherever a counterexample turns out spurious	CPAchecker
Temporal logic: LTL, CTL	properties over time, such as every request being answered eventually	SPIN, nuXmv
Probabilistic model checking	probabilities and expected costs over systems that make random choices	PRISM, Storm
Partial-order reduction	interleavings that differ only in the order of independent steps explored once	SPIN
Stateless model checking	every thread schedule of a concurrent program run, without storing states	GenMC
CSP	processes and their communication as an algebra, checked by refinement	FDR
Automated theorem proving	first-order goals proved without guidance	Vampire, E
Interactive theorem proving	proofs written with a person steering and a kernel checking each step	Rocq, Isabelle, Lean
Proof checking	a small kernel that accepts or rejects a finished proof, so trust rests on the kernel alone	Lean, Rocq, Isabelle

test (enforcement level)

concept	what it gives a check	example tools
Unit testing	one unit's behavior on chosen inputs	pytest, JUnit
Integration testing	components run against their real collaborators	Testcontainers
System testing	the whole system through its external interface	Robot Framework
Regression testing	behavior that worked stays working across changes	pytest, JUnit
Property-based testing	a stated property over generated inputs, with a failing case shrunk to a minimal one	QuickCheck, Hypothesis
Coverage-guided fuzzing	inputs mutated toward new code coverage until one fails	AFL++, libFuzzer, honggfuzz
Grammar-based fuzzing	inputs generated from a grammar, so they pass the parser and reach the logic behind it	Grammarinator
Structure-aware fuzzing	mutations over a typed structure rather than bytes	libprotobuf-mutator
Stateful fuzzing	sequences of calls or messages, reaching states no single input can	Hypothesis
Differential testing	two implementations fed the same input, and any disagreement reported	Csmith
Metamorphic testing	a relation between the outputs of related inputs, where nothing gives the right output itself	Hypothesis
Mutation testing	faults planted in the code; a suite that passes over one has not tested it	PIT, Stryker
Combinatorial testing	every pair, or every t-tuple, of parameter values covered by few cases	ACTS
Search-based testing	test inputs found by optimizing toward a coverage goal	EvoSuite
Coverage analysis	which lines, branches or conditions a suite ran; a measure that stops measuring once it is a target, as goodharts-law says	llvm-cov, gcov

runtime (enforcement level)

concept	what it gives a check	example tools
Dynamic analysis	facts observed on real executions, exact for the runs seen and silent about the rest	Valgrind, DynamoRIO
Runtime verification	a monitor checking a specification against the trace of a running program	RV-Monitor
Memory instrumentation	every access checked against allocation bounds and lifetimes	AddressSanitizer, Valgrind
Race detection	unsynchronized conflicting accesses found from the happens-before order of a run	ThreadSanitizer, Helgrind
Dynamic taint analysis	untrusted bytes tracked through a running program to where they are used	Triton
Deadlock analysis	lock-order cycles seen in one run, which can deadlock in another	Helgrind, ThreadSanitizer

Languages by rung

rung	Rust	Go	Python	TypeScript	shell
text	native	native	native	native	native
syntax	consumer-owned external gate: ast-grep	consumer-owned external gate: ast-grep	consumer-owned external gate: ast-grep	consumer-owned external gate: ast-grep	consumer-owned external gate: ast-grep
semantic	published toolchain id: clippy (uphold-cargo-clippy)	consumer-owned external gate: go vet, staticcheck	consumer-owned external gate: mypy, ruff	consumer-owned external gate: tsc, eslint	consumer-owned external gate: shellcheck
proof	consumer-owned external gate: Verus	consumer-owned external gate: Gobra	consumer-owned external gate: CrossHair, Nagini	not covered	not covered

Dafny, compiled to Go or Python for a verified core, is a proof entry that belongs to no single column: consumer-owned external gate, Dafny.

The Rust proof cell is about a consumer's Rust tree. Verifying this binary's own evaluator core with Verus is issue 213; that is this repository as its own consumer, and it puts no proof rung into anyone else's tree.

The syntax rung is the consumer's ast-grep

A structural rule, such as "no .unwrap() outside #[cfg(test)]", is an ast-grep rule in the consumer's own tree, run from the consumer's own hook config. uphold carries no rule form over the parse tree and no wrapper around ast-grep: the consumer owns the rule and its gate, so changing either does not require an uphold release. The entry, for pre-commit or prek:

- repo: local
  hooks:
    - id: ast-grep
      name: ast-grep scan
      entry: ast-grep scan
      language: system
      pass_filenames: false

ast-grep scan reads sgconfig.yml and every rule under its ruleDirs, and exits 1 on a finding at error. pass_filenames: false because the project file, not the staged list, decides what each rule reads. language: system because the binary is the consumer's, like its compiler. This repository runs the same entry on itself, beside an ast-grep-rule-tests hook running ast-grep test.

In three cases ast-grep reports nothing where it did not look (measured on 0.45.3). An adopter must handle all three:

• Every rule sets severity: error. A rule with no severity is a hint: its findings print and the exit is 0.

• Every language gets a companion rule matching kind: ERROR. ast-grep matches inside a tree the grammar recovered and exits by what it matched, so a file that did not parse reads like a clean one. The companion refuses a file with an ERROR node:

  id: unparsed-rust
  language: rust
  severity: error
  message: the grammar could not read this region, so no rule here looked at it
  rule:
    kind: ERROR

  Its limit: recovery that only inserts a MISSING node produces no ERROR node, and the companion exits 0 over it. fn broken( { is one such file, repaired by an inserted ). No ast-grep rule matches a MISSING node. The backstop is the semantic row: the compiler or linter refuses that file.

• Top-level keys need checking in review. ast-grep refuses a misspelled key inside rule:, and drops one at the top level of a rule or of sgconfig.yml silently: constraint: for constraints: runs the rule without its constraint, and ruleDir: for ruleDirs: runs no rule and exits 0.

Rules a stock linter already carries

Four structural rules were proposed for this binary, one per language. Each is already a stock rule in the linter the semantic row names, so uphold's only part is the pointer:

language	the rule	where it already is
shell	an unquoted $var as an argument	ShellCheck SC2086, for every command and not only rm
Python	a bare except:	ruff E722 (pycodestyle), also flake8 E722
TypeScript	any in an exported signature	typescript-eslint no-explicit-any, with explicit-module-boundary-types for the exported half
Go	panic( outside _test.go	golangci-lint forbidigo, with a panic pattern and _test.go excluded

A rule of the consumer's own that no linter carries is an ast-grep rule, as above.

The comment checks are text, not syntax

comment_regexp and trivial_comments are text-rung checks with a parsed comment extractor, not a syntax rung. The extractor parses Rust, Python and Go with their tree-sitter grammars, so a // TODO inside a string literal is not a comment to them, and reads the # lines of TOML, YAML, ini, dotfiles and shell scripts named .sh, .bash, .zsh or .fish, where a line whose first non-blank character is # is the comment. It reads no TypeScript. What each check then does with a comment is a regex or a word comparison, which is why the text row holds them; a rule over the parse tree itself is the syntax row, and that row is the consumer's ast-grep. The rule table in REFERENCE.md states the same file kinds.