Reading uninitialized memory gives symbolic value rather than error

[nchong-at-aws]

In the following program we read from uninitialized memory so the program is undefined [0]. Using CBMC as our symbolic engine means Kani does not warn of this error. Instead the value of v[0] is symbolic/nondet. Adding a "poison" value for freshly allocated objects is likely to be a large change for CBMC. For now, we can document this behavior.

fn main() {
    let mut v: Vec<u8> = Vec::with_capacity(8);
    unsafe {
        v.set_len(3);
    }
    let _b = v[0]; //< reading uninitialized memory
}

[0] https://doc.rust-lang.org/reference/behavior-considered-undefined.html#behavior-considered-undefined

Uninitialized memory is also implicitly invalid for any type that has a restricted set of valid values. In other words, the only cases in which reading uninitialized memory is permitted are inside unions and in “padding” (the gaps between the fields/elements of a type).

[nchong-at-aws]

I think the quoted para isn't appropriate to the example since all values of 0..255 are okay for a u8. Instead, I now think the cause is the line:

An integer (i*/u*), floating point value (f*), or raw pointer obtained from uninitialized memory, or uninitialized memory in a str.

[danielsn]

We should support the examples from https://doc.rust-lang.org/stable/std/mem/union.MaybeUninit.html

[zhassan-aws]

Related to diffblue/cbmc#7014

[giltho]

It turns out that Kani's own test suite has undefined behaviour that isn't really caught because of that, with a mix of that and the any_raw issue, pointed out there and partially fixed there.

Take the test result3.rs.
It's initialized with kani::any_raw, which means that both the discriminent field and value field are nondet.

Then foo is called, with the any_raw value.
And here's the code generated by kani (in demangled c form):

unsigned int foo(struct std::result::Result<u32, Unit> *input)
{
  unsigned int var_0;
  long int var_2;
  unsigned int *num;

bb0:
  ;
  var_2 = (long int)input->case;
  if(!(var_2 == 0))
    goto bb2;


bb1:
  ;
  num = &input->cases.Ok.0;
  var_0 = *num;
  goto bb3;

bb2:
  ;
  var_0 = 3;

bb3:
  ;
  return var_0;
}

The issue is: the compiler has no connection between the discriminant and the value.
Because the value is an enum, Kanillian sees that the union is either a u32, or a ZST. And as specified by the Rust documentation, writing to a ZST is no-op, in which case the field stays uninitialized, i.e. poisoned.

Therefore, I have a branch where the chosen case of the union is 0, but the value is still uninitialized. In that case, my execution fails with *num trying to load poison.

[tedinski]

@giltho wrote a test showing this, but we decided not to merge it as a "fixme" since it's more of a feature request, but recording it here for future reference:

• add an uninitialized memory access fixme test #1666