Skip to content

Commit

Permalink
[move-prover] Add a wellformed-check after havoc of &mut parameters.
Browse files Browse the repository at this point in the history 
This adds a wellformed assumption after havoc of &mut parameters, following up on a suspicion that new timeouts might be caused by this missing. It appears it did not fix the timeouts, but is needed anyway.

Closes: diem#7834
  • Loading branch information
@wrwg @bors-libra
wrwg authored and bors-libra committed Mar 10, 2021
1 parent 3703a57 commit a73ddaf
Show file tree
Hide file tree
Showing 4 changed files with 52 additions and 47 deletions.
43 changes: 24 additions & 19 deletions language/move-prover/bytecode/src/spec_instrumentation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -494,34 +494,39 @@ impl<'a> Instrumenter<'a> {
// they are `&mut`, they are never modified, and this is not expressed in the
// specifications. We treat this by skipping the Havoc for them. TODO: find a better
// solution
for src in &srcs {
let ty = &self.builder.data.local_types[*src];
if ty.is_mutable_reference()
&& !self
.builder
.global_env()
.is_wellknown_event_handle_type(ty.skip_reference())
{
self.builder
.emit_with(|id| Call(id, vec![], Operation::Havoc, vec![*src], None));
}
}

// Emit post conditions as assumptions.
for (_, cond) in std::mem::take(&mut callee_spec.post) {
self.builder.emit_with(|id| Prop(id, Assume, cond));
let mut_srcs = srcs
.iter()
.cloned()
.filter(|src| {
let ty = &self.builder.data.local_types[*src];
ty.is_mutable_reference()
&& !self
.builder
.global_env()
.is_wellknown_event_handle_type(ty.skip_reference())
})
.collect_vec();
for src in &mut_srcs {
self.builder
.emit_with(|id| Call(id, vec![], Operation::Havoc, vec![*src], None));
}

// Emit placeholders for assuming well-formedness of return values.
for dest in dests {
// Emit placeholders for assuming well-formedness of return values and mutable ref
// parameters.
for idx in mut_srcs.into_iter().chain(dests.iter().cloned()) {
let exp = self.builder.mk_call(
&BOOL_TYPE,
ast::Operation::WellFormed,
vec![self.builder.mk_temporary(dest)],
vec![self.builder.mk_temporary(idx)],
);
self.builder.emit_with(move |id| Prop(id, Assume, exp));
}

// Emit post conditions as assumptions.
for (_, cond) in std::mem::take(&mut callee_spec.post) {
self.builder.emit_with(|id| Prop(id, Assume, cond));
}

// Emit the events in the `emits` specs of the callee.
for (_, msg, handle, cond) in std::mem::take(&mut callee_spec.emits) {
let temp_msg = self.builder.emit_let(msg).0;
Expand Down
4 changes: 2 additions & 2 deletions language/move-prover/bytecode/tests/spec_instrumentation/generics.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,8 +57,8 @@ fun Generics::remove_u64($t0|a: address): Generics::R<u64> {
8: goto 17
9: label L3
10: modifies global<Generics::R<u64>>($t0)
11: assume Not(exists<Generics::R<u64>>($t0))
12: assume WellFormed($t3)
11: assume WellFormed($t3)
12: assume Not(exists<Generics::R<u64>>($t0))
# << opaque call: $t1 := Generics::remove<u64>($t0)
13: nop
14: label L1
Expand Down
40 changes: 20 additions & 20 deletions language/move-prover/bytecode/tests/spec_instrumentation/modifies.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -245,8 +245,8 @@ pub fun B::move_from_test_incorrect($t0|addr1: address, $t1|addr2: address): B::
8: trace_abort($t6)
9: goto 29
10: label L3
11: assume Eq<u64>($t7, select A::S.x(global<A::S>($t1)))
12: assume WellFormed($t7)
11: assume WellFormed($t7)
12: assume Eq<u64>($t7, select A::S.x(global<A::S>($t1)))
# << opaque call: $t5 := A::read_at($t1)
13: nop
# VC: caller does not have permission to modify `B::T` at given address at tests/spec_instrumentation/modifies.move:65:17+9
Expand All @@ -260,8 +260,8 @@ pub fun B::move_from_test_incorrect($t0|addr1: address, $t1|addr2: address): B::
20: trace_abort($t6)
21: goto 29
22: label L5
23: assume Eq<u64>($t10, select A::S.x(global<A::S>($t1)))
24: assume WellFormed($t10)
23: assume WellFormed($t10)
24: assume Eq<u64>($t10, select A::S.x(global<A::S>($t1)))
# << opaque call: $t7 := A::read_at($t1)
25: nop
26: assert Eq<u64>($t7, $t10)
Expand Down Expand Up @@ -295,8 +295,8 @@ pub fun B::move_to_test_incorrect($t0|account: signer, $t1|addr2: address) {
8: trace_abort($t5)
9: goto 31
10: label L3
11: assume Eq<u64>($t6, select A::S.x(global<A::S>($t1)))
12: assume WellFormed($t6)
11: assume WellFormed($t6)
12: assume Eq<u64>($t6, select A::S.x(global<A::S>($t1)))
# << opaque call: $t4 := A::read_at($t1)
13: nop
14: $t7 := 2
Expand All @@ -312,8 +312,8 @@ pub fun B::move_to_test_incorrect($t0|account: signer, $t1|addr2: address) {
22: trace_abort($t5)
23: goto 31
24: label L5
25: assume Eq<u64>($t10, select A::S.x(global<A::S>($t1)))
26: assume WellFormed($t10)
25: assume WellFormed($t10)
26: assume Eq<u64>($t10, select A::S.x(global<A::S>($t1)))
# << opaque call: $t7 := A::read_at($t1)
27: nop
28: assert Eq<u64>($t6, $t10)
Expand Down Expand Up @@ -346,8 +346,8 @@ pub fun B::mutate_S_test1_incorrect($t0|addr1: address, $t1|addr2: address) {
8: trace_abort($t5)
9: goto 38
10: label L3
11: assume Eq<u64>($t6, select A::S.x(global<A::S>($t1)))
12: assume WellFormed($t6)
11: assume WellFormed($t6)
12: assume Eq<u64>($t6, select A::S.x(global<A::S>($t1)))
# << opaque call: $t4 := A::read_at($t1)
13: nop
# >> opaque call: A::mutate_at($t0)
Expand All @@ -372,8 +372,8 @@ pub fun B::mutate_S_test1_incorrect($t0|addr1: address, $t1|addr2: address) {
29: trace_abort($t5)
30: goto 38
31: label L7
32: assume Eq<u64>($t9, select A::S.x(global<A::S>($t1)))
33: assume WellFormed($t9)
32: assume WellFormed($t9)
33: assume Eq<u64>($t9, select A::S.x(global<A::S>($t1)))
# << opaque call: $t5 := A::read_at($t1)
34: nop
35: assert Eq<u64>($t6, $t9)
Expand Down Expand Up @@ -404,8 +404,8 @@ pub fun B::mutate_S_test2_incorrect($t0|addr: address) {
6: trace_abort($t4)
7: goto 36
8: label L3
9: assume Eq<u64>($t5, select A::S.x(global<A::S>($t0)))
10: assume WellFormed($t5)
9: assume WellFormed($t5)
10: assume Eq<u64>($t5, select A::S.x(global<A::S>($t0)))
# << opaque call: $t3 := A::read_at($t0)
11: nop
# >> opaque call: A::mutate_at($t0)
Expand All @@ -430,8 +430,8 @@ pub fun B::mutate_S_test2_incorrect($t0|addr: address) {
27: trace_abort($t4)
28: goto 36
29: label L7
30: assume Eq<u64>($t8, select A::S.x(global<A::S>($t0)))
31: assume WellFormed($t8)
30: assume WellFormed($t8)
31: assume Eq<u64>($t8, select A::S.x(global<A::S>($t0)))
# << opaque call: $t4 := A::read_at($t0)
32: nop
33: assert Eq<u64>($t5, $t8)
Expand Down Expand Up @@ -467,8 +467,8 @@ pub fun B::mutate_at_test_incorrect($t0|addr1: address, $t1|addr2: address) {
8: trace_abort($t6)
9: goto 34
10: label L3
11: assume Eq<u64>($t7, select A::S.x(global<A::S>($t1)))
12: assume WellFormed($t7)
11: assume WellFormed($t7)
12: assume Eq<u64>($t7, select A::S.x(global<A::S>($t1)))
# << opaque call: $t5 := A::read_at($t1)
13: nop
# VC: caller does not have permission to modify `B::T` at given address at tests/spec_instrumentation/modifies.move:38:17+17
Expand All @@ -487,8 +487,8 @@ pub fun B::mutate_at_test_incorrect($t0|addr1: address, $t1|addr2: address) {
25: trace_abort($t6)
26: goto 34
27: label L5
28: assume Eq<u64>($t12, select A::S.x(global<A::S>($t1)))
29: assume WellFormed($t12)
28: assume WellFormed($t12)
29: assume Eq<u64>($t12, select A::S.x(global<A::S>($t1)))
# << opaque call: $t9 := A::read_at($t1)
30: nop
31: assert Eq<u64>($t7, $t12)
Expand Down
12 changes: 6 additions & 6 deletions language/move-prover/bytecode/tests/spec_instrumentation/opaque_call.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -151,9 +151,9 @@ fun Test::incr_twice() {
11: label L3
12: @2 := save_mem(Test::R)
13: modifies global<Test::R>($t0)
14: assume Eq<u64>(select Test::R.v(global<Test::R>($t0)), Add(select Test::R.v(global[@2]<Test::R>($t0)), 1))
15: assume Eq<u64>($t3, select Test::R.v(global<Test::R>($t0)))
16: assume WellFormed($t3)
14: assume WellFormed($t3)
15: assume Eq<u64>(select Test::R.v(global<Test::R>($t0)), Add(select Test::R.v(global[@2]<Test::R>($t0)), 1))
16: assume Eq<u64>($t3, select Test::R.v(global<Test::R>($t0)))
# << opaque call: $t1 := Test::get_and_incr($t0)
17: nop
18: destroy($t3)
Expand All @@ -171,9 +171,9 @@ fun Test::incr_twice() {
28: label L5
29: @3 := save_mem(Test::R)
30: modifies global<Test::R>($t4)
31: assume Eq<u64>(select Test::R.v(global<Test::R>($t4)), Add(select Test::R.v(global[@3]<Test::R>($t4)), 1))
32: assume Eq<u64>($t6, select Test::R.v(global<Test::R>($t4)))
33: assume WellFormed($t6)
31: assume WellFormed($t6)
32: assume Eq<u64>(select Test::R.v(global<Test::R>($t4)), Add(select Test::R.v(global[@3]<Test::R>($t4)), 1))
33: assume Eq<u64>($t6, select Test::R.v(global<Test::R>($t4)))
# << opaque call: $t3 := Test::get_and_incr($t2)
34: nop
35: destroy($t6)
Expand Down

0 comments on commit a73ddaf

Please sign in to comment.