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.


------------------------------------------------------------------------------
Last updated on 30 October 2024 by alex@absint.com. Copyright 2024 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
absint.com/releasenotes/compcert/24.10