From 6142f77448d6b2763b6d3025bfca2eea522439a6 Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Fri, 11 Oct 2024 00:18:23 -0700 Subject: [PATCH] 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 | 4 - 8 files changed, 188 insertions(+), 16 deletions(-) create mode 100644 third_party/move/move-prover/tests/sources/functional/abort_in_fun.move 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..c68af17276762 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 $Uninterpreted_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..740f8a5d284eb 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!( + "$Uninterpreted_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!( + "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 00ce62137346b..325fd07c23065 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 @@ -43,7 +43,6 @@ error: induction case of the loop invariant does not hold = at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2 = a = = 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 = @@ -100,9 +99,6 @@ 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:85: nested_loop2 = = = i =