Failing verification for proptest example using format!

[nchong-at-aws]

I tried this code, which is a slightly modified example from the proptest book (https://altsysrq.github.io/proptest-book/proptest/getting-started.html):

#![allow(unused)]

fn __nondet<T>() -> T {
    unimplemented!()
}

fn __VERIFIER_assume(cond: bool) {
    unimplemented!()
}

fn parse_date(s: &str) -> Option<(u32, u32, u32)> {
    if 10 != s.len() {
        return None;
    }

    if "-" != &s[4..5] || "-" != &s[7..8] {
        return None;
    }

    let year = &s[0..4];
    let month = &s[5..7]; //< fixed from example that can be found using proptest
    let day = &s[8..10];

    year.parse::<u32>().ok().and_then(|y| {
        month
            .parse::<u32>()
            .ok()
            .and_then(|m| day.parse::<u32>().ok().map(|d| (y, m, d)))
    })
}

pub fn main() {
    let y: u32 = __nondet();
    let m: u32 = __nondet();
    let d: u32 = __nondet();
    __VERIFIER_assume(0 <= y && y < 10000);
    __VERIFIER_assume(1 <= m && m < 13);
    __VERIFIER_assume(1 <= d && d < 32);
    let (y2, m2, d2) = parse_date(&format!("{:04}-{:02}-{:02}", y, m, d)).unwrap();
    assert!(y == y2);
    assert!(m == m2);
    assert!(d == d2);
}

using the following command line invocation:

rmc example.rs

with RMC version: a728d8d

I expected to see this happen: VERIFICATION SUCCESSFUL

Instead, this happened: VERIFICATION FAILED

[nchong-at-aws]

This also fails:

pub fn main() {
  assert!("2021".parse::<u32>().unwrap() == 2021);
}

[zhassan-aws]

Experiment with switching to running goto-instrument with --generate-function-body assert-false-assume-false.

We should also replace the call to the function with codegen_unimplemented so that we get a proper error message on what is unsupported.

[celinval]

@zhassan-aws Do you mind adding taking a look at this one while you are looking into adding compiler warnings to codegen_unimplemented? Thanks

[zhassan-aws]

Summarizing a discussion from Friday 4/8:

• For the program involving "2021".parse::<u32>(), the failure is due to a missing definition for an std function, which is caused by Kani not linking the standard library.
• The reported failure is not user friendly as it involves the mangled name of the missing function as well as an unclear description ("assertion false"):

Check 3:  _ZN4core3num60_$LT$impl$u20$core..str..traits..FromStr$u20$for$u20$u32$GT$8from_str17hbdfd7c3b5dc0b1b5E.assertion.1
         - Status: FAILURE
         - Description: "assertion false"
         - Location: Unknown File in function _ZN4core3num60_$LT$impl$u20$core..str..traits..FromStr$u20$for$u20$u32$GT$8from_str17hbdfd7c3b5dc0b1b5E

• The longer term fix is for Kani to link the standard library so that the definitions of those functions are brought in. This however requires:
  1. Changing the Kani flow so that it codegens the std crate when compiling a file/package, or including the symtab/goto binary of the std crate in the Kani release package
  2. Performing some sort of slicing (e.g. via CBMC's --reachability-slice or via implementing our own linker/slicer) to aggressively prune the code that gets analyzed (much more than what is pruned by CBMC's --drop-unused-functions).
• This requires some effort, so in the short term, we will just clean up the reported failure using the result parser/post-processor by:
  1. Showing the original (unmangled) name of the missing function
  2. Improving the description of the failure

[celinval]

I believe this issue has been fixed by the MIR Linker (#1588). The following test has been added to our regression to ensure we can correctly handle parse function.

Unfortunately, I wasn't able to run the original test from this issue in a reasonable time. The test no longer fail, but symbolic execution is just taking too long. Maybe we should create a different issue to track the performance part of it.