From 2c9bf736680f60475c731957f29fb96778867328 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 +- .../move-prover/boogie-backend/src/lib.rs | 21 ++++ .../boogie-backend/src/prelude/prelude.bpl | 12 ++ .../boogie-backend/src/spec_translator.rs | 11 +- .../sources/functional/abort_in_fun.move | 115 ++++++++++++++++++ .../functional/loops_with_memory_ops.exp | 3 +- .../functional/loops_with_memory_ops.v2_exp | 4 - 7 files changed, 161 insertions(+), 7 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 1077b7b3af83ee..dd9fd65ae14021 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-prover/boogie-backend/src/lib.rs b/third_party/move/move-prover/boogie-backend/src/lib.rs index 7db2a28429d370..4766ad01758606 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 117131d1cc8274..c68af17276762e 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 53235c65f11161..71499e5924318f 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 @@ -991,13 +991,22 @@ 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)) }, 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 00000000000000..e9cf4886b34d97 --- /dev/null +++ b/third_party/move/move-prover/tests/sources/functional/abort_in_fun.move @@ -0,0 +1,115 @@ +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 + } + + fun call_abort_generic_struct_concrete(x: u64, y: u64): T { + let sx = S { + value: T { + v: x + } + }; + let sy = S { + value: T { + v: y + } + }; + abort_generic_struct(sx, sy).value + } + + spec call_abort_generic_struct_concrete { + aborts_if x == y; + ensures result == call_abort_generic_struct_concrete(x, y); + 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 6a012dba56f8d3..32b6d76bc6da8b 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 00ce62137346b0..325fd07c230658 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 =