Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Combined pthread programs use 32bit architecture #55

Open
sim642 opened this issue Apr 12, 2023 · 0 comments
Open

Combined pthread programs use 32bit architecture #55

sim642 opened this issue Apr 12, 2023 · 0 comments
Labels

Comments

@sim642
Copy link
Member

sim642 commented Apr 12, 2023

Here's a NULL pointer check which has been combined by CIL on a 32bit architecture, as indicated by the casts to unsigned int:

bench/pthread/aget_comb.c

Lines 934 to 941 in f2dedc3

he = gethostbyname((char const *)(req___0->host));
if ((unsigned int )he == (unsigned int )((void *)0)) {
tmp___2 = __h_errno_location();
tmp___3 = hstrerror(*tmp___2);
Log((char *)"Error: Cannot resolve hostname for %s: %s", req___0->host, tmp___3);
exit(1);
}
tmp___4 = inet_ntoa(*((struct in_addr *)*(he->h_addr_list + 0)));

(Those casts being inserted at all for pointer equality is a whole other mystery to me.)

On 64bit architectures those casts would be to unsigned long. When such combined programs are now analyzed by Goblint on a 64bit machine (which all of us do), then Goblint's special handling of ignoring those casts for pointer equality don't apply because the downcast is not injective.

This causes precision problems since branch refinement cannot refine he from {?, NULL} in either branch. This leads to unnecessary NULL/unknown pointer dereferences even if the uncombined program explicitly protects against it.

@sim642 sim642 added the bug label Apr 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant