#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.
• ✅ 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.33

import {
  "riantr/moonbit_static_analysis@0.4.33",
}

#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.33_0.1.20260920_20261009T155222Z.mmd
moonbitlang-core_0.1.20260920+7d59c7ec9_0.1.20260920_20261009T051925Z.mmd
tree_unknown_0.1.20260920_20261009T051511Z.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	...\CI/pof/pkg.generated.mbti
PARTIAL	.mbt	defects=2	notices=1	read up to line 36, 57 after it not shown	...\CI/pof/aggregator.mbt
12:3 - error: ... (UndefinedName) [behavior]
PARSED	32/107 files understood (29.9%); 75 more read only up to their first parse error
SUMMARY	files=107	parsed=32	actionable=57	notices=211	unreliable=15759	withheld=6769	total=16027	(actionable+notices+unreliable = total; withheld ⊆ unreliable)

• 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.
• 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.

#Coverage and limits

#What this tool does not compete with

#The constructs the frontend reads past

#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 58 actionable findings, where the module view reports 33. Not one of the 58 is a defect in the analysed code.

family	n	what the lens claimed
A	12	a hex float literal (0x1.0p1023) is not read, so its exponent part is reported as an undefined name
B	5	a BigInt literal's N suffix (0N) is not read
C	6	== between two arrays
D	3	Int + Char and List + List
E	3	* on a struct
F	9	a name the analyzer cannot see — a sibling-file helper, a type parameter's method, an internal API absent from the .mbti index, a module qualifier
G	11	unreachable code — the lens's own claim about the code
H	2	a local assigned and never read — the lens's own claim about the code
I	1	abs on a Double
J	1	* on two function values
K	3	a local call with a named argument
L	2	the documented #doc(hidden) limit

"Accepted" is measured, not assumed. moon check --target all on moonbitlang/core reports exactly one error, in json/README.mbt.md, and it is not one of the twenty-four files that carry a finding. 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 those files in a copy and requires the error back — 24 of 24.

The two 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 @locale.LocalePreferences::resolve is still reported as an undefined function in proton 0.3.4. 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/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

#Verification

moon check --target all --deny-warn   # 0 errors, 0 warnings (js / native / wasm / wasm-gc)
moon test --deny-warn                # 1163/1163 on wasm; 1083/1083 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

#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