CompCert Release 19.10
----------------------


If-conversion optimization
-------------------------
The instruction selection pass has been extended 
with an if-conversion optimization.

In certain circumstances, the conditional operator "?:", 
the logical operators "&&" and "||", and if/then/else 
statements are converted into "select" operations, which in turn 
can be compiled down to branchless instruction sequences 
if the target architecture supports them.

The conversion only applies to constructs of the form:

  cond ? a1 : a2
  a1 && a2
  a1 || a2
  if (cond) { x = a1; } else { x = a2; }
  if (cond) { x = a1; }
  if (cond) { /*skip*/; } else { x = a2; }

where a1 and a2 are "safe" expressions, containing no operations 
that can fail at run-time, such as memory loads or integer divisions.

A heuristic controls when the optimization occurs, and the new 
command line option -Obranchless enforces that it is always applied.
The optimization is controlled by the flag -f(no)if-conversion.

Improved built-in functions
--------------------------
● __builtin_bswap64 is now available for all backends.

● CompCert now features a mechanism to specify formal semantics 
  for built-in functions and run-time functions, enabling 
  optimizations of calls to those. 
  
  The following built-in functions now have formal semantics:

  __builtin_sel
  __builtin_fabs
  __builtin_fsqrt
  __builtin_bswap16
  __builtin_bswap
  __builtin_bswap32
  __builtin_bswap64


New diagnostics
---------------
● New diagnostic for multiple unnamed void parameters.
● New diagnostic for wrong parameters of calls of unprototyped functions.
● New diagnostic "non-linear-cond-expr" that generates a diagnostic 
  for conditional expressions that may not be transformed by if-conversion.

Other improvements
------------------
● Improved constant propagation for 64-bit PowerPCs.
● New tracing option for clightgen to dump the pre-processed source code.
● New predefined macros for checking the CompCert version and build number.

Fixes
-----
● Fixed normalization of switch expression in clightgen.
● The inline optimization is now also disabled if -O0 is specified.


------------------------------------------------------------------------------
Last updated on 20 September 2019 by alex@absint.com. Copyright 2019 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
absint.com/releasenotes/compcert/19.10