This repository has been archived by the owner on May 4, 2024. It is now read-only.
Pushing Aptos changes upstream #1066
Merged
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
GitOrigin-RevId: c218c01a35bb551a6fbd269b667c3c7aabca4352
GitOrigin-RevId: e28d32f58ea770797ed8e7e6c9fbd75724412950
If there's a generic, the Fat type parsing didn't use the type from the type arguments, which caused it to fail to parse. Now, this will take in the type arguments to properly parse the inputs. GitOrigin-RevId: ba8c0de4e81e23bbe88e7c90ea6356e4c20b5c24
GitOrigin-RevId: 8244cda0130337e8c864f6f6fbc33b0a510e97cf
This introduces the new type of patterns into the model. Patterns are like expressions but represent lvalues or matches. This is used to implement type checking of assignment. Lets also have been refactored to use patterns during checking, but this isn't yet pushed into the AST, which will be a larger breaking change. GitOrigin-RevId: d5c6a8139d96fb16c3fc8bc8d09aaeb28498c57c
GitOrigin-RevId: 51cc46a991d2e2e5445c591ef39da7975f60818a
…lver::Error) and introduce "dyn" instead of "impl" at boundaries (#7817) GitOrigin-RevId: 54f0ce8f8aabac0685174456139e7e2e2ea006cb
…er and simplifier This replaces the use of `LocalVarDecl` accross the model with the new `Pattern` type. This applies to `Block`, `Quant`, and 'Lambda` expression variants. It also removes some code which is currently not used in applications, namely the stackless bytecode interpreter, the spec simplifier and the flattener. While we are refactoring, we have better agility without this code. We can bring it back from git history later if needed. GitOrigin-RevId: a514e89e805b5a5d552c443dd5dad6b5ae117a03
GitOrigin-RevId: 70e6068d2c690209232dbf5896d7ac89496f228f
* refactor a bit * remove arc from VM * Fix is_resource_group * fix build error * temp * tmp * refactor * add utils * remove generic type params * remove unused * revert * fmt * Add new macro * undo changes * improve map_err * remove map_err GitOrigin-RevId: 41cf4715bbfd3a2d7862e810e12ebd1b5d87485d
This reverts commit 41cf4715bbfd3a2d7862e810e12ebd1b5d87485d. GitOrigin-RevId: 04e2662ad9d47b1ecebada305af5376a6575830a
GitOrigin-RevId: b6f79f71b373799d4b21c2e3180119e868320d62
* Revert "Revert "refactor a bit (#7918)"" This reverts commit 04e2662ad9d47b1ecebada305af5376a6575830a. * check * remove cache fallback GitOrigin-RevId: a26b2821feabdc36f83f19f5c16018335daf22a1
* Refactor resolver with metadata * Further refactor * fix api * fix module publishing * make get_resource member of MoveResolver trait * rename remote -> resolver * Address coments * another comment * make session just carry movevm * fix metadata mismatch GitOrigin-RevId: 0e3956259aa7c823e27e16f379d9e63233e6ed6f
GitOrigin-RevId: 0f9891e346180661375e65ef0e1800116cf7e8d7
…t error with storage error GitOrigin-RevId: ebd06050196e4900fe912983453d67f22143d3cb
This is a large refactor of the `move-model` to become independent of bytecode, and an essential step towards the new compiler. In Originally the move-model was designed to work from bytecode as generated by the Move compiler. As such it was input the prover, docgen, and other tools. This PR makes this dependency optional: - The model can still operate base off bytecode, supporting all exisiting use cases and tests. This is important for the incremental introduction of the new compiler infra. - In a new execution path enabled by this PR, the model can also operate without having bytecode as input. In this case, the model builder will completely compile the model from the Move sources. The focus of this PR is preparing the 2nd operation mode without breaking the first. This PR also removes a number of unused crates to simplify refactoring: - stackless bytecode interpreter - legacy read-write set analysis - legacy escape analysis GitOrigin-RevId: eecbcfc1c627048418a0e62e59aa8d69803cc6cd
Move `ChangeSet` and `AccountChangeSet` types are now generic. The motivation for this change is to avoid any particular representation being used to communicate changes. All Move code is fully compatible with the change, all old APIs are preserved. However, additionally session can take a hook which dictates how resources should be outputed. The hook is implemented as a callback which the user can pass on the adapter's side. GitOrigin-RevId: 1e6db1183ec924ca5fe5490e1fd4b571867c150e
GitOrigin-RevId: 65d160be3a168d5dd887eca0218261c881db8808
GitOrigin-RevId: a8ca28437a4ddb1e0f09d8621cf59a2f706c1011
* Add accurate resource group gas metering * Add accurate resource group gas metering * fix * add test * Correct feature version * change trait signature * Clear any resource cache after proloque * bump gas feature * add comment * fix trigger condition for build jobs * test loadtest * add improvement * Fix respawn session whatever that maybe --------- Co-authored-by: gerben <[email protected]> Co-authored-by: geekflyer <[email protected]> GitOrigin-RevId: 09359aa961e909699939783bd438e967ca381bdb
* fix apply schema * fix coin spec * fix trigger condition for build jobs --------- Co-authored-by: geekflyer <[email protected]> GitOrigin-RevId: aaadc26166e57780c01e566cedc1588ecadd9d78
This commit introduces a new fuzzer crate that hosts fuzz tests for aptos-core. The first version of the fuzzer includes these fuzz tests: - Move Bytecode Verifier CodeUnit and Mixed modules - Move execute entry function - Move MoveValue decorate/undecorate - Move MoveValue deserialize - Move Value deserialize - Signed Transaction deserialize GitOrigin-RevId: e267e3ed1f07e1f5a430256854dcff33e71c2263
GitOrigin-RevId: faff4ee44632e772ff6881d12eb5d2eabdf69566
* Fix aptos-labs/aptos-core#7932 Docgen should output attributes (#7932). Output attributes (e.g., #[view] or #[resource_group(scope = global)]) from docgen for move code. Currently only handles attibutes on Function, Script/Module, and Struct/Resource. Note that attributes are allowed on some other syntactic objects (address scope, use statement, const definition, spec), but how to format these usefully in docgen is unclear. for these in docgen is unclear. Also fix an unrelated bug discovered when adapting attribute_placement.move as a test of docgen: previously, only a single Module/Script per input file would be output in docgen. * Update move library docs with new docgen. --------- Co-authored-by: Brian R. Murphy <[email protected]> GitOrigin-RevId: bea5520c277d8e57982798a36c6b60c5aa8bee00
GitOrigin-RevId: 1e65e9703625693801fb335d83fc27690354c2c7
This creates a new crate `move-compiler-v2`, containing a few basic components: - A model of options and experiments for the compiler. This has been adapted from the Move-to-Yul compiler from last year. - A test driver which supports experiments, with a first smoke test to ensure basic functionality of the setup. - Top level entry function to call the compiler. It invokes the new compilation mode of the move-model, which types check and constructs an AST. After that is unimplemented. The PR also adds an additional entry point for the move-model to support the above. GitOrigin-RevId: 1b7b553f3682f1a2ae060e113b4720bfd0799d7e
GitOrigin-RevId: 66de618e4ddb823ca2c2aabaa3726a0e3a43a6eb
GitOrigin-RevId: f4a2a656156071dd162333924e4ec02732d8a27b
GitOrigin-RevId: ad4adbea8c95a82205f22d13058bca9cf433e543
GitOrigin-RevId: 54304af41e5b2d2d2aa5210c89f30ca1c98560ca
* initial commit * Support gas payer * Remove relics * Fix * Make verification know about gas payer bit * update comments * Remove merge conflict * Give MSB a good name * Reformat * improve * add comment * Fix spec GitOrigin-RevId: 6d4b49514f1fba0a23c2d515f67b7345ec7c1603
This allows --dev to be added to use the [dev-addresses] as well as updates that really confusing error message to match GitOrigin-RevId: 9b4c616057b234cad468bde2e8539004701752ca
GitOrigin-RevId: 8b5d8548721ad88b166440fb55558bf7d6e5c1cf
The previous dependent dependencies were using an incompatible changes with rust 1.70. This should fix it and condense some of the dependencies. GitOrigin-RevId: c67c15f5bbc5e8d7a65b7d9acabe3fad995f812d
GitOrigin-RevId: 9004a5157fba7380419661c9a223014142f8d646
This PR contains two test cases to show how vector theories might have
an impact on the prover's ability on proving complicated propositions
w.r.t vector, especially with heavy involvement of quantifiers:
- On test case `f1`:
- `BoogieArray` (the default vector theory) will given a verification
error with an inconsistent counterexample while
- `BoogieArrayIntern` and `SmtSeq` can prove the proposition
- On test case `f2`:
- `BoogieArray` times out while
- `BoogieArrayIntern` and `SmtSeq` can prove the proposition
GitOrigin-RevId: d3522e12878e7ffbf125cd55bb867ab07838e90e
GitOrigin-RevId: cb39784fad84d6ae32759f3056c9bf7ccddb4a21
…d fixing issues This ports the tests from the v1 compiler for name resolution into the v2 compiler and fixes related issues: - Add support for macros (`assert!`) which are expanded before type checking - Renames and extends the builtin function representation to capture all Move builtins - Distinguishing between symbols defined both in spec and impl or only one of those - Improve error messages - Fixes issues as needed to pass tests GitOrigin-RevId: 691b520464e2fa5927de5807713644a876f676e2
… inlined method. (#8867) Includes test case illustrating original bug (aptos-labs/aptos-core#8516) plus a number of tests to check corner cases of multiple inlining and recursive inlining. (Several failed without this fix.) Also replace panic!("ICE expected function parameter to be a lambda") with a more useful diag output. GitOrigin-RevId: ea19ce1b272e5e2e979057bd58990e76e6c4d03a
* [Spec] add spec to the math modules * Added `math8.move` as the Prover test GitOrigin-RevId: 3d281ad455bd5881c41ae86cd7982b1fa2092cbf
…nline fun declaration. (#8934) (#8958) GitOrigin-RevId: 564f66ad09f3fe26cfa10e63c834c2de69a7ca31
This ports some first batch of 100 test cases from the v1 compiler related to typing, and adapts the implementation to handles those scenarios correctly. - Adds the concept of _constraints_ to type unification. These are basically a first simple version of (for now) builtin traits. For example, a constant `0` has type `X where Constraint::SomePrimitive(u8,u16,..,u256)`. This was needed to match the behavipr of the v1 compiler regards inference related to constants, bu in a more general way. It was not needed previously in the specification language checker because there, we have a unified `num` type for integers. - Implements `&` class of operators in the checker, which weren't supported before. - Cleans up state of the `ExpBuilder` with an `ExpBuilderMode` type instead of multiple booleans. - Multiple smaller improvements, reporting additional errors, making error messages more clearer, etc. GitOrigin-RevId: c8e0581f9b8a8aa1888f118c881a8073d1e5172a
GitOrigin-RevId: c107cbeff4cad50f67ecc49997264bb526029666
* Add stack trace for invariant violation to error message * fmt GitOrigin-RevId: 91bf46d8d639abfce8e3bf5395fdd5dd347cb159
GitOrigin-RevId: 723e57b89a3d24bd94440ab0e0d2632512225751
…hecker This ports the remaining 200+ tests of the v1 compiler `typing` testsuite and refines the v2 compiler to handle those correctly. Major changes include: - Introducing ordering in type unification. This is necessary to deal with conversions like `&mut T` to `&T`. The general mechanism will allow us to have also other conversions if we need down the road. - Introducing a mechanism to define a default for type inference via constraints. If a type variable has no unique instantiation, then the default is chosen. For example, the default for integer constants is `u64`. - Implementing the remaining expansion AST constructs from the Move parser. All expression variants are now handled. With this, we should have a fairly feature complete and tested type checker. This doesn't do, however: - visibility checking (private/friend) - mutation checking (whether something which is mutated can be actually mutated) - ability (copy, drop, ...) checking - reference safety (borrow) checking Those phases have been merged partly into the v1 type checker. For the v2 compiler, the plan is to handle them on bytecode level, similar as in the bytecode verifier. GitOrigin-RevId: b69b4de30cd37f4ca6799c096b6c1069771ba3fd
GitOrigin-RevId: 9510d7896510c4bb179220acfd4bbaf70e544c2b
…erhaul the AST pretty printer for that. GitOrigin-RevId: d0a02371edfbe647d46f99f18e59458831ca3a91
rahxephon89
approved these changes
Jul 12, 2023
wrwg
force-pushed
the
to_move
branch
2 times, most recently
from
5b51997
to
5b4409b
Compare
This is a collection of commits submitted to the Aptos version of the Move tree.
vgao1996
approved these changes
Jul 12, 2023
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.
This is a collection of commits submitted to the Aptos version of the Move tree since April, bringing the
aptos-mainbranch up-to-date with the current state of Move at aptos.