aptos-labs / aptos-core

Aptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.
https://aptosfoundation.org
Other
6.18k stars 3.64k forks source link

[Feature Request][move-compiler-v2] Invariant checking pass for stackless-bytecode as used in V2 compiler #11958

Open brmataptos opened 8 months ago

brmataptos commented 8 months ago

🚀 Feature Request

The V2 compiler has code which is making assumptions about invariants in the program IR which are currently true within the compiler but are not enforced by any mechanism. These should be documented, but even better, should be checked by an invariant checker which can serve as the documentation. Checks should have comments linking to code that makes use of these invariants so that if they are ever changed that code can be changed.

For example:

Until this is implemented, feel free to add or clarify invariants on this issue. After that, we can have an invariant checker pass to add new assumptions to.

fEst1ck commented 8 months ago

Critical edge processor is expecting that no abort action is used in call instructions.

fEst1ck commented 8 months ago

No duplicate labels; cf. https://github.com/aptos-labs/aptos-core/pull/11894#discussion_r148324750

This is likely also assumed by the control flow graph builder.