Different field access on imprecise address set

[sim642]

I continued looking at chrony after #712 and found another little bit of unsoundness: the callback function name_resolve_handler is never called.
The problem is that at an intermediate level of callbacks in sched.c, the eventual callback name_resolve_handler is stored in the intermediate callback's opaque argument, which ends up being an ambiguous set of addresses pointing to structs of different types. This is because in other places the same sched.c mechanism is used for something else as well. Later when trying to access a particular field of that, we immediately get VD.top since simple structs are implemented using a MapTop domain, where looking up the other struct's field gives the default VD.top.

I've extracted the problem to https://github.com/goblint/analyzer/tree/ambig-field. A minimized test case is the following:

analyzer/tests/regression/01-cpa/56-ambig-field.c

Lines 21 to 38 in ab70c9b

	struct S1 s1 = {.f1 = &foo};
	struct S2 s2 = {.f2 = &bar};
	int r; // rand
	void *sp;
	if (r)
	sp = &s1;
	else
	sp = &s2;
	// simulate imprecision
	// in chrony this wouldn't be path-based but joined in the global invariant
	// one of these field accesses is randomly invalid
	void (*fp1)(void) = ((struct S1*)sp)->f1;
	void (*fp2)(void) = ((struct S2*)sp)->f2;
	// but we shouldn't forget &foo and &bar here and consider both dead
	fp1();
	fp2();

Simple structs

Tracing the program reveals the two structs being joined, giving an empty struct (remember, this is MapTop, which is reversed):

          %%% get: Singlethreaded mode.
          %%% get: var = mapping {
                           f1 ->   {&foo}
                         }, {&s1} = mapping {
                                        f1 ->   {&foo}
                                      }
          %%% get: Singlethreaded mode.
          %%% get: var = mapping {
                           f2 ->   {&bar}
                         }, {&s2} = mapping {
                                        f2 ->   {&bar}
                                      }
          %%% get: Result: mapping {
                             }

Then of course accessing either field on the result returns VD.top and completely forgets the known pointers.

Set structs

One might hope that a more powerful structs domain (sets) would help here, but no:

          %%% get: Singlethreaded mode.
          %%% get: var = {mapping {
                            f1 ->   {&foo}
                          }}, {&s1} = {mapping {
                                           f1 ->   {&foo}
                                         }}
          %%% get: Singlethreaded mode.
          %%% get: var = {mapping {
                            f2 ->   {&bar}
                          }}, {&s2} = {mapping {
                                           f2 ->   {&bar}
                                         }}
          %%% get: Result: {mapping {
                              f1 ->   {&foo}
                            }, mapping {
                                   f2 ->   {&bar}
                                 }}
        %%% cast: (tests/regression/01-cpa/56-ambig-field.c:34:3-34:43)
  cast {mapping {
          f1 ->   {&foo}
        }, mapping {
               f2 ->   {&bar}
             }} from ? to struct S1  is {mapping {
                                             f1 ->   Unknown
                                           }}!

Here the join preserves both possibilities as a set, but then casting them elementwise to the particular struct type will still give VD.top in the field, again forgetting the known pointers.

Further thoughts

The thing to note here (which I was also surprised by) is that when looking up fields from ambiguous addresses, we don't apply eval_offset on each ambiguous possibility separately and then join the results, but instead join the structs and apply one eval_offset on the joined result. So the base analysis is super non-relational here, which makes this additionally annoying to fix. If it was the other way around, it would be possible in base to only filter out the possibilities, where the offset actually exists. In its current form, the struct domain must at the intermediate stage be able to represent the ambiguous struct and then allow eval_offset to just use the field it needs, ignoring other possibilities.

It's very much possible that we have the same problem on zstd as well (it might even be the source of the VD.tops we try to ignore with #707) because the overall construction is the same: each job is represented by a struct consisting of a function pointer and an opaque argument pointer to it. Since we are so non-relational here, we end up passing all the possible argument pointers (to structs of different types) to all the function pointers. Most of these combinations are nonsense, but we don't say anything, don't assume anything, but just become very imprecise (to the point of unsoundness by forgetting function pointers that might be called).