#moonbit_static_analysis

1. Program-code revision — analyze programs in the fast-evolving MoonBit language (undefined names, unused bindings, type mismatches, dead branches, unreachable code);
2. Static state revision — a generic machine-table audit for multi-layer state machines (src/statecheck), where the audited subject calls this module and feeds its machine tables in as plain data.

#Contents

• Features
• Installation
• Quick start
• Use 1: program-code revision
• Use 2: static state revision
• API reference
• CLI reference
• Understanding the output
• Coverage and limits
• File kinds
• Project structure
• Verification
• Release history
• Contributing
• License
• References

#Features

• ✅ Three inspections, one report — structural walk → types/symbols → abstract interpretation, merged so one defect is one finding whose lens tag is the union of the lenses that saw it. The merge is lossless: the counts before and after are both kept.
• ✅ Every MoonBit file kind — .mbt / .mbtx / .mbti / .mbt.md / .mbtp, including the three the compiler does not audit at all.
• ✅ Reads, never writes — the analysed repository neither depends on this module nor is modified by it. The tool only ever reads the target's files, at scan time.
• ✅ Cross-file symbol resolution — --extern-iface-dir indexes .mbti declarations, so a type used from another package is not reported as undefined.
• ✅ Honest coverage — a file the frontend could not finish is reported PARTIAL, and its post-boundary findings are counted and not shown.
• ✅ A notice only where it can matter — a notice is printed per line only when it can hide a finding; the rest are counted by shape in one table. --show-notices brings the whole list back.
• ✅ State-machine audit — the same three inspections over plain-data machine tables: states as bindings, drive slots as a type contract, the course as abstract execution.
• ✅ Mermaid diagram output — --mmd / --mmd-auto, opt-in, and a truncated diagram says so in its own header.
• ✅ Provenance in the filename — package, version, toolchain and timestamp, so a scan can be compared with a later one.
• ⚠️ --per-function — a second entry point for the behavioral lens. Read Coverage and limits before using its numbers.

#Installation

moon add riantr/moonbit_static_analysis@0.4.47

import {
  "riantr/moonbit_static_analysis@0.4.47",
}

#The host your toolchain has to be

0.4.45 and later need a MoonBit toolchain bundling moonbitlang/core 0.10.20+65efd5b93 or later — moon 0.1.20261104 or later. A toolchain that still bundles the standalone moonbitlang/async cannot instantiate this artifact, and upgrading this package alone will not change that: the import surface is a property of the published bytes.

LinkError: WebAssembly.Instance(): Import #5 "moonbitlang/async" "thread_pool/make_write_console_job": function import requires a callable

#Quick start

#Scan another project — no dependency, no changes

moonx riantr/moonbit_static_analysis@latest riantr/moonbit_doubleML@latest

#Use it as a library

// Use 1: revise a MoonBit (current-subset) program
let result : @pipeline.PipelineResult =
  @pipeline.run(source, "main.mbt", @core.IfaceSymTab::empty())
println(@pipeline.render_result(result))

// Use 2: audit a state machine (machine tables come in as plain data)
let spec : @statecheck.MachineSpec = { name: "主体", states: [...], ... }
println(@statecheck.render(spec))

#Run the demo

moon run src/cli          # 6 samples × 3 inspections, the file-kind demos, a sample machine

#Use 1: program-code revision

=== undefined.mbt ===
2:10 - error: undefined variable 'missing' (UndefinedName) [structural+type+behavior]
  in main() at undefined.mbt:4
  in g at undefined.mbt:1
Summary: 1 finding(s) (before merge: structural 1, type 2, behavior 1)

#Use 2: static state revision

let spec : @statecheck.MachineSpec = { name: "主体", states: [...], ... }
let findings : Array[@report.Report] = @statecheck.audit(spec)
let text : String = @statecheck.render(spec)   // merged text report

规格 | 计数
---|---
状态 | 034
迁移 | 053
触发→槽 | 049 → 8
无路组合（带理由） | 228
修习历程 | 031 站

未预期发现：**0 条**

The pyroduct-shaped sample machine printed at the end of moon run src/cli is this module's own 8-state toy (statecheck.pyroduct_flavored()), not pyroduct's real tables. It carries coordinates like 182:12; those are stable pseudo-spans hashed from the state name, not positions in any source file.

#API reference

#Program analysis — src/pipeline

#Machine tables — src/statecheck

#Diagrams and provenance — src/sa

#Provenance — the artifact name

moonbit_static_analysis_0.4.47_0.1.20261023_20261024T060000Z.mmd
moonbitlang-core_0.1.20261105+65efd5b93_0.1.20261104_20261114T060000Z.mmd
tree_unknown_unknown_0.1.20261104_20261114T055946Z.mmd     # version not determined

#Reports — src/report

#CLI reference

moonx riantr/moonbit_static_analysis@latest <target> [flags]

The CLI cannot exit non-zero. MoonBit exposes no process-exit entry point in the packages available here, so a target that cannot be located prints ERROR and still exits 0 — a caller must read the output, not the exit code.

#Understanding the output

SCANNED	107 files under ...\ML\CI
CLEAN	.mbti	unchecked=0	...\CI/pof/pkg.generated.mbti
PARTIAL	.mbt	defects=1	notices=2	unchecked=17	read up to line 36, 57 after it not shown	...\CI/pof/aggregator.mbt
12:3 - notice: ... (UndefinedName) [behavior, MSA-002, low]
PARSED	32/107 files understood (29.9%); 75 more read only up to their first parse error
SUMMARY	files=107	parsed=32	actionable=56	notices=212	unreliable=15759	withheld=6769	unchecked=2841	total=16027	(actionable+notices+unreliable = total; withheld ⊆ unreliable; unchecked calls are not findings)

• PARSED is the headline. The frontend covers a SUBSET of MoonBit, so what it cannot read measures the tool's blind spot, not your code.
• A partly-understood file is still worth reading. The parser records the first line it genuinely failed on; findings before it are reported (PARTIAL), and everything after is counted in unreliable and never shown — it comes from a tree that is already wrong, so presenting it as results would reintroduce the exact failure this tool started with.
• Skipped declarations do not move that boundary. "This test block is not analysed" leaves the code after it readable, so such a file is FOUND.
• actionable excludes notices. A declaration form we chose not to analyse is not a defect in your code — and it does not pretend to be one: a scope limit is rendered notice:, not error:.
• Unparsed files are grouped BY REASON rather than listed one per line.
• actionable + notices + unreliable = total, asserted in the line. withheld is reported alongside it but is a subset of unreliable, so it is intentionally not part of the sum. unchecked is not a finding count either: it is how many calls the type lens could not check, and it is printed beside the sum precisely so it cannot be read as part of it.
• A notice is printed only when it can hide a finding. Since 0.4.36 the scan prints a notice per line only when its region lies inside some function's extent -- that is, when a conclusion may have been withheld because of it -- and counts every other notice by shape in one NOTICES table at the end of the scan:

NOTICES	TOTAL	notices=13520	printed=1705	aggregated=11815	1705 of them are printed per line: the ones that can hide a finding, and the low-confidence ones, which name a place. The other 11815 are counted by shape below
NOTICES	count=7947	test declaration is outside the analyzed subset; its body was not analyzed

#Confidence, ids, profiles and nosec

12:3 - notice: no visible binding for 'cmd' (UndefinedName) [structural, MSA-002, low]

let x = cmd()          // nosec              -- silences every finding on this line
let y = cmd()          // nosec MSA-002      -- silences that one family on this line

#Coverage and limits

#What this tool does not compete with

#What a finding is worth: sound, complete, useful

• sound — it reports no false negative: everything it reports is really there;
• complete — it reports no false positive: everything that is really there is reported;
• useful — sound or complete, but never both.

#The constructs the frontend reads past

#ParseError: one family, two meanings

#A region silences the bindings it could have read, and no others

#The two blind spots in UndefinedName

• a #doc(hidden) API appears in no .mbti, so it cannot be indexed from the dependency's source;
• a top-level cross-package reference written @pkg.fn(1, 2) is not folded into a callable name by the parser, so it is reported even when the package is indexed.

#--per-function: the behavioral lens at each function

This view is not yet sound, and the flag is opt-in for that reason. It is measured across all seven pinned corpora by _verify/census_perfunction.ps1, and the release gate pins the number. Today it reports 47 actionable findings — 46 of them on moonbitlang/core and one on moonbit_labeler — where the module view reports 30 and 1. The census classifies them: 26 are constructs this frontend does not read or operators it does not model, 20 are dead stores — a value nobody reads, and the lens's own claim about the code — and one — a local assigned and never read in moonbit_labeler — is still the first true defect this tool has published on any corpus.

Every one of them is in a NAMED family. The census keeps a bucket for findings it cannot classify, and that bucket held nine MSA-015 dead stores until 0.4.45 — a family reporting a store as unread while the read sat inside a region the frontend had declared outside its subset. The rule that fixes them is the one the frame audit already applies: a function with a hole in it is not audited.

family	n	what the lens claimed
C	6	== between two arrays
D	4	Int + Char and List + List
E	3	* on a struct
G	8	unreachable code — the lens's own claim about the code
H	1	a local assigned and never read — the lens's own claim about the code, and the one finding in the census that is a real defect
I	1	abs on a Double
J	1	* on two function values
K	3	a local call with a named argument
M	20	a dead store — a value nobody reads — the lens's own claim about the code

AND 17 MORE ARE DEMOTED. Since 0.4.38 a finding the analyzer does not stand behind is rendered notice: and counted as a notice rather than as actionable, and the census keeps the demoted set in its own table and its own total — a set of findings that leaves the census is a set that can go missing silently. Every one of the 17 carries the confidence low, and every one of them is a name the analyzer could not resolve.

THE MODULE VIEW COUNTS 14 OF THEM, AND IT IS NOT THE SAME 14. The two views are two analyses — this one takes every function as an entry point, the module view takes the module — so they do not find the same names: in moonbit_core this view reports 17 and the module view 14, and only 8 of those are the same site. That is the same difference as the 46 against the 30 above, and the two views stay separate, not additive.

demoted family	n	what the lens claimed
B	8	a BigInt literal's N suffix (0N) is not read
F	1	a name the analyzer cannot see — a sibling-file helper, a type parameter's method, an internal API absent from the .mbti index
L	8	the documented #doc(hidden) limit

FAMILY A IS GONE, AND IT IS GONE BECAUSE IT WAS FIXED. It was the hex float: the lexer read 0x1.0p1023 as the integer 0x1 followed by the name p1023, and every exponent part it could not read became an undefined name. The lexer reads a hex float as ONE literal now, with the value the toolchain computes for it, so the family has no members left — and the row is kept in the census, empty, so that a hex float that leaks a name again is caught rather than reported as something the census could not classify.

"Accepted" is measured, not assumed. moon check --target all on moonbitlang/core reports no diagnostic at all: the pinned core is self-hosted and the toolchain type-checks interface files, and this version of the core passes that check cleanly. That is only half of it: a file with no diagnostic is indistinguishable from a file nobody opened, so _verify/control_perfunction_census.ps1 appends a deliberate type error to each of the seventeen files that carry a finding in a copy and requires the error back — the requirement is 17 of 17, and the control reads 17 of 17 today.

(That row was red from 0.4.43 to 0.4.46, and the reason was the corpus and not the analyzer: the old pin carried one diagnostic of its own — abort/pkg.mbti:4, where the String of fn[T] abort(String) -> T is out of scope — and the checker bails on it before it type-checks anything else, so every probe came back carrying that one error and the probe's own error never appeared. The re-pin to 0.1.20261105+65efd5b93 brought a corpus this toolchain can check end to end, and the row turned green with it.)

The eight in family L are the documented limit rather than a defect: a cross-package #doc(hidden) function cannot be indexed from the dependency's source — only from its .mbti — so the new_uninitialized constructors of io are still reported as undefined functions: @io.Utf8TextView::new_uninitialized on four sites, @io.Utf8Writer::new_uninitialized on two and @io.Utf8Reader::new_uninitialized on two. Answering them would mean growing the analyzer into a source indexer, which is a different project. Use the view to see the lens, not to gate a build on it.

(This note said 116 → 2 until 0.4.32, and the "2" was the census of six corpora — moonbit_core was not in it, and it carries more findings than all six put together. The number was true of the corpora that were measured and false of the ones that were not. The history is in CHANGELOG.md.)

#File kinds

#Project structure

src/core      Span/Severity/Lens/Family(merge_group contract)/Frame + Family::advice
src/report    Report struct and rendering (union lens tags, vst frames)
src/flow      data-flow framework: CFG + four solvers (round-robin, the
              edge-transfer variant, and the before-node and forward work lists,
              run against each other in tests),
              basic blocks and the CFG over them,
              live variables (may, backward), the
              interval domain with widening, available expressions (must,
              forward — the dual reading of the same solver), constant
              propagation (the same lattice, read over a CFG), the call
              graph (the whole-program graph, over the trait hierarchy),
              and the pointer analysis read three more times: with a context
              (call-site / object), with a scope (on demand), and without a
              heap at all (access paths -- the storeless model)
src/sa        scan entry + aggregate() + mermaid_states() (public, library)
src/lexer     MoonBit lexer frontend
src/parser    MoonBit syntax → ast
src/ast       MoonBit abstract syntax
src/walk      structural inspection: binding tables + structural findings
src/types     type inspection: Ty/Ty?/Sig inference
src/interp    behavior inspection: AbsVal lattice + dispatch + virtual stacks
src/pipeline  assembly: run the three inspections + merge_group merge
src/moonfiles the other file kinds: .mbt.md per-block three-inspection / .mbti
              interface audit / .mbtp proof lint
src/statecheck use 2: generic machine-table audit (plain-data MachineSpec bridge)
src/samples   demo samples (embedded MoonBit source)
src/cli       executable entry (program demo + file-kind demo + sample machine audit)
src/jsoncli   the DeepSeek Harness JSON bridge

#The data-flow framework carries both directions

#And under the CFG there are basic blocks

#And under the blocks there is the three-address code the rules are written over

#And the arrow the deck prints in the footer: 3AC -> SSA

if e goto L1
goto L2
x₀ = 0
goto L3
x₁ = 1
x₂ = ∅(x₀,x₁)
y = x₂ + 7

SSA-COST	files=208	unreadable=0	functions=961	converted=5	partial=956	declined=5080	…

#Verification

moon check --target all --deny-warn   # 0 errors, 0 warnings (js / native / wasm / wasm-gc)
moon test --deny-warn                # 1600/1600 on wasm; 1458/1458 on js and wasm-gc
moon run src/cli                     # program demo + file-kind demo + sample machine audit

#The one release entry point

powershell -NoProfile -ExecutionPolicy Bypass -File _verify\release.ps1

moon fmt --check
moon check --deny-warn
moon test --target js
moon test --target wasm
moon test --target wasm-gc
moon build --target wasm
moon build --release --target wasm
the host contract of the artifact (what a user's toolchain must supply)
grammar probe control (its verdicts can go red)
self-scan (own source)
ssa cost (own source)
README links, anchors, versions and counts
gate roster: self-test (seven injected defects must be caught)
gate roster: one harness, one list, and a count that matches
the shared harness: the INCONCLUSIVE verdict, shown to go red
proof contracts: no false #proof_pure
package contents: the junk stays out, the evidence stays in
notice labels: a scope limit is a notice, a defect is an error
the family roster: one id each, contiguous, and reversible
frame audit: a region silences the bindings it could have read, and no others
match arms: the arms are read, the findings are true ones, and the fallback is exact
published self-scan self-test
published package self-scan
the notice reconciliation can go red (a real defect is seen)
corpus SUMMARY vs pinned baseline
per-function census vs pinned baseline
per-function census control (the files are READ by moon check)
the behavior lens: measured against its own header
the region suppression: what it hides, measured and pinned
the reach of the `raise?` construct, measured and pinned
the premises of the 0505 porting plan, measured
the notice flood: which notices deserve a line, measured
the three bandit transfers: measured, not asserted
the confidence demotion: measured, not asserted
the transfer scope: the requirements document, the three rows, and where they landed

#What the three transfers were asked for

#Formal verification (moon prove)

The command does not run green today, and the reason is measured. moon prove src/core --why3-config .why3.conf fails with unbound type symbol 'map'. src/core grew IfaceSymTab on 2026-10-08 — a struct whose fields are Map[String, Bool] — and the toolchain's proof prelude has no Map theory, so the generated Why3 file declares map int bool and neither moon prove nor why3 can load it. The 19 lemmas never touch IfaceSymTab: it is the package that is proved, and the package carries the type. The fix is to move IfaceSymTab out of the proof subject, and that changes this package's public API (@core.IfaceSymTab is exported), so it is a version-line decision rather than a patch.

Two #proof_pure annotations were also false: on path_tail and unqualified, whose bodies build a StringBuilder, which the prover rejects (error 4207). One false annotation stops the whole file from proving, and both of those arrived on 2026-10-09. They are removed, and _verify/check_prove_contracts.ps1 now fails the release if any #proof_pure body is one the prover rejects.

#Release history

#Contributing

1. Fork the repository and create a feature branch.
2. Add tests for new functionality.
3. Run the release gate and make it green:

   powershell -NoProfile -ExecutionPolicy Bypass -File _verify\release.ps1

4. Open a pull request.

#License

#References

• MoonBit Language Guide
• moonbitlang/core — the pinned corpus
• moonbitlang/parser@0.4.3 and moonbitlang/lexer@0.4.2 — the toolchain's own grammar, cross-checked against
• riantr/pyroduct — the reference consumer of the machine-table audit
• skills.mooncakes.io — the published skill
• Nanjing University, Static Program Analysis (Yue Li, Fall 2026) — the lecture series this tool's analyses follow; the map of what this tree implements is in _verify/NARRATIVE.md §0564