Fails on macOS Sequoia ver. 15.1.1 INTEL #306
Comments
|
I got the same issue on MacBookPro M1 (Sequoia ver. 15.1.1 too) |
|
For information, I am able to build and run the tools manually on v3.4 : The need to use : |
|
@DamZera Is this tag 3.4 or is this the current master? I ask because issue #292 fixed a problem that people were finding in newer versions of Python (and with never versions of macOS). |
|
It was on tag v3.4. I try the fix from #292 but it did not resolve my tests failed. I will dig when I have more to play with it. |
|
Is IKOS working otherwise? Were the tests working before? It could be a separate problem. |
|
MacOS Sequoia $ brew install nasa-sw-vnv/core/ikos
==> Auto-updating Homebrew...
Adjust how often this is run with HOMEBREW_AUTO_UPDATE_SECS or disable with
HOMEBREW_NO_AUTO_UPDATE. Hide these hints with HOMEBREW_NO_ENV_HINTS (see `man brew`).
==> Fetching nasa-sw-vnv/core/ikos
==> Downloading https://files.pythonhosted.org/packages/7e/ae/26808275fc76bf2832deb10d3a3ed3107bc4de01b85dcccbe525f2cd6d1e/Pygments-2.4.2.tar.gz
Already downloaded: /Users/ignacylatka/Library/Caches/Homebrew/downloads/6ca94f739e0ce8b61064d8fa84dcd6adf34e71e1a606f1ec9403a187965de88c--Pygments-2.4.2.tar.gz
==> Downloading https://github.com/NASA-SW-VnV/ikos/archive/refs/tags/v3.4.tar.gz
Already downloaded: /Users/ignacylatka/Library/Caches/Homebrew/downloads/c1ac6a3a7673251b28ad826e61187ec64a562d110633a344ae2068bc960755ef--ikos-3.4.tar.gz
==> Installing ikos from nasa-sw-vnv/core
==> python3 -m venv --system-site-packages --without-pip /opt/homebrew/Cellar/ikos/3.4_1/libexec
==> python3 -m pip --python=/opt/homebrew/Cellar/ikos/3.4_1/libexec/bin/python install /private/tmp/ikos--Pygments-20241219-21948-dak2fc/Pygments-2.4.2
==> cmake -G Unix Makefiles -DGMP_ROOT=/opt/homebrew/opt/gmp -DMPFR_ROOT=/opt/homebrew/opt/mpfr -DPPL_ROOT=/opt/homebrew/opt/ppl -DAPRON_ROOT=/opt/homebrew/opt/apron -DCUSTO
==> make install
Last 15 lines from /Users/ignacylatka/Library/Logs/Homebrew/ikos/04.make:
[ 11%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/bundle.cpp.o
[ 13%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/code.cpp.o
[ 13%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context.cpp.o
[ 13%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context_impl.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/data_layout.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/function.cpp.o
[ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/intrinsic.cpp.o
[ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/statement.cpp.o
[ 18%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/type.cpp.o
[ 18%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/value.cpp.o
[ 19%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/frontend.cpp.o
[ 19%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/type.cpp.o
[ 21%] Linking CXX static library libikos-ar.a
[ 21%] Built target ikos-ar
make: *** [all] Error 2 |
|
Please note that I have the same brew install problem but on an ARM M3 MacBookPro. |
|
I've been able to replicate this issue. The problems seems to stem from g++ being unable to find standard includes like I'm trying to debug it using Github actions but the feedback loop is ofc slow and I don't have a terminal. I'd appreciate the help from someone with a Mac. I'm happy to jump on a call if doing this together interactively can help. |
|
@latekvo The last compilation step |
|
You can see my experiments here: https://github.com/ivanperez-keera/ikos-test/ I'd appreciate the help to make this work. I don't have access to a modern Mac with root access. It's really hard to do it using github actions. |
|
@ivanperez-keera, I currently don't have access to the Mac machine, but I've encountered similar issues on my Linux machine. upon running:
I encountered the following error: -- Found LLVM: /usr (found version "18.1.8")
CMake Error at frontend/llvm/CMakeLists.txt:107 (message):
LLVM 14 is required.Please note, that it found the 18.1.8 version only after manually setting some env vars, before that no version was found. Fixed this issue by explicitly setting the
Continuing with installation:
Resulted in the following error: armado@arche:~/dev/ikos/build (master %) $ make
[ 0%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/dot.cpp.o
[ 1%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/namer.cpp.o
[ 1%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/text.cpp.o
[ 3%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/add_loop_counters.cpp.o
[ 3%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/add_partitioning_variables.cpp.o
[ 4%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/name_values.cpp.o
[ 4%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/pass.cpp.o
[ 6%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_cfg.cpp.o
[ 6%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_upcast_comparison.cpp.o
[ 7%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/bundle.cpp.o
[ 7%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/code.cpp.o
[ 9%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context.cpp.o
[ 9%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context_impl.cpp.o
[ 11%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/data_layout.cpp.o
[ 11%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/function.cpp.o
[ 11%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/intrinsic.cpp.o
[ 12%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/statement.cpp.o
[ 12%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/type.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/value.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/frontend.cpp.o
[ 15%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/type.cpp.o
[ 15%] Linking CXX static library libikos-ar.a
[ 15%] Built target ikos-ar
[ 15%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/initialize.cpp.o
[ 17%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_cst_expr.cpp.o
[ 17%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_select.cpp.o
[ 19%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/mark_internal_inline.cpp.o
[ 19%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/name_values.cpp.o
[ 20%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_printf_calls.cpp.o
[ 20%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_unreachable_blocks.cpp.o
[ 22%] Linking CXX static library libikos-pp.a
[ 22%] Built target ikos-pp-lib
[ 23%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp.dir/src/ikos_pp.cpp.o
[ 23%] Linking CXX executable ikos-pp
/usr/bin/ld: cannot find -lLLVMAggressiveInstCombine: No such file or directory
/usr/bin/ld: cannot find -lLLVMAnalysis: No such file or directory
/usr/bin/ld: cannot find -lLLVMAsmParser: No such file or directory
/usr/bin/ld: cannot find -lLLVMBitReader: No such file or directory
/usr/bin/ld: cannot find -lLLVMBitWriter: No such file or directory
/usr/bin/ld: cannot find -lLLVMCodeGen: No such file or directory
/usr/bin/ld: cannot find -lLLVMCore: No such file or directory
/usr/bin/ld: cannot find -lLLVMCoroutines: No such file or directory
/usr/bin/ld: cannot find -lLLVMInstCombine: No such file or directory
/usr/bin/ld: cannot find -lLLVMInstrumentation: No such file or directory
/usr/bin/ld: cannot find -lLLVMipo: No such file or directory
/usr/bin/ld: cannot find -lLLVMIRReader: No such file or directory
/usr/bin/ld: cannot find -lLLVMMC: No such file or directory
/usr/bin/ld: cannot find -lLLVMObjCARCOpts: No such file or directory
/usr/bin/ld: cannot find -lLLVMScalarOpts: No such file or directory
/usr/bin/ld: cannot find -lLLVMTarget: No such file or directory
/usr/bin/ld: cannot find -lLLVMTransformUtils: No such file or directory
/usr/bin/ld: cannot find -lLLVMVectorize: No such file or directory
collect2: error: ld returned 1 exit status
make[2]: *** [frontend/llvm/CMakeFiles/ikos-pp.dir/build.make:108: frontend/llvm/ikos-pp] Error 1
make[1]: *** [CMakeFiles/Makefile2:1969: frontend/llvm/CMakeFiles/ikos-pp.dir/all] Error 2
make: *** [Makefile:146: all] Error 2For now i got stuck on this issue. $ ls /usr/lib/llvm14/* 2
/usr/lib/llvm14/bin:
bugpoint dsymutil llvm-cxxdump llvm-libtool-darwin llvm-PerfectShuffle llvm-tapi-diff
c-index-test FileCheck llvm-cxxfilt llvm-link llvm-profdata llvm-tblgen
clang llc llvm-cxxmap llvm-lipo llvm-profgen llvm-tli-checker
clang++ lli llvm-debuginfod-find llvm-lto llvm-ranlib llvm-undname
clang-14 lli-child-target llvm-diff llvm-lto2 llvm-rc llvm-windres
clang-check llvm-addr2line llvm-dis llvm-mc llvm-readelf llvm-xray
clang-cl llvm-ar llvm-dlltool llvm-mca llvm-readobj not
clang-cpp llvm-as llvm-dwarfdump llvm-ml llvm-reduce obj2yaml
clang-extdef-mapping llvm-bcanalyzer llvm-dwp llvm-modextract llvm-rtdyld opt
clang-offload-bundler llvm-bitcode-strip llvm-extract llvm-mt llvm-sim sancov
clang-offload-wrapper llvm-cat llvm-gsymutil llvm-nm llvm-size sanstats
clang-refactor llvm-cfi-verify llvm-ifs llvm-objcopy llvm-split split-file
clang-repl llvm-config llvm-install-name-tool llvm-objdump llvm-stress verify-uselistorder
clang-scan-deps llvm-cov llvm-jitlink llvm-opt-report llvm-strings yaml2obj
count llvm-c-test llvm-jitlink-executor llvm-otool llvm-strip yaml-bench
diagtool llvm-cvtres llvm-lib llvm-pdbutil llvm-symbolizer
/usr/lib/llvm14/include:
clang clang-c llvm llvm-c
/usr/lib/llvm14/lib:
clang libclang-cpp.so.14 libclang.so.14.0.6 libLLVMDemangle.a libLLVMTableGen.a libRemarks.so
cmake libclang.so libLLVM-14.0.6.so libLLVM.so libLTO.so libRemarks.so.14
libclang-cpp.so libclang.so.13 libLLVM-14.so libLLVMSupport.a libLTO.so.14 LLVMgold.so
/usr/lib/llvm14/share:
opt-viewer
I tried the following things, but none worked:
I'll let you know if i make any progress on the linux machine, but for now it's broken for both linux, and mac for me. |
|
Thanks for the thorough exploration. This seems like an Arch-specific thing. We should open a separate issue for it. I suspect the following is strongly against Arch philosophy (and I'm no fan of snap myself) but FYI there is an IKOS snap. For Debian/Ubuntu, it's in non-free/multiverse. I'd be happy to have a dockerfile with arch that we run regularly against |
|
I'd be happy to help with the Arch workflow setup, I'm also quite sure there must be some ready solutions for this as well. A quick update on the build errors: The Then, after running armado@arche:~/dev/ikos/build (master *%) $ make 2
CMake Deprecation Warning at CMakeLists.txt:41 (cmake_minimum_required):
Compatibility with CMake < 3.10 will be removed from a future version of
CMake.
Update the VERSION argument <min> value. Or, use the <min>...<max> syntax
to tell CMake that the project requires at least <min> but has been updated
to work with policies introduced by <max> or earlier.
-- Install prefix: /home/armado/dev/ikos/install
-- Build type: Release
-- CMake version: 3.31.3
-- CMake generator: Unix Makefiles
-- Including core
CMake Deprecation Warning at core/CMakeLists.txt:41 (cmake_minimum_required):
Compatibility with CMake < 3.10 will be removed from a future version of
CMake.
Update the VERSION argument <min> value. Or, use the <min>...<max> syntax
to tell CMake that the project requires at least <min> but has been updated
to work with policies introduced by <max> or earlier.
Found Boost: /usr/lib/cmake/Boost-1.86.0 (found version "1.55.0")
Found Boost components:
unit_test_framework
-- Could NOT find APRON. Please provide -DAPRON_ROOT=/path/to/apron (missing: APRON_INCLUDE_DIR APRON_APRON_LIB APRON_BOX_LIB APRON_OCT_LIB APRON_POLKA_LIB APRON_PPL_LIB APRON_PKGRID_LIB)
-- Including ar
CMake Deprecation Warning at ar/CMakeLists.txt:41 (cmake_minimum_required):
Compatibility with CMake < 3.10 will be removed from a future version of
CMake.
Update the VERSION argument <min> value. Or, use the <min>...<max> syntax
to tell CMake that the project requires at least <min> but has been updated
to work with policies introduced by <max> or earlier.
Found Boost: /usr/lib/cmake/Boost-1.86.0 (found version "1.55.0")
-- Including frontend/llvm
CMake Deprecation Warning at frontend/llvm/CMakeLists.txt:41 (cmake_minimum_required):
Compatibility with CMake < 3.10 will be removed from a future version of
CMake.
Update the VERSION argument <min> value. Or, use the <min>...<max> syntax
to tell CMake that the project requires at least <min> but has been updated
to work with policies introduced by <max> or earlier.
Found Boost: /usr/lib/cmake/Boost-1.86.0 (found version "1.55.0")
Found Boost components:
filesystem;system
CMake Error at frontend/llvm/CMakeLists.txt:107 (message):
LLVM 14 is required.
-- Configuring incomplete, errors occurred!
make: *** [Makefile:968: cmake_check_build_system] Error 1This is the exact issue we encountered earlier, except this time invoked by After that, running In summary for future reference, to get it running on
I'll look into the issues later, I think they should all be simple to fix. Unfortunately I'm not too familiar with C++, and especially make & cmake, so i'm not certain what kind of fixes are acceptable. |
|
Ah, sorry for polluting this issue with Arch stuff, I'll move the comments to a separate issue. Moved to #307 |
|
When I try to compile on Mac, the output includes: It's pointing to the wrong SDK (I think). You can check out the history of https://github.com/ivanperez-keera/ikos-test. I don't seem to be able to get clang to pick up a path under |
|
I tried modifying the formula to adjust the environment variable, but nothing seems to affect those paths being passed to clang. I don't know how to tell it to find the headers under I added a simple @arthaud Do you know why this may be happening? Is there something in how LLVM is found and set up on the EDIT: I figured out a workaround, see #306 (comment). |
|
I think I found the issue. It's just homebrew picking the wrong SDK. I managed to get it to build in Github actions. Modifying the formula to set I'm going to clean it up and I'll report back. |
|
I figured out what may be a first workaround for Mac. I've put some files here: https://github.com/ivanperez-keera/ikos-test That repo contains a modified Please try it and let me know if that works for you. You can see in https://github.com/ivanperez-keera/ikos-test/blob/master/.github/workflows/install-ikos-homebrew.yml how it is installed from source. It should have some protection for other OS (e.g., |
==> Installing ikos from nasa-sw-vnv/core
==> python3 -m venv --system-site-packages --without-pip /usr/local/Cellar/ikos/3.4_1/libexec
==> python3 -m pip --python=/usr/local/Cellar/ikos/3.4_1/libexec/bin/python install /private/tmp/ikos--Pygments-20241129-21798-6mrf8k/Pygments-2.4.2
==> cmake -G Unix Makefiles -DGMP_ROOT=/usr/local/opt/gmp -DMPFR_ROOT=/usr/local/opt/mpfr -DPPL_ROOT=/usr/local/opt/ppl -DAPRON_ROOT=/usr/local/opt/apron -DCUSTOM_BOOST
==> make install
Last 15 lines from /Users/hegp/Library/Logs/Homebrew/ikos/04.make:
make[1]: *** Waiting for unfinished jobs....
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/code.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context_impl.cpp.o
[ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/data_layout.cpp.o
[ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/function.cpp.o
[ 18%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/intrinsic.cpp.o
[ 18%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/statement.cpp.o
[ 19%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/type.cpp.o
[ 19%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/value.cpp.o
[ 21%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/frontend.cpp.o
[ 21%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/type.cpp.o
[ 22%] Linking CXX static library libikos-ar.a
[ 22%] Built target ikos-ar
make: *** [all] Error 2
The text was updated successfully, but these errors were encountered: