Skip to content

Commit 203e7a8

Browse files
andreistefanescugithub-actions[bot]claude
authored
fix: preserve mutation path in opaque spec calls (#545) (#551)
* fix: preserve mutation path in opaque spec calls (#545) when calling an opaque spec function with &mut parameters, wrap results with $UpdateMutation to preserve mutation path and location: - function-style (deterministic): use $UpdateMutation wrapper instead of direct assignment - datatypes (multiple returns): wrap &mut src extractions with $UpdateMutation - procedure-style (non-deterministic): save &mut refs before call, restore paths after Co-authored-by: Andrei Stefanescu <andreistefanescu@users.noreply.github.com> * test: add snapshot for framing opaque mutation test Co-authored-by: Andrei Stefanescu <andreistefanescu@users.noreply.github.com> Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: claude[bot] <41898282+claude[bot]@users.noreply.github.com> Co-authored-by: Andrei Stefanescu <andreistefanescu@users.noreply.github.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 2ba9e17 commit 203e7a8

File tree

3 files changed

+128
-9
lines changed

3 files changed

+128
-9
lines changed

‎crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs‎

Lines changed: 102 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2601,6 +2601,43 @@ impl<'env> FunctionTranslator<'env> {
26012601
);
26022602
}
26032603

2604+
// declare save variables for mutable references in procedure-style opaque calls
2605+
{
2606+
let id = self.fun_target.func_env.get_qualified_id();
2607+
for bc in fun_target.get_bytecode() {
2608+
if let Bytecode::Call(
2609+
_,
2610+
_,
2611+
Operation::Function(callee_mid, callee_fid, _),
2612+
srcs,
2613+
_,
2614+
) = bc
2615+
{
2616+
let callee_qid = callee_mid.qualified(*callee_fid);
2617+
let is_spec_call =
2618+
self.parent.targets.get_fun_by_spec(&id) == Some(&callee_qid);
2619+
let use_impl = self.style == FunctionTranslationStyle::Opaque
2620+
&& self.parent.targets.omits_opaque(&id);
2621+
if is_spec_call && !use_impl && !self.should_use_opaque_as_function(false) {
2622+
for &src in srcs.iter() {
2623+
if self.get_local_type(src).is_mutable_reference() {
2624+
let ty = self.get_local_type(src);
2625+
let num_oper = global_state
2626+
.get_temp_index_oper(mid, fid, src, baseline_flag)
2627+
.unwrap_or(&Bottom);
2628+
emitln!(
2629+
writer,
2630+
"var $mut_save_{}: {};",
2631+
src,
2632+
self.boogie_type_for_fun(env, &ty, num_oper)
2633+
);
2634+
}
2635+
}
2636+
}
2637+
}
2638+
}
2639+
}
2640+
26042641
// Declare temp variables for calls to multi-return pure functions
26052642
{
26062643
let mut seen = BTreeSet::new();
@@ -4353,15 +4390,70 @@ impl<'env> FunctionTranslator<'env> {
43534390
}
43544391

43554392
let call_line = if use_func { "" } else { "call " };
4393+
let has_mut_src = srcs
4394+
.iter()
4395+
.any(|&idx| self.get_local_type(idx).is_mutable_reference());
4396+
4397+
// save mutable references before procedure-style opaque spec call
4398+
if is_spec_call
4399+
&& !use_impl
4400+
&& !self.should_use_opaque_as_function(false)
4401+
{
4402+
for &src in srcs.iter() {
4403+
if self.get_local_type(src).is_mutable_reference() {
4404+
emitln!(
4405+
self.writer(),
4406+
"$mut_save_{} := {};",
4407+
src,
4408+
str_local(src)
4409+
);
4410+
}
4411+
}
4412+
}
43564413

4357-
emitln!(
4358-
self.writer(),
4359-
"{}{} := {}({});",
4360-
call_line,
4361-
dest_str,
4362-
fun_name,
4363-
args_str
4364-
);
4414+
// preserve mutation path for function-style spec calls with mutable reference results
4415+
if is_spec_call
4416+
&& !use_impl
4417+
&& use_func
4418+
&& !use_func_datatypes
4419+
&& has_mut_src
4420+
{
4421+
emitln!(
4422+
self.writer(),
4423+
"{} := $UpdateMutation({}, $Dereference({}({})));",
4424+
dest_str,
4425+
dest_str,
4426+
fun_name,
4427+
args_str
4428+
);
4429+
} else {
4430+
emitln!(
4431+
self.writer(),
4432+
"{}{} := {}({});",
4433+
call_line,
4434+
dest_str,
4435+
fun_name,
4436+
args_str
4437+
);
4438+
}
4439+
4440+
// restore mutation paths after procedure-style opaque spec call
4441+
if is_spec_call
4442+
&& !use_impl
4443+
&& !self.should_use_opaque_as_function(false)
4444+
{
4445+
for &src in srcs.iter() {
4446+
if self.get_local_type(src).is_mutable_reference() {
4447+
emitln!(
4448+
self.writer(),
4449+
"{} := $UpdateMutation($mut_save_{}, $Dereference({}));",
4450+
str_local(src),
4451+
src,
4452+
str_local(src)
4453+
);
4454+
}
4455+
}
4456+
}
43654457
}
43664458
}
43674459

@@ -4399,7 +4491,8 @@ impl<'env> FunctionTranslator<'env> {
43994491
.for_each(|(idx, val)| {
44004492
emitln!(
44014493
self.writer(),
4402-
"{} := {} -> $ret{};",
4494+
"{} := $UpdateMutation({}, $Dereference({} -> $ret{}));",
4495+
str_local(*val),
44034496
str_local(*val),
44044497
func_datatypes_var,
44054498
dests.len() + idx

‎crates/sui-prover/tests/inputs/opaque/framing.ok.move‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
module 0x42::framing_tests;
2+
3+
use prover::prover::{ensures, requires};
4+
5+
fun set(x: &mut u8) {
6+
*x = 0
7+
}
8+
9+
#[spec(prove)]
10+
fun set_spec(x: &mut u8) {
11+
set(x)
12+
}
13+
14+
#[spec(prove, focus)]
15+
fun frame(v: &mut vector<u8>, i: u64, j: u64) {
16+
requires(j < v.length());
17+
requires(i < j);
18+
let vj = v[j];
19+
set(&mut v[i]);
20+
ensures(v[j] == vj);
21+
}

‎crates/sui-prover/tests/snapshots/opaque/framing.ok.move.snap‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
---
2+
source: crates/sui-prover/tests/integration.rs
3+
expression: output
4+
---
5+
Verification successful

0 commit comments

Comments
 (0)