[move-prover] disable aptos-labs#9545 temporarily and catch warnings …

…in testsuite

I mistakenly assumed that warnings are captured in the move prover tests
but turns out that this is not. This commit adds the capturing of
warnings as well.

Consequently, aptos-labs#9545 actually creates many warnings when trying to verify
DPN with Move Prover because a couple of invariants cannot be
instantiated. Although the DPN still veriies, seeing a log of warnings
are not pretty. So, let's temporarily disable the effects of aptos-labs#9545 (and
hence the warnings). This will allow me to investigate a bit more on how
we handle un-related type parameters in a generic invariant.

Closes: aptos-labs#9569

language/move-prover/bytecode/src/global_invariant_analysis.rs

@@ -393,7 +393,7 @@ impl PerFunctionRelevance {
                 mem_related.iter(),
                 inv_related,
                 fun_type_params_arity,
-                /* allow_uninstantiated_invariant */ false,
+                /* allow_uninstantiated_invariant */ true,
             );
 
             if is_return {

language/move-prover/bytecode/tests/global_invariant_analysis/uninst_type_param_in_inv.exp

@@ -116,26 +116,3 @@ Demo::f1: [
 @0 => invariant<T1, T2>
             (exists<S1<T1>>(@0x2) && exists<S2<T2>>(@0x2))
                 ==> global<S1<T1>>(@0x2).v == 0;
-
-============ Diagnostics ================
-warning: Failed to instantiate all type parameters in this global invariant
-   ┌─ tests/global_invariant_analysis/uninst_type_param_in_inv.move:23:9
-   │
-14 │               *&mut borrow_global_mut<S1<bool>>(addr).v = 0;
-   │               --------------------------------------------- When instrumenting the global invariant here
-   ·
-23 │ ╭         invariant<T1, T2>
-24 │ │             (exists<S1<T1>>(@0x2) && exists<S2<T2>>(@0x2))
-25 │ │                 ==> global<S1<T1>>(@0x2).v == 0;
-   │ ╰────────────────────────────────────────────────^
-
-warning: Failed to instantiate all type parameters in this global invariant
-   ┌─ tests/global_invariant_analysis/uninst_type_param_in_inv.move:23:9
-   │
-18 │               *&mut borrow_global_mut<S1<u64>>(addr).v = 0;
-   │               -------------------------------------------- When instrumenting the global invariant here
-   ·
-23 │ ╭         invariant<T1, T2>
-24 │ │             (exists<S1<T1>>(@0x2) && exists<S2<T2>>(@0x2))
-25 │ │                 ==> global<S1<T1>>(@0x2).v == 0;
-   │ ╰────────────────────────────────────────────────^

language/move-prover/tests/sources/regression/mono_after_global_invariant.exp

@@ -1,14 +1,4 @@
 Move prover returns: exiting with boogie verification errors
-warning: Failed to instantiate all type parameters in this global invariant
-   ┌─ tests/sources/regression/mono_after_global_invariant.move:44:9
-   │
-10 │           move_to(s, B {});
-   │           ------- When instrumenting the global invariant here
-   ·
-44 │ ╭         invariant<T> update
-45 │ │             Base::has_b() ==> (has_r<T>() ==> old(has_r<T>()));
-   │ ╰───────────────────────────────────────────────────────────────^
-
 error: global memory invariant does not hold
    ┌─ tests/sources/regression/mono_after_global_invariant.move:44:9
    │

language/move-prover/tests/testsuite.rs

@@ -180,16 +180,11 @@ fn test_runner_for_feature(path: &Path, feature: &Feature) -> datatest_stable::R
         Err(err) => format!("Move prover returns: {}\n", err),
     };
     if baseline_valid {
+        diags += &String::from_utf8_lossy(&error_writer.into_inner()).to_string();
         if let Some(ref path) = baseline_path {
-            diags += &String::from_utf8_lossy(&error_writer.into_inner()).to_string();
             verify_or_update_baseline(path.as_path(), &diags)?
         } else if !diags.is_empty() {
-            return Err(anyhow!(
-                "Unexpected prover output (expected none): {}{}",
-                diags,
-                String::from_utf8_lossy(&error_writer.into_inner())
-            )
-            .into());
+            return Err(anyhow!("Unexpected prover output (expected none): {}", diags).into());
         }
     }