reachability-slice changes verification from FAILED to SUCCESSFUL

[avanhatt]

CBMC version: 5.40.0 (0cdc654) with PR 6376 and 5.31.0
Operating system: Both Ubuntu 20 and macOS 11.6 (20G165)
Exact command line resulting in the issue:

$ cbmc --version
5.31.0 (cbmc-5.31.0)
$ cbmc --object-bits 11 --unwinding-assertions --unwind 2 before-slice.out &> before-log.txt
$ goto-instrument --reachability-slice before-slice.out after-slice.out 
Reading GOTO program from 'before-slice.out'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Performing a reachability slice
Writing GOTO program to 'after-slice.out'
$ cbmc --object-bits 11 --unwinding-assertions --unwind 2 after-slice.out &> after-log.txt
$ cat before-log.txt | grep VERIFICATION
VERIFICATION FAILED
$ cat after-log.txt | grep VERIFICATION
VERIFICATION SUCCESSFUL

The issue seems to be this function goes from nontrivial to an assume(0) despite being reachable:

// _ZN3std2io5error5Error3new17h1430579a7771a700E
// file /home/ubuntu/rmc/library/std/src/io/error.rs line 407 column 5 function std::io::Error::new
struct _5372671742868111021 _ZN3std2io5error5Error3new17h1430579a7771a700E(struct _5803772184803114267 kind, struct _12284072475024233176 error)
{
  struct _5372671742868111021 var_0;
  struct _5803772184803114267 var_3;
  struct _194830641207493724 var_4;
  struct _194830641207493724 var_5;
  struct _12284072475024233176 var_6;

bb0:
  ;
  var_3 = kind;
  var_5=_ZN50_$LT$T$u20$as$u20$core__convert__Into$LT$U$GT$$GT$4into17h248557188006561aE(var_6);

bb1:
  ;
  var_4 = var_5;
  var_0=_ZN3std2io5error5Error4_new17h9c927d8b7dad0d7aE(var_3, var_4);

bb2:
  ;
  return var_0;
}

to

// _ZN3std2io5error5Error3new17h1430579a7771a700E
// file /home/ubuntu/rmc/library/std/src/io/error.rs line 407 column 5 function std::io::Error::new
struct _5372671742868111021 _ZN3std2io5error5Error3new17h1430579a7771a700E(struct _5803772184803114267 kind, struct _12284072475024233176 error)
{
  __CPROVER_assume(0);

bb2:
  ;
}

What behaviour did you expect: same result
What happened instead: verification result changes

Binaries included here, apologies that they are large, so far unable to replicate on a minimal example:
reachability-slice-bug.zip

[SaswatPadhi]

Not sure if these are related, but there is another (super old) issue about --full-slice being unsound: #260.

[zhassan-aws]

Attaching another example where I'm observing similar behavior with CBMC version 5.36.0:

before-reach-slice.tar.gz

Steps to reproduce:

1. tar xvzf before-reach-slice.tar.gz
2. cbmc before-reach-slice.gb
   This produces:

** Results:
[precondition_instance.1] memcpy src/dst overlap: SUCCESS
[precondition_instance.2] memcpy source region readable: FAILURE
[precondition_instance.3] memcpy destination region writeable: FAILURE
/home/ubuntu/examples/new-iss/foo/src/lib.rs function main
[main.assertion.1] line 7 assertion failed: b[0] == 0: SUCCESS

/home/ubuntu/tools/rmc/library/core/src/slice/mod.rs function core::slice::<impl [T]>::copy_from_slice
[core::slice::<impl [T]>::copy_from_slice.assertion.1] line 3055 a panicking function core::slice::<impl [T]>::copy_from_slice::len_mismatch_fail is invoked: SUCCESS

** 2 of 5 failed (2 iterations)
VERIFICATION FAILED

3. goto-instrument --reachability-slice before-reach-slice.gb after-reach-slice.gb
4. cbmc after-reach-slice.gb
   This produces:

** Results:
/home/ubuntu/examples/new-iss/foo/src/lib.rs function main
[main.assertion.1] line 7 assertion failed: b[0] == 0: SUCCESS

/home/ubuntu/tools/rmc/library/core/src/slice/mod.rs function core::slice::<impl [T]>::copy_from_slice
[core::slice::<impl [T]>::copy_from_slice.assertion.1] line 3055 a panicking function core::slice::<impl [T]>::copy_from_slice::len_mismatch_fail is invoked: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL

[jimgrundy]

We also need to review the use of "--slice-global-inits" as that is part of the starter-kit

[tautschnig]

The issue (in both examples provided) were functions the body of which was not available. #6505 addresses this issue.