From 7cc65683e9a18b73ff2f0609e0799c90da497b99 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 28 Apr 2022 17:49:41 -0400 Subject: [PATCH] UI fix : Fix missing function check descriptions (#1126) * Fix missing function check descriptions Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- scripts/cbmc_json_parser.py | 42 +++++++++++++++---- .../missing-function/{ => extern_c}/expected | 3 +- .../{ => extern_c}/extern_c.rs | 0 .../replaced-description/expected | 3 ++ .../replaced-description/main.rs | 11 +++++ .../rust-by-example-description/expected | 3 ++ .../rust-by-example-description/main.rs | 16 +++++++ 7 files changed, 67 insertions(+), 11 deletions(-) rename tests/ui/missing-function/{ => extern_c}/expected (74%) rename tests/ui/missing-function/{ => extern_c}/extern_c.rs (100%) create mode 100644 tests/ui/missing-function/replaced-description/expected create mode 100644 tests/ui/missing-function/replaced-description/main.rs create mode 100644 tests/ui/missing-function/rust-by-example-description/expected create mode 100644 tests/ui/missing-function/rust-by-example-description/main.rs diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py index ad43a48cb6f51..5215674139508 100755 --- a/scripts/cbmc_json_parser.py +++ b/scripts/cbmc_json_parser.py @@ -51,6 +51,8 @@ class GlobalMessages(str, Enum): REACH_CHECK_DESC = "[KANI_REACHABILITY_CHECK]" REACH_CHECK_KEY = "reachCheckResult" CHECK_ID = "KANI_CHECK_ID" + ASSERTION_FALSE = "assertion false" + DEFAULT_ASSERTION = "assertion" CHECK_ID_RE = CHECK_ID + r"_.*_([0-9])*" UNSUPPORTED_CONSTRUCT_DESC = "is not currently supported by Kani" UNWINDING_ASSERT_DESC = "unwinding assertion loop" @@ -273,6 +275,22 @@ def extract_solver_information(cbmc_response_json_array): return properties, solver_information +def modify_undefined_function_checks(properties): + """ + 1. Searches for any check which has unknown file location or missing defition and replaces description + 2. If a function with missing definition is reachable, then we turn all SUCCESS status to UNDETERMINED. + If there are no reachable functions with missing definitions, then the verification is not affected, so we retain all of the SUCCESS status. + """ + has_unknown_location_checks = False + for property in properties: + # Specifically trying to capture assertions that CBMC generates for functions with missing definitions + if GlobalMessages.ASSERTION_FALSE in property["description"] and extract_property_class( + property) == GlobalMessages.DEFAULT_ASSERTION and not hasattr(property["sourceLocation"], "file"): + property["description"] = "Function with missing definition is unreachable" + if property["status"] == "FAILURE": + has_unknown_location_checks = True + return has_unknown_location_checks + def extract_errors(solver_information): """ Extract errors from the CBMC output, which are messages that have the @@ -309,6 +327,7 @@ def postprocess_results(properties, extra_ptr_check): has_reachable_unsupported_constructs = has_check_failure(properties, GlobalMessages.UNSUPPORTED_CONSTRUCT_DESC) 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) annotate_properties_with_reach_results(properties, reach_checks) remove_check_ids_from_description(properties) @@ -318,7 +337,7 @@ def postprocess_results(properties, extra_ptr_check): for property in properties: property["description"] = get_readable_description(property) - if has_reachable_unsupported_constructs or has_failed_unwinding_asserts: + if has_reachable_unsupported_constructs or has_failed_unwinding_asserts or has_reachable_undefined_functions: # Change SUCCESS to UNDETERMINED for all properties if property["status"] == "SUCCESS": property["status"] = "UNDETERMINED" @@ -481,6 +500,17 @@ def replace(self, msg): } +def extract_property_class(prop): + """ + This function extracts the property class from the property string. + Property strings have the format of -([.].) + """ + prop_class = prop["property"].rsplit(".", 3) + # Do nothing if prop_class is diff than cbmc's convention + class_id = prop_class[-2] if len(prop_class) > 1 else None + return class_id + + def filter_ptr_checks(props): """This function will filter out extra pointer checks. @@ -488,10 +518,7 @@ def filter_ptr_checks(props): can result in lots of spurious failures. By default, we filter them out. """ def not_extra_check(prop): - """ Retrieve class id ([.].)""" - prop_class = prop["property"].rsplit(".", 3) - class_id = prop_class[-2] if len(prop_class) > 1 else None - return class_id not in ["pointer_arithmetic", "pointer_primitives"] + return extract_property_class(prop) not in ["pointer_arithmetic", "pointer_primitives"] return list(filter(not_extra_check, props)) @@ -503,10 +530,7 @@ def get_readable_description(prop): temporary variable. """ original = prop["description"] - # Id is structured as [.]. - prop_class = prop["property"].rsplit(".", 3) - # Do nothing if prop_class is diff than cbmc's convention - class_id = prop_class[-2] if len(prop_class) > 1 else None + class_id = extract_property_class(prop) if class_id in CBMC_DESCRIPTIONS: # Contains a list for potential message translation [String]. prop_type = [check.replace(original) for check in CBMC_DESCRIPTIONS[class_id] if check.matches(original)] diff --git a/tests/ui/missing-function/expected b/tests/ui/missing-function/extern_c/expected similarity index 74% rename from tests/ui/missing-function/expected rename to tests/ui/missing-function/extern_c/expected index 96d77b5fad4c2..50cf7e77f453f 100644 --- a/tests/ui/missing-function/expected +++ b/tests/ui/missing-function/extern_c/expected @@ -1,5 +1,4 @@ -Status: UNREACHABLE\ +Status: UNDETERMINED\ Description: "assertion failed: x == 5" VERIFICATION:- FAILED - diff --git a/tests/ui/missing-function/extern_c.rs b/tests/ui/missing-function/extern_c/extern_c.rs similarity index 100% rename from tests/ui/missing-function/extern_c.rs rename to tests/ui/missing-function/extern_c/extern_c.rs diff --git a/tests/ui/missing-function/replaced-description/expected b/tests/ui/missing-function/replaced-description/expected new file mode 100644 index 0000000000000..5f8ef600e5c8b --- /dev/null +++ b/tests/ui/missing-function/replaced-description/expected @@ -0,0 +1,3 @@ +.assertion.1\ +Status: FAILURE\ +Description: "Function with missing definition is unreachable" diff --git a/tests/ui/missing-function/replaced-description/main.rs b/tests/ui/missing-function/replaced-description/main.rs new file mode 100644 index 0000000000000..39321438f2309 --- /dev/null +++ b/tests/ui/missing-function/replaced-description/main.rs @@ -0,0 +1,11 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test is to check if the description for undefined functions has been updated to "Function with missing definition is unreachable" + +#[kani::proof] +fn main() { + let x = String::from("foo"); + let y = x.clone(); + assert_eq!("foo", y); +} diff --git a/tests/ui/missing-function/rust-by-example-description/expected b/tests/ui/missing-function/rust-by-example-description/expected new file mode 100644 index 0000000000000..5f8ef600e5c8b --- /dev/null +++ b/tests/ui/missing-function/rust-by-example-description/expected @@ -0,0 +1,3 @@ +.assertion.1\ +Status: FAILURE\ +Description: "Function with missing definition is unreachable" diff --git a/tests/ui/missing-function/rust-by-example-description/main.rs b/tests/ui/missing-function/rust-by-example-description/main.rs new file mode 100644 index 0000000000000..765d10d1f2278 --- /dev/null +++ b/tests/ui/missing-function/rust-by-example-description/main.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --enable-unstable --cbmc-args --unwind 4 --object-bits 9 +// This test is to check if the description for undefined functions has been updated to "Function with missing definition is unreachable" + +#![allow(unused)] +#[kani::proof] +pub fn main() { + let strings = vec!["tofu", "93", "18"]; + let numbers: Vec<_> = strings + .into_iter() + .filter_map(|s| s.parse::().ok()) + .collect(); + println!("Results: {:?}", numbers); +}