-
Notifications
You must be signed in to change notification settings - Fork 3.7k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[move][stdlib] Implement mem::swap native move call
- Loading branch information
1 parent
2e349cf
commit ac25522
Showing
14 changed files
with
660 additions
and
10 deletions.
There are no files selected for viewing
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
1 change: 1 addition & 0 deletions
1
aptos-move/e2e-move-tests/src/tests/code_publishing.data/pack_stdlib/sources/mem.move
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
../../../../../../framework/move-stdlib/sources/mem.move |
1 change: 1 addition & 0 deletions
1
...-move/e2e-move-tests/src/tests/code_publishing.data/pack_stdlib_incompat/sources/mem.move
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
../../../../../../framework/move-stdlib/sources/mem.move |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,115 @@ | ||
|
||
<a id="0x1_mem"></a> | ||
|
||
# Module `0x1::mem` | ||
|
||
Module with methods for safe memory manipulation. | ||
|
||
|
||
- [Function `swap`](#0x1_mem_swap) | ||
- [Function `replace`](#0x1_mem_replace) | ||
- [Specification](#@Specification_0) | ||
- [Function `swap`](#@Specification_0_swap) | ||
- [Function `replace`](#@Specification_0_replace) | ||
|
||
|
||
<pre><code></code></pre> | ||
|
||
|
||
|
||
<a id="0x1_mem_swap"></a> | ||
|
||
## Function `swap` | ||
|
||
Swap contents of two passed mutable references. | ||
|
||
Move prevents from having two mutable references to the same value, | ||
so <code>left</code> and <code>right</code> references are always distinct. | ||
|
||
|
||
<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="mem.md#0x1_mem_swap">swap</a><T>(left: &<b>mut</b> T, right: &<b>mut</b> T) | ||
</code></pre> | ||
|
||
|
||
|
||
<details> | ||
<summary>Implementation</summary> | ||
|
||
|
||
<pre><code><b>public</b>(<b>friend</b>) <b>native</b> <b>fun</b> <a href="mem.md#0x1_mem_swap">swap</a><T>(left: &<b>mut</b> T, right: &<b>mut</b> T); | ||
</code></pre> | ||
|
||
|
||
|
||
</details> | ||
|
||
<a id="0x1_mem_replace"></a> | ||
|
||
## Function `replace` | ||
|
||
Replace the value reference points to with the given new value, | ||
and return the value it had before. | ||
|
||
|
||
<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="mem.md#0x1_mem_replace">replace</a><T>(ref: &<b>mut</b> T, new: T): T | ||
</code></pre> | ||
|
||
|
||
|
||
<details> | ||
<summary>Implementation</summary> | ||
|
||
|
||
<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="mem.md#0x1_mem_replace">replace</a><T>(ref: &<b>mut</b> T, new: T): T { | ||
<a href="mem.md#0x1_mem_swap">swap</a>(ref, &<b>mut</b> new); | ||
new | ||
} | ||
</code></pre> | ||
|
||
|
||
|
||
</details> | ||
|
||
<a id="@Specification_0"></a> | ||
|
||
## Specification | ||
|
||
|
||
<a id="@Specification_0_swap"></a> | ||
|
||
### Function `swap` | ||
|
||
|
||
<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="mem.md#0x1_mem_swap">swap</a><T>(left: &<b>mut</b> T, right: &<b>mut</b> T) | ||
</code></pre> | ||
|
||
|
||
|
||
|
||
<pre><code><b>pragma</b> opaque; | ||
<b>aborts_if</b> <b>false</b>; | ||
<b>ensures</b> right == <b>old</b>(left); | ||
<b>ensures</b> left == <b>old</b>(right); | ||
</code></pre> | ||
|
||
|
||
|
||
<a id="@Specification_0_replace"></a> | ||
|
||
### Function `replace` | ||
|
||
|
||
<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="mem.md#0x1_mem_replace">replace</a><T>(ref: &<b>mut</b> T, new: T): T | ||
</code></pre> | ||
|
||
|
||
|
||
|
||
<pre><code><b>pragma</b> opaque; | ||
<b>aborts_if</b> <b>false</b>; | ||
<b>ensures</b> result == <b>old</b>(ref); | ||
<b>ensures</b> ref == new; | ||
</code></pre> | ||
|
||
|
||
[move-book]: https://aptos.dev/move/book/SUMMARY |
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
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
/// Module with methods for safe memory manipulation. | ||
module std::mem { | ||
// TODO - functions here are `public(friend)` here for one release, | ||
// and to be changed to `public` one release later. | ||
#[test_only] | ||
friend std::mem_tests; | ||
|
||
/// Swap contents of two passed mutable references. | ||
/// | ||
/// Move prevents from having two mutable references to the same value, | ||
/// so `left` and `right` references are always distinct. | ||
public(friend) native fun swap<T>(left: &mut T, right: &mut T); | ||
|
||
/// Replace the value reference points to with the given new value, | ||
/// and return the value it had before. | ||
public(friend) fun replace<T>(ref: &mut T, new: T): T { | ||
swap(ref, &mut new); | ||
new | ||
} | ||
|
||
spec swap<T>(left: &mut T, right: &mut T) { | ||
pragma opaque; | ||
aborts_if false; | ||
ensures right == old(left); | ||
ensures left == old(right); | ||
} | ||
|
||
spec replace<T>(ref: &mut T, new: T): T { | ||
pragma opaque; | ||
aborts_if false; | ||
ensures result == old(ref); | ||
ensures ref == new; | ||
} | ||
} |
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
// Copyright © Aptos Foundation | ||
// SPDX-License-Identifier: Apache-2.0 | ||
|
||
//! Implementation of native functions for memory manipulation. | ||
use aptos_gas_schedule::gas_params::natives::move_stdlib::MEM_SWAP_BASE; | ||
use aptos_native_interface::{ | ||
safely_pop_arg, RawSafeNative, SafeNativeBuilder, SafeNativeContext, SafeNativeError, | ||
SafeNativeResult, | ||
}; | ||
use aptos_types::error; | ||
use move_vm_runtime::native_functions::NativeFunction; | ||
use move_vm_types::{ | ||
loaded_data::runtime_types::Type, | ||
values::{Reference, Value}, | ||
}; | ||
use smallvec::{smallvec, SmallVec}; | ||
use std::collections::VecDeque; | ||
|
||
/// The feature is not enabled. | ||
pub const EFEATURE_NOT_ENABLED: u64 = 1; | ||
|
||
/*************************************************************************************************** | ||
* native fun native_swap | ||
* | ||
* gas cost: MEM_SWAP_BASE | ||
* | ||
**************************************************************************************************/ | ||
fn native_swap( | ||
context: &mut SafeNativeContext, | ||
_ty_args: Vec<Type>, | ||
mut args: VecDeque<Value>, | ||
) -> SafeNativeResult<SmallVec<[Value; 1]>> { | ||
if !context | ||
.get_feature_flags() | ||
.is_native_memory_operations_enabled() | ||
{ | ||
return Err(SafeNativeError::Abort { | ||
abort_code: error::unavailable(EFEATURE_NOT_ENABLED), | ||
}); | ||
} | ||
|
||
debug_assert!(args.len() == 2); | ||
|
||
context.charge(MEM_SWAP_BASE)?; | ||
|
||
let left = safely_pop_arg!(args, Reference); | ||
let right = safely_pop_arg!(args, Reference); | ||
|
||
left.swap_values(right)?; | ||
|
||
Ok(smallvec![]) | ||
} | ||
|
||
/*************************************************************************************************** | ||
* module | ||
**************************************************************************************************/ | ||
pub fn make_all( | ||
builder: &SafeNativeBuilder, | ||
) -> impl Iterator<Item = (String, NativeFunction)> + '_ { | ||
let natives = [("swap", native_swap as RawSafeNative)]; | ||
|
||
builder.make_named_natives(natives) | ||
} |
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
Oops, something went wrong.