From 0ccd0a02a31847283a334a7b986b1aee98dadd43 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Tue, 3 May 2022 17:47:41 -0400
Subject: [PATCH] Filter sanity checks (#1146)

Properties which are sanity checks needed to be removed from the UI. They are now marked with the property_class "sanity_check" which makes it easy to filter such checks out as the pipeline to add, remove and edit checks based on their property_class has already been setup.
---
 scripts/cbmc_json_parser.py                   | 15 +++++++-
 tests/ui/filter-sanity-checks/expected        |  3 ++
 .../filter-sanity-checks/sanity_check_fail.rs | 38 +++++++++++++++++++
 3 files changed, 55 insertions(+), 1 deletion(-)
 create mode 100644 tests/ui/filter-sanity-checks/expected
 create mode 100644 tests/ui/filter-sanity-checks/sanity_check_fail.rs

diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py
index e0f0c1117abc..c3f96fb6a237 100755
--- a/scripts/cbmc_json_parser.py
+++ b/scripts/cbmc_json_parser.py
@@ -329,6 +329,7 @@ def postprocess_results(properties, extra_ptr_check):
     has_failed_unwinding_asserts = has_check_failure(properties, GlobalMessages.UNWINDING_ASSERT_DESC)
     has_reachable_undefined_functions = modify_undefined_function_checks(properties)
     properties, reach_checks = filter_reach_checks(properties)
+    properties = filter_sanity_checks(properties)
     annotate_properties_with_reach_results(properties, reach_checks)
     remove_check_ids_from_description(properties)
 
@@ -369,10 +370,22 @@ def has_check_failure(properties, message):
             return True
     return False
 
-
 def filter_reach_checks(properties):
     return filter_properties(properties, GlobalMessages.REACH_CHECK_DESC)
 
+def filter_sanity_checks(properties):
+    """
+    Specific filter for sanity_check checks that removed checks with SUCCESS status
+    """
+    filtered_properties = []
+    property_class = "sanity_check"
+    for property in properties:
+        if property_class in extract_property_class(property) and property["status"] == "SUCCESS":
+            pass
+        else:
+            filtered_properties.append(property)
+
+    return filtered_properties
 
 def filter_properties(properties, message):
     """
diff --git a/tests/ui/filter-sanity-checks/expected b/tests/ui/filter-sanity-checks/expected
new file mode 100644
index 000000000000..70607c9626fa
--- /dev/null
+++ b/tests/ui/filter-sanity-checks/expected
@@ -0,0 +1,3 @@
+sanity_check.1\
+Status: FAILURE\
+Description: "Reached assignment statement with unequal types Pointer { typ: StructTag("tag-Unit") } StructTag("tag-Unit")"
diff --git a/tests/ui/filter-sanity-checks/sanity_check_fail.rs b/tests/ui/filter-sanity-checks/sanity_check_fail.rs
new file mode 100644
index 000000000000..ac9dbe140c38
--- /dev/null
+++ b/tests/ui/filter-sanity-checks/sanity_check_fail.rs
@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// This testcase is currently failing with the following error:
+///
+/// [assertion.2] Reached assignment statement with unequal types Pointer { typ:
+/// StructTag("tag-Unit") } Pointer { typ: StructTag("tag-_3943305294634710273") }: FAILURE
+///
+/// If you run:
+/// ```
+/// RUSTFLAGS="--cfg=ok" kani fixme_niche_opt.rs
+/// ```
+/// This test will succeed.
+///
+/// Issue: https://github.com/model-checking/kani/issues/729
+
+enum Error {
+    Error1,
+    Error2,
+}
+
+/// This version fails.
+#[cfg(not(ok))]
+fn to_option<T: Copy, E>(result: &Result<T, E>) -> Option<T> {
+    if let Ok(v) = result { Some(*v) } else { None }
+}
+
+/// This version succeeds.
+#[cfg(ok)]
+fn to_option<T: Copy, E>(result: &Result<T, E>) -> Option<T> {
+    if let Ok(v) = *result { Some(v) } else { None }
+}
+
+#[kani::proof]
+fn main() {
+    let result: Result<(), Error> = Ok(());
+    assert!(to_option(&result).is_some());
+}