[Cryptech Tech] The compcert compiler

[Peter Gutmann]

Rob Austein <sra at hactrn.net> writes:

>Unclear how close it is to being a drop-in replacement for gcc. Command line
>syntax as shown in the manual is very gcc-like, but stm32 builds use enough
>fiddly gcc options that there are likely to be divergences, the questions
>would be how serious and how hard to fix.

>Unclear how close it is to being a drop-in replacement for gcc. Command line
>syntax as shown in the manual is very gcc-like, but stm32 builds use enough
>fiddly gcc options that there are likely to be divergences, the questions
>would be how serious and how hard to fix.

I looked at it a while back and it's kinda painful to work with, you need a
bunch of other oddball tools, and specific versions of some of the tools, and
those tools need further tools, and eventually you end up going down a rabbit
hole of dependencies to the point where I gave up before getting anything
working.  From what I've read about it it's a decent-enough compiler, but if
you just want to play with it for a bit to see what it's like it's a bit too
much effort.

(It seems to be a built-in misfeature of a lot of code and binary analysis
tools that they were developed to work with one very specific config and don't
work with anything else.  Not a criticism of compcert, but of all the
code/binary-analysis tools that are written up in reports and conference
papers:

 - The vast majority are never published.
 - Of the ones that are published, many will never work outside the specific
   environment that the authors have set up.
 - Of the ones that are published and can be made to work on a generic
   system, way too much work is typically required to get them running.
   And when they are set up, updates to any of them components they use
   can break them.

So sticking with clang or gcc is a pretty safe option, you can move to the
latest version and (a) it'll just work and (b) it probably won't break
things).
 
Peter.