From 7634e060eab566389ff2ddf69e1f6684e9344a69 Mon Sep 17 00:00:00 2001 From: "Jens A. Koch" Date: Mon, 16 Dec 2024 20:51:53 +0100 Subject: [PATCH] added ikos on trixie, ref. issue #14 --- .devcontainer/debian/bookworm/Dockerfile | 15 +- .devcontainer/debian/trixie/Dockerfile | 136 +++++++++++++++++-- .devcontainer/scripts/show-tool-locations.sh | 3 + .devcontainer/scripts/show-tool-versions.sh | 4 + CHANGELOG.md | 3 + build-tools/cspell/repo-words.txt | 12 ++ 6 files changed, 161 insertions(+), 12 deletions(-) diff --git a/.devcontainer/debian/bookworm/Dockerfile b/.devcontainer/debian/bookworm/Dockerfile index d06c725..a39bcd3 100644 --- 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 index 5691b7d..c82ab08 100644 --- 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,6 +220,7 @@ LABEL \ # "Y88P" ENV DEBIAN_FRONTEND=noninteractive \ + DEBCONF_NOWARNINGS="yes" \ CURL_OPTIONS="--silent --show-error --retry 5 --location" RUN echo "Packages" && \ @@ -136,8 +228,17 @@ 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 \ + 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 index 40fb6ba..40f471c 100644 --- 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 index 4640c87..94814da 100644 --- 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 index f97186b..32aa76c 100644 --- 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 index 550e379..c416788 100644 --- 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