Skip to content

Commit

Permalink
add borrow_mut_with_default (#7352)
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89
rahxephon89 authored Mar 24, 2023
1 parent be17a8f commit d957664
Show file tree
Hide file tree
Showing 7 changed files with 98 additions and 46 deletions.
1 change: 1 addition & 0 deletions third_party/move/extensions/move-table-extension/sources/Table.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ spec extensions::table {
map_del_must_exist = remove,
map_borrow = borrow,
map_borrow_mut = borrow_mut,
map_borrow_mut_with_default = borrow_mut_with_default,
map_spec_get = spec_get,
map_spec_set = spec_set,
map_spec_del = spec_remove,
Expand Down
5 changes: 5 additions & 0 deletions third_party/move/move-model/src/pragmas.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,10 @@ pub const INTRINSIC_FUN_MAP_BORROW: &str = "map_borrow";
/// `[move] fun map_borrow_mut<K, V>(m: &mut Map<K, V>, k: K): &mut V`
pub const INTRINSIC_FUN_MAP_BORROW_MUT: &str = "map_borrow_mut";

/// Mutable borrow of a value from the map, add the entry (k,default) if the key does not exist
/// `[move] fun map_borrow_mut<K, V>(m: &mut Map<K, V>, k: K, default: V): &mut V`
pub const INTRINSIC_FUN_MAP_BORROW_MUT_WITH_DEFAULT: &str = "map_borrow_mut_with_default";

/// All intrinsic functions associated with the map type
pub static INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS: Lazy<BTreeMap<&'static str, bool>> =
Lazy::new(|| {
Expand All @@ -177,6 +181,7 @@ pub static INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS: Lazy<BTreeMap<&'static str, bool>
(INTRINSIC_FUN_MAP_DEL_RETURN_KEY, true),
(INTRINSIC_FUN_MAP_BORROW, true),
(INTRINSIC_FUN_MAP_BORROW_MUT, true),
(INTRINSIC_FUN_MAP_BORROW_MUT_WITH_DEFAULT, true),
])
});

Expand Down
7 changes: 6 additions & 1 deletion third_party/move/move-prover/boogie-backend/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,8 @@ use move_model::{
model::{GlobalEnv, QualifiedId, StructId},
pragmas::{
INTRINSIC_FUN_MAP_ADD_NO_OVERRIDE, INTRINSIC_FUN_MAP_ADD_OVERRIDE_IF_EXISTS,
INTRINSIC_FUN_MAP_BORROW, INTRINSIC_FUN_MAP_BORROW_MUT, INTRINSIC_FUN_MAP_DEL_MUST_EXIST,
INTRINSIC_FUN_MAP_BORROW, INTRINSIC_FUN_MAP_BORROW_MUT,
INTRINSIC_FUN_MAP_BORROW_MUT_WITH_DEFAULT, INTRINSIC_FUN_MAP_DEL_MUST_EXIST,
INTRINSIC_FUN_MAP_DEL_RETURN_KEY, INTRINSIC_FUN_MAP_DESTROY_EMPTY,
INTRINSIC_FUN_MAP_HAS_KEY, INTRINSIC_FUN_MAP_IS_EMPTY, INTRINSIC_FUN_MAP_LEN,
INTRINSIC_FUN_MAP_NEW, INTRINSIC_FUN_MAP_SPEC_DEL, INTRINSIC_FUN_MAP_SPEC_GET,
Expand Down Expand Up @@ -84,6 +85,7 @@ struct MapImpl {
fun_del_return_key: String,
fun_borrow: String,
fun_borrow_mut: String,
fun_borrow_mut_with_default: String,
// spec functions
fun_spec_new: String,
fun_spec_get: String,
Expand Down Expand Up @@ -379,6 +381,9 @@ impl MapImpl {
fun_borrow_mut: Self::triple_opt_to_name(
decl.get_fun_triple(env, INTRINSIC_FUN_MAP_BORROW_MUT),
),
fun_borrow_mut_with_default: Self::triple_opt_to_name(
decl.get_fun_triple(env, INTRINSIC_FUN_MAP_BORROW_MUT_WITH_DEFAULT),
),
fun_spec_new: Self::triple_opt_to_name(
decl.get_fun_triple(env, INTRINSIC_FUN_MAP_SPEC_NEW),
),
Expand Down
19 changes: 19 additions & 0 deletions third_party/move/move-prover/boogie-backend/src/prelude/native.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -383,6 +383,25 @@ returns (dst: $Mutation ({{V}}), m': $Mutation ({{Self}})) {
}
{%- endif %}

{%- if impl.fun_borrow_mut_with_default != "" %}
procedure {:inline 2} {{impl.fun_borrow_mut_with_default}}{{S}}(m: $Mutation ({{Self}}), k: {{K}}, default: {{V}})
returns (dst: $Mutation ({{V}}), m': $Mutation ({{Self}})) {
var enc_k: int;
var t: {{Self}};
var t': {{Self}};
enc_k := {{ENC}}(k);
t := $Dereference(m);
if (!ContainsTable(t, enc_k)) {
m' := $UpdateMutation(m, AddTable(t, enc_k, default));
t' := $Dereference(m');
dst := $Mutation(l#$Mutation(m'), ExtendVec(p#$Mutation(m'), enc_k), GetTable(t', enc_k));
} else {
dst := $Mutation(l#$Mutation(m), ExtendVec(p#$Mutation(m), enc_k), GetTable(t, enc_k));
m' := m;
}
}
{%- endif %}

{%- if impl.fun_spec_len != "" %}
function {:inline} {{impl.fun_spec_len}}{{S}}(t: ({{Self}})): int {
LenTable(t)
Expand Down
6 changes: 4 additions & 2 deletions third_party/move/move-prover/bytecode/src/borrow_analysis.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ use move_binary_format::file_format::CodeOffset;
use move_model::{
ast::TempIndex,
model::{FunctionEnv, GlobalEnv, QualifiedInstId},
pragmas::INTRINSIC_FUN_MAP_BORROW_MUT,
pragmas::{INTRINSIC_FUN_MAP_BORROW_MUT, INTRINSIC_FUN_MAP_BORROW_MUT_WITH_DEFAULT},
ty::Type,
well_known::VECTOR_BORROW_MUT,
};
Expand Down Expand Up @@ -504,7 +504,9 @@ fn get_custom_annotation_or_none(
// check whether this borrow has known special semantics
if fun_env.is_well_known(VECTOR_BORROW_MUT) {
Some(summarize_custom_borrow(IndexEdgeKind::Vector, &[0], &[0]))
} else if fun_env.is_intrinsic_of(INTRINSIC_FUN_MAP_BORROW_MUT) {
} else if fun_env.is_intrinsic_of(INTRINSIC_FUN_MAP_BORROW_MUT)
|| fun_env.is_intrinsic_of(INTRINSIC_FUN_MAP_BORROW_MUT_WITH_DEFAULT)
{
Some(summarize_custom_borrow(IndexEdgeKind::Table, &[0], &[0]))
} else if fun_env.is_native_or_intrinsic() {
// non-borrow related native/intrinsic has no borrow semantics
Expand Down
86 changes: 43 additions & 43 deletions third_party/move/move-prover/tests/sources/functional/verify_custom_table.exp
View file
Original file line number Diff line number Diff line change
@@ -1,88 +1,88 @@
Move prover returns: exiting with verification errors
error: post-condition does not hold
┌─ tests/sources/functional/verify_custom_table.move:249:9
┌─ tests/sources/functional/verify_custom_table.move:269:9
│
249 │ ensures spec_get(result.t, k1) == 23;
269 │ ensures spec_get(result.t, k1) == 23;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at tests/sources/functional/verify_custom_table.move:245: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:246: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:242: add_R_fail
= at tests/sources/functional/verify_custom_table.move:223: make_R
= at tests/sources/functional/verify_custom_table.move:265: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:266: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:262: add_R_fail
= at tests/sources/functional/verify_custom_table.move:243: make_R
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:224: make_R
= at tests/sources/functional/verify_custom_table.move:244: make_R
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:225: make_R
= at tests/sources/functional/verify_custom_table.move:245: make_R
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:226: make_R
= at tests/sources/functional/verify_custom_table.move:246: make_R
= result = <redacted>
= at tests/sources/functional/verify_custom_table.move:227: make_R
= at tests/sources/functional/verify_custom_table.move:247: make_R
= result = <redacted>
= at tests/sources/functional/verify_custom_table.move:243: add_R_fail
= at tests/sources/functional/verify_custom_table.move:247: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:248: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:249: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:263: add_R_fail
= at tests/sources/functional/verify_custom_table.move:267: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:268: add_R_fail (spec)
= at tests/sources/functional/verify_custom_table.move:269: add_R_fail (spec)

error: post-condition does not hold
┌─ tests/sources/functional/verify_custom_table.move:74:9
┌─ tests/sources/functional/verify_custom_table.move:76:9
│
74 │ ensures spec_get(result, 1) == 1;
76 │ ensures spec_get(result, 1) == 1;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at tests/sources/functional/verify_custom_table.move:67: add_fail
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:68: add_fail
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:69: add_fail
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:70: add_fail
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:71: add_fail
= result = <redacted>
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:72: add_fail
= at tests/sources/functional/verify_custom_table.move:74: add_fail (spec)
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:73: add_fail
= result = <redacted>
= at tests/sources/functional/verify_custom_table.move:74: add_fail
= at tests/sources/functional/verify_custom_table.move:76: add_fail (spec)

error: post-condition does not hold
┌─ tests/sources/functional/verify_custom_table.move:199:9
┌─ tests/sources/functional/verify_custom_table.move:219:9
│
199 │ ensures result == spec_new();
219 │ ensures result == spec_new();
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at tests/sources/functional/verify_custom_table.move:194: create_and_insert_fail1
= at tests/sources/functional/verify_custom_table.move:214: create_and_insert_fail1
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:195: create_and_insert_fail1
= at tests/sources/functional/verify_custom_table.move:215: create_and_insert_fail1
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:196: create_and_insert_fail1
= at tests/sources/functional/verify_custom_table.move:216: create_and_insert_fail1
= result = <redacted>
= at tests/sources/functional/verify_custom_table.move:197: create_and_insert_fail1
= at tests/sources/functional/verify_custom_table.move:199: create_and_insert_fail1 (spec)
= at tests/sources/functional/verify_custom_table.move:217: create_and_insert_fail1
= at tests/sources/functional/verify_custom_table.move:219: create_and_insert_fail1 (spec)

error: post-condition does not hold
┌─ tests/sources/functional/verify_custom_table.move:208:9
┌─ tests/sources/functional/verify_custom_table.move:228:9
│
208 │ ensures result == spec_set(spec_new(), 1, 2);
228 │ ensures result == spec_set(spec_new(), 1, 2);
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at tests/sources/functional/verify_custom_table.move:203: create_and_insert_fail2
= at tests/sources/functional/verify_custom_table.move:223: create_and_insert_fail2
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:204: create_and_insert_fail2
= at tests/sources/functional/verify_custom_table.move:224: create_and_insert_fail2
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:205: create_and_insert_fail2
= at tests/sources/functional/verify_custom_table.move:225: create_and_insert_fail2
= result = <redacted>
= at tests/sources/functional/verify_custom_table.move:206: create_and_insert_fail2
= at tests/sources/functional/verify_custom_table.move:208: create_and_insert_fail2 (spec)
= at tests/sources/functional/verify_custom_table.move:226: create_and_insert_fail2
= at tests/sources/functional/verify_custom_table.move:228: create_and_insert_fail2 (spec)

error: post-condition does not hold
┌─ tests/sources/functional/verify_custom_table.move:190:9
┌─ tests/sources/functional/verify_custom_table.move:210:9
│
190 │ ensures result == spec_set(spec_new(), 1, 2);
210 │ ensures result == spec_set(spec_new(), 1, 2);
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at tests/sources/functional/verify_custom_table.move:182: create_and_insert_fail_due_to_typed_key_encoding
= at tests/sources/functional/verify_custom_table.move:202: create_and_insert_fail_due_to_typed_key_encoding
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:183: create_and_insert_fail_due_to_typed_key_encoding
= at tests/sources/functional/verify_custom_table.move:203: create_and_insert_fail_due_to_typed_key_encoding
= t = <redacted>
= at tests/sources/functional/verify_custom_table.move:184: create_and_insert_fail_due_to_typed_key_encoding
= at tests/sources/functional/verify_custom_table.move:204: create_and_insert_fail_due_to_typed_key_encoding
= result = <redacted>
= at tests/sources/functional/verify_custom_table.move:185: create_and_insert_fail_due_to_typed_key_encoding
= at tests/sources/functional/verify_custom_table.move:190: create_and_insert_fail_due_to_typed_key_encoding (spec)
= at tests/sources/functional/verify_custom_table.move:205: create_and_insert_fail_due_to_typed_key_encoding
= at tests/sources/functional/verify_custom_table.move:210: create_and_insert_fail_due_to_typed_key_encoding (spec)
20 changes: 20 additions & 0 deletions third_party/move/move-prover/tests/sources/functional/verify_custom_table.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ module 0x42::table {
map_del_return_key = remove_return_key,
map_borrow = borrow,
map_borrow_mut = borrow_mut,
map_borrow_mut_with_default = borrow_mut_with_default,
map_spec_new = spec_new,
map_spec_get = spec_get,
map_spec_set = spec_set,
Expand All @@ -28,6 +29,7 @@ module 0x42::table {
public native fun upsert<K: copy + drop, V>(table: &mut Table<K, V>, key: K, val: V);
public native fun borrow<K: copy + drop, V>(table: &Table<K, V>, key: K): &V;
public native fun borrow_mut<K: copy + drop, V>(table: &mut Table<K, V>, key: K): &mut V;
public native fun borrow_mut_with_default<K: copy + drop, V>(table: &mut Table<K, V>, key: K, default: V): &mut V;
public native fun length<K: copy + drop, V>(table: &Table<K, V>): u64;
public native fun empty<K: copy + drop, V>(table: &Table<K, V>): bool;
public native fun remove<K: copy + drop, V>(table: &mut Table<K, V>, key: K): V;
Expand Down Expand Up @@ -162,6 +164,24 @@ module 0x42::VerifyTable {
ensures spec_get(result, 2) == 3;
}

fun borrow_mut_with_default(): Table<u8, u64> {
let t = table::new<u8, u64>();
table::add(&mut t, 1, 2);
table::add(&mut t, 2, 3);
let r = table::borrow_mut_with_default(&mut t, 1, 2);
*r = 4;
table::borrow_mut_with_default(&mut t, 3, 5);
t
}
spec borrow_mut_with_default {
ensures spec_contains(result, 1) && spec_contains(result, 2);
ensures spec_contains(result, 3);
ensures spec_len(result) == 3;
ensures spec_get(result, 1) == 4;
ensures spec_get(result, 2) == 3;
ensures spec_get(result, 3) == 5;
}

fun create_empty(): Table<u8, u64> {
table::new()
}
Expand Down

0 comments on commit d957664

Please sign in to comment.