Limitation due to semantics of undef causes SVComp incorrect false results

[AdamZsofi]

I came across more than one SVComp task, that gives back incorrect false values, because the call of the error function depends on the value of a global variable, which wasn't explicitly initialized to any value. The initialization of these static storage values is in the C11 standard, under 6.7.9/10:

"If an object that has automatic storage duration is not initialized explicitly, its value is indeterminate. If an object that has static or thread storage duration is not initialized explicitly, then: — if it has pointer type, it is initialized to a null pointer; — if it has arithmetic type, it is initialized to (positive or unsigned) zero; — if it is an aggregate, every member is initialized (recursively) according to these rules, and any padding is initialized to zero bits; — if it is a union, the first named member is initialized (recursively) according to these rules, and any padding is initialized to zero bits;"

Here's an example, which should be handled as a correct program, but gazer-bmc gives back a fail with the trace below:

int a;
void reach_error();
int main() {
  int b;
  if (b)
    b = a;
  if (b)
    reach_error();
}

Error trace:
------------
#0 in function main():
  Undefined behavior (read of an undefined value: #0bv32)	
  b := 1	(0b00000000000000000000000000000001)	 at 5:7
  Undefined behavior (read of an undefined value: #1bv32)

The other examples I've seen use global char arrays, but the issue is the same as here.

[radl97]

The problem is not with initializing globals, and is already a documented lmitation: See https://github.com/ftsrg/gazer/blob/master/doc/Limitations.md#undefined-behavior-in-llvm

The problem is in pure LLVM code, in PromoteMemoryToRegisterPass.

Update: here

[radl97]

Solution proposal: After all alloca instructions, insert a store:

For readability, LL without types :D

alloca %b

will be transform to:

alloca %b
%b_val := call gazer.undef()
store %b_val, %b

@sallaigy Can this work?

UPDATE: use call gazer.undef() instead of undef to be sure

[sallaigy]

@radl97 This seems feasible to me, however we probably should only do this for allocas the we do not immediately see clobbered by a store. Otherwise we probably would ruin a lot of optimizations and the trace would fill up with irrelevant undefined value steps.

[radl97]

@sallaigy The additional check is feasible too. (probably we would need the same optimizations that are used by PromoteMemToRegPass). However, this pass would only be called before promoting to registers (as that part of the code ruins our verification). That means when promotion is possible, we do not lose any optimization later (as it will be equivalent to the one above.)

[AdamZsofi]

This branch solves the issue as proposed, but aborts when handling arrays due to an early optimization, which replaces stores with extractvalue instructions. (This instruction isn't supported by Gazer.) Due to this it works, when the --no-optimize flag is used.