Move : [transactional-tests] More migrated tests - (128)

[rutkaracn]

[transactional-tests] More migrated tests #9042

Motivation

• Migrated linker_tests/, method_decorators/, module_member_types/, modules/, mutate_tests/, and mutation/
• Most tests were bytecode verifier tests, with a few VM tests
• Nearly done migrating bytecode verifier/VM related IR tests to transactional tests.

Test Plan

CI/CD testcases covered.

[move-prover] minor improvements to the verification analysis pass #9053

Motivation

Two improvements are made in the new verification analysis pass:

• [move-prover] only verify functions that directly modifies a target invariant the prior behavior is to verify functions that directly accesses a target invariant, which unnecessarily leaves many functions to be marked as verified.
  NOTE: only memory modifications cause global invariants to be asserted; memory accesses without modification leads to assumption of global invariants only, but not assertions.
• [move-prover] improve error reporting on invariant suspension pramgas. The prior errors are too verbose.

Test Plan

• CI/CD
• This new pass is not turned on as of now. It will be made as default in a later PR.

[move-prover] algorithm for progressive instantiation #9056

Motivation

This algorithm deals with finding a complete set of instantiation combinations for all type parameters when unifying two types.

// problem definition
The algorithm is encapsulated in struct TypeInstantiationDerivation and is not conceptually hard to understand.

// algorithm description
The algorithm works by finding all instantiations for X0 first, and then progress to X1, X2, ..., until finishing Xn.

// other notes

• The implementation has a bit of fine-tuning rooted by the fact that sometimes we want to treat a type parameter as a variable (i.e., participate in type unification) while in other cases, we want to treat a type parameter as a concrete type (i.e., do not participate in type unification).
• We also have a fine-tuning on whether we treat a type parameter that does not have any valid instantiations as an error or remains as a concrete type parameter. This is rooted by the differentation of type parameters in function vs type parameters in a global invariant. Essentially, all type parameters in a global invariant must be instantiated in order for the invariant to be instrumented. But not all function type paramters need to be instantiated.
• This is not the most efficient algorithm, especially when we have a large number of type parameters. But a vast majority of Move code we have seen so far have at most one type parameter, so in this commit, we trade-off efficiency with simplicity.

Test Plan

CI/CD testcases were covered.

[move-prover] dump bytecode and result in output dir #9052

Motivation

Previous dumping location is at the first Move source location, which may pollute the source directories. Furthermore, if we pass a directory as the first source location, the process will panic.

This commit changes the default output location for --dump-bytecode to the parent directory of the output.bpl file, and format the bytecode dumps with bytecode_{step_number}_{step_name}.bytecode.

Test Plan

• CI
• cargo run -p move-prover -- <dir-name>/<file-name>.move --dump-bytecode. Note that the bytecode dumps are generated at the current work directory instead of under <dir-name>.

[move prover] Arithmetic mutations #8980

Motivation

This change updates two components of the mutation tester. First, it adds the sub-add, mul-div, and div-mul mutation operators. Second, it provides a fix to needing to provide addresses when working on the Diem framework.

Test Plan

CI/CD testcases were covered.

[move-prover] an analysis pass for the global invariants #9072

Motivation

This pass collects information on how to inject global invariants into the bytecode of a function.
The end result of this analysis is summarized in two structs:

/// A named struct for holding the information on how an invariant is
/// relevant to a bytecode location.
struct PerBytecodeRelevance {
    /// for each `inst_fun` (instantiation of function type parameters) in the key set, the
    /// associated value is a set of `inst_inv` (instantiation of invariant type parameters) that
    /// are applicable to the concrete function instance `F<inst_fun>`.
    insts: BTreeMap<Vec<Type>, BTreeSet<Vec<Type>>>,
}

/// A named struct for holding the information on how invariants are relevant to a function.
struct PerFunctionRelevance {
    /// Invariants that needs to be assumed at function entrypoint
    /// - Key: global invariants that needs to be assumed before the first instruction,
    /// - Value: the instantiation information per each related invariant.
    entrypoint_assumptions: BTreeMap<GlobalId, PerBytecodeRelevance>,

    /// For each bytecode at given code offset, the associated value is a map of
    /// - Key: global invariants that needs to be asserted after the bytecode instruction and
    /// - Value: the instantiation information per each related invariant.
    per_bytecode_assertions: BTreeMap<CodeOffset, BTreeMap<GlobalId, PerBytecodeRelevance>>,
}

A note about PerBytecodeRelevance : in fact, in this phase, we don't intend to instantiation the function nor do we want to collect information on how this function (or this bytecode) needs to be instantiated. All we care is how the invariant should be instantiated in order to be instrumented at this code point, with a generic function (generic bytecode).

But unfortunately, based on how the type unification logic is written now, this two-step instantiation is needed in order to find all possible instantiations of the invariant. I won't deny that there might be a way to collect invariant instantiation combinations without instantiating the function type parameters, but I haven't iron out one so far.

Test Plan

CI/CD testcases were covered.

Add support for CRSNs #8528

Motivation

Bottom Commit

Implements CRSNs and the CRSN logic according to DIP-168. These changes have been approved in #8403.

Middle Commit

Adds support for CRSNs to mempool. In particular, updates needed to be performed in order to support:

• Processing of transactions in a non-blocking manner
• Eviction of transactions based on the LHS of the sliding nonce of the account, and not on the committed transactions sequence nonce (since this method does not work in the CRSN case).

I'm not that familiar with mempool, so there might be something I've forgotten that I need to change -- please let me know if that's the case. Also feel free to add reviewers if I've forgotten to add someone.

The general methodology for implementation here is:

• When a transaction hits mempool we determine if it is a CRSN or seqno transaction
• Validation will return both the LHS of the CRSN window and k
• Transactions will be removed from mempool if the transaction's seqnonce < the current LHS when a new transaction is added
• A transaction will be accepted to mempool if the transaction's seqnonce >= LHS
• A transaction will be considered for processing as long as it is >= LHS and < LHS + k
• On commit of a transaction, other transactions may be evicted from mempool based off of the LHS of the account at the time the transaction entered mempool.
  This adds a number of tests to verify the expected behavior for transactions with CRSNs.

Top Commit

Adds support for CRSNs to the prologue/epilogue.

Test Plan

CI/CD tetscases were covered.

[move] type layout generation from modules #9073

Motivation

This is the clone of #8968 just because I don't know how to commandar that PR.

Add code in the move-binary-format crate to create a MoveTypeLayout from a CompiledModule
In the cli, add new generate struct-layout command that leverages this functionality to dump layouts in YAML format
The eventual goal is to have the CLI spit out YAML that can be used directly by serde-generate to create typed struct bindings in any language supported by serde-generate
Added the error propagation comparing to ([move] type layout generation from modules #8968).

Test Plan

CI/CD testcases were covered.

[diem-framework] Port DiemTimestamp to unit tests #9079

Motivation

Ports the tests for DiemTimestamp to use unit tests. Adds additional tests for full coverage of the module.

TestPlan

CI/CD testcases were covered.

[move-prover] Rewrite the access control spec as two state invariants #9025

Motivation

This PR defines is_txn_signer, and replaced is_signer with it because the previous implementation of is_signer didn't fit for purpose (see the issue [Bug] issue with is_signer #9018).

The existing access control spec uses the schema application which is verbose. To simplify the access control spec and make it easier to read, this PR rewrites the existing access control spec as two state invariants with the new spec construct is_txn_signer_addr (and is_txn_signer).

This PR is mostly about cleaning-up the spec for the role-based access control in the Diem Framework. The next step is to look into the capability-based one (e.g., MintCapability, ...)

Test Plan

cargo test

[move-prover] an instrumentation pass for the global invariants #9077

Motivation

An instrumentation pass that consumes the information produced by the global invariant analysis pass and instrument the global invariants into the function.

The instrumenter supports two mode of operations, depending on whether the prover backend supports monomorphization or not:

• With the option --boogie-poly, the instrumenter will instrument instantiated invariants in the generic function (and the generic instance is the only function instance).
• Without the --boogie-poly option, the instrumenter will instrument instantiated invariants per each instantiation of a generic function (this is the traditional workflow). And this means that a function will have multiple instances for verification.

This is not exactly the plan we had before (and does not clearly adhere to the paper). The original plan is to go for option 1 first and defer the instantiation of functions to the mono pass. Therefore, the option 2 here is essentially a combination of

• instrumentation,
• monomorphization, and
• optimization (eliminating redundant expressions)

But option 2 does not completely solve the "type-dependent" code problem because the (move_to<T>, move_to<u64>) case still requires a second step of function instantiation and still requires the mono pass to perform such instantiation.

The main reason why we still have option 2 (and not only that, we made option 2 as default as of now) is three-fold:
1.I am uncertain of Boogie's monomorphization implementation matches the complexity of what we have done here.
2.I want to get at least the whole Diem Framework verifying again to test out the whole transformation pipeline, in order to boost our confidence.
3.Solving the move_to<T>; move_to<u64>; problem requires more than instantiation; we need spec language support as well to express the fact that the function will surely abort if T == u64 and may not abort otherwise.

With this final piece, we complete the new invariant instrumentation
pipeline (modulus the misaligned implementation plan mentioned above)
and the next PR will switch the pipeline into the new one and fix the
specs in the Diem Framework.

Test Plan

CI/CD tetscases were covered.

[transactional-tests] Migrate remaining VM/Bytecode verifier IR tests #9078

Motivation

• migrated remaining tests
• tests left over are either for the DF or the IR compiler itself
• Check for tokens after module or script in IR. Caused silent test failures

Test Plan

CI/CD testcases were covered.

[ankitkacn]

/canary

[bors-diem]

💔 Test Failed - ci-test

[ankitkacn]

/canary

[bors-diem]

💥 Tests timed-out

[rutkaracn]

/canary

[bors-diem]

☀️ Canary successful

[ankitkacn]

/land