Region analysis type mismatch failures in SV-COMP SoftwareSystems

[sim642]

In my own run of Goblint on SV-COMP SoftwareSystems category, Goblint crashed with

exception Failure("Type mismatch!")

https://github.com/goblint/analyzer/blob/3164939e27b7908839fe083f036ca165eb54d7ea/src/cdomains/lval.ml#L508-L514

from region analysis domain (which uses PartitionDomain and collapse functions) on the following benchmarks:

• [ ] ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--arcnet--rfc1201.ko-entry_point.cil.out.i
• [ ] ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--micrel--ks8842.ko-entry_point.cil.out.i
• [ ] ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--ath--ath6kl--ath6kl_usb.ko-entry_point.cil.out.i
• [ ] ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--libertas--usb8xxx.ko-entry_point.cil.out.i
• [ ] ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--mwifiex--mwifiex_usb.ko-entry_point.cil.out.i
• [ ] ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--rtl818x--rtl8180--rtl818x_pci.ko-entry_point.cil.out.i
• [ ] ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point.cil.out.i
• [ ] ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--misc--sgi-gru--gru.ko.cil.i
• [ ] ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--gadget--udc--net2272.ko.cil.c

[sim642]

ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--arcnet--rfc1201.ko-entry_point.cil.out.i

All but the last two contain an identical set_impl thing which is the common problem. After a whole day of investigation I can say this:

1. Region offsets are a complete mess (see also #107):

   1. In the analysis, index offsets are stored very precisely (the index is a CIL expression) but when they are actually used in part_access they're all replaced with literal ?. What's the point?
   2. The analysis implements an extremely rudimentary symbolic analysis of these indices: https://github.com/goblint/analyzer/blob/3ba6714305fdd0ca7cbc162cd057026acf5cc5fa/src/cdomains/regionDomain.ml#L129-L136 Basically the region set_impl[last_index] is converted into set_impl[last_index - 1] when there's a statement last_index++. Why is this even done? Removing this passes our regression test just as well.
   3. (Bonus point, which doesn't have anything to do with this issue, or anything else for that matter) The Equ component of region analysis is meticulously updated but it's never queried. So it's another crappy symbolic analysis.
   4. Operations on regions with offsets are weird: set_impl[last_index] joined with set_impl[last_index - 1] gives just set_impl without any offset, as opposed to something like set_impl[unknown_exp]. This the reason (or at least one of them) why the crash later happens: set_impl[last_index - 1].rfc1201 is computed to belong to the region set_impl.rfc1201 which isn't type-correct any more. I highly doubt fixing that join would solve anything because how should the regions set_impl, set_impl[last_index - 1] and set_impl[unknown_exp] compare?
   5. Region offsets lack clear semantics. Without this it's pointless to try to fix the implementation if we don't even know in theory what the correct behavior would be and why.
   6. It might be saner to just disable them in their current form, considering how many issues they already have recently caused and how there seems no end to this madness.

2. sync makes things unnecessarily complicated and confusing:

   1. Region analysis never directly side effects to globals but (conditionally) keeps what it wants side-effected in the Vars components of its local domain, which eventually is flushed via sync and shenanigans.
   2. The whole technique of doing global side effects via a diff component in the local domain is also error-prone, as illustrated by the region analysis. The on assignments the update function from above is applied to RegPart and RegMap which seems comprehensive but isn't because it forgets to modify the Vars local component into which it already put something. This is fixable in the region analysis but I think wouldn't really change anything because region offsets still need to be joined right. It just made debugging those 10× harder because looking at all the trace output from solving was very confusing: somehow side-effects appeared with old values that were already changed but of course they did thanks to this mechanism.

[vesalvojdani]

So I don't really see any good reason to keeping the localized vars set... I think the motivation may have been trying to deal with cases where regions collapse and then are restored within a critical section, such as moving elements from one list to another. But then, the attempts to handle this were instead implemented in shape.ml. Anyway, a sync function that always flushes makes no sense to me. Do you see that it actually achieves anything?

[sim642]

The one subtle thing it achieves is supporting "side effects" during global initializers (which currently just fail) by actually sync-ing them on main entry inside the analysis where global domain is actually available.

I will try to add basic global support to the global initializers. This is hopefully easier than getting global initializers to part of the constraint system entirely, which would be nice though. It's very ironic that global initializers cannot access globals...

[michael-schwarz]

The minimizer arrived at the following example program that triggers the bug, though it does not appear helpful here, especially as it does not compile.

#include<stdlib.h>
struct a {
  int b;
};
struct c {
  struct a d;
} typedef *e;

struct c *j;
e l[1];
int m;

g(struct a *n) { n->b = k(); }
main() { g(&j->d); }

int *k() {
  void *h = calloc(1, 8);
  l[m] = h;
  m = m + 1;
  return h;
}

[michael-schwarz]

For reference, here are the current occurrences of this issue:

[sim642]

The minimizer arrived at the following example program that triggers the bug, though it does not appear helpful here, especially as it does not compile.

Additionally conditioning a creduce script to require compilation to succeed (possibly without warnings) would be beneficial here. If the program itself contains weird type inconsistencies, then mismatches in Goblint aren't surprising.