Support atomic functions

[schuessf]

This PR adds support for atomic functions (mostly read/write atomically without data-races) as defined in stdatomic.h. Since we currently only support preprocessed files from GCC, we need to support the builtin atomic functions from here.

Every atomic-function has an additional memory-order-argument (see here). For sequential consistency (which is just the constant 5 in GCC 🙂), we simply wrap every statement produced by the translation into an atomic-block. We currently do not support other memory orders (and will not in the near future), so I just try to overapproximate the other cases. Therefore the general translation (as handled in StandardFunctionHandler::buildWrtMemoryOrder) looks like this:

if (memory_order == 5) {
  atomic { <modelled reads/writes> }
} else {
  assert false { :overapproximation "memory order" };
}

For all the modelled function, we also introduce data-race-checks, because atomic read/writes can still lead to data races, if the read/writes of another thread is not atomic.

Note regarding SV-COMP: Currently theses functions are currently only used in AWS-benchmarks, which are not even concurrent. It does however not hurt, if we support them properly, they might occur in concurrent benchmarks in the future. However, benchmarks that model atomic reads/writes using __VERIFIER_atomic_begin and __VERIFIER_atomic_end with normal assignments are quite a bit easier for us to verify than atomic functions in C (because every function introduces additional memory accesses).

[schuessf]

I just added an optimization to improve the performance of our verification on atomic functions. Most of the atomic function that are supported with this PR require pointers. So if you have a variable x with a primitive type, you always need its address &x in the calls of atomic functions like __atomic_store_n(&x, val, 5). Since the programs takes the address of x, we add this variable to the heap and thus it is translated to a pointer in Boogie. So the translation of this C-statement is similar to write~...(x, val) (which is basically a write to the memory-array). However, if the address is only used for atomic functions (there are possible other cases where this applies as well), we do not really need to model x using a pointer, we can then simply translate it to an assignment x := val. Therefore we do not introduce any operations on the memory array, if only primitive types are used in atomic operations. I had to add an exception for & to ignore it if it occurs in an atomic function in 4dfe1f3e10f5abd8d98b1e371f9e78b9d4aa3126. While it works as expected in our case, this is probably more specific than necessary and we should try to generalize it.