LintQ in Soufflé

01Overview

LintQ lifts Qiskit programs into quantum-specific domain abstractions (Circuits, Registers, Gate Applications, Measurements) and checks them for well-known correctness anti-patterns. The original is built on CodeQL — powerful, but with heavy database-compilation overhead, proprietary licensing, and friction for standalone CI embedding.

This reimplementation keeps the same idea but swaps the engine: a thin Python frontend extracts facts from a Qiskit script, and Soufflé compiles the analysis rules to a native C++ binary. The result is a dependency-free executable that lints quantum codebases in milliseconds.

02Architecture

A target Qiskit script is lowered to tab-separated EDB facts, reasoned over by the Soufflé core engine, and emitted as diagnostic CSVs.

Control-flow graph of the sample circuit

The extractor turns sample_circuit.py into a CFG whose edges are exactly the statement order above. This is the structure the analyses reason over.

Diagram rendered with Mermaid. If it does not display, the same control flow is the CFGEdge.facts edge list shown in §04.

03The analyses

Four correctness checks across the two engines. Each rule is shown from the actual .dl source.

1 · OpAfterMeas — gate after a measurement

A unitary gate acts on a qubit after that qubit was measured, with no reset along the CFG path between the measurement and the gate. A measured qubit holds classical information, so further gates are almost always a bug.

// engine/lintq.dl (extractor schema)
WarnOpAfterMeas(g, c, gate, q, m) :-
    ReachableAfterMeasure(c, q, g),
    GateOp(g, c, gate, q),
    MeasureOp(m, c, q, _),
    gate != "reset".

// rules/lintq.dl (Op/ActsOn/Succ schema)
WarnOpAfterMeas(op, q, m) :-
    Op(m, "meas"), ActsOn(m, q),
    Op(op, "gate"), ActsOn(op, q),
    Reach(m, op),
    ! ResetBetween(m, op, q).

2 · DoubleMeas — redundant consecutive measurement

Two measurements of the same qubit with no operation on that qubit between them along the CFG — a redundant, consecutive measure that discards the first result.

// engine/lintq.dl
WarnDoubleMeas(m2, c, q, m1) :-
    MeasReachesMeas(c, q, m1, m2),
    MeasureOp(m2, c, q, _),
    m1 != m2.

// rules/lintq.dl
WarnDoubleMeas(a, b, q) :-
    Op(a, "meas"), ActsOn(a, q),
    Op(b, "meas"), ActsOn(b, q),
    a != b, Reach(a, b),
    ! OpBetween(a, b, q).

3 · MissingReset — use of an uninitialised qubit

The first operation that touches a qubit is not a reset — the qubit is used or measured while uninitialised.

// rules/lintq.dl
WarnMissingReset(op, q) :-
    FirstOp(op, q),
    Op(op, kind), kind != "reset".

4 · GhostCompose — discarded compose() return

A qc.compose(sub) call whose return value is discarded. compose is non-mutating in Qiskit, so the call has no effect — a silent no-op.

// engine/lintq.dl
WarnGhostCompose(s, c, sub) :-
    CircuitCall(s, "compose", c, sub),
    ! AssignedStmt(s).

04Real sample warnings

Both engines were run on real inputs and produced exactly the expected diagnostics. No false positives on clean programs.

The buggy program

from qiskit import QuantumCircuit

qc = QuantumCircuit(2, 2)
qc.h(0)
qc.cx(0, 1)
qc.measure(0, 0)
qc.measure(0, 0)          # DoubleMeas: qubit 0 measured twice, no gate between

qc2 = QuantumCircuit(1, 1)
qc2.h(0)
qc2.measure(0, 0)
qc2.h(0)                  # OpAfterMeas: gate on qubit 0 after measurement

sub = QuantumCircuit(1, 1)
sub.h(0)
qc.compose(sub)           # GhostCompose: return value discarded

Extracted facts (extractor schema)

# Stmt.facts (id, line, func)
1	1	global
2	11	global
3	13	global
...
14	26	global

# MeasureOp.facts (stmt, circ, q, c)
6	qc	0	0
7	qc	0	0
10	qc2	0	0

# GateOp.facts (stmt, circ, gate, q)
4	qc	h	0
5	qc	cx	0
11	qc2	h	0
13	sub	h	0

# CFGEdge.facts (from, to) — source order
1	2
2	3
3	4
4	5
5	6
6	7
7	8
8	9
9	10
10	11
11	12
12	13
13	14

Warnings emitted (engine/, extractor schema)

Rules engine on an independent fact set

The rules/ engine was verified against injected Op/ActsOn/Succ facts covering three bug patterns; it produced exactly the expected rows and zero on a clean program.

✓ Verified end-to-end with Soufflé 2.5: engine/ emits all three warnings (exit 0); rules/ run.sh exits 0 with the three rows above and no false positives.

05Run it

Prerequisites: Python 3.11+ and Soufflé 2.5.

Engine A — extractor → engine/

# end-to-end: extractor then the Soufflé analyses
bash run.sh                       # lints extractor/sample_circuit.py
bash run.sh path/to/your_circuit.py

# what run.sh does (equivalent manual steps):
python3 extractor/ast_to_facts.py your_circuit.py --out extractor/facts
souffle -F extractor/facts -D engine/out engine/lintq.dl
cat engine/out/WarnOpAfterMeas.csv engine/out/WarnDoubleMeas.csv engine/out/WarnGhostCompose.csv

# unit tests for the extractor
python3 -m unittest extractor.test_extractor   # 13/13 pass

Engine B — rules/

# expects EDB facts (Op.facts, ActsOn.facts, Succ.facts) under ./facts
cd rules
bash run.sh                      # creates out/ then runs souffle -F ../facts -D out
cat out/WarnOpAfterMeas.csv out/WarnDoubleMeas.csv out/WarnMissingReset.csv

06Source & project layout

The full reimplementation is in the souffle-lintq/ folder. This page is souffle-lintq/web/index.html.