added ikos on trixie, ref. issue #14

jakoch · Dec 16, 2024 · 7634e06 · 7634e06
1 parent 4c3c504
commit 7634e06
Show file tree

Hide file tree

Showing 6 changed files with 161 additions and 12 deletions.
diff --git a/.devcontainer/debian/bookworm/Dockerfile b/.devcontainer/debian/bookworm/Dockerfile
@@ -48,6 +48,7 @@ FROM debian:bookworm-slim AS downloader
 ARG VULKAN_VERSION
 
 ENV DEBIAN_FRONTEND=noninteractive \
+    DEBCONF_NOWARNINGS="yes" \
     CURL_OPTIONS="--silent --show-error --retry 5 --location"
 
 WORKDIR /tmp
@@ -109,14 +110,24 @@ LABEL \
 #                                                  "Y88P"
 
 ENV DEBIAN_FRONTEND=noninteractive \
+    DEBCONF_NOWARNINGS="yes" \
     CURL_OPTIONS="--silent --show-error --retry 5 --location"
 
 RUN echo "Packages" && \
     apt-get update && apt-get install --no-install-recommends --assume-yes \
     gnupg2 ca-certificates software-properties-common \
     build-essential \
-    cppcheck valgrind linux-perf lcov strace ltrace \
     wget git nano jq \
+    # code analysis
+    cppcheck \
+    valgrind \
+    # profiling
+    gprof \
+    linux-perf \
+    # code coverage
+    gcovr lcov \
+    # tracing
+    strace ltrace \
     # required by Visual Studio
     g++ gdb make ninja-build rsync zip sudo \
     # required by VCPKG
@@ -129,7 +140,7 @@ RUN echo "Packages" && \
     locales \
     # shell
     zsh \
-    # optional tools for Doxygen
+    # optional tools for Doxygen: Sphinx + Graphviz
     python3 python3-pip \
     python3-sphinx python3-sphinx-rtd-theme python3-defusedxml sphinx-common \
     graphviz && \

diff --git a/.devcontainer/debian/trixie/Dockerfile b/.devcontainer/debian/trixie/Dockerfile
@@ -65,14 +65,17 @@ FROM debian:trixie-slim AS downloader
 #ARG GCC_VERSION
 ARG VULKAN_VERSION
 ARG MESA_VERSION
+ARG IKOS_VERSION=3.4
 
 ENV DEBIAN_FRONTEND=noninteractive \
+    DEBCONF_NOWARNINGS="yes" \
     CURL_OPTIONS="--silent --show-error --retry 5 --location"
 
 WORKDIR /tmp
 RUN echo "Download Stage" && \
     apt-get update && apt-get install --no-install-recommends --assume-yes \
     ca-certificates curl && \
+    curl $CURL_OPTIONS -o ikos.xz https://github.com/NASA-SW-VnV/ikos/archive/refs/tags/v${IKOS_VERSION}.tar.gz && \
 #   curl $CURL_OPTIONS -o gcc.xz "http://ftp.gnu.org/gnu/gcc/gcc-14.2.0/gcc-14.2.0.tar.xz" && \
     curl $CURL_OPTIONS -o vulkansdk.xz "https://sdk.lunarg.com/sdk/download/${VULKAN_VERSION}/linux/vulkansdk-linux-x86_64-${VULKAN_VERSION}.tar.xz" && \
     curl $CURL_OPTIONS -o mesa.xz "https://archive.mesa3d.org/mesa-${MESA_VERSION}.tar.xz" && \
@@ -83,6 +86,94 @@ RUN echo "Download Stage" && \
     # List files in /tmp
     ls -la /tmp
 
+# +-----------------------------+
+# | IKOS Build Stage            |
+# +-----------------------------+
+
+FROM debian:trixie-slim AS ikos-builder
+
+ARG DEBIAN_VERSION=13
+ARG DEBIAN_VERSION_NAME=trixie
+ARG LLVM_VERSION=14
+
+ENV DEBIAN_FRONTEND=noninteractive \
+    DEBCONF_NOWARNINGS="yes" \
+    CURL_OPTIONS="--silent --show-error --retry 5 --location"
+
+RUN echo "Packages" && \
+    apt-get update && apt-get install --no-install-recommends --assume-yes \
+        curl tar xz-utils sed perl \
+        gcc g++ \
+        cmake \
+        make \
+        libgmp-dev \
+        libboost-dev libboost-filesystem-dev libboost-thread-dev libboost-test-dev \
+        libsqlite3-dev \
+        libtbb-dev \
+        libz-dev \
+        libzstd-dev \
+        libedit-dev \
+        libmpfr-dev \
+        libppl-dev \
+        libgmp-dev \
+        python3 python3-pip python3-venv
+
+# https://github.com/NASA-SW-VnV/ikos?tab=readme-ov-file#dependencies
+SHELL ["/bin/bash", "-o", "pipefail", "-c"]
+RUN echo "LLVM 14" && \
+    if [ "$DEBIAN_VERSION_NAME" == "trixie" ]; then DEBIAN_VERSION_NAME="unstable"; fi && \
+    if [ "$DEBIAN_VERSION_NAME" == "unstable" ]; then LINKNAME=""; else LINKNAME="-$DEBIAN_VERSION_NAME"; fi && \
+    curl -s https://apt.llvm.org/llvm-snapshot.gpg.key | tee /etc/apt/trusted.gpg.d/apt.llvm.org.asc && \
+    echo "deb http://apt.llvm.org/$DEBIAN_VERSION_NAME/ llvm-toolchain$LINKNAME-$LLVM_VERSION main" >> /etc/apt/sources.list.d/llvm.list && \
+    echo "deb http://httpredir.debian.org/debian sid main" >> /etc/apt/sources.list.d/sid.list && \
+    apt-get update && apt-get install --no-install-recommends --assume-yes \
+        llvm-14 llvm-14-dev llvm-14-tools clang-14
+
+RUN echo "APRON" && \
+    cd tmp && \
+    echo "Download" && \
+    curl $CURL_OPTIONS -o apron.xz https://github.com/antoinemine/apron/archive/refs/tags/v0.9.15.tar.gz && \
+    echo "Extract" && \
+    tar xzf apron.xz && \
+    mv apron-* apron && \
+    cd apron && \
+    echo "Build" && \
+    ./configure && \
+    make -j4 && \
+    make install && \
+    echo "Cleanup" && \
+    rm -rf /tmp/*
+
+COPY --from=downloader /tmp/ikos.xz /tmp/ikos.xz
+
+RUN echo "IKOS" && \
+    echo "Extract" && \
+    cd /tmp && \
+    tar zxf ikos.xz && \
+    # remove version from folder name
+    mv ikos-* ikos && \
+    cd /tmp/ikos && \
+    # Patch IKOS to allow LLVM14+
+    #sed -i 's/(LLVM_VERSION VERSION_LESS "14") OR (NOT (LLVM_VERSION VERSION_LESS "15"))/(LLVM_VERSION VERSION_LESS "14")/g' analyzer/CMakeLists.txt frontend/llvm/CMakeLists.txt && \
+    echo "Build" && \
+    mkdir build && cd build && \
+    cmake \
+    -DCMAKE_INSTALL_PREFIX="/opt/ikos" \
+    -DCMAKE_BUILD_TYPE="Debug" \
+    -DLLVM_CONFIG_EXECUTABLE="/usr/lib/llvm-$LLVM_VERSION/bin/llvm-config" \
+    -DMPFR_ROOT=/usr \
+    -DPPL_ROOT=/usr \
+    -DAPRON_ROOT=/usr/local \
+    .. && \
+    make -j4 && \
+    make install && \
+    echo "Test" && \
+    /opt/ikos/bin/ikos --version && \
+    echo "Cleanup" && \
+    apt-get autoremove -y && \
+    apt-get clean autoclean && \
+    rm -rf /var/lib/apt/lists/* /tmp/* /var/tmp/*
+
 # +-----------------------------+
 # | BASE IMAGE                  |        See https://hub.docker.com/_/debian
 # +-----------------------------+
@@ -129,15 +220,25 @@ LABEL \
 #                                                  "Y88P"
 
 ENV DEBIAN_FRONTEND=noninteractive \
+    DEBCONF_NOWARNINGS="yes" \
     CURL_OPTIONS="--silent --show-error --retry 5 --location"
 
 RUN echo "Packages" && \
     apt-get update && apt-get install --no-install-recommends --assume-yes \
     gnupg2 ca-certificates \
     # package seems gone, was used in LLVM section below: software-properties-common \
     build-essential \
-    cppcheck valgrind linux-perf lcov strace ltrace \
     wget git nano jq \
+    # code analysis
+    cppcheck \
+    valgrind \
+    # profiling
+    gprof \
+    linux-perf \
+    # code coverage
+    gcovr lcov \
+    # tracing
+    strace ltrace \
     # required by Visual Studio
     g++ gdb make ninja-build rsync zip sudo \
     # required by VCPKG
@@ -150,7 +251,7 @@ RUN echo "Packages" && \
     locales \
     # shell
     zsh \
-    # optional tools for Doxygen
+    # optional tools for Doxygen: Sphinx + Graphviz
     python3 python3-pip \
     python3-sphinx python3-sphinx-rtd-theme python3-defusedxml sphinx-common \
     graphviz && \
@@ -262,14 +363,14 @@ RUN echo "CCACHE" && \
 	rm ccache-$version-linux-x86_64.tar.xz
 
 #
-#  8888888b.   .d88888b.  Y88b   d88P Y88b   d88P  .d8888b.  8888888888 888b    888
-#  888  "Y88b d88P" "Y88b  Y88b d88P   Y88b d88P  d88P  Y88b 888        8888b   888
-#  888    888 888     888   Y88o88P     Y88o88P   888    888 888        88888b  888
-#  888    888 888     888    Y888P       Y888P    888        8888888    888Y88b 888
-#  888    888 888     888    d888b        888     888  88888 888        888 Y88b888
-#  888    888 888     888   d88888b       888     888    888 888        888  Y88888
-#  888  .d88P Y88b. .d88P  d88P Y88b      888     Y88b  d88P 888        888   Y8888
-#  8888888P"   "Y88888P"  d88P   Y88b     888      "Y8888P88 8888888888 888    Y888
+#  888  .d8888b.  8888888b.  888    888 8888888888 888b    888
+#  888 d88P  Y88b 888   Y88b 888   d88P 888        8888b   888
+#  888 888    888 888    888 888  d8P   888        88888b  888
+#  888 888        888   d88P 888d88K    8888888    888Y88b 888
+#  888 888        8888888P"  8888888b   888        888 Y88b888
+#  888 888    888 888        888  Y88b  888        888  Y88888
+#  888 Y88b  d88P 888        888   Y88b 888        888   Y8888
+#  888  "Y8888P"  888        888    Y88b 8888888888 888    Y888
 #
 
 # We are using the prebuilt binaries for x64.
@@ -285,6 +386,21 @@ RUN echo "DOXYGEN" && \
     ln -s /opt/doxygen/bin/doxygen /usr/bin && \
     rm doxygen-$version_number.linux.bin.tar.gz
 
+#
+#  8888888 888    d8P   .d88888b.   .d8888b.
+#    888   888   d8P   d88P" "Y88b d88P  Y88b
+#    888   888  d8P    888     888 Y88b.
+#    888   888d88K     888     888  "Y888b.
+#    888   8888888b    888     888     "Y88b.
+#    888   888  Y88b   888     888       "888
+#    888   888   Y88b  Y88b. .d88P Y88b  d88P
+#  8888888 888    Y88b  "Y88888P"   "Y8888P"
+#
+
+COPY --from=ikos-builder /opt/ikos /opt/ikos
+
+ENV PATH="/opt/ikos/bin:${PATH}"
+
 #
 #  888      888      888     888 888b     d888
 #  888      888      888     888 8888b   d8888

diff --git a/.devcontainer/scripts/show-tool-locations.sh b/.devcontainer/scripts/show-tool-locations.sh
@@ -44,10 +44,13 @@ show_tool_locations() {
   get_command_paths clang-tidy
   get_command_paths clang-format
   get_command_paths cppcheck
+  get_command_paths ikos
   get_command_paths gprof
   get_command_paths perf
   get_command_paths strace
   get_command_paths ltrace
+  get_command_paths lcov
+  get_command_paths gcovr
   get_command_paths doxygen
   get_command_paths sphinx-build
   get_command_paths git

diff --git a/.devcontainer/scripts/show-tool-versions.sh b/.devcontainer/scripts/show-tool-versions.sh
@@ -69,10 +69,13 @@ show_tool_versions() {
     clang_tidy_version=$(clang-tidy --version | head -n1 | awk '{print $4}')
     clang_format_version=$(clang-format --version | head -n1 | awk '{print $4}')
     cppcheck_version=$(cppcheck --version | awk '{print $2}')
+    ikos_version=$(ikos --version | head -n1 | awk '{print $2}')
     gprof_version=$(gprof --version | head -n1 | awk '{print $7}')
     perf_version=$(perf --version | awk '{print $3}')
     strace_version=$(strace --version | head -n1 | awk '{print $4}')
     ltrace_version=$(ltrace --version | head -n1 | awk '{print $2}')
+    lcov=$(lcov --version | head -n1 | awk '{print $4}')
+    gcovr=$(gcovr --version | head -n1 | awk '{print $2}')
     doxygen_version=$(doxygen -v | awk '{print $1}')
     sphinx_version=$(sphinx-build --version | awk '{print $2}')
     git_version=$(git --version | cut -c 13-)
@@ -97,6 +100,7 @@ show_tool_versions() {
     print_row "lldb" "$lldb_version"
     print_row "Valgrind" "$valgrind_version"
     print_row "cppcheck" "$cppcheck_version"
+    print_row "ikos" "$ikos_version"
     print_row "gprof" "$gprof_version"
     print_row "perf" "$perf_version"
     print_row "strace" "$strace_version"

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -14,6 +14,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [1.0.6] - 2024-12-xx
 
 **Added**
+- trixie: added ikos static analyzer
 - bookworm & trixie images: added linux-perf, strace, ltrace
 - added gprof and linux-perf to show-tool-versions.sh
 - added echo statements for each run command section
@@ -27,6 +28,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - bookworm image: updated LLVM to 19
 - CURL_OPTIONS cleanup, removed CURL_OPTIONS_BAR
 - instead "-y" use "--assume-yes" on apt-get
+- silence warning "debconf: delaying package configuration, since apt-utils is not installed"
+  by using ENV DEBCONF_NOWARNINGS="yes"
 
 ## [1.0.5] - 2024-07-09
 

diff --git a/build-tools/cspell/repo-words.txt b/build-tools/cspell/repo-words.txt
@@ -16,15 +16,20 @@ clocale
 cppcheck
 cuda
 CXXFLAGS
+DAPRON
 DCMAKE
+DDEFAULT
 debian
 defusedxml
 DESTDIR
 devbox
 dfsg
+DLLVM
+DMPFR
 Dockerfiles
 DOCKERHUB
 dpkg
+DPPL
 Filemode
 fontconfig
 githubcli
@@ -34,11 +39,13 @@ glvnd
 gprof
 graphviz
 hadolint
+ikos
 jakoch
 jlumbroso
 keyrings
 lavapipe
 libatomic
+libboost
 libc
 libclang
 libclc
@@ -55,9 +62,12 @@ libmpc
 libmpfr
 libomp
 libpolly
+libppl
 libquadmath
 libsanitizer
+libsqlite
 libstdcxx
+libtbb
 libudev
 libunwind
 libvulkan
@@ -69,6 +79,7 @@ libxfixes
 libxrandr
 libxshmfence
 libxxf
+libz
 libzstd
 linux
 lldb
@@ -102,6 +113,7 @@ tzdata
 udate
 valgrind
 vcpkg
+venv
 vkcube
 vtable
 vulkan