#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.38

import {
  "riantr/moonbit_static_analysis@0.4.38",
}

#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.38_0.1.20261023_20261024T060000Z.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	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=10114	printed=1162	aggregated=8952	1162 of them are printed per line: the ones that can hide a finding, and the low-confidence ones, which name a place. The other 8952 are counted by shape below
NOTICES	count=6148	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

#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 29 actionable findings, where the module view reports 10. 28 of the 29 are constructs this frontend does not read or operators it does not model; the twenty-ninth is a genuine finding — a local assigned and never read in moonbit_labeler, and the first true defect this tool has published on any corpus.

family	n	what the lens claimed
C	6	== between two arrays
D	3	Int + Char and List + List
E	3	* on a struct
G	11	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

AND 21 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 21 carries the confidence low, and every one of them is a name the analyzer could not resolve.

THE MODULE VIEW COUNTS 18 OF THEM, AND IT IS NOT THE SAME 18. 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 19 and the module view 18, and only 15 of those are the same site. That is the same difference as the 29 against the 10 above, and the two views stay separate, not additive.

demoted 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
F	2	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
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 sixteen 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 — 16 of 16.

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                # 1330/1330 on wasm; 1204/1204 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