0xMiden / 0xMiden/miden-vm

Perform stack effect analyses during assembly

Offen
#3,070 0 Kommentare 1 Reaktion 1 zugewiesene Person Beansprucht von @bitwalker Auf GitHub ansehen
assembly
Vorherrschende Sprache
Rust
Sterne
772
Forks
352
Ø Merge
1 T. 12 Std.
Gemergte PRs (30 T.)
93

Beschreibung

This issue is meant to track the implementation of a new stack effect analysis that would be applied during assembly, to catch various bugs that can arise in programs. This analysis is contingent on procedures being annotated with type signatures (currently optional, but we should explore making them required).

Without a type signature, the analysis can determine for a procedure:

* Whether a procedure is operand stack neutral (i.e. has no effects from the perspective of the caller), and if not, what those effects are, i.e. how many operands must be on the operand stack for it to succeed, and how many operands will be on the operand stack at exit.
* Whether the operand stack is in a sane state at join points in the control flow graph (i.e. the state of the operand stack at exit from `if.true`/`while.true` is equivalent regardless of which branch is taken).

In some cases, we may not be able to fully analyze a procedure due to missing information (e.g. a procedure is referenced by MAST root, but we do not have that procedure on hand; or a procedure is invoked dynamically, and we are unable to trace the callee operand to a known `procref`). In such cases, we'd at most produce an informational warning/lint about this, which could be silenced via `miden-project.toml`.

In the presence of type signatures, the analysis can be more precise (with the same caveat I just mentioned above):

* It can determine if a procedure is operand stack neutral after taking into account type signature information (i.e. arguments are expected to be consumed by the callee, results are expected as outputs). This can catch when internal state of the procedure accidentally leaks to the caller (i.e. some value deeper in the operand stack was not cleaned up); as well as when the procedure body requires more operands than it declares as arguments.
* It can trace the types of input operands and ensure that they are not incorrectly used.
* It can perform some basic type checking of procedure invocations, and ensure that results are not incorrectly used (e.g. a `u32` used where a `u64` is expected, or a `felt` used where a `u32` is expected without using `u32assert` to validate it).

Not only can this catch a lot of subtle mistakes in MASM code, it will also encourage us to tighten up semantics in places where analysis is currently intractable, for example:

* It is undefined behavior for the operand stack to be in different states depending on whether `while.true` evaluates the loop body or not - but we do not even warn about this currently, and there is absolutely no reason to allow it.
* It may be desirable to require that `dyncall`/`dynexec` specify the type of their callee, so that we can catch mistakes around indirect procedure invocation.
* We do not currently define a variable-length argument calling convention, but `execute_foreign_procedure` relies on dynamically-sized argument lists, and so its calling convention needs to be well-defined.
* We do not validate that procedure invocations adhere to the existing calling conventions

Some of details of these are orthogonal to stack effect analysis - but all of them are improved by it, or make it more precise.

Proposed design:

* Surface a bit more of the linker API and project assembly functionality, so that we can perform project context initialization and linking _without_ assembly. This allows us to reuse that part of the assembler for other tools.
* Implement a new `Linker::analyze(&self, root: GlobalProcedureIndex, analysis: A)` method, which performs some analysis `A`, by visiting the procedure graph of `root` in topological sort order. This facility would provide the basis for doing whole-program analysis, such as the stack effect analysis.

The `Analysis` trait would look something like:

```rust
pub struct AnalysisContext<'a> {
procedure: GlobalProcedureIndex,
linker: &'a Linker,
preserved_analyses: HashMap>,
}

pub struct AnalysisKey {
analysis: TypeId,
procedure: GlobalProcedureIndex,
}

pub trait Analysis {
type State: Sized;

fn analyze(&mut self, context: &AnalysisContext<'_>) -> Result;
}
```

* Introduce an operand stack data structure to be used during abstract interpretation, that has a notion of both value types and the underlying operand stack representation. The compiler currently has exactly such a data structure, which we use for analysis and codegen. I'd propose implementing more or less the same data structure in the assembler (the compiler one has some compiler-specific details in it, so they can't be shared, but it's not _that_ complicated anyway where duplication is a problem).
* Implementation of the stack effect analysis using abstract interpretation of a procedure. The analysis will receive the current procedure being assembled, including all its available metadata such as type signature; as well as the analysis state of all other procedures assembled so far. Since every procedure is assembled after the procedures it references, we're guaranteed that each procedure will have all available analysis it requires (though the analysis state for any given procedure may be indeterminate due to missing information). The analysis state at each operation, would be one of the following values:
a. `indeterminate(reason)`, i.e. we could not complete analysis because `reason`, where reason provides the specific corner case which prevented us from fully analyzing a procedure
b. `partial(operand_stack, inferred_signature)`, which indicates that we did not have a procedure signature available, and are attempting to infer the signature of the procedure via its stack effects. `operand_stack` is the current operand stack state, while `inferred_signature` carries the signature we've inferred up to that point.
c. `complete(operand_stack, inferred_signature)`, indicates that we had a procedure signature, and are checking that the declared signature and inferred signature are equivalent (in terms of their stack effects).
* Linting would be implemented in the form of an analysis that evaluates some number of lint rules, and emits diagnostics. Lint rules would be named, and expressed as two parts: predicate and matcher. The predicate is evaluated to determine whether or not the rule should be applied at all (based on global configuration). The matcher is a function that receives the current operation context, as well as the before and after analysis states, and returns `Result<(), Report>`, where `Ok` means the rule did not match, and `Err` means that the rule matched and a diagnostic was produced.

I've been working on something similar in my spare time recently, as part of an effort to disassemble MASM into HIR (our compiler IR), so that I can use the much more sophisticated analysis framework in the compiler for LSP diagnostics - but if we implement this part in the assembler, not only can we use it as validation of assembled programs, but downstream use cases like mine can focus

Beitragsleitfaden

Beitragsleitfaden öffnen

Bewertung

Dieses Issue wurde noch nicht bewertet.

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.