Skip to content

Combined pthread programs use 32bit architecture #55

Open
@sim642

Description

@sim642

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions