This repository has been archived by the owner on May 4, 2024. It is now read-only.
thanks #1089
Open
thanks #1089
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* [move-stdlib] fix vector docs * generate the docs
…ge#420) * [move-compiler] implement the `#[verify_only]` attribute As title suggests, this is an implementation of the `#[verify_only]` annotation that can be used in a way that is similar to `#[test_only]`. The semantics of `#[verify_only]` is the following: Any AST element (in both source of in the library definitions) annotated with the `#[verify_only]` attribute will be removed after parsing, unless the `verify` flag is set when invoking the compiler. `#[verify_only]` has no interaction with unit-testing related attributes such as `#[test]`, `#[test_only]` or `#[abort]`, `#[expect_failure]` etc. A function that is marked `#[verify_only]` has no knowledge of that a `#[test_only]` function might exist, unless both `verify` and `testing` flags are set when invoking the compiler. A large portion of this PR is in fact an refactoring of the `#[test_only]` implementation as both `#[test_only]` and `#[verify_only]` involves filtering AST nodes. This common functionality is abstracted and placed into the `move-compiler/parser/filter.rs` file, and in particular, as a `FilterContext` trait which can be customized as needed. * [move-compiler] new test cases for the `#[verify_only]` annotation
* update rust 1.63 * remove clippy::single-char-pattern * remove clippy::needless_late_init * remove clippy::needless_borrow * remove clippy::unwrap_or_else_default * remove clippy::derivable-impls
Modules got changed to lowercase letters.
…guage#430) Boogies does not always give an augmented execution trace. Handle such cases gracefully instead of giving out a mysterious error.
* Support loop unrolling in Move prover backend * Remove debug line
…anguage#429) * [move-model] re-use the address map produced by move compiler When constructing address aliases for the move model, use the `NamedAddressMap` produced by the compiler instead of a handwritten one. This allows move-model (and hence move-prover) to work even when source and deps paths are supplied in directory format (instead of via the package system). * fixup! [move-model] re-use the address map produced by move compiler
* [book and move-book-zh] update vector * supplement and determine the translation of vetor
* [move-book-zh] add contributing guide * add comma specification * update readme and contributing * fix * add a prompt * add comma and colon specifications
…nguage#443) Adding new native functions to a running chain is cumbersome because a 2-staged roll out is needed: before the Move code with the new function can be loaded into a given node, that node must have upgraded so the native functions is available. We would rather like to control such upgrades by on-chain flags, that is allow an unbound native function but avoid calling it before we know the native code has been rolled out. This PR adds a feature flag `lazy_natives` to the VM which if set, allows unbound native functions during bytecode verification time, but instead only errors if such a function is actually called. The change is safe because the linkage check is only postponed, not skipped. There is no performance implication because the current code loader does not cache resolution of natives, so that happens anyway already at execution time again.
The vm used the fact that a native function resolved also to identify whether a function is native or not. This decouples this decision to make the lazy binding produce the expected error.
* explain error when publishing in bundle mode explain the error generated when publish multiple modules in bundle mode Co-authored-by: JerryKwan <Jinzhong.Guan@gmailcom>
) This commit introduces preliminary support on verifying code that uses reflection to obtain type information at runtime. We use a hyperthetical (and intrinsic) call `fun extension::type_info::type_name<T>(): String` that returns the type name of `T`. Being a pure function, this reflection function can be called from the spec context as well. In handling reflection, the high-level idea is: - if `T` is statically known when `type_name<T>` is called, replace this call with a constant - if `T` is unknown, full or partially, when this call is invoked, replace the `type_name` for `T` with a fresh variable `var #T_name: Vec int`, in particular: - if `T` is fully unknown, `type_name<T>` will be `#T_name` - if `T` is partially unknown (e.g., `type_name<vector<T>>`), then the `type_name` call will be replaced as `ConcatVec(ConcatVec("vector<", #T_name), ">")` This instrumentation happens at the translation phase, on the way to Boogie.
…ve-language#462) The `type_of` primitive is another type reflection feature supported by the move prover: At its core, the `type_of` function returns information about a user-defined struct type: ```move struct TypeInfo has copy, drop, store { account_address: address, module_name: vector<u8>, struct_name: vector<u8>, } public native fun type_of<T>: TypeInfo; ``` This is similar to the `type_name` feature with the following complication: - `type_of<T>` will panic if `T` is not a user-defined struct type. `type_of<vector<bool>>` will cause the Move VM to abort. This needs to be captured by the prover as well. On the other hand, `type_name` will never panic and will always return a canonical representation of the passed in type tag. - `type_of<T>` does not care about the type arguments of the struct type. E.g., if there is a struct `Foo<K, V>`, then both `type_of<Foo<bool, int>>` and `type_of<Foo<int, bool>>` will return exactly the same information. With that said, `type_of` is handled in a similar way to `type_name`: - If the type argument `T` is statically known, all fields of the `TypeInfo` struct will be pre-determined as constants. However, there is a caveat when `T` is not a user-defined type in spec function context. - If the type argument `T` is symbolic in the verification context, we rely on the following newly introduced fresh variables to model the information of `T`, including - `#T_is_struct: bool;` to model whether `T` is a user-defined struct - `#T_account_address: int;` - `#T_module_name: Vec int;` - `#T_struct_name: Vec int;`, for these variables, the name says all In the bytecode context (i.e., Move function context), a `type_of<T>` function call is translated as: ``` if (!<predicate_is_struct>) { call $ExecFailureAbort(); } else { retval := <struct_info_variable>; } ``` In this way, we still capture the fact that `type_of<T>()` may abort when `T` is not a struct type. However, in spec function context, due to the fact that a spec function is essentially an expression. The rewriting mechanism does not allow us (or at least it is not easy) to instrument an additional check that `T` must be a struct type. In light of this, the `<is_struct>` flag is ignored and we assume `T` passed in is a struct.
…age#461) Explain how feature requests should be created and how they progress, add graveyard of features that were not accepted.
…ge#467) * [move-prover] switch src/dst pair for the havoc operator The `havoc` operator has been modeled as: ``` () := havoc($i); ``` i.e., 0 output and 1 input. This commit switches the src and dest pair into ``` $i := havoc(); ``` This is in fact closer to the semantic of `havoc`: it re-assigns the target with an arbitrary value. therefore, the target should be on the receiving end. This has important effect on our program analysis passes, especially reaching definition analysis and live-var analysis.
Parsing pragma properties in the same declaration used to be stateless, i.e., each property is not aware of other properties listed in the same declaration. This commit enables this stateful awareness.
…guage#906) * enable bytecode compilation in move-package * remove unused import * fix error message
…guage#918) Previously, a type instantiation w/ >1 type parameters was printed without a comma separator (e.g., `S<u64bool>` instead of `S<u64,bool>`for `S<T1,T2>` instantiated with `u64` and `bool`). This PR adds a comma separator and a test.
…rated boogie file (move-language#958) A type parameter that has the key-ability can have a memory space. This PR makes Prover declare the memory variables for type parameters in the generated boogie file.
The reporting logic here attempted to suppress warnings in dependencies, but this was a bit too aggressive and ended up suppressing everything. Changing the logic to report all warnings, particularly given that this is an experimental analysis + the "report all" configuration is needed to reproduce the results from the robust safety paper.
…uage#950) * [verifier] limit the number of back edges * [verifier] fix incorrect error code for per-module back edge limit check * copyloc-pop test (move-language#54) * [gas] allow natives to read the gas balance * [bytecode-verifier] Add metering logic and apply to absint based analysis (move-language#58) This adds a simple meter to the bytecode verifier which counts the number of abstract operations performed and can enforce a limit. The meter is for now only connected to locals and reference analysis, but plumped to all phases of the verifier so they can easily make use of it. A set of test cases have been added which exercise the new meter for a number of known pathological cases. PR history: - Add metering in type safety, to capture cost of very large types. This reduces timing of large_type_test to 1/4 - Adjusting max metering units upwards and adding a new sample which needs it - Addressing reviewer comments - Add links to security advisories, and verify that all are covered. - Switching metering granularity from function to module. - Adding non-linear growing penalty to using input refs x output refs relations (bicycles), for dealing better with `test_bicliques`. Adding printing size in benchmarks. * [bytecode verifer] Adjust metering to decrease runtime of some tests. (move-language#62) Specifically the test below now runs in 1/2 of the time. This adjustment appeard useful because the overall time allocation had to be increased to 8000 million units in production. Adjusted this as the default here too. ``` --> test_merge_state: verification time: 59.414ms, result: CONSTRAINT_NOT_SATISFIED, size: 63kb ``` Also adjusts the default to what aptos uses now in production. * [bytecode verifier] Meter type instantiations (move-language#64) Instead of just metering size of types on the operand stack, also meter size of type instantiations in calls and other places. This e.g. capture the size of types in calls like `f<T>()`, where the type does not appear on the operand stack. --------- Co-authored-by: Victor Gao <vgao1996@gmail.com> Co-authored-by: Teng Zhang <rahxephon89@163.com>
"At the end of a function (when `Ret` is reached), *no local* whose type is of resource kind must be empty, i.e., the value must have been moved out of the local." I suppose that should be *any local* instead.
- Removed incorrect overflow guard - Added tests
Fix constant warning in compilation: INCLUDING DEPENDENCY MoveStdlib BUILDING BasicCoin warning[W10007]: potential issue with attribute value ┌─ ./sources/BasicCoin.move:94:24 │ 94 │ #[expected_failure(abort_code = 2)] // Can specify an abort code │ ^^^^^^^^^^ - Replace value with constant from expected module or add `location=...` attribute. │ │ │ WARNING: passes for an abort from any module.
Add lint and rename c_n to n.
Functions cannot start with '_'
move-language#1069) continue in while loop causes an unexpected error. Cherry-pick: MystenLabs/sui#13349 Bugfix: move-language#1068
* [move-stdlib] formatting the string module codes * generate the docs
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Motivation
(Write your motivation for proposed changes here.)
Have you read the Contributing Guidelines on pull requests?
(Write your answer here.)
Test Plan
(Share your test plan here. If you changed code, please provide us with clear instructions for verifying that your changes work.)