Casting pointer through integer fails

[rafaelsamenezes]

The following program:

#include <inttypes.h>

#define _4KB        0x1000
#define _32KB       0x8000
 
#define _4KB_MASK   (~(_4KB - 1))

#define UINT32 uint32_t 
#define UINT64 uint64_t
void Test()
{
  void *Heap = __ESBMC_alloca(_32KB);
  __ESBMC_assume((UINT64)Heap < 0xFF); 
  
  UINT64 *TabPhy = (UINT64*)(((UINT64)Heap + _4KB) & _4KB_MASK);
  UINT64 *TabPhy_Entry = (UINT64*)(((UINT64)TabPhy + _4KB) & _4KB_MASK);
  
  TabPhy[0] = ((UINT64)TabPhy_Entry);  
  __ESBMC_assert(TabPhy == &TabPhy[0], "i-st of TabPhy is TabPhy[0]");
  int i = 0;
  __ESBMC_assert((*(UINT64 *)TabPhy) == TabPhy[i], "value of TabPhy is TabPhy[i] value");
}

Fails on the last assertion, even though ESBMC knows that they are pointing to the same place. There are also two strange behaviors:

1. If we remove the mask & _4KB_MASK then the assertion does not fail.
2. If we replace TabPhy[i] with TabPhy[0], then the assertion does not fail.

@fbrausse could you take a look into it?

[fbrausse]

@rafaelsamenezes sure, I'll take a look.

1. If we remove the mask & _4KB_MASK then the assertion does not fail.

When you remove the & _4KB_MASK expressions the only ones left are additions, right? Support for + and - in the value-set analysis I added some time ago, but not other expressions. I agree that support for bit-ops should be added around https://github.com/esbmc/esbmc/blob/ee09a075517a6643ec3867710b65ce3c45e2f190/src/pointer-analysis/value_set.cpp#L549

2. If we replace TabPhy[i] with TabPhy[0], then the assertion does not fail.

In #575 we had the same issue.

[mikhailramalho]

Maybe duplicate of #92?

[fbrausse]

Maybe duplicate of #92?

Related indeed. The whole "is it a binary operation? Then just recurse on both operands" falls apart with pointers. I'll fix the patch in PR #679 and try to handle all those cases. I fear though, that we'll never get them all since I do not know what to do in case both operands are type-casted pointers. The canonical test case for that would be the doubly-linked list where each item just stores the XOR of prev and next...

[fbrausse]

The canonical test case for that would be the doubly-linked list where each item just stores the XOR of prev and next...

Maybe not. k-induction and incremental-bmc both can handle xor-dlist.c with #679 and the "recurse on both sides" approach for XOR, but fail when both pointers are connected by + in plus-dlist.c. Not sure if it's this issue or an unrelated one.