Inconsistent behavior of string literals between reference interpreter and generated object code

[monniaux]

On x86-64 (possibly on other architectures) the following program returns 1:

int main() {
  const char * const a = "ABBA";
  const char * const b = "BA";
  return (b==a+2);
}

This is due to the use of string literal linker sections that the linker is allowed to merge: if a string is a right substring of another, then it will be merged into the other string. (This is reasonable especially for printf format strings.)

Yet CompCert's interpreter returns 0, as it considers that a and b point to two different string literals, each living in its own block.

This is not a serious issue. Maybe a word of warning in the manual? Or an option for disallowing mergeable linker sections?

[xavierleroy]

The C standard (C11 6.4.5 (7)) allows sharing between string literals, but doesn't mandate it, so both the CompCert C semantics (which doesn't share) and the linker (which sometimes shares) are correct. Actually, the CompCert C semantics, and therefore the reference interpreter, has no notion of string literal, it treats then as const arrays of chars, for which sharing is not allowed, so there's no choice here.

Shareable string literals were introduced kind of by accident (they are the default on macOS), then made to work reliably in a2c0973. I wouldn't mind removing this support altogether, as I don't think it makes a big difference in data size in practice.