Encode and enforce read-only markings in memory handling

[invd]

This ticket is opened on behalf of @jhoenicke, who has suggested it during the last meeting.

To my knowledge, Ultimate currently has no concept of memory areas which are supposed to be treated as read-only, and @jhoenicke is proposing to encode this information in some sort, eg. in an extended valid flag as well as matching checks on write operations.

Motivation: this feature is required for correct handling of const char strings, for example:

//#Unsafe

int main() 
{
  const char *conststring = "42";
  conststring[0] = '0';
  return 1;
} 

Writing to such a structure is forbidden, and gcc will not compile:

error: assignment of read-only location ‘*conststring’
   conststring[0] = '0';

Yet currently, Ultimate has no issue with such a write access:

  - AllSpecificationsHoldResult: All specifications hold
    3 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!

Toolchain used for this example:

• AutomizerMemDerefMemtrack.xml

Settings:

• svcomp-DerefFreeMemtrack-32bit-Automizer_Default.epf
• svcomp-DerefFreeMemtrack-32bit-Automizer_Bitvector.epf

[invd]

Ultimate still happily returns "Ultimate proved your program to be correct!" for the example program that does not even compile due to gcc read-only checks. ("assignment of read-only location")

Since this lack of support is effectively a large problem for verification soundness of programs involving const variables, I'd argue it deserves an elevated priority with regards to future changes to the memory implementation.

[invd]

The newest cf7845638a016090978a13501adca3f0b2bbcea4 Ultimate is still affected by this and returns unsound answers:

RESULT: Ultimate proved your program to be correct!

What is the roadmap on this issue?

[danieldietsch]

There is general progress in this direction (changes in our memory model) but I do not expect a resolution in the next 3 months.