more work on ikos static analyzer, ref #14

.devcontainer/debian/bookworm/Dockerfile

@@ -46,6 +46,7 @@ FROM debian:bookworm-slim AS downloader
 
 # Reuse global arguments
 ARG VULKAN_VERSION
+ARG IKOS_VERSION=3.4
 
 ENV DEBIAN_FRONTEND=noninteractive \
     DEBCONF_NOWARNINGS="yes" \
@@ -55,6 +56,7 @@ 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-13.3.0/gcc-13.3.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" && \
 	# Cleanup
@@ -64,6 +66,103 @@ RUN echo "Download Stage" && \
     # List files in /tmp
     ls -la /tmp
 
+# +-----------------------------+
+# | IKOS Build Stage            |
+# +-----------------------------+
+#
+# Well... IKOS is a bit of a pain to build.
+# It requires LLVM 14, which is not available in the Debian 12 "bookworm" repositories.
+# https://apt.llvm.org/bookworm/pool/main/l/ (15-19, snapshot)
+# https://apt.llvm.org/unstable/pool/main/l/ (all versions)
+# So we a trixie slim image is used to install LLVM 14.
+
+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 python3-pygments python3-setuptools
+
+# 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 && \
+    # Download
+    url="https://github.com/antoinemine/apron/archive/refs/tags/v0.9.15.tar.gz"; echo "Download URL: \"$url\"" && \
+    curl $CURL_OPTIONS -o apron.xz -O $url && \
+    # Extract
+    tar xzf apron.xz && \
+    mv apron-* apron && \
+    # Build
+    cd apron && \
+    ./configure && \
+    make -j4 && \
+    make install && \
+    # Cleanup
+    rm -rf /tmp/*
+
+COPY --from=downloader /tmp/ikos.xz /tmp/ikos.xz
+
+RUN echo "IKOS" && \
+    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 && \
+    # Build IKOS
+    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 && \
+	# https://github.com/NASA-SW-VnV/ikos/blob/master/TROUBLESHOOTING.md#could-not-find-ikos-python-module-while-running-ikos
+	#ls -lahr /opt/ikos/lib/python*/site-packages/ikos && \
+    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
 # +-----------------------------+
@@ -278,6 +377,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

.devcontainer/debian/trixie/Dockerfile

@@ -101,6 +101,7 @@ ENV DEBIAN_FRONTEND=noninteractive \
     CURL_OPTIONS="--silent --show-error --retry 5 --location"
 
 RUN echo "Packages" && \
+    # avoid debconf: delaying package configuration, since apt-utils is not installed
     apt-get update && apt-get install --no-install-recommends --assume-yes \
         curl tar xz-utils sed perl \
         gcc g++ \
@@ -129,11 +130,15 @@ RUN echo "LLVM 14" && \
     apt-get update && apt-get install --no-install-recommends --assume-yes \
         llvm-14 llvm-14-dev llvm-14-tools clang-14
 
-RUN echo "Installing APRON" && \
+RUN echo "APRON" && \
     cd tmp && \
-    curl $CURL_OPTIONS -o apron.xz https://github.com/antoinemine/apron/archive/refs/tags/v0.9.15.tar.gz && \
+    # Download
+    url="https://github.com/antoinemine/apron/archive/refs/tags/v0.9.15.tar.gz"; echo "Download URL: \"$url\"" && \
+    curl $CURL_OPTIONS -o apron.xz -O $url && \
+    # Extract
     tar xzf apron.xz && \
     mv apron-* apron && \
+    # Build
     cd apron && \
     ./configure && \
     make -j4 && \
@@ -143,16 +148,17 @@ RUN echo "Installing APRON" && \
 
 COPY --from=downloader /tmp/ikos.xz /tmp/ikos.xz
 
-RUN echo "IKOS" && \
+RUN echo "Extract" && \
     cd /tmp && \
     tar zxf ikos.xz && \
     # remove version from folder name
-    mv ikos-* ikos && \
-    cd /tmp/ikos && \
+    mv ikos-* ikos
+
+RUN 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 && \
     # Build IKOS
-    echo "Build" && \
+    echo "Build IKOS" && \
     mkdir build && cd build && \
     cmake \
     -DCMAKE_INSTALL_PREFIX="/opt/ikos" \
@@ -225,13 +231,12 @@ RUN echo "Packages" && \
     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 \
+    # gprof
     linux-perf \
     # code coverage
     gcovr lcov \

.devcontainer/devcontainer.json

@@ -5,7 +5,7 @@
     // The repository contains two images:
     // - "./debian/bookworm/Dockerfile" (default)
     // - "./debian/trixie/Dockerfile"
-    "dockerfile": "./debian/trixie/Dockerfile",
+    "dockerfile": "./debian/bookworm/Dockerfile",
     // sets the run context to this .devcontainer folder
     "context": "."
   },

CHANGELOG.md

@@ -15,17 +15,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 **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
-- added streetsidesoftware.vscode-spellchecker as vscode extensions,
-  including configuration. main config is cspell.json in root folder.
-  the file points to /build-tools/cspell, which contain the cspell.config.json.
-- added whitelist for spell checking: /build-tools/cspell/repo-words.txt
+- added linux-perf, strace, ltrace
+- added spellchecker (streetsidesoftware.vscode-spellchecker as vscode extension)
+- added spellchecker configuration. the main config is '/cspell.json', which
+  points to '/build-tools/cspell/cspell.config.json'.
+- added whitelist for spell checking: '/build-tools/cspell/repo-words.txt'
 
 **Changed**
 - bookworm & trixie images: updated VulkanSDK to 1.3.296.0
 - bookworm image: updated LLVM to 19
+- updated show-tool-versions.sh and show-tool-locations.sh
 - 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"

build-tools/cspell/repo-words.txt

@@ -19,7 +19,9 @@ CXXFLAGS
 DAPRON
 DCMAKE
 DDEFAULT
-debian
+Debian
+debconf
+DEBCONF
 defusedxml
 DESTDIR
 devbox
@@ -91,6 +93,7 @@ mlibc
 multiarch
 multilib
 noninteractive
+NOWARNINGS
 objdump
 ohmyzsh
 omyzsh