Closed vogler closed 4 years ago
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
Try if this helps: https://github.com/sosy-lab/crest/commit/512de07f8a46f66e9d48e7cba93495cdbc8cc54b
It helped me to get the regression tests running
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).
Same for
$ CC=gcc-9 ./configure
$ CC=gcc-9 make doc
Not crucial, just noticed it because I have OPAMWITHDOC=true
in my zshenv.
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
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
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
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?
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.
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.
[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
...
The cause of kernel1
failing was also using clang instead of gcc.
As of be553fe1, builds and tests pass on MacOS too.
Running
OPAMWITHDOC=true opam switch create .
fails atmake doc
.Without docs it works: