Bug: C2Boogie translation crashes when pointers are subtracted

[bahnwaerter]

The current C2Boogie translation crashes when pointers are subtracted. This issue can be reproduced with the latest version of Ultimate Automizer (0.2.4-dev-5afc37e with OpenJDK 11.0.22) using the following input:

//#SAFE

typedef long unsigned int uint32_t;

typedef struct GPIO_Type {
  volatile uint32_t CRL;
  volatile uint32_t CRH;
  volatile uint32_t IDR;
  volatile uint32_t ODR;
  volatile uint32_t BSRR;
  volatile uint32_t BRR;
  volatile uint32_t LCKR;
} GPIO_TypeDef;

#define PERIPH_BASE      0x40000000UL
#define APB2PERIPH_BASE (PERIPH_BASE + 0x00010000UL)

#define GPIOA_BASE      (APB2PERIPH_BASE + 0x00000800UL)
#define GPIOB_BASE      (APB2PERIPH_BASE + 0x00000C00UL)

#define GPIOA           ((GPIO_TypeDef *)GPIOA_BASE)
#define GPIOB           ((GPIO_TypeDef *)GPIOB_BASE)

int main()
{
  assert(0 < (GPIOB - GPIOA));
  return 0;
}

Considering this example input, the C2Boogie translation crashes when trying to translate the subtraction of the two pointer addresses (GPIOB - GPIOA).

[bahnwaerter]

The source of error can be tracked down to a limitation in the CExpressionTranslator of the C2Boogie translation. The sanity check that compares the types of the two pointers is too strict.

The error can be fixed by replacing the strict check (!leftPointsToType.equals(rightPointsToType)) with the weaker check !leftPointsToType.isCompatibleWith(rightPointsToType).

Is this a fix that really solves the issue, or does it introduce other problems?

[schuessf]

I just checked it, we have two different named-types in our translation for this example, but with the same underlying type. So I just implemented your suggested fix, it should not be problematic, since we only use the underlying type anyway.

[maul-esel]

Is the relation isCompatibleWith symmetric? If not, is there a specific reason why we only test one direction? Also, if the two types are compatible but different, is it always sound to use the left type?

Just because the example has two named types with the same underlying type, doesn't mean that this is the only case that can appear. Maybe an alternative solution would be to check equality of the underlying types instead.

[schuessf]

I think isCompatibleWith was designed to be symmetric. However, the specification is not really precise 🙃:

This is a special notion of type compatibility that we use for matching function signatures. -- i.e. for the most part we say void is "compatible" with everything.. TODO: think about how general this notion is.

Also I found out that the fix is the only place, where isCompatibleWith is used, so maybe we should rather get rid of this method and use your proposed fix. This should also be inline with the C-standard:

When two pointers are subtracted, both shall point to elements of the same array object, or one past the last element of the array object.