Partitioned Memory Model for Ultimate

[alexandernutz]

Just throwing out some thoughts related to the memory model of the C translation. I am trying to evaluate if this is a reasonable approach for Ultimate. Depending on how difficult/time-consuming it is, I might implement it, or perhaps it is just one more thing that would be nice to have.

Proposed Addition to the C translation:

• run a pointer analysis on the C program
• use the may-not alias information from that pointer analysis to create several memory~X arrays instead of one
• create the variants of memory~X according to the equivalence classes of pointer variables that are induced by the pointer analysis, i.e., pointer variables in different equivalence classes are guaranteed by the pointer analysis to not alias

This approach is proposed in several papers. One example, including some smart refinements, is Wang, Barret, Wies, Partitioned Memory Models for Program Analysis .

You might ask: Why do that in the C translation?/What is the difference to what the "heap separator" does? Answer: pointer analysis on C is much simpler than its Boogie counterpart because of the following line of reasoning:

• We can assume there is no undefined behaviour in the program. (If there is, this must remain detectable in the translated program, but we can still do the pointer analysis using that assumption.)
• Thus a pointer that points to an invalid memory location is never used to access memory.
• Thus we can ignore the following cases in the alias analysis
  • a pointer holds an indeterminate value
  • a pointer is 0

Example: Say two pointers p and q are both 0 at some point in the program. Then the heap separator must check "Are p and q used to access memory while they have the same value?".
A pointer analysis for C programs can simply make the assumption that neither of them is accessed while it is 0 since that would be undefined behaviour.

[Heizmann]

I do not understand all details here. But I am interested to discuss this after the SV-COMP deadline.