Add the MVP_TEST_INCONSISTENCY to cargo test -p move-prover

- This adds the `MVP_TEST_INCONSISTENCY` flag to the `cargo test` for Prover Closes: #7984
move-language · Mar 23, 2021 · 229eaf7 · 229eaf7
1 parent 856d13f
commit 229eaf7
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 6 deletions.
diff --git a/language/move-prover/tests/README.md b/language/move-prover/tests/README.md
@@ -11,9 +11,9 @@ configuring the prover are not set as described there, all tests and this direct
 those files, use `UPBL=1 cargo test`. To update or test a single file, you can also provide a fragment of the move
 source path.
 
-*Note*: there are two sets of tests here. The basic ones are those in `./sources` and in `../../diem-framework`. Those are run
-by default and are merge blockers for submitting changes. An extended set of tests is found `./xsources`. Those
-are only run if the environment variable `MVP_TEST_X=1` is set.
+*Note*: there are three sets of tests here. The basic ones are those in `./sources`, in `../../diem-framework`, and in
+`../../move-stdlib`. Those are run by default and are merge blockers for submitting changes. An extended set of tests is
+found `./xsources`. Those are only run if the environment variable `MVP_TEST_X=1` is set.
 
 There is a convention for test cases under this directory. In general, there are two kinds of test cases, which can be
 mixed in a file. The first type of test cases are "correct" Move functions which are expected to be proven so.
@@ -44,6 +44,16 @@ be able to pass at least with `-T=20`. To do so use
 MVP_TEST_FLAGS="-T=20" cargo test -p move-prover
 ```
 
+## Inconsistency Check
+If the flag `--check-inconsistency` is given, the prover not only verifies a target, but also checks if there is any
+inconsistent assumption in the verification. If the environment variable `MVP_TEST_INCONSISTENCY=1` is set, `cargo test`
+will perform the inconsistency check while running the tests in `../../diem-framework` and `../../move-stdlib` (i.e.,
+the prover will run those tests with the flag `--check-inconsistency`).
+
+```shell script
+MVP_TEST_INCONSISTENCY=1 cargo test -p move-prover
+```
+
 ## Code coverage
 
 Analyzing the test coverage of the diem repo is regularly done in CI, and the result updates the online report at

diff --git a/language/move-prover/tests/testsuite.rs b/language/move-prover/tests/testsuite.rs
@@ -20,7 +20,13 @@ use std::sync::atomic::{AtomicBool, Ordering};
 
 const ENV_FLAGS: &str = "MVP_TEST_FLAGS";
 const ENV_TEST_EXTENDED: &str = "MVP_TEST_X";
-const STDLIB_FLAGS: &[&str] = &[
+const MVP_TEST_INCONSISTENCY: &str = "MVP_TEST_INCONSISTENCY";
+const INCONSISTENCY_TEST_FLAGS: &[&str] = &[
+    "--dependency=../move-stdlib/modules",
+    "--dependency=../diem-framework/modules",
+    "--check-inconsistency",
+];
+const REGULAR_TEST_FLAGS: &[&str] = &[
     "--dependency=../move-stdlib/modules",
     "--dependency=../diem-framework/modules",
 ];
@@ -227,11 +233,22 @@ fn cvc4_deny_listed(path: &Path) -> bool {
 fn get_flags(temp_dir: &Path, path: &Path) -> anyhow::Result<(Vec<String>, Option<PathBuf>)> {
     // Determine the way how to configure tests based on directory of the path.
     let path_str = path.to_string_lossy();
+
+    let stdlib_test_flags = if read_env_var(MVP_TEST_INCONSISTENCY).is_empty() {
+        REGULAR_TEST_FLAGS
+    } else {
+        INCONSISTENCY_TEST_FLAGS
+    };
+
     let (base_flags, baseline_path, modifier) =
         if path_str.contains("diem-framework/") || path_str.contains("move-stdlib/") {
-            (STDLIB_FLAGS, None, "std_")
+            (stdlib_test_flags, None, "std_")
         } else {
-            (STDLIB_FLAGS, Some(path.with_extension("exp")), "prover_")
+            (
+                REGULAR_TEST_FLAGS,
+                Some(path.with_extension("exp")),
+                "prover_",
+            )
         };
     let mut flags = base_flags.iter().map(|s| (*s).to_string()).collect_vec();
     // Add any flags specified in the source.