make doc fails on macOS

[vogler]

Running OPAMWITHDOC=true opam switch create . fails at make doc.

Preprocessing cilcode.tmp/ex21.cil.c
Compiling cilcode.tmp/ex21.cil.i into cilcode.tmp/ex21.o

***Found CIL code at line 642
Preprocessing cilcode.tmp/ex22.c
Frontc is parsing cilcode.tmp/ex22.i
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.14.sdk/usr/include/sys/stdio.h[39:80-86] : syntax error
Parsing errorFatal error: exception Frontc.ParseError("Parse error")

Without docs it works:

  ∗ install conf-gmp   1      [required by zarith]
  ∗ install conf-perl  1      [required by zarith]
  ∗ install ocamlbuild 0.14.0 [required by cil]
  ∗ install conf-m4    1      [required by ocamlfind]
  ∗ install ocamlfind  1.8.1  [required by cil]
  ∗ install zarith     1.9.1  [required by cil]
  ∗ install cil        1.7.3*

[vogler]

Changing CC=gcc-9 in Makefile:

...
if gcc-9 -D_GNUCC -m64 src/machdep-ml.c -o _build/machdep-ml64.exe ;then \
	  sed -e "s|nogcc64model|`_build/machdep-ml64.exe --env`|" lib/perl5/App/Cilly.pm > lib/perl5/App/Cilly.pm.tmp; \
	  mv lib/perl5/App/Cilly.pm.tmp lib/perl5/App/Cilly.pm; \
	fi
Generating CIL_MACHINE machine dependency information string (for CIL)
cd lib/perl5; perl Makefile.PL INSTALL_BASE="/usr/local"
Checking if your kit is complete...
Looks good
Generating a Unix-style Makefile
Writing Makefile for cilly
Writing MYMETA.yml and MYMETA.json
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C lib/perl5
cp App/Cilly/KeptFile.pm blib/lib/App/Cilly/KeptFile.pm
cp App/Cilly/OutputFile.pm blib/lib/App/Cilly/OutputFile.pm
cp App/Cilly.pm blib/lib/App/Cilly.pm
cp App/Cilly/TempFile.pm blib/lib/App/Cilly/TempFile.pm
cp App/Cilly/CilCompiler.pm blib/lib/App/Cilly/CilCompiler.pm
cp App/Cilly/CilConfig.pm blib/lib/App/Cilly/CilConfig.pm
cp ../../bin/cilly blib/script/cilly
"/usr/local/Cellar/perl/5.30.0/bin/perl" -MExtUtils::MY -e 'MY->fixin(shift)' -- blib/script/cilly
rm -rf doc/html/cil
mkdir -p doc/html/cil
mkdir -p doc/html/cil/examples
cd doc; perl cilcode.pl cil.tex >cilpp.tex.tmp

***Found CIL code at line 392
Preprocessing cilcode.tmp/ex1.c
Error: interface mismatch on Machdep
Fatal error: exception Errormsg.Error
Raised at file "string.ml", line 115, characters 19-34
Called from file "string.ml", line 119, characters 16-42
Error running CIL for cilcode.tmp/ex1.c at cilcode.pl line 79, <> line 399.
make: *** [doc/cilpp.tex] Error 25

[michael-schwarz]

Try if this helps: sosy-lab/crest@512de07

It helped me to get the regression tests running

[vogler]

No, that doesn't change anything. 'interface mismatch' is only found in the binary, it's something inserted by the OCaml compiler. I guess src/machdep-ml.c.in is used to generate _build/machdep.o and once it uses gcc-9 (gcc) and once gcc (clang).

[vogler]

Same for

$ CC=gcc-9 ./configure
$ CC=gcc-9 make doc

Not crucial, just noticed it because I have OPAMWITHDOC=true in my zshenv.

[michael-schwarz]

A lot of the regression tests also fail with this issue.

Another project that uses CIL has this workaround:
http://tigress.cs.arizona.edu/machine.html#darwin

[michael-schwarz]

I tried the workaround for combinealias_1.c, it resolves the parse error in stdio.h[39:80-86] but there is still one more in /usr/include/stdio.h[360:94-99] : syntax error, so it looks like there is still something else in that header that causes an issue.
See https://travis-ci.com/goblint/cil/jobs/254024026#L7911

[vogler]

On my machine that test works.

Successful tests:     366
Failed as expected:   30
Unexpected success:   4
Unexpected failure:   4

Whereas on travis:

Successful tests:     305
Failed as expected:   31
Unexpected success:   3
Unexpected failure:   65

macOS 10.14.6 (18G95)
$ gcc --version
Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.14.sdk/usr/include/c++/4.2.1
Apple LLVM version 10.0.1 (clang-1001.0.46.4)
$ gcc-9 --version
gcc-9 (Homebrew GCC 9.2.0_1) 9.2.0
$ cpp-9 -v
Using built-in specs.
COLLECT_GCC=cpp-9
Target: x86_64-apple-darwin18
Configured with: ../configure --build=x86_64-apple-darwin18 --prefix=/usr/local/Cellar/gcc/9.2.0_1 --libdir=/usr/local/Cellar/gcc/9.2.0_1/lib/gcc/9 --disable-nls --enable-checking=release --enable-languages=c,c++,objc,obj-c++,fortran --program-suffix=-9 --with-gmp=/usr/local/opt/gmp --with-mpfr=/usr/local/opt/mpfr --with-mpc=/usr/local/opt/libmpc --with-isl=/usr/local/opt/isl --with-system-zlib --with-pkgversion='Homebrew GCC 9.2.0_1' --with-bugurl=https://github.com/Homebrew/homebrew-core/issues --disable-multilib --with-native-system-header-dir=/usr/include --with-sysroot=/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk
Thread model: posix
gcc version 9.2.0 (Homebrew GCC 9.2.0_1)
COLLECT_GCC_OPTIONS='-E' '-v' '-mmacosx-version-min=10.14.0' '-asm_macosx_version_min=10.14' '-mtune=core2'
 /usr/local/Cellar/gcc/9.2.0_1/libexec/gcc/x86_64-apple-darwin18/9.2.0/cc1 -E -quiet -v -D__DYNAMIC__ - -fPIC -mmacosx-version-min=10.14.0 -mtune=core2
ignoring nonexistent directory "/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/local/include"
ignoring nonexistent directory "/usr/local/Cellar/gcc/9.2.0_1/lib/gcc/9/gcc/x86_64-apple-darwin18/9.2.0/../../../../../../x86_64-apple-darwin18/include"
ignoring nonexistent directory "/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/Library/Frameworks"
#include "..." search starts here:
#include <...> search starts here:
 /usr/local/Cellar/gcc/9.2.0_1/lib/gcc/9/gcc/x86_64-apple-darwin18/9.2.0/include
 /usr/local/Cellar/gcc/9.2.0_1/lib/gcc/9/gcc/x86_64-apple-darwin18/9.2.0/include-fixed
 /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include
 /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/System/Library/Frameworks
End of search list.

/usr/local/Cellar/gcc/9.2.0_1/lib/gcc/9/gcc/x86_64-apple-darwin18/9.2.0/include-fixed/stdio.h: https://termbin.com/ay5u
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.14.sdk/usr/include/stdio.h: https://termbin.com/cj0k

[vogler]

make doc also fails on WSL Ubuntu:

$ opam install goblint-cil
The following actions will be performed:
  ∗ install conf-gmp    1     [required by zarith]
  ∗ install zarith      1.9.1 [required by goblint-cil]
  ∗ install goblint-cil 1.7.4
===== ∗ 3 =====
Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[goblint-cil.1.7.4] found in cache
[zarith.1.9.1] found in cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed conf-gmp.1
∗ installed zarith.1.9.1
[ERROR] The compilation of goblint-cil failed at "/usr/bin/make doc".

#=== ERROR while compiling goblint-cil.1.7.4 ==================================#
# context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.09.0 | https://opam.ocaml.org#ef92414c
# path        ~/.opam/default/.opam-switch/build/goblint-cil.1.7.4
# command     /usr/bin/make doc
# exit-code   2
# env-file    ~/.opam/log/goblint-cil-5402-d4902a.env
# output-file ~/.opam/log/goblint-cil-5402-d4902a.out
### output ###
# [...]
# /usr/bin/make -C lib/perl5
# make[1]: Entering directory '/home/voglerr/.opam/default/.opam-switch/build/goblint-cil.1.7.4/lib/perl5'
# make[1]: Leaving directory '/home/voglerr/.opam/default/.opam-switch/build/goblint-cil.1.7.4/lib/perl5'
# rm -rf doc/html/cil
# mkdir -p doc/html/cil
# mkdir -p doc/html/cil/examples
# cd doc; perl cilcode.pl cil.tex >cilpp.tex.tmp
#
# ***Found CIL code at line 392
# Cannot find GNUCC version
# Error running CIL for cilcode.tmp/ex1.c at cilcode.pl line 79, <> line 399.
# make: *** [Makefile:244: doc/cilpp.tex] Error 25

$ uname -a
Linux i5-6600 4.4.0-18362-Microsoft #476-Microsoft Fri Nov 01 16:53:00 PST 2019 x86_64 x86_64 x86_64 GNU/Linux
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu Focal Fossa (development branch)
Release:        20.04
Codename:       focal
$ gcc --version
gcc (Ubuntu 9.2.1-21ubuntu1) 9.2.1 20191130
Copyright (C) 2019 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
$ gcc -dumpversion
9

Problem: https://github.com/goblint/cil/blob/develop/lib/perl5/App/Cilly.pm.in#L2215
I thought the patch should make it work with single-digit versions?

[michael-schwarz]

The problem does not occur on my Ubuntu machine with

$ gcc --version
gcc (Ubuntu 7.4.0-1ubuntu1~18.04.1) 7.4.0
Copyright (C) 2017 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

$ gcc -dumpversion
7

and the regex used in the code matches also on 9.

Best would probably be if you output the string to which perl is trying to match the regex to see if it is really 9.

Edit: Also works with Ubuntu 19.10 and GCC 9.2.1, so it is definitely not a general problem with GCC 9.

[michael-schwarz]

Now down to 4 tests failing for MacOS (from over 60). Achieved by setting CC=gcc-9.

- [76] A regression test command failed:
-   make scott/kernel1
- [117] A regression test command failed:
-   make test/asm4
- [392] A regression test command failed:
-   make testrunc99/c99-complex
- [395] A regression test command failed:
-   make testrunc99/c99-tgmath

We should probably take a look at the four that are still failing on an actual MacOS machine.

[michael-schwarz]

[117] A regression test command failed:
  make test/asm4
[392] A regression test command failed:
  make testrunc99/c99-complex
[395] A regression test command failed:
  make testrunc99/c99-tgmath

Those three seem to be related to newer versions of GCC and/or glibc, and not MacOS necessarily. Also fail on Ubuntu 19.10 with GCC 9 and glibc 2.30-0ubuntu2.

Which leaves kernel1...

[michael-schwarz]

The cause of kernel1 failing was also using clang instead of gcc.
As of be553fe, builds and tests pass on MacOS too.