Tracking function pointers in indirectly pointed structures

[jprotopopov-ut]

Goblint revision: e816b4a
The following snippet:

struct S {
	int type;
	void (*cb)(void);
	struct S *nested;
};

void test(const struct S *s) {
	for (; s && s->type; s++) {
		if (s->type == 1) {
			test(s->nested);
		} else {
			s->cb();
		}
	}
}

void dummy(void) {}

int main() {
	struct S s1[] = {
		{2, dummy},
		{0}
	};
	struct S s2[] = {
		{1, 0, s1},
		{0}
	};

	test(s2);
	return 0;
}

causes Goblint to output soundness warning:

[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call.

The snippet has been manually extracted from invokeCallbacksPRE_230228 function of AnalyzeThat rsync, where the same soundness warning is observed.

[michael-schwarz]

Are we sure the warning comes from the context where we should reasonably know what this points to.

It seems that the call chain goes

test(s2)
-> test(s1) (a)
---> dummy()
<--
-> (increment of s, points to s2 if the things are adjacent in memory) (b(

I guess this increment of s is not really guaranteed to work, as the locals s1 and s2 need not be placed right next to each other in the stack?

We don't have a linear memory layout for locals in Goblint, so we're bound to end up with nonsense when someone does address arithmetic across object boundaries. So if we don't know what to do in (b), that is sort of OK.

But if it's already the first call (a) that is problematic here, that's indeed bad!

[jprotopopov-ut]

I guess this increment of s is not really guaranteed to work, as the locals s1 and s2 need not be placed right next to each other in the stack?

I am not quite sure why do you believe local placement is relevant here. The execution starts with considering 1st element of s2 (note that it's an array), immediately going into the recursion, considering first element of s1, making a call, considering second element of s1 and exiting on loop condition (type is zero), then considering second element of s2 and exiting upon the loop condition.

[jprotopopov-ut]

To confirm, I have just re-tested with adding static to the definition of s1 to make sure that variables are clearly separated spatially, and also recompiled with ubsan. The sample is still functioning as expected.

[michael-schwarz]

note that it's an array

Yeah, didn't read it closely enough, never mind!

[michael-schwarz]

I thought adding --set ana.base.arrays.domain partitioned might make it better, but that makes it worse, with that one additionally gets:

[Warning][Deadcode] Function 'dummy' is uncalled: 1 LLoC (1.c:17:1-17:19)

[sim642]

Without having looked at the abstract states to see where pointers get lost... maybe our set-based (or keyed) struct domains are useful here?

Although one would hope to be sound regardless, but maybe there's too much joining happening with the 0s, causing value domain supertops.