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

…le_member_types/, modules/, mutate_tests/, and mutation/ - Migrated linker_tests/, method_decorators/, module_member_types/, modules/, mutate_tests/, and mutation/ - Most tests were bytecode verifier tests, with a few VM tests Closes: diem#9042

…nvariant 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.

To make it less verbose and more readable. Closes: diem#9053

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: Suppose we aim to unify `T1 [X0, X1, ..., Xm]` vs `T2 [Y0, Y1, ..., Yn]`, where `T1` and `T2` are types while `X`s and `Y`s are type parameters that show up in `T1` and `T2`, respectively. We want to find all instantiations to `<X0, X1, ..., Xm>` such that for each instantiation `(x0, x1, ..., xm)`, there exists a valid instantiation `(y0, y1, ..., yn)` which makes `T1` and `T2` equivelant, i.e., `T1<x0, x1, ..., xm> == T2<y0, y1, ..., yn>`. We put all these instantiation in a set denoted as `|(x0, x1, ..., xm)|` and this algorithm is about finding this set of instantiations. // algorithm description The algorithm works by finding all instantiations for `X0` first, and then progress to `X1`, `X2`, ..., until finishing `Xn`. - unify `T1 [X0, X1, ..., Xm]` vs `T2 [Y0, Y1, ..., Yn]`, get all possible substitutions for `X0`, denoted as `|x0|` - for each `x0 in |x0|`: - refine `T1` with `x0` - unify `T1 [X0 := x0, X1, ..., Xm]` vs `T2 [Y0, Y1, ..., Yn]`, get all possible substitutions for `X1`, denoted as `|x1|` - for each `x1 in |x1|`: - refine `T1` with `x1` - unify `T1 [X0 := x0, X1 := x1, ..., Xm]` vs `T2 [Y0, Y1, ..., Yn]`, get all possible substitutions for `X2`, denoted as `|x2|` - for each `x2` in `|x2|`: - ...... The process continues until we reach the end of `Xn`. After which, the algorithm should have collected all the legal instantiation combinations for type parameters `<X0, X1, ..., Xm>`. // 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. Closes: diem#9056

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 ihe bytecode dumps with `bytecode_{step_number}_{step_name}.bytecode`. Closes: diem#9052

Closes: diem#8980

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: ```rust /// 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 unction and generic code. 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. Closes: diem#9072

Closes: diem#8528

- 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 Closes: diem#9073

Closes: diem#9079

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_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, ...) This PR defines `is_txn_signer`, and replaced `is_signer` with it because the previous implementation of `is_signer` didn't fit for purpose. Closes: diem#9025

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: 1) With the option `--boogie-poly`, the instrumenter will instrument *instantiated* invariants in the *generic* function (and the generic instance is the only function instance). 2) 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 1) instrumentation, 2) monomorphization, and 3) 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. Closes: diem#9077

- 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 Closes: diem#9078 Closes: diem#10675

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

Commits on Jan 4, 2023