Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Type checker error translating LLVM bitcode to AR #187

Open
robertguetzkow opened this issue Apr 22, 2022 · 8 comments
Open

Type checker error translating LLVM bitcode to AR #187

robertguetzkow opened this issue Apr 22, 2022 · 8 comments

Comments

@robertguetzkow
Copy link

robertguetzkow commented Apr 22, 2022 •
edited

I attempted to analyze Blender with IKOS. It fails during the "Translating LLVM bitcode to AR" step with the following errors:

/home/dev/01-data/02-software/ikos-install/bin/ikos -a=nullity blender.bc
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
error: left operand of statement '%15 folt %19' is not a floating point
error: left operand of statement '%15 fuge %19' is not a floating point
error: result of statement '<4 x si32> %21 = sext %20' is not a signed integer
error: result of statement '<4 x float> %52 = sitofp %51' is not a floating point
[...]
ikos-analyzer: /tmp/ikos-aa2ksdqm/blender.pp.bc: error: type checker
ikos: error: a run-time error occurred

Please let me know if you need any additional information.
@ivanperez-keera
Copy link
Collaborator

ivanperez-keera commented Nov 8, 2023 •
edited

@robertguetzkow I am unable to reproduce this issue.

Are you able at all to provide a docker image where the problem manifests?

You can use this as a starting point and you can base it off of ubuntu:latest instead of debian:

#171 (comment)

Thanks!

@robertguetzkow
Copy link
Author

@ivanperez-keera Thank you for your reply. The original report is from more than a year ago and it might behave differently with current versions of IKOS and Blender. I'll try to find some time on a weekend and check if the issue still occurs on my end. If it does, I'll build a Dockerfile.

@ivanperez-keera
Copy link
Collaborator

Excellent. Thank you!

@robertguetzkow
Copy link
Author

robertguetzkow commented Nov 12, 2023 •
edited

IKOS compiles successfully, but running ikos-scan does not work. Right from the start CMake fails to detect ABI compatibility and the compiler test fails as well.

IKOS was build using the following commands and completes without reporting errors

cmake -DCMAKE_INSTALL_PREFIX="/home/dev/01-data/02-software/ikos-install" -DCMAKE_BUILD_TYPE="Release" -DLLVM_CONFIG_EXECUTABLE="/usr/lib/llvm-14/bin/llvm-config" ..
make
make install

Command used for the build attempt with Blender:

export PATH=/home/dev/01-data/02-software/ikos-install/bin:$PATH && ikos-scan make lite debug

From the CMakeError.log:

Compiling the C compiler identification source file "CMakeCCompilerId.c" failed.
Compiler: /home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc 
Build flags: 
Id flags:  

The output was:
1
/usr/lib/llvm-14/bin/llvm-link: No such file or directory


Compiling the CXX compiler identification source file "CMakeCXXCompilerId.cpp" failed.
Compiler: /home/dev/01-data/02-software/ikos-install/bin/ikos-scan-c++ 
Build flags: 
Id flags:  

The output was:
1
/usr/lib/llvm-14/bin/llvm-link: No such file or directory


Detecting C compiler ABI info failed to compile with the following output:
Change Dir: /home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp

Run Build Command(s):/usr/bin/gmake -f Makefile cmTC_0ddd3/fast && gmake[1]: Entering directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
/usr/bin/gmake  -f CMakeFiles/cmTC_0ddd3.dir/build.make CMakeFiles/cmTC_0ddd3.dir/build
gmake[2]: Entering directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
Building C object CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o
/home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc   -v -MD -MT CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o -MF CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o.d -o CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o -c /usr/share/cmake-3.22/Modules/CMakeCCompilerABI.c
Ubuntu clang version 14.0.0-1ubuntu1.1
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm-14/bin
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/11
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/9
Selected GCC installation: /usr/lib/gcc/x86_64-linux-gnu/11
Candidate multilib: .;@m64
Selected multilib: .;@m64
 (in-process)
 "/usr/lib/llvm-14/bin/clang" -cc1 -triple x86_64-pc-linux-gnu -emit-obj -mrelax-all --mrelax-relocations -disable-free -clear-ast-before-backend -disable-llvm-verifier -discard-value-names -main-file-name CMakeCCompilerABI.c -mrelocation-model pic -pic-level 2 -pic-is-pie -mframe-pointer=all -fmath-errno -ffp-contract=on -fno-rounding-math -mconstructor-aliases -funwind-tables=2 -target-cpu x86-64 -tune-cpu generic -mllvm -treat-scalable-fixed-error-as-warning -debugger-tuning=gdb -v -fcoverage-compilation-dir=/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp -resource-dir /usr/lib/llvm-14/lib/clang/14.0.0 -dependency-file CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o.d -MT CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o -sys-header-deps -internal-isystem /usr/lib/llvm-14/lib/clang/14.0.0/include -internal-isystem /usr/local/include -internal-isystem /usr/lib/gcc/x86_64-linux-gnu/11/../../../../x86_64-linux-gnu/include -internal-externc-isystem /usr/include/x86_64-linux-gnu -internal-externc-isystem /include -internal-externc-isystem /usr/include -fdebug-compilation-dir=/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp -ferror-limit 19 -fgnuc-version=4.2.1 -faddrsig -D__GCC_HAVE_DWARF2_CFI_ASM=1 -o CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o -x c /usr/share/cmake-3.22/Modules/CMakeCCompilerABI.c
clang -cc1 version 14.0.0 based upon LLVM 14.0.0 default target x86_64-pc-linux-gnu
ignoring nonexistent directory "/usr/lib/gcc/x86_64-linux-gnu/11/../../../../x86_64-linux-gnu/include"
ignoring nonexistent directory "/include"
#include "..." search starts here:
#include <...> search starts here:
 /usr/lib/llvm-14/lib/clang/14.0.0/include
 /usr/local/include
 /usr/include/x86_64-linux-gnu
 /usr/include
End of search list.
Linking C executable cmTC_0ddd3
/usr/bin/cmake -E cmake_link_script CMakeFiles/cmTC_0ddd3.dir/link.txt --verbose=1
/home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc  -v CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o -o cmTC_0ddd3 
Ubuntu clang version 14.0.0-1ubuntu1.1
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm-14/bin
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/11
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/9
Selected GCC installation: /usr/lib/gcc/x86_64-linux-gnu/11
Candidate multilib: .;@m64
Selected multilib: .;@m64
 "/usr/bin/ld" -pie -z relro --hash-style=gnu --build-id --eh-frame-hdr -m elf_x86_64 -dynamic-linker /lib64/ld-linux-x86-64.so.2 -o cmTC_0ddd3 /lib/x86_64-linux-gnu/Scrt1.o /lib/x86_64-linux-gnu/crti.o /usr/lib/gcc/x86_64-linux-gnu/11/crtbeginS.o -L/usr/lib/gcc/x86_64-linux-gnu/11 -L/usr/lib/gcc/x86_64-linux-gnu/11/../../../../lib64 -L/lib/x86_64-linux-gnu -L/lib/../lib64 -L/usr/lib/x86_64-linux-gnu -L/usr/lib/../lib64 -L/usr/lib/llvm-14/bin/../lib -L/lib -L/usr/lib CMakeFiles/cmTC_0ddd3.dir/CMakeCCompilerABI.c.o -lgcc --as-needed -lgcc_s --no-as-needed -lc -lgcc --as-needed -lgcc_s --no-as-needed /usr/lib/gcc/x86_64-linux-gnu/11/crtendS.o /lib/x86_64-linux-gnu/crtn.o
/usr/lib/llvm-14/bin/llvm-link: No such file or directory
gmake[2]: *** [CMakeFiles/cmTC_0ddd3.dir/build.make:100: cmTC_0ddd3] Error 1
gmake[2]: *** Deleting file 'cmTC_0ddd3'
gmake[2]: Leaving directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
gmake[1]: *** [Makefile:127: cmTC_0ddd3/fast] Error 2
gmake[1]: Leaving directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'




Determining if the C compiler works failed with the following output:
Change Dir: /home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp

Run Build Command(s):/usr/bin/gmake -f Makefile cmTC_d5e2d/fast && gmake[1]: Entering directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
/usr/bin/gmake  -f CMakeFiles/cmTC_d5e2d.dir/build.make CMakeFiles/cmTC_d5e2d.dir/build
gmake[2]: Entering directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
Building C object CMakeFiles/cmTC_d5e2d.dir/testCCompiler.c.o
/home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc    -MD -MT CMakeFiles/cmTC_d5e2d.dir/testCCompiler.c.o -MF CMakeFiles/cmTC_d5e2d.dir/testCCompiler.c.o.d -o CMakeFiles/cmTC_d5e2d.dir/testCCompiler.c.o -c /home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp/testCCompiler.c
Linking C executable cmTC_d5e2d
/usr/bin/cmake -E cmake_link_script CMakeFiles/cmTC_d5e2d.dir/link.txt --verbose=1
/home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc CMakeFiles/cmTC_d5e2d.dir/testCCompiler.c.o -o cmTC_d5e2d 
/usr/lib/llvm-14/bin/llvm-link: No such file or directory
gmake[2]: *** [CMakeFiles/cmTC_d5e2d.dir/build.make:100: cmTC_d5e2d] Error 1
gmake[2]: *** Deleting file 'cmTC_d5e2d'
gmake[2]: Leaving directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
gmake[1]: *** [Makefile:127: cmTC_d5e2d/fast] Error 2
gmake[1]: Leaving directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'

It seems ikos-scan is not executing the compiler as expected and llvm-link is getting no output to link. Note that this is CMake's "pre-flight" check before starting the actual build.

Unfortunately, I don't have more time today to investigate this further.

Executing task: export PATH=/home/dev/01-data/02-software/ikos-install/bin:$PATH && ikos-scan make lite debug 


Configuring Blender in "/home/dev/01-data/01-git/blender-git/build_linux_debug_lite" ...
loading initial cache file /home/dev/01-data/01-git/blender-git/blender/build_files/cmake/config/blender_lite.cmake
-- The C compiler identification is Clang 14.0.0
-- The CXX compiler identification is Clang 14.0.0
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - failed
-- Check for working C compiler: /home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc
-- Check for working C compiler: /home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc - broken
CMake Error at /usr/share/cmake-3.22/Modules/CMakeTestCCompiler.cmake:69 (message):
  The C compiler

    "/home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc"

  is not able to compile a simple test program.

  It fails with the following output:

    Change Dir: /home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp
    
    Run Build Command(s):/usr/bin/gmake -f Makefile cmTC_b585a/fast && gmake[1]: Entering directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
    /usr/bin/gmake  -f CMakeFiles/cmTC_b585a.dir/build.make CMakeFiles/cmTC_b585a.dir/build
    gmake[2]: Entering directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
    Building C object CMakeFiles/cmTC_b585a.dir/testCCompiler.c.o
    /home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc    -MD -MT CMakeFiles/cmTC_b585a.dir/testCCompiler.c.o -MF CMakeFiles/cmTC_b585a.dir/testCCompiler.c.o.d -o CMakeFiles/cmTC_b585a.dir/testCCompiler.c.o -c /home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp/testCCompiler.c
    Linking C executable cmTC_b585a
    /usr/bin/cmake -E cmake_link_script CMakeFiles/cmTC_b585a.dir/link.txt --verbose=1
    /home/dev/01-data/02-software/ikos-install/bin/ikos-scan-cc CMakeFiles/cmTC_b585a.dir/testCCompiler.c.o -o cmTC_b585a 
    /usr/lib/llvm-14/bin/llvm-link: No such file or directory
    gmake[2]: *** [CMakeFiles/cmTC_b585a.dir/build.make:100: cmTC_b585a] Error 1
    gmake[2]: *** Deleting file 'cmTC_b585a'
    gmake[2]: Leaving directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
    gmake[1]: *** [Makefile:127: cmTC_b585a/fast] Error 2
    gmake[1]: Leaving directory '/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeTmp'
    
    

  

  CMake will not be able to correctly generate this project.
Call Stack (most recent call first):
  CMakeLists.txt:108 (project)


-- Configuring incomplete, errors occurred!
See also "/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeOutput.log".
See also "/home/dev/01-data/01-git/blender-git/build_linux_debug_lite/CMakeFiles/CMakeError.log".
make: *** [GNUmakefile:365: all] Error 1

@robertguetzkow
Copy link
Author

I will provide a Dockerfile/Containerfile next weekend.

@ivanperez-keera
Copy link
Collaborator

ivanperez-keera commented Nov 13, 2023 •
edited

@robertguetzkow I think the error you are finding now is known (see #203). Any of the two following proposals would fix it:

PhilipBotha@fc95883
https://github.com/NASA-SW-VnV/ikos/pull/230/files

Let me know if either works for you.

I plan to address that issue in the upcoming release.

@robertguetzkow
Copy link
Author

robertguetzkow commented Nov 14, 2023 •
edited

Compiler is properly detected now and compiles correctly. However, the final step of creating the blender binary fails due to linking errors with OpenImageIO where required libraries aren't being found as they are supposed to (which does work correctly in the regular build without ikos). I'll have to investigate why that happens.

Consolidate compiler generated dependencies of target blender
[100%] Linking CXX executable ../../bin/blender
/usr/bin/ld: warning: libOpenEXR.so.30, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libOpenEXRCore.so.30, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libtbb.so.2, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libboost_thread.so.1.80.0, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libImath.so.30, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libIlmThread.so.30, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libIex.so.30, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libboost_chrono.so.1.80.0, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libboost_date_time.so.1.80.0, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)
/usr/bin/ld: warning: libboost_atomic.so.1.80.0, needed by /home/dev/01-data/01-git/blender-git/lib/linux_x86_64_glibc_228/openimageio/lib/libOpenImageIO.so, not found (try using -rpath or -rpath-link)

@robertguetzkow
Copy link
Author

robertguetzkow commented Nov 19, 2023 •
edited

Linking appears to work when using lld. However, IKOS still fails to analyze. I'm attempting to build an MWE Dockerfile to demonstrate this, but I'm running into issues with CMake's try-compile step in the container despite applying the patch. This means it fails very early on. It seems that something isn't correctly set up with the installed packages or IKOS. Apologies for the back and forth with me debugging individual steps.

If I find some time, I'll try to figure out the error.

The following does not work, while the build on the regular system does, except for the analysis.

FROM ubuntu:latest

RUN apt-get update \
    && apt-get install -y \
        python3 \
        git \
        build-essential \
        subversion \
        cmake \
        libx11-dev \
        libxxf86vm-dev \
        libxcursor-dev \
        libxi-dev \
        libxrandr-dev \
        libxinerama-dev \
        libegl-dev \
        libwayland-dev \
        wayland-protocols \
        libxkbcommon-dev \
        libdbus-1-dev \
        linux-libc-dev \
        libgmp-dev \
        libboost-dev \
        libboost-filesystem-dev \
        libboost-thread-dev \
        libboost-test-dev \
        libsqlite3-dev \
        libtbb-dev \
        libz-dev \
        libedit-dev \
        python3-pygments \
        python3-distutils \
        python3-pip \
        llvm-14 \
        llvm-14-dev \
        llvm-14-tools \
        clang-14 \
        lld-14 \
        wget

RUN mkdir ~/blender-git \
    && cd ~/blender-git \
    && git clone https://projects.blender.org/blender/blender.git

RUN mkdir ~/blender-git/lib \
    && cd ~/blender-git/lib \
    && svn checkout https://svn.blender.org/svnroot/bf-blender/trunk/lib/linux_x86_64_glibc_228

RUN mkdir ~/ikos-git \
    && cd ~/ikos-git \
    && git clone https://github.com/NASA-SW-VnV/ikos.git
    
RUN cd ~/ikos-git/ikos \
    && wget https://github.com/NASA-SW-VnV/ikos/commit/65e750c210d195d82be3c1f3ddf5c45c99b1eff7.patch \
    && git apply 65e750c210d195d82be3c1f3ddf5c45c99b1eff7.patch
    
RUN mkdir ~/ikos-git/ikos/build \
    && mkdir ~/ikos-git/ikos-install \
    && cd ~/ikos-git/ikos/build \
    && cmake -DCMAKE_INSTALL_PREFIX="~/ikos-git/ikos-install" \
             -DCMAKE_BUILD_TYPE="Release" \
             -DLLVM_CONFIG_EXECUTABLE="/usr/lib/llvm-14/bin/llvm-config" \
             .. \
    && make \
    && make install

ENV PATH "/root/ikos-git/ikos-install/bin:$PATH"

ENTRYPOINT ["/bin/bash"]
  1. Install either podman or docker
  2. Build the container image
    • Podman: podman build --squash -t ikos/blender:1.0 -f Dockerfile
    • Docker: docker build --squash -t ikos/blender:1.0 -f Dockerfile
  3. Run the container:
    • Podman: podman run -it --rm ikos/blender:1.0
    • Docker: docker run -it --rm ikos/blender:1.0
  4. Insides the container run:
    1. cd ~/blender-git/blender
    2. make update
    3. ~/ikos-git/ikos-install/bin/ikos-scan make lite

The image id can be found through podman images. Removal of the image is accomplished through podman rmi <image-id>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ivanperez-keera @robertguetzkow