[Prover] add support of abort in spec function

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()
                 },

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<T>(): TypeInfo {
-        Tuple()
+        Abort(1)
     }
 } // end 0x42::move_function_in_spec
 

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::<BTreeSet<_>>()
+        .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::<BTreeSet<_>>()
+        .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

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
 

third_party/move/move-prover/boogie-backend/src/spec_translator.rs

@@ -724,13 +724,18 @@
                 // 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 @@
                 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)
+                    ),
+                );
             },
         }
     }

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<Element: copy + drop>(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<Element: copy + drop> has copy, drop {
+        value: Element
+    }
+
+    fun abort_generic_struct<Element: copy + drop>(x: S<Element>, y: S<Element>): S<Element> {
+        if (x == y) {
+            abort 0
+        } else {
+            x
+        }
+    }
+
+    fun spec_abort_generic_struct<Element: copy + drop>(x: S<Element>, y: S<Element>): S<Element> {
+        if (x == y) {
+            abort 0
+        } else {
+            x
+        }
+    }
+
+    fun call_abort_generic_struct<Element: copy + drop>(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
+    }
+
+}

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 = <redacted>
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         i = <redacted>
@@ -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 = <redacted>
-   =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         i = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2

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 = <redacted>
-   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>
    =         i = <redacted>
@@ -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 = <redacted>
-   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = <redacted>
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>
    =         i = <redacted>

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 │ │     }
+   │ ╰─────^

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();
+        };
+    }
+
+}

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 │ │     }
+   │ ╰─────^