`compinfo` keys not updated incrementally

[sim642]

UpdateCil updates IDs of statements (sid) and variables (vid), but not compinfo keys (ckey). I already wondered this in #598 but now here's concrete evidence that not updating them causes issues for incremental updating as well.

Reproduction

Analyze the following program incrementally (before vs after patching): https://github.com/goblint/bench/tree/b79d0997d2bf3444f6296301e0bfc7bdebc8788c/cve-bench/CVE-2019-19537.
In order to see the problem, 5cfb7e6 needs to be reverted, because it simply hides the problematic accesses. Nevertheless, similar structs and unions could be used in actual user code, which the access analysis shouldn't ignore.

Before

On initial analysis, there's the following memory location with four accesses:

[Warning][Race] Memory location (struct usb_interface).dev(119532124,usb_interface).mutex(1002340388,device).wait_lock(655119850,mutex).__annonCompField18(448810155,spinlock).rlock(344401721,__anonunion____missing_field_name_256509364).raw_lock(706607406,raw_spinlock).__annonCompField17(637443086,arch_spinlock).tickets(201271018,__anonunion____missing_field_name_45265226).head(313990837,__raw_tickets)(119532124) (race with conf. 80):
  read with mhp:{tid=[], {usb_register_dev, usb_devnode}} (conf. 80) (file.c:68:2-68:32)
  read with mhp:{tid=[], {usb_register_dev}} (conf. 80) (file.c:200:2-200:114)
  write with mhp:{tid=[], {usb_register_dev, usb_devnode}} (conf. 80) (file.c:68:2-68:32)
  write with mhp:{tid=[], {usb_register_dev}} (conf. 80) (file.c:200:2-200:114)

Here the offset fields have debug printout of the ckey and cname of the compinfo they belong to.

After

After patching, the result differs when analyzed in server mode vs without it.

In server mode

Surprisingly, the number of safe and total memory locations goes up, because the previous four accesses now are split between two slightly different memory locations:

[Success][Race] Memory location (struct usb_interface).dev(119532124,usb_interface).mutex(1002340388,device).wait_lock(655119850,mutex).__annonCompField18(448810155,spinlock).rlock(344401721,__anonunion____missing_field_name_256509364).raw_lock(706607406,raw_spinlock).__annonCompField17(637443086,arch_spinlock).tickets(757927913,__anonunion____missing_field_name_45265226).head(313990837,__raw_tickets)(119532124) (safe):
  read with [mhp:{tid=[], {usb_register_dev}}, lock:{minor_rwsem}] (conf. 80) (file.c:201:2-201:114)
  write with [mhp:{tid=[], {usb_register_dev}}, lock:{minor_rwsem}] (conf. 80) (file.c:201:2-201:114)

[Warning][Race] Memory location (struct usb_interface).dev(119532124,usb_interface).mutex(1002340388,device).wait_lock(655119850,mutex).__annonCompField18(448810155,spinlock).rlock(344401721,__anonunion____missing_field_name_256509364).raw_lock(706607406,raw_spinlock).__annonCompField17(637443086,arch_spinlock).tickets(201271018,__anonunion____missing_field_name_45265226).head(313990837,__raw_tickets)(119532124) (race with conf. 80):
  read with mhp:{tid=[], {usb_register_dev, usb_devnode}} (conf. 80) (file.c:68:2-68:32)
  write with mhp:{tid=[], {usb_register_dev, usb_devnode}} (conf. 80) (file.c:68:2-68:32)

The difference in the locations is that the second-to-last field offset tickets belongs to different structs: for reused accesses it's with key 201271018 and for new accesses it's 757927913. This ckey difference in one offset component is enough to consider them completely separate memory locations.

This result is unsound because the old racing accesses also race with the new accesses that have the extra lock.

Without server mode

Outside of server mode, all four accesses remain together under one memory location, as expected.

Explanation

The problem is that compinfo keys are assigned from nextCompinfoKey in CIL. In server mode, both before and after programs are parsed during a single Goblint execution, therefore the counter doesn't reset in between. Without server mode, the before and after programs are parsed during separate Goblint execution, thus both start with the same counter value.

Even outside of server mode it only works by coincidence that the number and order of defined structs/unions does not change, such that they get identical keys. I haven't tested this but I suspect if that were to change, this could also cause issues outside of server mode.

So clearly UpdateCil also needs to fix up compinfo keys.

Additional notes

The problematic struct-union-emalgamation in Linux kernel headers is this:

typedef struct arch_spinlock {
	union {
		__ticketpair_t head_tail;
		struct __raw_tickets {
			__ticket_t head, tail;
		} tickets;
	};
} arch_spinlock_t;

In CIL:

• The keys are assigned incrementally here: https://github.com/goblint/cil/blob/da5e1941db81643ef0d2133960cd28a7de311131/src/cil.ml#L1498-L1499.
• This is also documented in the interface: https://github.com/goblint/cil/blob/da5e1941db81643ef0d2133960cd28a7de311131/src/cil.mli#L365-L369.
• Contradictorily, the ckey field documentation in the implementation says they are based on a name hash: https://github.com/goblint/cil/blob/da5e1941db81643ef0d2133960cd28a7de311131/src/cil.ml#L353-L357.
• Turns out that's what Mergecil does later: https://github.com/goblint/cil/blob/da5e1941db81643ef0d2133960cd28a7de311131/src/mergecil.ml#L1510.

This hashing explains why all the ckeys in the above output are so large. But it also poses issues for the incremental updating, because unlike sids and vids they aren't assigned sequentially (at least in the merged files that get compared).

And it also creates further confusion, because in both cases the corresponding cname is identical: __anonunion____missing_field_name_45265226. Nevertheless, somehow they end up with different keys. I'm not sure why, but might be because the anonymous union with a missing field name initially gets a different name and during merging the names are somehow unified but the keys are not?

[jerhard]

How did you test this with server mode? Were you using GobPie?

[sim642]

How did you test this with server mode? Were you using GobPie?

I probably used server mode from the command line, by starting it with

rlwrap ./goblint --enable server.enabled --enable server.reparse ...

and just entering the request JSON to stdin, e.g.

{"jsonrpc":"2.0","id":0,"method":"analyze","params":{}}

I thought we documented this somewhere, but apparently only in the interactive stories: https://github.com/goblint/bench/blob/8ff038ba93c6cdbdb0ed3d6f992083d14047c719/gobpie-demos/chrony/story.md.

[jerhard]

Does the server mode reset Cil data structures that are global, for example MergeCil.theFile? @stilscher and I were looking at this, and it we thought that maybe some of the data structures need to be reset, but aren't as of now.

It is strange that these muliple declarations of globals only appears in the server mode for this file.

[jerhard]

It seems that these data structures are reset in MergeCil.init, which in turn is called by MergeCil.merge, so one would assume that this works; but maybe some of the data structures are missed and not reset?

[sim642]

Might be useful to output which declaration it finds multiple of. Maybe it's somehow related to the original compinfo issue that the same struct declaration with the same name ends up having two different ckeys.

[jerhard]

Might be useful to output which declaration it finds multiple of.

There are two functions for which multiple declarations are found in the incremental server run:

static inline int pid_alive(const struct task_struct *p);
static __always_inline void data_access_exceeds_word_size(void)

Where __always_inline is defined as inline __attribute__((always_inline)). It is interesting that both functions are static inline functions. However, there are quite some static inline functions in the same source files that do not have this issue.
When running the incremental analysis multiple times in server mode, the number of declarations of the two functions above (or any others) does not further increase, i.e. the number of declarations of these functions stays at two starting from the first incremental run.

[jerhard]

However, there are quite some static inline functions in the same source files that do not have this issue.

While there are quite some other static inline functions, these two functions I could find were the only static inline functions that have a function declaration separate from the definition in bench/cve-bench/CVE-2019-19537.

[sim642]

It's still a bit odd that it happens only in server mode and only for the first incremental run.

Seems like Mergecil tries to only emit a single declaration for each function here: https://github.com/goblint/cil/blob/5a3b7bb7f4d9b67678826ab7698f8a9048891553/src/mergecil.ml#L1370-L1381. But somehow that's not working here. Maybe some of that processVarinfo logic, which also depends on inlining, is creating new instances for each declaration of an inline function, while it should only happen for definitions or something?