Function Contracts: Modifies for str

[pi314mm]

We would like to be able to verify mutable string references in kani contracts. In particular, the following test case should pass:

// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Zfunction-contracts

// Test that modifies a string

#[kani::requires(x == "aaa")]
#[kani::modifies(x)]
#[kani::ensures(|_| x == "AAA")]
fn to_upper(x: &mut str) {
    x.make_ascii_uppercase();
}

#[kani::proof_for_contract(to_upper)]
fn harness() {
    let mut s = String::from("aaa");
    let x: &mut str = s.as_mut_str();
    to_upper(x);
}

There seems to be an issue with the current compilation strategy for str within the modifies clause which should be properly investigated (#3295). The current test case (tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs in the PR) should be changed from being ignored to having a valid output.

In addition, we would like to test the kani::internal::write_any_str function. We want to create a friendly user experience that tells the user that this functionality doesn't exist due to utf8 verification issues. The test case for this would look like the one above, but additionally uses a stub_for_contract macro to force usage of the kani::internal::write_any_str function.

If possible, we should add utf8 verification to allow for the kani::internal::write_any_str function to work properly. The concerns are not of whether this is possible, but whether this is fast enough to reasonably verify in cbmc.