From d95766444addb4ab677fdf2d25a7be549f2d8e2d Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Fri, 24 Mar 2023 04:01:31 -0700 Subject: [PATCH] add borrow_mut_with_default (#7352) --- .../sources/Table.spec.move | 1 + third_party/move/move-model/src/pragmas.rs | 5 ++ .../move-prover/boogie-backend/src/lib.rs | 7 +- .../boogie-backend/src/prelude/native.bpl | 19 ++++ .../bytecode/src/borrow_analysis.rs | 6 +- .../functional/verify_custom_table.exp | 86 +++++++++---------- .../functional/verify_custom_table.move | 20 +++++ 7 files changed, 98 insertions(+), 46 deletions(-) diff --git a/third_party/move/extensions/move-table-extension/sources/Table.spec.move b/third_party/move/extensions/move-table-extension/sources/Table.spec.move index bfdd72f2cb5a6..77d3bb277f2ce 100644 --- a/third_party/move/extensions/move-table-extension/sources/Table.spec.move +++ b/third_party/move/extensions/move-table-extension/sources/Table.spec.move @@ -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, diff --git a/third_party/move/move-model/src/pragmas.rs b/third_party/move/move-model/src/pragmas.rs index 0abdbf61a4201..217a69ed6d3dd 100644 --- a/third_party/move/move-model/src/pragmas.rs +++ b/third_party/move/move-model/src/pragmas.rs @@ -155,6 +155,10 @@ pub const INTRINSIC_FUN_MAP_BORROW: &str = "map_borrow"; /// `[move] fun map_borrow_mut(m: &mut Map, 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(m: &mut Map, 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> = Lazy::new(|| { @@ -177,6 +181,7 @@ pub static INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS: Lazy (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), ]) }); diff --git a/third_party/move/move-prover/boogie-backend/src/lib.rs b/third_party/move/move-prover/boogie-backend/src/lib.rs index 7c0ebce05587f..dd3ddd36a57fd 100644 --- a/third_party/move/move-prover/boogie-backend/src/lib.rs +++ b/third_party/move/move-prover/boogie-backend/src/lib.rs @@ -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, @@ -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, @@ -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), ), diff --git a/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl b/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl index c6f79b54787dc..845bec4510428 100644 --- a/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl +++ b/third_party/move/move-prover/boogie-backend/src/prelude/native.bpl @@ -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) diff --git a/third_party/move/move-prover/bytecode/src/borrow_analysis.rs b/third_party/move/move-prover/bytecode/src/borrow_analysis.rs index 6a52ee583508c..221d753e5f021 100644 --- a/third_party/move/move-prover/bytecode/src/borrow_analysis.rs +++ b/third_party/move/move-prover/bytecode/src/borrow_analysis.rs @@ -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, }; @@ -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 diff --git a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.exp b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.exp index f7d809822213d..01d36033b0f20 100644 --- a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.exp +++ b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.exp @@ -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 = - = at tests/sources/functional/verify_custom_table.move:224: make_R + = at tests/sources/functional/verify_custom_table.move:244: make_R = t = - = at tests/sources/functional/verify_custom_table.move:225: make_R + = at tests/sources/functional/verify_custom_table.move:245: make_R = t = - = at tests/sources/functional/verify_custom_table.move:226: make_R + = at tests/sources/functional/verify_custom_table.move:246: make_R = result = - = at tests/sources/functional/verify_custom_table.move:227: make_R + = at tests/sources/functional/verify_custom_table.move:247: make_R = result = - = 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 = - = at tests/sources/functional/verify_custom_table.move:68: add_fail - = t = = at tests/sources/functional/verify_custom_table.move:69: add_fail = t = = at tests/sources/functional/verify_custom_table.move:70: add_fail = t = = at tests/sources/functional/verify_custom_table.move:71: add_fail - = result = + = t = = at tests/sources/functional/verify_custom_table.move:72: add_fail - = at tests/sources/functional/verify_custom_table.move:74: add_fail (spec) + = t = + = at tests/sources/functional/verify_custom_table.move:73: add_fail + = result = + = 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 = - = 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 = - = 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 = - = 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 = - = 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 = - = 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 = - = 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 = - = 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 = - = 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 = - = 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) diff --git a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.move b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.move index 324e3fddc332e..0192f10d14974 100644 --- a/third_party/move/move-prover/tests/sources/functional/verify_custom_table.move +++ b/third_party/move/move-prover/tests/sources/functional/verify_custom_table.move @@ -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, @@ -28,6 +29,7 @@ module 0x42::table { public native fun upsert(table: &mut Table, key: K, val: V); public native fun borrow(table: &Table, key: K): &V; public native fun borrow_mut(table: &mut Table, key: K): &mut V; + public native fun borrow_mut_with_default(table: &mut Table, key: K, default: V): &mut V; public native fun length(table: &Table): u64; public native fun empty(table: &Table): bool; public native fun remove(table: &mut Table, key: K): V; @@ -162,6 +164,24 @@ module 0x42::VerifyTable { ensures spec_get(result, 2) == 3; } + fun borrow_mut_with_default(): Table { + let t = table::new(); + 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 { table::new() }