CompCert release 24.10

New features

• New optimization option -fextract-addr to improve code for addressing computations of global variables. Enabled by default.
• New Clang-compatible option -f(no)-color-diagnostics to enable/disable the diagnostics color.
• New configuration that instructs Valex to expect that symbols are not associated with a section in the compiled binary.

Improved value analysis

• More precise value analysis for:
  • comparison and selection instructions
  • function arguments
  • neg, add, sub
  • loads from pointers to _Bool, and the corresponding optimizations of casts to _Bool types
• Improved value analysis of:
  • divu, divs,
  • modu, mods,
  • mul, mulhs, and mulhu.

Improved if-conversion heuristic

• Limit recursive calls on if–then–else statements to avoid quadratic behaviors.
• Deactivate the if-conversion in cases where later optimization of conditional branches leads to better results.

ARM

• Improved pointer + imm offset addressing, especially in Thumb mode for smaller code.
• Improved constant propagation for andimm.

PowerPC

• Improved code generation for >= and <= comparisons.

Other improvements

• Optimize

  (x ^ n) != 0

  into

  x != n

  for PowerPC, ARM and AArch64.
• More conservative analysis of pointer equality and difference.
• Mark stack as non-executable in binaries produced by ccomp for BSD and Linux targets.
• More precise CSE analysis for redundant load instructions.
• Improvements to the CSE optimization.

Valex

• Fixed false alarm for symbols with large addresses.