This post describes the implementation of pysmtgcc. See “GCC Translation Validation” for background information.

This post describes the implementation of pysmtgcc. See “GCC Translation Validation” for background information.

This post describes the implementation of pysmtgcc. See “GCC Translation Validation” for background information.

This post describes the implementation of pysmtgcc. See “GCC Translation Validation” for background information.

This post describes the implementation of pysmtgcc. See “GCC Translation Validation” for background information.

I am planning to do some work with SMT solvers and GCC. I usually start new projects by doing a naive implementation of the critical part to get a feel for the problems and find out what I need to learn before the real implementation. So I started this project by building a simple translation validator, similar to the LLVM Alive2 (but with many limitations).

I have recently seen several discussions on Twitter where people have been surprised/annoyed by what the compilers do to their branchless code. Here are some random comments on what the compilers do (and why).

GCC per default enables one optimization for x86_64 that can change the result of floating-point operations: -ffp-contract=fast.¹ This allows the compiler to do floating-point expression contraction such as combining multiplication and addition instructions with an FMA instruction.²

My previous blog post said that computations producing Inf, NaN, or -0.0 in programs compiled with -ffinite-math-only and -fno-signed-zeros might cause the program to behave in strange ways, such as not evaluating either the true or false part of an if-statement.

This blog post describes the optimizations enabled by -ffast-math when compiling C or C++ code with GCC 11 for x86_64 Linux (other languages/operating systems/CPU architectures may enable slightly different optimizations).