model-checking
Reading uninitialized memory gives symbolic value rather than error
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).
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.
We should support the examples from https://doc.rust-lang.org/stable/std/mem/union.MaybeUninit.html
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.
@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:
- https://github.com/model-checking/kani/pull/1666
