SV-COMP: unreach-call failure in reducercommutativity/max.i

[RyanGlScott]

crux-llvm-svcomp incorrectly concludes that reach_error is reachable in the reducercommutativity/max.i SV-COMP benchmark program:

$ cabal run exe:crux-llvm-svcomp -- --config crux-llvm/svcomp/config-files/unreach-call.config --svcomp-arch 32bit --svcomp-spec /home/rscott2/bench-defs/sv-benchmarks/c/properties/unreach-call.prp /home/rscott2/bench-defs/sv-benchmarks/c/reducercommutativity/max.i
Resolving dependencies...
Up to date
[Crux] Using pointer width: 32 for file crux-build/crux~max.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Counterexample found, skipping remaining goals
[Crux] Found counterexample for verification goal
[Crux]   rscott2/bench-defs/sv-benchmarks/c/reducercommutativity/max.i:12:83: error: in reach_error
[Crux]   Call to assert()
[Crux]   Details:
[Crux]     void reach_error()
[Crux] Goal status:
[Crux]   Total: 56
[Crux]   Proved: 54
[Crux]   Disproved: 1
[Crux]   Incomplete: 1
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.
[SVCOMP] Verification result: FALSIFIED (unreach-call)

There are several other programs of a similar caliber that also give the same error, but max.i is probably the most self-contained example. Crux claims that N = 0x20 is a counterexample, which is untrue. I think the use of iteration-bound: 50 in unreach-call.config might be partially responsible for this, but I'm not sure.

[robdockins]

A little experimentation leads me to believe that the counterexample chosen is usually (always?) the largest power of 2 which is below the chosen iteration bound, so it does seem related.

[robdockins]

The iteration bound and the choice of the length of the array is a red herring. Fixing the value of N to a concrete value still causes the counterexample.

I think the actual issue here is the reads from the uninitialized array x. The way we've implemented these reads is that each read of uninitialized memory creates a fresh uninterpreted value. I suspect that this benchmark only succeeds if we return the same uninterpreted value each time.

[RyanGlScott]

Oh wow, you're exactly right. Here is an even smaller program which exhibits the same issue when compiled with -O0:

#include <stdlib.h>

int main() {
  int x;
  if (x && !x) {
    abort();
  }

  return 0;
}

Logically, one would expect that x and !x could never simultaneously be true. However, each load of x results in a completely different value, which allows abort() to be reachable. Urk.

How should we fix this? I suppose one option is to check for variables that are declared without being initialized during translation, and if lax-loads-and-stores is enabled, initialize them with a specific symbolic value. Actually, that won't work so well in LLVM, where the declaration of a value and its initialization can be arbitrarily far away. Perhaps we have to maintain some mapping of uninitialized variables to their symbolic contents to make sure we read from the same contents consistently? That sounds kind of tiresome, but I'm not sure how we would do better.

[robdockins]

I think we have two options.

1. On every alloca and malloc, write a fresh uninterpreted value of the right shape when lax-loads-and-stores is enabled, and undo the special case handing in the memory model. We don't need to check which ones will be initialized, as they will be be overwritten later (although, we might want to omit them as an optimization in cases where it is easy). This has a certain appeal, as it makes the memory model simpler.

2. In the lax-loads-and-stores base case, keep a cache of uninterpreted values that is populated on demand. If an uninitialized value is read, generate or load an uninterpreted value large enough to cover the allocation and slice out the part that was read.

[travitch]

For (1), would we fall back to the degenerate (wrong-ish) behavior if the size was symbolic? I know that a symbolic size is probably going to be bad in general anyway

[robdockins]

I don't think a symbolic size is a problem, as long as we're careful. We should be able to use an uninterpreted SMT array to write enough fresh bytes in that case (or, in every case?)

[RyanGlScott]

We should be able to use an uninterpreted SMT array to write enough fresh bytes in that case (or, in every case?)

Indeed, I'm wondering if we shouldn't just use doArrayStore to write a fresh byte array of the appropriate size each time when invoking doAlloca or doMalloc. We could conceivably propagate the argument type in the alloca instruction to doAlloca and supply it to storeRaw, but this would involve a fair bit of code churn. Moreover, I don't think the same trick would work for doMalloc, as we don't have easy access to the argument type when calling malloc—all we have is the number of bytes to allocate.

[langston-barrett]

Logically, one would expect that x and !x could never simultaneously be true.

I don't think it's relevant to the behavior of lax-* flags, which already lie outside of the "official" C/C++ semantics, but this expectation isn't one that's respected by (certain versions of) Clang nor rustc:

https://www.ralfj.de/blog/2019/07/14/uninit.html

https://godbolt.org/z/TWrvcq

[RyanGlScott]

A very good point. I should be more precise and avoid saying "logically" but rather "what SV-COMP expects to happen". As far as I can tell, SV-COMP expects something like (1) in #844 (comment), although I can't find any official documentation stating as such. Oh well.

[RyanGlScott]

I whipped up an implementation of (1) from #844 (comment) at #906. It makes the test case from #844 (comment) pass, and it makes reducercommutativity/max.i report UNKNOWN instead of FALSIFIED, which is just peachy. Any feedback on the design is welcome.

[robdockins]

Thanks for those links Langston. That lead me to the following:
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1793.pdf

I've only skimmed it so far, but it seems like an excellent analysis of this question from the C standardization angle. EDIT: and it touches on the bitfield questions we have been grappling with recently as well.