From 7fc181e8786de6f3ee4498bcd9a19473987b51cf Mon Sep 17 00:00:00 2001 From: igor-aptos <110557261+igor-aptos@users.noreply.github.com> Date: Thu, 10 Oct 2024 16:24:35 -0700 Subject: [PATCH 1/2] [single-node-performance] Add runner information in the output (#14932) * [single-node-performance] Add runner information in the output * adding skip move e2e * recalibration From eafc03f8618107deac1ee6a320ae1fa94ecfd9e1 Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Fri, 11 Oct 2024 00:18:23 -0700 Subject: [PATCH 2/2] add support of abort when in spec --- .../src/env_pipeline/spec_rewriter.rs | 2 +- .../specs/move_function_in_spec_ok.exp | 2 +- .../move-prover/boogie-backend/src/lib.rs | 21 +++ .../boogie-backend/src/prelude/prelude.bpl | 12 ++ .../boogie-backend/src/spec_translator.rs | 39 ++++-- .../sources/functional/abort_in_fun.move | 121 ++++++++++++++++++ .../functional/loops_with_memory_ops.exp | 3 +- .../functional/loops_with_memory_ops.v2_exp | 5 +- .../spec_fun_imperative_expression_err.exp | 13 ++ .../spec_fun_imperative_expression_err.move | 26 ++++ .../spec_fun_imperative_expression_err.v2_exp | 13 ++ 11 files changed, 242 insertions(+), 15 deletions(-) create mode 100644 third_party/move/move-prover/tests/sources/functional/abort_in_fun.move create mode 100644 third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.exp create mode 100644 third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.move create mode 100644 third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.v2_exp diff --git a/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs b/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs index 1077b7b3af83e..dd9fd65ae1402 100644 --- a/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs +++ b/third_party/move/move-compiler-v2/src/env_pipeline/spec_rewriter.rs @@ -377,7 +377,7 @@ impl<'a> ExpRewriterFunctions for SpecConverter<'a> { .into_exp() }, // Deal with removing various occurrences of Abort and spec blocks - Call(id, Abort, _) | SpecBlock(id, ..) => { + SpecBlock(id, ..) => { // Replace direct call by unit Call(*id, Tuple, vec![]).into_exp() }, diff --git a/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp b/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp index 4ba45bf526215..b9a89a9fa7950 100644 --- a/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp +++ b/third_party/move/move-compiler-v2/tests/checking/specs/move_function_in_spec_ok.exp @@ -35,7 +35,7 @@ module 0x42::move_function_in_spec { } } spec fun $type_of(): TypeInfo { - Tuple() + Abort(1) } } // end 0x42::move_function_in_spec 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 7db2a28429d37..4766ad0175860 100644 --- a/third_party/move/move-prover/boogie-backend/src/lib.rs +++ b/third_party/move/move-prover/boogie-backend/src/lib.rs @@ -184,6 +184,27 @@ pub fn add_prelude( sh_instances = vec![]; bv_instances = vec![]; } + + let mut all_types = mono_info + .all_types + .iter() + .filter(|ty| ty.can_be_type_argument()) + .map(|ty| TypeInfo::new(env, options, ty, false)) + .collect::>() + .into_iter() + .collect_vec(); + let mut bv_all_types = mono_info + .all_types + .iter() + .filter(|ty| ty.can_be_type_argument()) + .map(|ty| TypeInfo::new(env, options, ty, true)) + .filter(|ty_info| !all_types.contains(ty_info)) + .collect::>() + .into_iter() + .collect_vec(); + all_types.append(&mut bv_all_types); + context.insert("uninterpreted_instances", &all_types); + context.insert("sh_instances", &sh_instances); context.insert("bv_instances", &bv_instances); let mut vec_instances = mono_info diff --git a/third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl b/third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl index 117131d1cc827..af262f11c9fbf 100644 --- a/third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl +++ b/third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl @@ -24,6 +24,18 @@ options provided to the prover. {% include "custom-natives" %} {%- endif %} + +// Uninterpreted function for all types + +{% for instance in uninterpreted_instances %} + +{%- set S = "'" ~ instance.suffix ~ "'" -%} +{%- set T = instance.name -%} + +function $Arbitrary_value_of{{S}}(): {{T}}; + +{% endfor %} + // ============================================================================================ // Primitive Types diff --git a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs index 53235c65f1116..43e54ef7ceff7 100644 --- a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs +++ b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs @@ -724,13 +724,18 @@ impl<'env> SpecTranslator<'env> { // Single-element sequence is just a wrapped value. self.translate_exp(exp_vec.first().expect("list has an element")); }, - ExpData::Return(..) - | ExpData::Sequence(..) - | ExpData::Loop(..) - | ExpData::Assign(..) - | ExpData::Mutate(..) - | ExpData::SpecBlock(..) - | ExpData::LoopCont(..) => panic!("imperative expressions not supported"), + ExpData::Return(id, ..) + | ExpData::Sequence(id, ..) + | ExpData::Loop(id, ..) + | ExpData::Assign(id, ..) + | ExpData::Mutate(id, ..) + | ExpData::SpecBlock(id, ..) + | ExpData::LoopCont(id, ..) => { + self.env.error( + &self.env.get_node_loc(*id), + "imperative expressions not supported in specs", + ); + }, } } @@ -991,15 +996,31 @@ impl<'env> SpecTranslator<'env> { self.translate_call(node_id, oper, &[args[args.len() - 1].clone()]); emit!(self.writer, &")".repeat(count)); }, + Operation::Abort => { + let exp_bv_flag = global_state.get_node_num_oper(node_id) == Bitwise; + emit!( + self.writer, + &format!( + "$Arbitrary_value_of'{}'()", + boogie_type_suffix_bv(self.env, &self.get_node_type(node_id), exp_bv_flag) + ) + ); + }, Operation::MoveFunction(_, _) | Operation::BorrowGlobal(_) | Operation::Borrow(..) | Operation::Deref | Operation::MoveTo | Operation::MoveFrom - | Operation::Abort | Operation::Old => { - panic!("operation unexpected: {}", oper.display(self.env, node_id)) + self.env.error( + &self.env.get_node_loc(node_id), + &format!( + "bug: operation {} is not supported \ + in the current context", + oper.display(self.env, node_id) + ), + ); }, } } diff --git a/third_party/move/move-prover/tests/sources/functional/abort_in_fun.move b/third_party/move/move-prover/tests/sources/functional/abort_in_fun.move new file mode 100644 index 0000000000000..bc1fbf119fd3f --- /dev/null +++ b/third_party/move/move-prover/tests/sources/functional/abort_in_fun.move @@ -0,0 +1,121 @@ +module 0x42::TestAbortInFunction { + + fun aborts_with(x: u64, y: u64): u64 { + if (x == 1) { + abort 2 + } else if (y == 2) { + abort 3 + } else { + x + } + } + spec aborts_with { + aborts_if x == 1 with 2; + aborts_if y == 2 with 3; + ensures result == x; + } + + fun call_aborts_with(): u64 { + aborts_with(2, 3) + } + + spec call_aborts_with { + ensures result == aborts_with(2, 3); + } + + fun abort_generic(x: Element, y: Element): Element { + if (x == y) { + abort 0 + } else { + x + } + } + + fun call_aborts_generic(): u64 { + abort_generic(2, 3) + } + + spec call_aborts_generic { + ensures result == abort_generic(2, 3); + } + + struct S has copy, drop { + value: Element + } + + fun abort_generic_struct(x: S, y: S): S { + if (x == y) { + abort 0 + } else { + x + } + } + + fun spec_abort_generic_struct(x: S, y: S): S { + if (x == y) { + abort 0 + } else { + x + } + } + + fun call_abort_generic_struct(x: Element, y: Element): Element { + let sx = S { + value: x + }; + let sy = S { + value: y + }; + abort_generic_struct(sx, sy).value + } + + spec call_abort_generic_struct { + aborts_if x == y; + ensures result == call_abort_generic_struct(x, y); + } + + struct T has copy, drop { + v: u64 + } + + spec T { + pragma bv=b"0"; + } + + fun call_abort_generic_struct_concrete(x: u64, y: u64, test_assert1: bool): T { + let sx = S { + value: T { + v: x + } + }; + let sy = S { + value: T { + v: y + } + }; + assert!(test_assert1, 0); + abort_generic_struct(sx, sy).value + } + + spec call_abort_generic_struct_concrete { + aborts_if x == y; + aborts_if !test_assert1; + ensures result == call_abort_generic_struct_concrete(x, y, test_assert1); + ensures result == spec_call_abort_generic_struct_concrete(x, y); + } + + spec fun spec_call_abort_generic_struct_concrete(x: u64, y: u64): T { + let sx = S { + value: T { + v: x + } + }; + let sy = S { + value: T { + v: y + } + }; + spec_abort_generic_struct(sx, sy).value + } + +} diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp index 6a012dba56f8d..32b6d76bc6da8 100644 --- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp +++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp @@ -45,6 +45,7 @@ error: induction case of the loop invariant does not hold = at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = b = + = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = a = = at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2 = i = @@ -104,8 +105,8 @@ error: unknown assertion failed = at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = b = - = a = = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 + = a = = at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2 = i = = at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2 diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp index 4da1a9c4977ce..294a93f8a4f5a 100644 --- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp +++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp @@ -42,7 +42,7 @@ error: induction case of the loop invariant does not hold = at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = a = - = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 + = b = = at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2 = = = i = @@ -99,9 +99,8 @@ error: unknown assertion failed = at tests/sources/functional/loops_with_memory_ops.move:75: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 - = a = - = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = b = + = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2 = = = i = diff --git a/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.exp b/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.exp new file mode 100644 index 0000000000000..0fb3da8c0043d --- /dev/null +++ b/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.exp @@ -0,0 +1,13 @@ +Move prover returns: exiting with condition generation errors +error: imperative expressions not supported in specs + ┌─ tests/sources/functional/spec_fun_imperative_expression_err.move:2:27 + │ + 2 │ fun sequential(): u64 { + │ ╭───────────────────────────^ + 3 │ │ let _x = 2; + 4 │ │ let _y = 3; + 5 │ │ while(_y > 0) { + · │ +16 │ │ _x +17 │ │ } + │ ╰─────^ diff --git a/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.move b/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.move new file mode 100644 index 0000000000000..2196a453b5bc3 --- /dev/null +++ b/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.move @@ -0,0 +1,26 @@ +module 0x42::M { + fun sequential(): u64 { + let _x = 2; + let _y = 3; + while(_y > 0) { + break + }; + if (_x > 0) { + abort(0) + }; + let _z = if (_x > 5) { + _x + } else { + _y + }; + _x + } + + fun m() { + let _z = 2; + spec { + assert _z == sequential(); + }; + } + +} diff --git a/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.v2_exp b/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.v2_exp new file mode 100644 index 0000000000000..0fb3da8c0043d --- /dev/null +++ b/third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.v2_exp @@ -0,0 +1,13 @@ +Move prover returns: exiting with condition generation errors +error: imperative expressions not supported in specs + ┌─ tests/sources/functional/spec_fun_imperative_expression_err.move:2:27 + │ + 2 │ fun sequential(): u64 { + │ ╭───────────────────────────^ + 3 │ │ let _x = 2; + 4 │ │ let _y = 3; + 5 │ │ while(_y > 0) { + · │ +16 │ │ _x +17 │ │ } + │ ╰─────^