Fix alias analysis

[xeren]

Several regression tests and fixes to the alias analysis.

• Multi-level aggregate indexes were reduced to their last index.
• ModifierTrait.MdLinear missed some inclusions had spurious inclusions.
• ModifierTrait.SdLinear lost some overlaps when shrunk to an object's bounds.
• Storing only null pointers and one valid address into an array lead to false must-alias verdicts. Fixed by adding null provenance.
• Some cycles avoided detection, rendering the analysis non-terminating. Fixed by running a thorough detector when the analysis takes too long.

[ThomasHaas]

ModifierTrait.MdLinear missed some inclusions.

So this is a soundness issue in the default analysis, right? Do you expect any regression on existing tests?

[xeren]

Unlikely, although the false inclusions include cases like $(k\cdot k')\cdot\mathbb Z\not\subseteq k\cdot\mathbb N$. The effect of the bug would be that the union of the two modifiers discards the larger one, while keeping only the smaller one. This further requires that (1) $k'>1$ or that (2) the smaller one is learned later.

An affected program must feature some point where these modifiers join. I do not recall anything like this in the existing tests.

*x = 0
*x = *x + 1 // cyclic inclusion -> accelerated to Md[0, [1]]
r = *x
r = ite(nondet_bool(), nondet_int(), r) // joins Md[0, [-1]] with Md[0, [1]]
s = *(z + r + 1)
t = *(z + 0) // suddenly Md[1, [1]] cannot alias Md[0, []]

[github-actions]

Performance comparison

Linux x64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	12.597 ± 0.099 s	12.623 ± 0.065 s	➖ -0.2% [-7.5%, +7.0%]	UNKNOWN
benchmarks/locks/mutex_musl.c	25.571 ± 2.871 s	25.409 ± 3.188 s	➖ -0.8% [-123.4%, +121.9%]	UNKNOWN
benchmarks/lfds/dglm.c	16.792 ± 1.309 s	16.018 ± 0.539 s	➖ +4.4% [-24.5%, +33.3%]	UNKNOWN
benchmarks/lfds/ms.c	29.470 ± 4.370 s	32.146 ± 5.028 s	➖ -12.1% [-188.8%, +164.6%]	UNKNOWN
benchmarks/lfds/treiber.c	8.495 ± 0.138 s	8.372 ± 0.108 s	➖ +1.4% [-5.5%, +8.4%]	UNKNOWN
benchmarks/lfds/safe_stack.c	6.250 ± 0.190 s	6.395 ± 0.166 s	➖ -2.4% [-33.7%, +28.8%]	UNKNOWN
benchmarks/challenging/cna.c	31.629 ± 0.479 s	32.880 ± 2.179 s	➖ -4.0% [-51.6%, +43.5%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	6.338 ± 0.106 s	6.475 ± 0.072 s	➖ -2.2% [-12.2%, +7.9%]	UNKNOWN
benchmarks/challenging/cna.c	11.471 ± 0.796 s	12.316 ± 0.468 s	➖ -7.6% [-35.8%, +20.6%]	UNKNOWN
benchmarks/challenging/wsq.c	5.527 ± 0.054 s	21.095 ± 0.203 s	❌ -281.7% [-321.6%, -241.8%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	16.217 ± 0.296 s	16.121 ± 0.043 s	➖ +0.6% [-11.3%, +12.4%]	UNKNOWN
benchmarks/locks/mutex_musl.c	16.430 ± 0.540 s	15.843 ± 0.455 s	➖ +3.5% [-20.7%, +27.7%]	UNKNOWN
benchmarks/lfds/ms.c	18.264 ± 0.501 s	18.442 ± 0.067 s	➖ -1.0% [-15.3%, +13.3%]	UNKNOWN
benchmarks/lfds/treiber.c	13.254 ± 0.355 s	12.921 ± 0.367 s	➖ +2.4% [-25.6%, +30.5%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	218.305 ± 6.688 s	237.056 ± 3.440 s	➖ -8.7% [-35.0%, +17.6%]

4 benchmark(s) omitted because both averages were below 5 seconds.

macOS ARM64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	21.256 ± 0.944 s	17.828 ± 2.696 s	➖ +16.4% [-36.3%, +69.1%]	UNKNOWN
benchmarks/locks/mutex_musl.c	23.944 ± 0.881 s	22.667 ± 0.172 s	➖ +5.3% [-12.3%, +22.8%]	UNKNOWN
benchmarks/lfds/dglm.c	36.740 ± 4.591 s	35.108 ± 1.999 s	➖ +3.9% [-31.2%, +39.1%]	UNKNOWN
benchmarks/lfds/ms.c	52.918 ± 4.258 s	59.810 ± 0.203 s	➖ -13.5% [-65.4%, +38.4%]	UNKNOWN
benchmarks/lfds/treiber.c	11.976 ± 0.090 s	12.415 ± 0.112 s	➖ -3.7% [-9.2%, +1.9%]	UNKNOWN
benchmarks/lfds/safe_stack.c	8.389 ± 0.081 s	8.462 ± 0.410 s	➖ -0.8% [-23.4%, +21.7%]	UNKNOWN
benchmarks/challenging/cna.c	36.739 ± 2.899 s	36.126 ± 1.913 s	➖ +1.5% [-12.5%, +15.6%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	16.092 ± 1.766 s	15.173 ± 0.236 s	➖ +5.0% [-53.8%, +63.7%]	UNKNOWN
benchmarks/locks/mutex_musl.c	10.522 ± 0.074 s	10.467 ± 0.290 s	➖ +0.5% [-17.5%, +18.5%]	UNKNOWN
benchmarks/lfds/dglm.c	9.639 ± 0.197 s	10.430 ± 0.669 s	➖ -8.2% [-35.7%, +19.4%]	PASS
benchmarks/lfds/ms.c	10.016 ± 0.152 s	10.224 ± 0.076 s	➖ -2.1% [-9.8%, +5.6%]	UNKNOWN
benchmarks/challenging/cna.c	27.627 ± 2.090 s	27.711 ± 4.585 s	➖ -0.1% [-66.1%, +65.9%]	UNKNOWN
benchmarks/challenging/wsq.c	14.960 ± 2.386 s	76.333 ± 8.327 s	❌ -413.2% [-572.6%, -253.8%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	36.256 ± 2.800 s	36.160 ± 2.585 s	➖ -0.2% [-65.0%, +64.6%]	UNKNOWN
benchmarks/locks/mutex_musl.c	32.106 ± 3.423 s	30.945 ± 2.209 s	➖ +3.2% [-39.5%, +45.9%]	UNKNOWN
benchmarks/lfds/dglm.c	6.734 ± 0.105 s	7.628 ± 0.205 s	➖ -13.3% [-31.9%, +5.3%]	UNKNOWN
benchmarks/lfds/ms.c	36.084 ± 0.070 s	39.341 ± 0.064 s	❌ -9.0% [-11.2%, -6.8%]	UNKNOWN
benchmarks/lfds/treiber.c	17.492 ± 0.577 s	17.701 ± 0.104 s	➖ -1.3% [-17.6%, +15.1%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	409.489 ± 8.206 s	474.529 ± 7.758 s	❌ -15.9% [-24.0%, -7.8%]

[xeren]

As a reaction to the Out-of-memory failure for Asm Tests, I reverted the semantic change of having an omnipotent null provenance. Instead, I gave this semantics to non-deterministic values. This did not solve all problems, though:

The SPIRV test spirv/vulkan/gpuverify/atomics/histo.spvasm is not supposed to find any data races. It contains the following snippet:

         %25 = OpAccessChain %_ptr_Input_uint %gl_LocalInvocationID %uint_0
         %26 = OpLoad %uint %25
         %28 = OpAccessChain %_ptr_Workgroup_uint %14 %26
         %29 = OpLoad %uint %28

It looks like this in our IR, where %gl_LocalInvocationID@T0 is initialized to a non-deterministic value:

bv32 %26 = load(&%gl_LocalInvocationID@T0)
bv32 %29 = load(&%14@W0 + (sext (bv32 %26 * bv32(4)) to bv64))

It accesses a static base with a non-deterministic index. The index guesses the difference between that base and the address of another object. The result points into that other object.

Solutions:

1. Let the alias results stay as strict as in development for tests like this.
   1. Erase provenance of products like above.
   2. Differentiate between non-deterministic values that can carry provenance and those that cannot.
2. Let alias results be as imprecise as they are in this PR, but the SMT-Solver will not find appropriate values to have them actually alias.
   1. Add dynamic bounds-checks for Spir-V constructs like OpAccessChain. This says OOB is supposed to be UB.
3. Do not introduce the concept of addresses with arbitrary provenance. This includes the "conservative fallback" where a guaranteed null pointer dereference gets to alias everything.

[ThomasHaas]

As a reaction to the Out-of-memory failure for Asm Tests, I reverted the semantic change of having an omnipotent null provenance. Instead, I gave this semantics to non-deterministic values. This did not solve all problems, though:

I think neither the null object nor non-deterministic choice should have any provenance (accesses are always invalid).

It looks like this in our IR, where %gl_LocalInvocationID@T0 is initialized to a non-deterministic value:

If %gl_LocalInvocationID has a non-deterministic value, then the code is clearly buggy. I don't think this variable should be non-determinstic (it needs at least a constraint to force it into a valid range).

Do not introduce the concept of addresses with arbitrary provenance. This includes the "conservative fallback" where a guaranteed null pointer dereference gets to alias everything

The issue in the original benchmark was not may-aliasing but must-aliasing. I'm wondering if we can just tackle the must-aliasing part. Indeed, how much performance do we lose by disabling must-aliasing completely?