SPARK2014 and FSF GCC

This is a note about building SPARK (i.e. gnatprove) against an FSF GCC.

AdaCore’s repository’s README has a note in section 7.2,

To build SPARK with GNAT version from FSF, you need to use the corresponding branch of this repository which follows the latest changes pushed at FSF[…]

The “latest changes pushed at FSF” are in the trunk branch, presently (2022-02-18) building GCC 12.0.1 (this is effectively a release candidate), so the first thing is to build GCC 12.0.1, which I did using these scripts, branch gcc-12. The scripts deliberately install the compiler at /opt/gcc-12.0.1, because of macOS’s handling of dynamic libraries (.dylibs); if I deliver to you a dynamic library A, which was built against dynamic library B, A remembers where B was on my filesystem. If you install B somewhere else, A can’t find it; similarly for executables. There are 19 dynamic libraries in this build, each of which would need adjustment; I used to provide the ability to install at a location of your choice, but it’s very complicated, see the script starting here.

More on shared libraries here.

Installing opam

opam is a package manager for OCaml. I have release 2.0.8, though later ones work just fine; there are binary releases on Github. Look for the opam-x.y.z-x86_64-macos asset for your desired release x.y.z.

What you download is the opam executable, but you have to rename it to opam, make it executable, and remove the “quarantine” attribute:

mv opam-x.y.z-x86_64-macos opam
chmod +x opam
xattr -d com.apple.quarantine opam

and, of course, put it somewhere on your PATH (like /usr/local/bin).

GMP

The GNU Multiple Precision Arithmetic Library is needed to install some OCaml packages. OCaml’s builder dune is described by its builders as opinionated and by me as opaque (I expect they’d say the same about gprbuild).

dune compiles C code with the command line

cc -c -I/opt/homebrew/include -I/opt/local/include -I/usr/local/include foo.c

which means it’ll cope with a Homebrew or Macports setup; I won’t use either, and I can’t find a supported way of telling it to use gcc (cc is clang).

The reprehensible workround I came up with (won’t affect users) was:

cd /opt
sudo ln -s /opt/gcc-12.0.1 local

so that not only does dune find the right includes, it finds libgmp.dylib, which knows where it is:

$ otool -L /opt/local/lib/libgmp.dylib
/opt/local/lib/libgmp.dylib:
	/opt/gcc-12.0.1/lib/libgmp.10.dylib (compatibility version 15.0.0, current version 15.1.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.0.0)

Building gnatprove

Building gnatprove and friends was straighforward enough, following the instructions in the README and the Makefile.

The README says to use opam to install a number of packages

• camlzip library
• menhir parser
• ocamlgraph library
• ocplib-simplex library
• zarith library

but I found that most of this (incomplete) list is needed for the prover alt-ergo; since (see later) I couldn’t build the alt-ergo submodule, I only needed

• menhir
• num
• ocamlfind
• yojson

which are sufficient to build why3.

Note, gnatprove and gnat2why are installed to install/bin, other components (e.g.why3) are installed under install/libexec/spark.

Building the provers

I built a common script to set up environment variables:

# GCC stuff
RELEASE=12.0.1
TOP=/opt
COMPILER=$TOP/gcc-$RELEASE

# Cmake stuff -- needed for cvc4
CMAKE=/Applications/CMake.app/Contents

PATH=$COMPILER/bin:$CMAKE/bin:$PATH

CVC4

This was less than straightforward.

This script was the result of several attempts. GCC 12.0.1 is a pre-release compiler, so it’s built with many more checks; compilations can take twice as long as you’d expect from a released compiler.

#!/bin/sh

source common.sh

PREFIX=$PWD/install/libexec/spark

cd cvc4

antlr3=deps/install/bin/antlr3
test -f $antlr3 -a -x $antlr3 || contrib/get-antlr-3.4

CC=gcc CXX=g++                                  \
    ./configure.sh                              \
    --prefix=$PREFIX                            \
    --gpl                                       \
    --gmp-dir=$COMPILER

cd build

make

make install

install_name_tool                               \
  -change                                       \
  @rpath/libcvc4parser.7.dylib                  \
  @executable_path/../lib/libcvc4parser.7.dylib \
  $PREFIX/bin/cvc4

install_name_tool                               \
  -change                                       \
  @rpath/libcvc4.7.dylib                        \
  @executable_path/../lib/libcvc4.7.dylib       \
  $PREFIX/bin/cvc4

See here for more on the last two commands.

Z3

#!/bin/sh

source common.sh

PREFIX=$PWD/install/libexec/spark

cd z3

rm -rf build

CC=gcc CXX=g++                                  \
    python scripts/mk_make.py                   \
    --prefix=$PREFIX                            \
    --gmp

cd build

make

make install

Alt-Ergo

I started off trying to build from the alt-ergo submodule, using this:

#!/bin/sh

source common.sh

PREFIX=$PWD/install/libexec/spark

cd alt-ergo

make clean

./configure                                     \
    --prefix=$PREFIX

# no GTK, so can't build the gui; omit 'make altgr-ergo', do the
# components by hand.

make gen

make alt-ergo-lib
make install-lib

make alt-ergo-parsers
make install-parsers

make alt-ergo
make install-bin

After several failed attempts - I thought, “I’m sure it worked once - was it on the other computer?” (maybe) “Shall I install opam again?” (no) “Why can’t it find the alt-ergo-lib it just built?” …

“Just maybe - opam install alt-ergo and look for an executable …” and there it was, in ~/.opam/default/bin.

Copy this to $PREFIX/bin and there we are! (some problems with actually proving, though).

The script now reads

#!/bin/sh

source common.sh

PREFIX=$PWD/install/libexec/spark

opam install alt-ergo

cp $HOME/.opam/default/bin/alt-ergo $PREFIX/bin