0xMiden / 0xMiden/compiler

Make MASM advice taint analysis usable on the miden-vm core library

Ouverte
#1,209 1 commentaire 0 réactions 0 personnes assignées Voir sur GitHub
Langage dominant
Rust
Étoiles
115
Forks
84
Merge moyen
1 j 8 h
PR mergées (30 j)
15

Description

## Problem

[compiler PR 1135](https://github.com/0xMiden/compiler/pull/1135) introduced MASM-to-HIR lifting and `AdviceTaintAnalysis`. We would like to use that pass from `miden-vm` CI, as in [miden-vm PR 3052](https://github.com/0xMiden/miden-vm/pull/3052), rather than keep a separate MASM lint stack.

We can call the compiler APIs and the pass works on small MASM projects. It does not run on `miden-vm`'s core MASM library because disassembly fails before the taint pass gets a HIR world.

## What we tried

We built a small external tool against compiler commit `53d39713160b4d8651dc7979e8eac5ec1754534e`. It calls:

- [`disassemble_project_target_from_path`](https://github.com/0xMiden/compiler/blob/53d39713160b4d8651dc7979e8eac5ec1754534e/frontend/masm/src/lib.rs#L149-L162)
- [`DisassemblerConfig { infer_missing_signatures: true }`](https://github.com/0xMiden/compiler/blob/53d39713160b4d8651dc7979e8eac5ec1754534e/frontend/masm/src/lib.rs#L41-L48)
- `AnalysisManager::get_analysis::()`, matching the compiler's own [`analyze` stage](https://github.com/0xMiden/compiler/blob/53d39713160b4d8651dc7979e8eac5ec1754534e/midenc-compile/src/stages/analyze.rs#L40-L50)

[`AdviceTaintAnalysis`](https://github.com/0xMiden/compiler/blob/53d39713160b4d8651dc7979e8eac5ec1754534e/dialects/hir/src/analyses/advice_taint/mod.rs#L38-L89) exposes the public findings/diagnostic surface we need.

This works on a tiny MASM project where `adv_push` flows into `u32wrapping_add`.

Directly passing `crates/lib/core/asm/miden-project.toml` fails earlier, while parsing `mod.masm`, because the core library root uses module-index syntax:

```masm
pub mod collections
pub mod crypto
...
```

As a workaround, we generated a temporary adapter project:

- keep namespace `miden::core`
- write a synthetic `lint_root.masm`
- copy non-index `.masm` files from `crates/lib/core/asm`
- skip files containing `pub mod`
- run `disassemble_project_target_from_path` on the generated manifest

That got past the `pub mod` parse failure. The adapter copied 32 MASM modules and skipped 11 module-index files.

The next failure is signature inference:

```text
if branches leave different inferred stack depths at SourceSpan { ... }: then=4, else=10
```

Per-file probing showed the same shape more broadly: 4 non-index core modules lifted, 28 failed. The failures were missing cross-module signature metadata, stack/type inference failures, or hard aborts when one procedure could not be inferred.

## Where it fails today

`AdviceTaintAnalysis` runs on HIR. If MASM-to-HIR disassembly aborts, there is nothing for the pass to analyze.

The current inference path hard-errors when branch exits have different inferred stack depths in [`infer_if`](https://github.com/0xMiden/compiler/blob/53d39713160b4d8651dc7979e8eac5ec1754534e/frontend/masm/src/infer.rs#L612-L638). The project lifter then treats failed inferred signatures as a project-level failure in [`infer_missing_signatures`](https://github.com/0xMiden/compiler/blob/53d39713160b4d8651dc7979e8eac5ec1754534e/frontend/masm/src/lift.rs#L287-L325).

That is reasonable for compilation. It is too brittle for linting, where partial coverage plus explicit skipped-procedure reasons is useful.

## Useful model from miden-vm PR 3052

[miden-vm PR 3052](https://github.com/0xMiden/miden-vm/pull/3052), at commit [`152186a644c29f8a8746d614ca83fb69b4993876`](https://github.com/0xMiden/miden-vm/commit/152186a644c29f8a8746d614ca83fb69b4993876), is not the implementation we want to keep forever. It does show the pieces that made this analysis work against the VM core library.

The CLI is a developer tool over paths and library roots, separate from released crates: [`masm-lint/main.rs`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-analysis/src/bin/masm-lint/main.rs#L10-L20).

The parts worth mirroring upstream are:

- [`ProcSignature::Known | Unknown`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/signature/domain.rs#L37-L61), with required input depth, outputs, net effect, preserved inputs, and dependencies
- a provenance stack that separates preserving reads from side-effecting reads: [`ProvenanceStack`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/signature/domain.rs#L213-L280)
- call-summary application that preserves pass-through input provenance: [`apply_signature`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/signature/domain.rs#L292-L339)
- bottom-up call graph inference that records `Unknown` instead of aborting: [`infer_signatures`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/signature/analysis.rs#L11-L29)
- branch handling that marks unsupported branch shapes as `Unknown` for that procedure: [`visit_if`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/signature/analysis.rs#L155-L180)
- stack-effect metadata with `pops`, `pushes`, and `required_depth`: [`StackEffect`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/signature/effects.rs#L8-L21), with representative effects in [`effects.rs`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/signature/effects.rs#L127-L229)
- workspace loading for path-based invokes: [`Workspace::load_dependencies`](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/tools/masm-lint/crates/masm-decompiler/src/frontend/workspace.rs#L60-L77)

This lint work also found MASM that needed real fixes. For example, PR 3052 adds [`u32assert` checks before advice-derived pointers are used as memory addresses](https://github.com/0xMiden/miden-vm/blob/152186a644c29f8a8746d614ca83fb69b4993876/crates/lib/core/asm/collections/sorted_array.masm#L29-L50) in `collections/sorted_array.masm`. The ask here is not to hide those issues. It is to let the compiler reach the analysis stage and report them.

## Suggested upstream work

1. Support `pub mod` module-index roots, or expose a public project-resolution API that lets a lint tool avoid a synthetic root.

2. Add a lint-oriented signature summary layer before typed HIR lifting. It should return `Known` or `Unknown` per procedure instead of failing the whole project.

3. Make project-scope inference best-effort. Return lifted procedures, skipped procedures, and skip reasons.

4. Centralize MASM stack-effect metadata with correct `required_depth` semantics for non-consuming reads such as `u32assert*`, `u32test*`, memory ops, Merkle ops, advice ops, and stack-family ops.

5. Resolve cross-module MASM calls from source modules inside the same project or library root before treating them as missing external metadata.

6. Consider an analysis-first public API for external CI tools, for example:

```rust
let result = analyze_masm_project_for_advice_taint(manifest_path, config, context)?;
for diagnostic in result.diagnostics() { ... }
for skipped in result.skipped_procedures() { ... }
```

The exact API can differ. The important part is that a CI tool can get taint diagnostics and coverage/skipped-procedure information without requiring a fully successful compile-oriented lift.

Guide de contribution

Ouvrir le guide de contribution

Piste de recherche

The issue is about enabling the MASM advice taint analysis to work on the miden-vm core library. Start by examining the compiler's frontend/masm/src/lift.rs and infer.rs to understand the current signature inference that fails. Look at the miden-vm PR 3052's masm-decompiler crate for the signature analysis model. The goal is to modify the compiler's disassembly and inference to be best-effort for linting, returning known/unknown procedures instead of aborting. Test changes by trying to run the analysis on the core library's asm files.

Rédigé par le modèle d'indexation à partir du texte de l'issue.

Évaluation

Stack technique
rust
Domaine
compilers, devtools
Type d'issue
Fonctionnalité
Difficulté
4/5
Temps estimé
3-5 jours
Activité
Calme
Clarté
Plutôt claire
Accessibilité débutants
35/100

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.