Uninitialized variables should have possibly-distinct values.

[michael-emmi]

Currently smack is translating reads of uninitilized variables to reads of an $UNDEF constant. This is not ideal, since to be sound, distinct uninitialized variables need not be equal, i.e., each may have their own value.

Note: I am not exactly sure where LLVM introduces the "UndefValue" which gets translated to $UNDEF (perhaps in some optimization pass?), but the following is what SMACK is currently generating.

Source C code:

int r1;
int r2; 
int result1;
int result2;
result1 = foo(r1);
result2 = foo(r2);

Generated LLVM bitcode:

%1 = load i32* %r1, align 4, !dbg !35
%2 = call i32 @foo(i32 %1), !dbg !35
store i32 %2, i32* %result1, align 4, !dbg !35
%3 = load i32* %r2, align 4, !dbg !36
%4 = call i32 @foo(i32 %3), !dbg !36
store i32 %4, i32* %result2, align 4, !dbg !36

Generated Boogie code:

call $p := foo($UNDEF);
call $p1 := foo($UNDEF);

[michael-emmi]

Note: it is the --mem2reg flag, which we pass to llvm, that ultimately introduces these "undefined" values.

[michael-emmi]

At the moment, the only way I see to resolve this issue is to disable LLVM's mem2reg pass, which I advise against, due to the mess of additional memory operations in the code we would generate if we did.

[michael-emmi]

According to the LLVM reference manual, each "undef" should correspond to a unique uninitialized value, so actually the previous comment is irrelevant.

[shaobo-he]

I was wondering if it's still valid to assume that undefined values should hold the same value. I couldn't find any references now and intuitively they should be distinct.

[zvonimir]

How do we translate this now?

[shaobo-he]

We create a global variable for undefined values of a type.

[zvonimir]

If I remember this correctly, undef is between our current implementation and using verifier_nondet to model it. In particular, I think that undef in a loop for example should always evaluate to the same nondeterministic value. If that makes sense. I can't find this discussion anywhere now.