From 192649899901085148dd246cd97a6fc6e151015c Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Mon, 3 Jul 2023 17:31:30 +0200 Subject: [PATCH 01/38] Build and package Ultimate for Docker --- .gitignore | 2 + packaging/docker/Dockerfile | 277 +++++++++++++++++++++ packaging/docker/README.md | 42 ++++ packaging/docker/docker-compose.yml | 12 + packaging/docker/ultimate-webbackend.env | 22 ++ packaging/docker/web.config.properties.tpl | 48 ++++ 6 files changed, 403 insertions(+) create mode 100644 packaging/docker/Dockerfile create mode 100644 packaging/docker/README.md create mode 100644 packaging/docker/docker-compose.yml create mode 100644 packaging/docker/ultimate-webbackend.env create mode 100644 packaging/docker/web.config.properties.tpl diff --git a/.gitignore b/.gitignore index 62178d2fecb..2cd55d48ec2 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,8 @@ hs_err_pid* *.md.backup +/packaging/docker/*.env + /releaseScripts/default/DeltaDebugger-linux/* /releaseScripts/default/DeltaDebugger-win32/* /releaseScripts/default/UAutomizer-linux/* diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile new file mode 100644 index 00000000000..aa88a3ac2d4 --- /dev/null +++ b/packaging/docker/Dockerfile @@ -0,0 +1,277 @@ +#------------------------------------------------------------------------------ +# Dockerfile: compile and package Ultimate toolchains +#------------------------------------------------------------------------------ +# Author: Manuel Bentele +# Copyright (c) 2023 +#------------------------------------------------------------------------------ +# common build arguments for multi-staged Docker build +#------------------------------------------------------------------------------ +ARG REPO_MAVEN_ROOT="trunk/source/BA_MavenParentUltimate" +ARG REPO_DIR_BUILD="trunk/source/BA_SiteRepository/target/products" +ARG REPO_DIR_TOOLS="releaseScripts/default/adds" +ARG DIR_BUILD="/home/build" +ARG DIR_ULTIMATE="${DIR_BUILD}/ultimate" +ARG DIR_OUTPUT="${DIR_ULTIMATE}/${REPO_DIR_BUILD}" +ARG DIR_TOOLS="${DIR_ULTIMATE}/${REPO_DIR_TOOLS}" + +#------------------------------------------------------------------------------ +# 1st build stage: compile and materialize Ultimate +#------------------------------------------------------------------------------ +FROM debian:bullseye AS build + +ARG REPO_URL="https://github.com/ultimate-pa/ultimate.git" +ARG REPO_BRANCH="dev" + +ARG REPO_MAVEN_ROOT +ARG REPO_DIR_BUILD +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT + +# install build dependencies for an entire Ultimate build +RUN apt-get update && \ + apt-get install -y "git" \ + "maven" \ + "openjdk-11-jdk" && + rm -rf /var/lib/apt/lists/* + +# clone fresh Ultimate Git repository +RUN mkdir -p "${DIR_BUILD}" && \ + git clone --depth=1 --branch="${REPO_BRANCH}" "${REPO_URL}" "${DIR_ULTIMATE}" + +# build all Ultimate products +WORKDIR "${DIR_ULTIMATE}" +RUN mvn -f "${REPO_MAVEN_ROOT}" clean package -P materialize + +#------------------------------------------------------------------------------ +# 2nd build stage: package Ultimate CLI +#------------------------------------------------------------------------------ +FROM debian:bullseye AS ultimate-cli + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT +ARG DIR_TOOLS + +# install runtime dependencies for Ultimate product +RUN apt-get update && \ + apt-get install -y "apt-utils" && \ + apt-get install -y "openjdk-11-jre" && + rm -rf /var/lib/apt/lists/* + +# install already built Ultimate product +RUN mkdir -p "${DIR_ULTIMATE}" +WORKDIR "${DIR_ULTIMATE}" +COPY --from=build "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64" "${DIR_ULTIMATE}" +RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" + +# install alread compiled tools for Ultimate +COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" +COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" +COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" +COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" + +# default entry point to print installed Ultimate version +CMD ["Ultimate", "--version"] + +#------------------------------------------------------------------------------ +# 2nd build stage: package Ultimate Debug UI +#------------------------------------------------------------------------------ +FROM debian:bullseye AS ultimate-debug + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT +ARG DIR_TOOLS + +# install runtime dependencies for Ultimate product +RUN apt-get update && \ + apt-get install -y "apt-utils" && \ + apt-get install -y "openjdk-11-jre" && + rm -rf /var/lib/apt/lists/* + +# install already built Ultimate product +RUN mkdir -p "${DIR_ULTIMATE}" +WORKDIR "${DIR_ULTIMATE}" +COPY --from=build "${DIR_OUTPUT}/Debug-E4/linux/gtk/x86_64" "${DIR_ULTIMATE}" +RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" + +# install alread compiled tools for Ultimate +COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" +COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" +COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" +COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" + +# default entry point to print installed Ultimate version +CMD ["Ultimate", "--version"] + +#------------------------------------------------------------------------------ +# 2nd build stage: package Ultimate ReqAnalyzer +#------------------------------------------------------------------------------ +FROM debian:bullseye AS ultimate-reqanalyzer + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT +ARG DIR_TOOLS + +# install runtime dependencies for Ultimate product +RUN apt-get update && \ + apt-get install -y "apt-utils" && \ + apt-get install -y "openjdk-11-jre" && + rm -rf /var/lib/apt/lists/* + +# install already built Ultimate product +RUN mkdir -p "${DIR_ULTIMATE}" +WORKDIR "${DIR_ULTIMATE}" +COPY --from=build "${DIR_OUTPUT}/ReqAnalyzer/linux/gtk/x86_64" "${DIR_ULTIMATE}" +RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" + +# install alread compiled tools for Ultimate +COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" +COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" +COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" +COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" + +# default entry point to print installed Ultimate version +CMD ["Ultimate", "--version"] + +#------------------------------------------------------------------------------ +# 2nd build stage: package Ultimate DeltaDebugger +#------------------------------------------------------------------------------ +FROM debian:bullseye AS ultimate-deltadebugger + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT +ARG DIR_TOOLS + +# install runtime dependencies for Ultimate product +RUN apt-get update && \ + apt-get install -y "apt-utils" && \ + apt-get install -y "openjdk-11-jre" && + rm -rf /var/lib/apt/lists/* + +# install already built Ultimate product +RUN mkdir -p "${DIR_ULTIMATE}" +WORKDIR "${DIR_ULTIMATE}" +COPY --from=build "${DIR_OUTPUT}/DeltaDebugger/linux/gtk/x86_64" "${DIR_ULTIMATE}" +RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" + +# install alread compiled tools for Ultimate +COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" +COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" +COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" +COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" + +# default entry point to print installed Ultimate version +CMD ["Ultimate", "--version"] + +#------------------------------------------------------------------------------ +# 2nd build stage: package Ultimate Eliminator +#------------------------------------------------------------------------------ +FROM debian:bullseye AS ultimate-eliminator + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT +ARG DIR_TOOLS + +# install runtime dependencies for Ultimate product +RUN apt-get update && \ + apt-get install -y "apt-utils" && \ + apt-get install -y "openjdk-11-jre" && + rm -rf /var/lib/apt/lists/* + +# install already built Ultimate product +RUN mkdir -p "${DIR_ULTIMATE}" +WORKDIR "${DIR_ULTIMATE}" +COPY --from=build "${DIR_OUTPUT}/UltimateEliminator/linux/gtk/x86_64" "${DIR_ULTIMATE}" +RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" + +# install alread compiled tools for Ultimate +COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" +COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" +COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" +COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" + +# default entry point to print installed Ultimate version +CMD ["Ultimate", "--version"] + +#------------------------------------------------------------------------------ +# 2nd build stage: package Ultimate WebBackend +#------------------------------------------------------------------------------ +FROM debian:bullseye AS ultimate-webbackend + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT +ARG DIR_TOOLS + +ARG REPO_DIR_WEBSITE_CONFIG="releaseScripts/website-config" +ARG DIR_WEBSITE_CONFIG="${DIR_ULTIMATE}/${REPO_DIR_WEBSITE_CONFIG}" + +ENV ULTIMATE_DIR_TMP="/tmp/ultimate" + +# install runtime dependencies for Ultimate product +RUN apt-get update && \ + apt-get install -y "apt-utils" && \ + apt-get install -y "openjdk-11-jre" + +# install 'dockerize' for automatic configuration file creation +ENV DOCKERIZE_VERSION="v0.7.0" +RUN apt-get update && \ + apt-get install -y "wget" \ + "curl" && \ + wget -O - "https://github.com/jwilder/dockerize/releases/download/${DOCKERIZE_VERSION}/dockerize-linux-amd64-${DOCKERIZE_VERSION}.tar.gz" | tar xzf - -C "/usr/local/bin" && \ + apt-get autoremove -yqq --purge "wget" && \ + rm -rf /var/lib/apt/lists/* + +# install already built Ultimate product +RUN mkdir -p "${DIR_ULTIMATE}" +WORKDIR "${DIR_ULTIMATE}" +COPY --from=build "${DIR_OUTPUT}/WebBackend/linux/gtk/x86_64" "${DIR_ULTIMATE}" +RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" + +# install alread compiled tools for Ultimate +COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" +COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" +COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" +COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" + +# add configuration files and templates for 'dockerize' and Ultimate +COPY --from=build "${DIR_WEBSITE_CONFIG}/backend/settings_whitelist.json" "${DIR_ULTIMATE}/settings_whitelist.json" +ADD "web.config.properties.tpl" "${DIR_ULTIMATE}/web.config.properties.tpl" +ENV ULTIMATE_BACKEND_SETTINGS_WHITELIST="${DIR_ULTIMATE}/settings_whitelist.json" + +# activate Ultimate Webbackend configuration +RUN echo "-Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog" >> "${DIR_ULTIMATE}/Ultimate.ini" && + echo "-DWebBackend.SETTINGS_FILE=${DIR_ULTIMATE}/web.config.properties" >> "${DIR_ULTIMATE}/Ultimate.ini" + +# create directory to store temporary files +RUN mkdir -p "${ULTIMATE_TMP_DIR}" + +# expose communication port of the Webbackend +EXPOSE "${ULTIMATE_WEBBACKEND_PORT}" + +# define health check to supervise the Ultimate Webbackend's availability +HEALTHCHECK --interval=1m --timeout=10s --start-period=20s \ + CMD curl -f "http://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" || exit 1 + +# default entry point to automatically configure and start the Ultimate Webbackend product +CMD dockerize -template "${DIR_ULTIMATE}/web.config.properties.tpl:${DIR_ULTIMATE}/web.config.properties" \ + -wait "tcp://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" \ + -timeout "${ULTIMATE_BACKEND_START_TIMEOUT}" \ + Ultimate diff --git a/packaging/docker/README.md b/packaging/docker/README.md new file mode 100644 index 00000000000..4579af26305 --- /dev/null +++ b/packaging/docker/README.md @@ -0,0 +1,42 @@ +# Package Ultimate for Docker + +## Build Ultimate Docker images +An Ultimate `PRODUCT` can be built with the following Docker call + +```shell +docker build -t --target . +``` + +where `PRODUCT` is a placeholder for one of the products + + - `ultimate-cli` + - `ultimate-debug` + - `ultimate-reqanalyzer` + - `ultimate-deltadebugger` + - `ultimate-eliminator` + - `ultimate-webbackend` + +shipped with the Ultimate program analysis framework. + +For validating the built Ultimate `PRODUCT` image, you can create and run a Docker container based on this image with the following Docker call. +```shell +docker run -it +``` +As an expected result, you should then receive the Ultimate version output from the executed Ultimate `PRODUCT` in the container. + + +## Run Ultimate Docker containers + +If you want to run Ultimate interactively for any verification input, you can spwan a bash in a created and started Ultimate `PRODUCT` container as follows. +```shell +docker run -it /bin/bash +Ultimate -tc -s -i +``` +Calling Ultimate within the container then follows as usual, where a `TOOLCHAIN`, `SETTINGS`, and `PROGRAM` file path should be specified for a verification run. + + +## Configure Ultimate Webbackend + +The specific Ultimate `PRODUCT` called `ultimate-webbackend` requires an extensive and valid configuration for the Web service to start. + + diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml new file mode 100644 index 00000000000..fa49ccaa340 --- /dev/null +++ b/packaging/docker/docker-compose.yml @@ -0,0 +1,12 @@ +version: "2" +services: + ultimate-webbackend: + build: + dockerfile: "Dockerfile" + target: "ultimate-webbackend" + image: "ultimate-webbackend" + env_file: + - "ultimate-webbackend.env" + ports: + - "${ULTIMATE_BACKEND_PORT}:${ULTIMATE_BACKEND_PORT}" + restart: "unless-stopped" diff --git a/packaging/docker/ultimate-webbackend.env b/packaging/docker/ultimate-webbackend.env new file mode 100644 index 00000000000..75cd655165e --- /dev/null +++ b/packaging/docker/ultimate-webbackend.env @@ -0,0 +1,22 @@ +############################################################################### +# Environment variables for 'ultimate-webbackend' service in docker-compose.yml +############################################################################### + +# backend settings +ULTIMATE_BACKEND_HOST=localhost +ULTIMATE_BACKEND_PORT=8080 +ULTIMATE_BACKEND_ROUTE=/api +ULTIMATE_BACKEND_START_TIMEOUT=30 + +# frontend settings +ULTIMATE_FRONTEND_SERVE=False +ULTIMATE_FRONTEND_PATH=/some/path +ULTIMATE_FRONTEND_ROUTE=/website + +# log settings +ULTIMATE_LOG_PATH=/dev/stdout +ULTIMATE_LOG_LEVEL=INFO + +# general settings +ULTIMATE_DIR_TMP=/tmp/ultimate +ULTIMATE_TIMEOUT=90 diff --git a/packaging/docker/web.config.properties.tpl b/packaging/docker/web.config.properties.tpl new file mode 100644 index 00000000000..f0a04ba3543 --- /dev/null +++ b/packaging/docker/web.config.properties.tpl @@ -0,0 +1,48 @@ +############################################################################### +# Autogenerated Ultimate Webbackend configuration. Do not edit! +############################################################################### + +#------------------------------------------------------------------------------ +# Ultimate WebBackend settings +#------------------------------------------------------------------------------ +# determines the port the jetty server will be listening +PORT={{ .Env.ULTIMATE_BACKEND_PORT }} + +# URL prefix, the API will be served at, e.g. /api results in +# http://localhost:PORT/api +BACKEND_ROUTE={{ .Env.ULTIMATE_BACKEND_ROUTE }} + +# path to a local user settings whitelist +SETTINGS_WHITELIST={{ .Env.ULTIMATE_BACKEND_SETTINGS_WHITELIST }} + +#------------------------------------------------------------------------------ +# Ultimate Frontend settings +#------------------------------------------------------------------------------ +# true will also serve the Frontend. If set to True, ULTIMATE_FRONTEND_PATH and +# ULTIMATE_FRONTEND_ROUTE should be set. +SERVE_WEBSITE={{ .Env.ULTIMATE_FRONTEND_SERVE }} + +# path to the `WebsiteStatic` folder containing the Frontend +FRONTEND_PATH={{ .Env.ULTIMATE_FRONTEND_PATH }} + +# URL prefix, the FRONTEND will be served at, e.g. /website results in +# http://localhost:PORT/website +FRONTEND_ROUTE={{ .Env.ULTIMATE_FRONTEND_ROUTE }} + +#------------------------------------------------------------------------------ +# Ultimate logging settings +#------------------------------------------------------------------------------ +# absolute (or relative from java.class.path) path to the log file +LOG_FILE_PATH={{ .Env.ULTIMATE_LOG_PATH }} + +# logging verbosity. Choose from: ALL, DEBUG, INFO, WARN, OFF +LOG_LEVEL={{ .Env.ULTIMATE_LOG_LEVEL }} + +#------------------------------------------------------------------------------ +# Ultimate general settings +#------------------------------------------------------------------------------ +# path to a directory storing temporary files +TMP_DIR={{ .Env.ULTIMATE_DIR_TMP }} + +# timeout in seconds for any request +FORCED_TIMEOUT={{ .Env.ULTIMATE_TIMEOUT }} From 793b707310fb111c27b5b46a8d56fc883c704473 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Mon, 3 Jul 2023 21:18:34 +0200 Subject: [PATCH 02/38] Fix newline escaping issues in Dockerfile --- packaging/docker/Dockerfile | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index aa88a3ac2d4..07f0cb4d4db 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -32,8 +32,8 @@ ARG DIR_OUTPUT RUN apt-get update && \ apt-get install -y "git" \ "maven" \ - "openjdk-11-jdk" && - rm -rf /var/lib/apt/lists/* + "openjdk-11-jdk" && \ + rm -rf /var/lib/apt/lists/* # clone fresh Ultimate Git repository RUN mkdir -p "${DIR_BUILD}" && \ @@ -58,7 +58,7 @@ ARG DIR_TOOLS # install runtime dependencies for Ultimate product RUN apt-get update && \ apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && + apt-get install -y "openjdk-11-jre" && \ rm -rf /var/lib/apt/lists/* # install already built Ultimate product @@ -91,7 +91,7 @@ ARG DIR_TOOLS # install runtime dependencies for Ultimate product RUN apt-get update && \ apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && + apt-get install -y "openjdk-11-jre" && \ rm -rf /var/lib/apt/lists/* # install already built Ultimate product @@ -124,7 +124,7 @@ ARG DIR_TOOLS # install runtime dependencies for Ultimate product RUN apt-get update && \ apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && + apt-get install -y "openjdk-11-jre" && \ rm -rf /var/lib/apt/lists/* # install already built Ultimate product @@ -157,7 +157,7 @@ ARG DIR_TOOLS # install runtime dependencies for Ultimate product RUN apt-get update && \ apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && + apt-get install -y "openjdk-11-jre" && \ rm -rf /var/lib/apt/lists/* # install already built Ultimate product @@ -190,7 +190,7 @@ ARG DIR_TOOLS # install runtime dependencies for Ultimate product RUN apt-get update && \ apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && + apt-get install -y "openjdk-11-jre" && \ rm -rf /var/lib/apt/lists/* # install already built Ultimate product @@ -257,7 +257,7 @@ ADD "web.config.properties.tpl" "${DIR_ULTIMATE}/web.config.properties.tpl" ENV ULTIMATE_BACKEND_SETTINGS_WHITELIST="${DIR_ULTIMATE}/settings_whitelist.json" # activate Ultimate Webbackend configuration -RUN echo "-Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog" >> "${DIR_ULTIMATE}/Ultimate.ini" && +RUN echo "-Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog" >> "${DIR_ULTIMATE}/Ultimate.ini" && \ echo "-DWebBackend.SETTINGS_FILE=${DIR_ULTIMATE}/web.config.properties" >> "${DIR_ULTIMATE}/Ultimate.ini" # create directory to store temporary files From f35243b80a749260ecf5aa9c66282b432bf948db Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Mon, 3 Jul 2023 23:22:16 +0200 Subject: [PATCH 03/38] Fix config issues regarding dockerize and worng paths --- packaging/docker/Dockerfile | 34 +++++++++++++++++++---------- packaging/docker/WebBackend.ini.tpl | 10 +++++++++ packaging/docker/docker-compose.yml | 2 +- 3 files changed, 34 insertions(+), 12 deletions(-) create mode 100644 packaging/docker/WebBackend.ini.tpl diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 07f0cb4d4db..c09dff39d60 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -223,7 +223,18 @@ ARG DIR_TOOLS ARG REPO_DIR_WEBSITE_CONFIG="releaseScripts/website-config" ARG DIR_WEBSITE_CONFIG="${DIR_ULTIMATE}/${REPO_DIR_WEBSITE_CONFIG}" +ENV ULTIMATE_BACKEND_HOST="localhost" +ENV ULTIMATE_BACKEND_PORT=8080 +ENV ULTIMATE_BACKEND_ROUTE="/api" + +ENV ULTIMATE_FRONTEND_SERVE="False" +ENV ULTIMATE_FRONTEND_PATH="/some/path" +ENV ULTIMATE_FRONTEND_ROUTE="/website" +ENV ULTIMATE_LOG_PATH="/dev/stdout" +ENV ULTIMATE_LOG_LEVEL="INFO" + ENV ULTIMATE_DIR_TMP="/tmp/ultimate" +ENV ULTIMATE_TIMEOUT=90 # install runtime dependencies for Ultimate product RUN apt-get update && \ @@ -243,7 +254,7 @@ RUN apt-get update && \ RUN mkdir -p "${DIR_ULTIMATE}" WORKDIR "${DIR_ULTIMATE}" COPY --from=build "${DIR_OUTPUT}/WebBackend/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" +RUN ln -s "${DIR_ULTIMATE}/WebBackend" "/usr/bin/WebBackend" # install alread compiled tools for Ultimate COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" @@ -254,24 +265,25 @@ COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" # add configuration files and templates for 'dockerize' and Ultimate COPY --from=build "${DIR_WEBSITE_CONFIG}/backend/settings_whitelist.json" "${DIR_ULTIMATE}/settings_whitelist.json" ADD "web.config.properties.tpl" "${DIR_ULTIMATE}/web.config.properties.tpl" -ENV ULTIMATE_BACKEND_SETTINGS_WHITELIST="${DIR_ULTIMATE}/settings_whitelist.json" +ADD "WebBackend.ini.tpl" "${DIR_ULTIMATE}/WebBackend.ini.tpl" +RUN rm -f "${DIR_ULTIMATE}/WebBackend.ini" -# activate Ultimate Webbackend configuration -RUN echo "-Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog" >> "${DIR_ULTIMATE}/Ultimate.ini" && \ - echo "-DWebBackend.SETTINGS_FILE=${DIR_ULTIMATE}/web.config.properties" >> "${DIR_ULTIMATE}/Ultimate.ini" +ENV ULTIMATE_BACKEND_SETTINGS_WHITELIST="${DIR_ULTIMATE}/settings_whitelist.json" +ENV ULTIMATE_BACKEND_SETTINGS_FILE="${DIR_ULTIMATE}/web.config.properties" # create directory to store temporary files -RUN mkdir -p "${ULTIMATE_TMP_DIR}" +RUN mkdir -p "${ULTIMATE_DIR_TMP}" # expose communication port of the Webbackend -EXPOSE "${ULTIMATE_WEBBACKEND_PORT}" +EXPOSE "${ULTIMATE_BACKEND_PORT}" # define health check to supervise the Ultimate Webbackend's availability HEALTHCHECK --interval=1m --timeout=10s --start-period=20s \ CMD curl -f "http://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" || exit 1 - +RUN echo "${DIR_ULTIMATE}" # default entry point to automatically configure and start the Ultimate Webbackend product -CMD dockerize -template "${DIR_ULTIMATE}/web.config.properties.tpl:${DIR_ULTIMATE}/web.config.properties" \ +CMD dockerize -template "web.config.properties.tpl:web.config.properties" \ + -template "WebBackend.ini.tpl:WebBackend.ini" \ -wait "tcp://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" \ - -timeout "${ULTIMATE_BACKEND_START_TIMEOUT}" \ - Ultimate + -timeout 20s \ + WebBackend diff --git a/packaging/docker/WebBackend.ini.tpl b/packaging/docker/WebBackend.ini.tpl new file mode 100644 index 00000000000..b94a94b21b7 --- /dev/null +++ b/packaging/docker/WebBackend.ini.tpl @@ -0,0 +1,10 @@ +-startup +plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar +--launcher.library +plugins/org.eclipse.equinox.launcher.gtk.linux.x86_64_1.1.1300.v20200819-0940 +-nosplash +-consoleLog +-vmargs +-Dosgi.noShutdown=true +-Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog +-DWebBackend.SETTINGS_FILE={{ .Env.ULTIMATE_BACKEND_SETTINGS_FILE }} diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index fa49ccaa340..504d59e4f93 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -8,5 +8,5 @@ services: env_file: - "ultimate-webbackend.env" ports: - - "${ULTIMATE_BACKEND_PORT}:${ULTIMATE_BACKEND_PORT}" + - "8080:8080" restart: "unless-stopped" From 3e472d2b6aa5d1b31abb96d04e3b7a9fbaa1174b Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Mon, 3 Jul 2023 23:29:47 +0200 Subject: [PATCH 04/38] Remove broken dockerize waiting until service is ready --- packaging/docker/Dockerfile | 2 -- 1 file changed, 2 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index c09dff39d60..1fab1ac9528 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -284,6 +284,4 @@ RUN echo "${DIR_ULTIMATE}" # default entry point to automatically configure and start the Ultimate Webbackend product CMD dockerize -template "web.config.properties.tpl:web.config.properties" \ -template "WebBackend.ini.tpl:WebBackend.ini" \ - -wait "tcp://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" \ - -timeout 20s \ WebBackend From 774692494491bb06925d20af3ebf9d774aed809e Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 4 Jul 2023 02:09:07 +0200 Subject: [PATCH 05/38] Optimize multi-stage Docker build for all Ultimate applications --- packaging/docker/Dockerfile | 149 +++++++++++++----------------------- packaging/docker/README.md | 20 ++++- 2 files changed, 69 insertions(+), 100 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 1fab1ac9528..e070af8340b 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -44,9 +44,9 @@ WORKDIR "${DIR_ULTIMATE}" RUN mvn -f "${REPO_MAVEN_ROOT}" clean package -P materialize #------------------------------------------------------------------------------ -# 2nd build stage: package Ultimate CLI +# 2nd build stage: package common Ultimate artifacts shared by all products #------------------------------------------------------------------------------ -FROM debian:bullseye AS ultimate-cli +FROM debian:bullseye AS ultimate-common ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -55,31 +55,45 @@ ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS -# install runtime dependencies for Ultimate product +# install runtime dependencies for all Ultimate products RUN apt-get update && \ apt-get install -y "apt-utils" && \ apt-get install -y "openjdk-11-jre" && \ rm -rf /var/lib/apt/lists/* -# install already built Ultimate product +# prepare installation directory for an Ultimate product RUN mkdir -p "${DIR_ULTIMATE}" WORKDIR "${DIR_ULTIMATE}" -COPY --from=build "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" -# install alread compiled tools for Ultimate +# install alread compiled tools for all Ultimate products COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" -# default entry point to print installed Ultimate version -CMD ["Ultimate", "--version"] +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate CLI +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-cli + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT +ARG DIR_TOOLS + +# install already built Ultimate CLI product +COPY --from=build "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64" "${DIR_ULTIMATE}" +RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" + +# default entry point to print installed Ultimate CLI version +CMD ["Ultimate", "-version"] #------------------------------------------------------------------------------ -# 2nd build stage: package Ultimate Debug UI +# 3rd build stage: package Ultimate Debug UI #------------------------------------------------------------------------------ -FROM debian:bullseye AS ultimate-debug +FROM ultimate-common AS ultimate-debug ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -88,31 +102,29 @@ ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS -# install runtime dependencies for Ultimate product +# install graphical dependencies for Ultimate Debug UI product RUN apt-get update && \ - apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && \ + apt-get install -y "libswt-gtk-4-jni" && \ + apt-get install -y "libswt-gtk-4-java" && \ + apt-get install -y "xauth" && \ rm -rf /var/lib/apt/lists/* -# install already built Ultimate product -RUN mkdir -p "${DIR_ULTIMATE}" -WORKDIR "${DIR_ULTIMATE}" +# install already built Ultimate Debug UI product COPY --from=build "${DIR_OUTPUT}/Debug-E4/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" +RUN ln -s "${DIR_ULTIMATE}/UltimateDebug" "/usr/bin/UltimateDebug" -# install alread compiled tools for Ultimate -COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" -COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" -COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" -COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" +# run the Ultimate Debug UI product as non-root user 'ultimate' +RUN useradd --no-create-home --home-dir "${DIR_ULTIMATE}" ultimate && \ + chown -R ultimate:ultimate "${DIR_ULTIMATE}" +USER ultimate # default entry point to print installed Ultimate version -CMD ["Ultimate", "--version"] +CMD ["UltimateDebug", "-version"] #------------------------------------------------------------------------------ -# 2nd build stage: package Ultimate ReqAnalyzer +# 3rd build stage: package Ultimate ReqAnalyzer #------------------------------------------------------------------------------ -FROM debian:bullseye AS ultimate-reqanalyzer +FROM ultimate-common AS ultimate-reqanalyzer ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -121,31 +133,17 @@ ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS -# install runtime dependencies for Ultimate product -RUN apt-get update && \ - apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && \ - rm -rf /var/lib/apt/lists/* - -# install already built Ultimate product -RUN mkdir -p "${DIR_ULTIMATE}" -WORKDIR "${DIR_ULTIMATE}" +# install already built Ultimate ReqAnalyzer product COPY --from=build "${DIR_OUTPUT}/ReqAnalyzer/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" - -# install alread compiled tools for Ultimate -COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" -COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" -COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" -COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" +RUN ln -s "${DIR_ULTIMATE}/ReqAnalyzer" "/usr/bin/ReqAnalyzer" # default entry point to print installed Ultimate version -CMD ["Ultimate", "--version"] +CMD ["ReqAnalyzer", "-version"] #------------------------------------------------------------------------------ -# 2nd build stage: package Ultimate DeltaDebugger +# 3rd build stage: package Ultimate DeltaDebugger #------------------------------------------------------------------------------ -FROM debian:bullseye AS ultimate-deltadebugger +FROM ultimate-common AS ultimate-deltadebugger ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -154,31 +152,17 @@ ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS -# install runtime dependencies for Ultimate product -RUN apt-get update && \ - apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && \ - rm -rf /var/lib/apt/lists/* - -# install already built Ultimate product -RUN mkdir -p "${DIR_ULTIMATE}" -WORKDIR "${DIR_ULTIMATE}" +# install already built Ultimate DeltaDebugger product COPY --from=build "${DIR_OUTPUT}/DeltaDebugger/linux/gtk/x86_64" "${DIR_ULTIMATE}" RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" -# install alread compiled tools for Ultimate -COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" -COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" -COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" -COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" - # default entry point to print installed Ultimate version -CMD ["Ultimate", "--version"] +CMD ["Ultimate", "-version"] #------------------------------------------------------------------------------ -# 2nd build stage: package Ultimate Eliminator +# 3rd build stage: package Ultimate Eliminator #------------------------------------------------------------------------------ -FROM debian:bullseye AS ultimate-eliminator +FROM ultimate-common AS ultimate-eliminator ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -187,31 +171,17 @@ ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS -# install runtime dependencies for Ultimate product -RUN apt-get update && \ - apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && \ - rm -rf /var/lib/apt/lists/* - -# install already built Ultimate product -RUN mkdir -p "${DIR_ULTIMATE}" -WORKDIR "${DIR_ULTIMATE}" +# install already built Ultimate Eliminator product COPY --from=build "${DIR_OUTPUT}/UltimateEliminator/linux/gtk/x86_64" "${DIR_ULTIMATE}" RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" -# install alread compiled tools for Ultimate -COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" -COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" -COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" -COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" - # default entry point to print installed Ultimate version -CMD ["Ultimate", "--version"] +CMD ["Ultimate", "-version"] #------------------------------------------------------------------------------ -# 2nd build stage: package Ultimate WebBackend +# 3rd build stage: package Ultimate WebBackend #------------------------------------------------------------------------------ -FROM debian:bullseye AS ultimate-webbackend +FROM ultimate-common AS ultimate-webbackend ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -236,32 +206,19 @@ ENV ULTIMATE_LOG_LEVEL="INFO" ENV ULTIMATE_DIR_TMP="/tmp/ultimate" ENV ULTIMATE_TIMEOUT=90 -# install runtime dependencies for Ultimate product -RUN apt-get update && \ - apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" - # install 'dockerize' for automatic configuration file creation ENV DOCKERIZE_VERSION="v0.7.0" RUN apt-get update && \ apt-get install -y "wget" \ "curl" && \ - wget -O - "https://github.com/jwilder/dockerize/releases/download/${DOCKERIZE_VERSION}/dockerize-linux-amd64-${DOCKERIZE_VERSION}.tar.gz" | tar xzf - -C "/usr/local/bin" && \ + wget -q -O - "https://github.com/jwilder/dockerize/releases/download/${DOCKERIZE_VERSION}/dockerize-linux-amd64-${DOCKERIZE_VERSION}.tar.gz" | tar xzf - -C "/usr/local/bin" && \ apt-get autoremove -yqq --purge "wget" && \ rm -rf /var/lib/apt/lists/* # install already built Ultimate product -RUN mkdir -p "${DIR_ULTIMATE}" -WORKDIR "${DIR_ULTIMATE}" COPY --from=build "${DIR_OUTPUT}/WebBackend/linux/gtk/x86_64" "${DIR_ULTIMATE}" RUN ln -s "${DIR_ULTIMATE}/WebBackend" "/usr/bin/WebBackend" -# install alread compiled tools for Ultimate -COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" -COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" -COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" -COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" - # add configuration files and templates for 'dockerize' and Ultimate COPY --from=build "${DIR_WEBSITE_CONFIG}/backend/settings_whitelist.json" "${DIR_ULTIMATE}/settings_whitelist.json" ADD "web.config.properties.tpl" "${DIR_ULTIMATE}/web.config.properties.tpl" @@ -280,7 +237,7 @@ EXPOSE "${ULTIMATE_BACKEND_PORT}" # define health check to supervise the Ultimate Webbackend's availability HEALTHCHECK --interval=1m --timeout=10s --start-period=20s \ CMD curl -f "http://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" || exit 1 -RUN echo "${DIR_ULTIMATE}" + # default entry point to automatically configure and start the Ultimate Webbackend product CMD dockerize -template "web.config.properties.tpl:web.config.properties" \ -template "WebBackend.ini.tpl:WebBackend.ini" \ diff --git a/packaging/docker/README.md b/packaging/docker/README.md index 4579af26305..99c109699f0 100644 --- a/packaging/docker/README.md +++ b/packaging/docker/README.md @@ -30,13 +30,25 @@ As an expected result, you should then receive the Ultimate version output from If you want to run Ultimate interactively for any verification input, you can spwan a bash in a created and started Ultimate `PRODUCT` container as follows. ```shell docker run -it /bin/bash -Ultimate -tc -s -i + -tc -s -i ``` -Calling Ultimate within the container then follows as usual, where a `TOOLCHAIN`, `SETTINGS`, and `PROGRAM` file path should be specified for a verification run. +Calling the Ultimate `PRODUCT` within the container then follows as usual, where a `TOOLCHAIN`, `SETTINGS`, and `PROGRAM` file path should be specified for a verification run. +An exception is a start of the graphical Ultimate Debug UI. +To do this, a graphic connection to the host system must be established via the X11 protocol, which can be done with the following Docker call. +```shell +docker run -it --network host \ + -e DISPLAY=$DISPLAY \ + -v :/home/build/ultimate/.Xauthority \ + -v /tmp/.X11-unix:/tmp/.X11-unix \ + ultimate-debug +``` +Note that the Docker call requires an `XAUTHORITY` file from the host system to grant the Ultimate Debug UI in the Docker container access to the graphical session on the host. +An `XAUTHORITY` file is, in the case of an X11 session, often located in the user's home directory on the host system and usually named `.Xauthority`. +In the case of a Wayland session, the `XAUTHORITY` file is often located under `/run/user/*/.*Xwaylandauth*`. +The `XAUTHORITY` file is mounted into the container by Docker along with a temporary Unix X11 socket to establish an X11 connection between host and container. +The Ultimate Debug UI application then uses this connection to render its graphical interface outside of the container on the host system. ## Configure Ultimate Webbackend The specific Ultimate `PRODUCT` called `ultimate-webbackend` requires an extensive and valid configuration for the Web service to start. - - From e722dde2fc1168c20e1afc38f6e12f427ff983fd Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 25 Jul 2025 17:40:48 +0200 Subject: [PATCH 06/38] Update Debian in Docker images to Debian Bookworm --- packaging/docker/Dockerfile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index e070af8340b..3a95a83e892 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -17,7 +17,7 @@ ARG DIR_TOOLS="${DIR_ULTIMATE}/${REPO_DIR_TOOLS}" #------------------------------------------------------------------------------ # 1st build stage: compile and materialize Ultimate #------------------------------------------------------------------------------ -FROM debian:bullseye AS build +FROM debian:bookworm AS build ARG REPO_URL="https://github.com/ultimate-pa/ultimate.git" ARG REPO_BRANCH="dev" @@ -32,7 +32,7 @@ ARG DIR_OUTPUT RUN apt-get update && \ apt-get install -y "git" \ "maven" \ - "openjdk-11-jdk" && \ + "openjdk-21-jdk" && \ rm -rf /var/lib/apt/lists/* # clone fresh Ultimate Git repository @@ -46,7 +46,7 @@ RUN mvn -f "${REPO_MAVEN_ROOT}" clean package -P materialize #------------------------------------------------------------------------------ # 2nd build stage: package common Ultimate artifacts shared by all products #------------------------------------------------------------------------------ -FROM debian:bullseye AS ultimate-common +FROM debian:bookworm AS ultimate-common ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -207,7 +207,7 @@ ENV ULTIMATE_DIR_TMP="/tmp/ultimate" ENV ULTIMATE_TIMEOUT=90 # install 'dockerize' for automatic configuration file creation -ENV DOCKERIZE_VERSION="v0.7.0" +ENV DOCKERIZE_VERSION="v0.9.5" RUN apt-get update && \ apt-get install -y "wget" \ "curl" && \ From d5fa9a8a95ad552b09cc7b1bdd3bcee528ecb068 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 25 Jul 2025 21:23:17 +0200 Subject: [PATCH 07/38] Execute Ultimate as non-root user and migrate Docker packaging to Alpine Linux --- packaging/docker/Dockerfile | 152 +++++++++++++++++----------- packaging/docker/README.md | 2 +- packaging/docker/WebBackend.ini.tpl | 4 +- packaging/docker/welcome.sh | 20 ++++ 4 files changed, 117 insertions(+), 61 deletions(-) create mode 100755 packaging/docker/welcome.sh diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 3a95a83e892..a76ea371de4 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -13,11 +13,14 @@ ARG DIR_BUILD="/home/build" ARG DIR_ULTIMATE="${DIR_BUILD}/ultimate" ARG DIR_OUTPUT="${DIR_ULTIMATE}/${REPO_DIR_BUILD}" ARG DIR_TOOLS="${DIR_ULTIMATE}/${REPO_DIR_TOOLS}" +ARG USER_NAME="ultimate" +ARG USER_GROUP="ultimate" +ARG USER_HOME="/home/${USER_NAME}" #------------------------------------------------------------------------------ # 1st build stage: compile and materialize Ultimate #------------------------------------------------------------------------------ -FROM debian:bookworm AS build +FROM alpine:3 AS build ARG REPO_URL="https://github.com/ultimate-pa/ultimate.git" ARG REPO_BRANCH="dev" @@ -29,11 +32,9 @@ ARG DIR_ULTIMATE ARG DIR_OUTPUT # install build dependencies for an entire Ultimate build -RUN apt-get update && \ - apt-get install -y "git" \ +RUN apk add --no-cache "git" \ "maven" \ - "openjdk-21-jdk" && \ - rm -rf /var/lib/apt/lists/* + "openjdk21" # clone fresh Ultimate Git repository RUN mkdir -p "${DIR_BUILD}" && \ @@ -46,7 +47,7 @@ RUN mvn -f "${REPO_MAVEN_ROOT}" clean package -P materialize #------------------------------------------------------------------------------ # 2nd build stage: package common Ultimate artifacts shared by all products #------------------------------------------------------------------------------ -FROM debian:bookworm AS ultimate-common +FROM alpine:3 AS ultimate-common ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS @@ -54,16 +55,21 @@ ARG DIR_BUILD ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME # install runtime dependencies for all Ultimate products -RUN apt-get update && \ - apt-get install -y "apt-utils" && \ - apt-get install -y "openjdk-11-jre" && \ - rm -rf /var/lib/apt/lists/* +RUN apk add --no-cache "libc6-compat" \ + "openjdk21-jre-headless" -# prepare installation directory for an Ultimate product -RUN mkdir -p "${DIR_ULTIMATE}" -WORKDIR "${DIR_ULTIMATE}" +# add the non-root user 'ultimate' for the Ultimate products and prepare +# installation directory for an Ultimate product +RUN mkdir -p "${USER_HOME}" && \ + addgroup "${USER_GROUP}" && \ + adduser -G "${USER_GROUP}" -H -h "${USER_HOME}" -D "${USER_NAME}" && \ + chown -R "${USER_NAME}:${USER_GROUP}" "${USER_HOME}" +WORKDIR "${USER_HOME}" # install alread compiled tools for all Ultimate products COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" @@ -71,6 +77,9 @@ COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" +# add Welcome script to print Ultimate version +ADD "welcome.sh" "/etc/profile.d/welcome.sh" + #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate CLI #------------------------------------------------------------------------------ @@ -82,13 +91,19 @@ ARG DIR_BUILD ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME # install already built Ultimate CLI product -COPY --from=build "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "/usr/bin/Ultimate" -# default entry point to print installed Ultimate CLI version -CMD ["Ultimate", "-version"] +# run the Ultimate CLI product as non-root user +USER "${USER_NAME}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate Debug UI @@ -101,25 +116,26 @@ ARG DIR_BUILD ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME # install graphical dependencies for Ultimate Debug UI product -RUN apt-get update && \ - apt-get install -y "libswt-gtk-4-jni" && \ - apt-get install -y "libswt-gtk-4-java" && \ - apt-get install -y "xauth" && \ - rm -rf /var/lib/apt/lists/* +RUN apk add --no-cache "openjdk21-jre" \ + "libcanberra-gtk3" \ + "dbus-x11" \ + "ttf-freefont" \ + "xauth" # install already built Ultimate Debug UI product -COPY --from=build "${DIR_OUTPUT}/Debug-E4/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/UltimateDebug" "/usr/bin/UltimateDebug" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/Debug-E4/linux/gtk/x86_64" "${USER_HOME}" +RUN ln -s "${USER_HOME}/UltimateDebug" "/usr/bin/UltimateDebug" -# run the Ultimate Debug UI product as non-root user 'ultimate' -RUN useradd --no-create-home --home-dir "${DIR_ULTIMATE}" ultimate && \ - chown -R ultimate:ultimate "${DIR_ULTIMATE}" -USER ultimate +# run the Ultimate Debug UI product as non-root user +#USER "${USER_NAME}" # default entry point to print installed Ultimate version -CMD ["UltimateDebug", "-version"] +ENTRYPOINT ["/bin/sh", "-l"] #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate ReqAnalyzer @@ -132,13 +148,19 @@ ARG DIR_BUILD ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME # install already built Ultimate ReqAnalyzer product -COPY --from=build "${DIR_OUTPUT}/ReqAnalyzer/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/ReqAnalyzer" "/usr/bin/ReqAnalyzer" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/ReqAnalyzer/linux/gtk/x86_64" "${USER_HOME}" +RUN ln -s "${USER_HOME}/ReqAnalyzer" "/usr/bin/ReqAnalyzer" + +# run the Ultimate ReqAnalyzer product as non-root user +USER "${USER_NAME}" # default entry point to print installed Ultimate version -CMD ["ReqAnalyzer", "-version"] +ENTRYPOINT ["/bin/sh", "-l"] #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate DeltaDebugger @@ -151,13 +173,16 @@ ARG DIR_BUILD ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME # install already built Ultimate DeltaDebugger product -COPY --from=build "${DIR_OUTPUT}/DeltaDebugger/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/DeltaDebugger/linux/gtk/x86_64" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "/usr/bin/Ultimate" # default entry point to print installed Ultimate version -CMD ["Ultimate", "-version"] +ENTRYPOINT ["/bin/sh", "-l"] #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate Eliminator @@ -170,13 +195,19 @@ ARG DIR_BUILD ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME # install already built Ultimate Eliminator product -COPY --from=build "${DIR_OUTPUT}/UltimateEliminator/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/Ultimate" "/usr/bin/Ultimate" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/UltimateEliminator/linux/gtk/x86_64" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "/usr/bin/Ultimate" + +# run the Ultimate Eliminator product as non-root user +USER "${USER_NAME}" # default entry point to print installed Ultimate version -CMD ["Ultimate", "-version"] +ENTRYPOINT ["/bin/sh", "-l"] #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate WebBackend @@ -189,6 +220,9 @@ ARG DIR_BUILD ARG DIR_ULTIMATE ARG DIR_OUTPUT ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME ARG REPO_DIR_WEBSITE_CONFIG="releaseScripts/website-config" ARG DIR_WEBSITE_CONFIG="${DIR_ULTIMATE}/${REPO_DIR_WEBSITE_CONFIG}" @@ -206,30 +240,32 @@ ENV ULTIMATE_LOG_LEVEL="INFO" ENV ULTIMATE_DIR_TMP="/tmp/ultimate" ENV ULTIMATE_TIMEOUT=90 +# create directory to store temporary files +RUN mkdir -p "${ULTIMATE_DIR_TMP}" + # install 'dockerize' for automatic configuration file creation ENV DOCKERIZE_VERSION="v0.9.5" -RUN apt-get update && \ - apt-get install -y "wget" \ +RUN apk add --no-cache "wget" \ + "openssl" \ "curl" && \ - wget -q -O - "https://github.com/jwilder/dockerize/releases/download/${DOCKERIZE_VERSION}/dockerize-linux-amd64-${DOCKERIZE_VERSION}.tar.gz" | tar xzf - -C "/usr/local/bin" && \ - apt-get autoremove -yqq --purge "wget" && \ - rm -rf /var/lib/apt/lists/* + wget -q -O - "https://github.com/jwilder/dockerize/releases/download/${DOCKERIZE_VERSION}/dockerize-alpine-linux-amd64-${DOCKERIZE_VERSION}.tar.gz" | tar xzf - -C "/usr/local/bin" && \ + apk del --no-cache "wget" -# install already built Ultimate product -COPY --from=build "${DIR_OUTPUT}/WebBackend/linux/gtk/x86_64" "${DIR_ULTIMATE}" -RUN ln -s "${DIR_ULTIMATE}/WebBackend" "/usr/bin/WebBackend" +# install already built Ultimate WebBackend product +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/WebBackend/linux/gtk/x86_64" "${USER_HOME}" +RUN ln -s "${USER_HOME}/WebBackend" "/usr/bin/WebBackend" -# add configuration files and templates for 'dockerize' and Ultimate -COPY --from=build "${DIR_WEBSITE_CONFIG}/backend/settings_whitelist.json" "${DIR_ULTIMATE}/settings_whitelist.json" -ADD "web.config.properties.tpl" "${DIR_ULTIMATE}/web.config.properties.tpl" -ADD "WebBackend.ini.tpl" "${DIR_ULTIMATE}/WebBackend.ini.tpl" -RUN rm -f "${DIR_ULTIMATE}/WebBackend.ini" +# run the Ultimate WebBackend product as non-root user +USER "${USER_NAME}" -ENV ULTIMATE_BACKEND_SETTINGS_WHITELIST="${DIR_ULTIMATE}/settings_whitelist.json" -ENV ULTIMATE_BACKEND_SETTINGS_FILE="${DIR_ULTIMATE}/web.config.properties" +# add configuration files and templates for 'dockerize' and Ultimate +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_WEBSITE_CONFIG}/backend/settings_whitelist.json" "${USER_HOME}/settings_whitelist.json" +ADD "web.config.properties.tpl" "${USER_HOME}/web.config.properties.tpl" +ADD "WebBackend.ini.tpl" "${USER_HOME}/WebBackend.ini.tpl" +RUN rm -f "${USER_HOME}/WebBackend.ini" -# create directory to store temporary files -RUN mkdir -p "${ULTIMATE_DIR_TMP}" +ENV ULTIMATE_BACKEND_SETTINGS_WHITELIST="${USER_HOME}/settings_whitelist.json" +ENV ULTIMATE_BACKEND_SETTINGS_FILE="${USER_HOME}/web.config.properties" # expose communication port of the Webbackend EXPOSE "${ULTIMATE_BACKEND_PORT}" @@ -239,6 +275,6 @@ HEALTHCHECK --interval=1m --timeout=10s --start-period=20s \ CMD curl -f "http://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" || exit 1 # default entry point to automatically configure and start the Ultimate Webbackend product -CMD dockerize -template "web.config.properties.tpl:web.config.properties" \ - -template "WebBackend.ini.tpl:WebBackend.ini" \ - WebBackend +ENTRYPOINT ["dockerize", "-template", "web.config.properties.tpl:web.config.properties", \ + "-template", "WebBackend.ini.tpl:WebBackend.ini", \ + "WebBackend"] diff --git a/packaging/docker/README.md b/packaging/docker/README.md index 99c109699f0..b912243dc56 100644 --- a/packaging/docker/README.md +++ b/packaging/docker/README.md @@ -38,7 +38,7 @@ To do this, a graphic connection to the host system must be established via the ```shell docker run -it --network host \ -e DISPLAY=$DISPLAY \ - -v :/home/build/ultimate/.Xauthority \ + -v :/home/ultimate/.Xauthority \ -v /tmp/.X11-unix:/tmp/.X11-unix \ ultimate-debug ``` diff --git a/packaging/docker/WebBackend.ini.tpl b/packaging/docker/WebBackend.ini.tpl index b94a94b21b7..56505c71540 100644 --- a/packaging/docker/WebBackend.ini.tpl +++ b/packaging/docker/WebBackend.ini.tpl @@ -1,7 +1,7 @@ -startup -plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar +plugins/org.eclipse.equinox.launcher_1.6.800.v20240513-1750.jar --launcher.library -plugins/org.eclipse.equinox.launcher.gtk.linux.x86_64_1.1.1300.v20200819-0940 +plugins/org.eclipse.equinox.launcher.gtk.linux.x86_64_1.2.1000.v20240506-2123 -nosplash -consoleLog -vmargs diff --git a/packaging/docker/welcome.sh b/packaging/docker/welcome.sh new file mode 100755 index 00000000000..21d6f3541dc --- /dev/null +++ b/packaging/docker/welcome.sh @@ -0,0 +1,20 @@ +#!/bin/sh + +check_and_print_version() { + for cmd in "${@}"; do + if command -v "${cmd}" >/dev/null 2>&1; then + "${cmd}" --version + return + fi + done +} + +echo "▗▖ ▗▖▗▖ ▗▄▄▄▖▗▄▄▄▖▗▖ ▗▖ ▗▄▖▗▄▄▄▖▗▄▄▄▖" +echo "▐▌ ▐▌▐▌ █ █ ▐▛▚▞▜▌▐▌ ▐▌ █ ▐▌ " +echo "▐▌ ▐▌▐▌ █ █ ▐▌ ▐▌▐▛▀▜▌ █ ▐▛▀▀▘" +echo "▝▚▄▞▘▐▙▄▄▖█ ▗▄█▄▖▐▌ ▐▌▐▌ ▐▌ █ ▐▙▄▄▖" +echo "┏━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓" +echo "┃ Program Analysis Framework ┃" +echo "┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛" +check_and_print_version "Ultimate" "UltimateDebug" "ReqAnalyzer" "WebBackend" +echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━" From 5b5e1d6cc60ec18b9e67978c14e90e289f22436e Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Mon, 28 Jul 2025 00:38:28 +0200 Subject: [PATCH 08/38] Add Docker image for Ultimate's web frontend based on Jekyll --- packaging/docker/Dockerfile | 108 ++++++++++++++++++++++ packaging/docker/README.md | 11 ++- packaging/docker/config.js.tpl | 31 +++++++ packaging/docker/docker-compose.yml | 17 +++- packaging/docker/ultimate-webfrontend.env | 18 ++++ 5 files changed, 181 insertions(+), 4 deletions(-) create mode 100644 packaging/docker/config.js.tpl create mode 100644 packaging/docker/ultimate-webfrontend.env diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index a76ea371de4..5ec70973c99 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -7,11 +7,13 @@ # common build arguments for multi-staged Docker build #------------------------------------------------------------------------------ ARG REPO_MAVEN_ROOT="trunk/source/BA_MavenParentUltimate" +ARG REPO_FRONTEND_ROOT="trunk/source/WebsiteStatic" ARG REPO_DIR_BUILD="trunk/source/BA_SiteRepository/target/products" ARG REPO_DIR_TOOLS="releaseScripts/default/adds" ARG DIR_BUILD="/home/build" ARG DIR_ULTIMATE="${DIR_BUILD}/ultimate" ARG DIR_OUTPUT="${DIR_ULTIMATE}/${REPO_DIR_BUILD}" +ARG DIR_OUTPUT_FRONTEND="${DIR_ULTIMATE}/${REPO_FRONTEND_ROOT}" ARG DIR_TOOLS="${DIR_ULTIMATE}/${REPO_DIR_TOOLS}" ARG USER_NAME="ultimate" ARG USER_GROUP="ultimate" @@ -44,6 +46,40 @@ RUN mkdir -p "${DIR_BUILD}" && \ WORKDIR "${DIR_ULTIMATE}" RUN mvn -f "${REPO_MAVEN_ROOT}" clean package -P materialize +#------------------------------------------------------------------------------ +# 2nd build stage: compile and build the Ultimate web interface +#------------------------------------------------------------------------------ +FROM build AS build-webfrontend + +ARG REPO_FRONTEND_ROOT +ARG REPO_DIR_BUILD +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT + +# install build dependencies for building the Ultimate web frontend +RUN apk add --no-cache "gcc" \ + "g++" \ + "make" \ + "libc-dev" \ + "libc++-dev" \ + "linux-headers" \ + "python3" \ + "ruby-full" \ + "ruby-dev" + +# build the Ultimate web frontend +WORKDIR "${REPO_FRONTEND_ROOT}" + +# patch the Jekyll installation to work under Ruby 3.4+ +RUN echo -e "gem 'csv'\n" \ + "gem 'base64'\n" \ + "gem 'bigdecimal'\n" \ + "gem 'logger'" >> Gemfile + +ENV PATH "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64:${PATH}" +RUN python3 scripts/build.py + #------------------------------------------------------------------------------ # 2nd build stage: package common Ultimate artifacts shared by all products #------------------------------------------------------------------------------ @@ -80,6 +116,78 @@ COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" # add Welcome script to print Ultimate version ADD "welcome.sh" "/etc/profile.d/welcome.sh" +#------------------------------------------------------------------------------ +# 2nd build stage: package Ultimate web frontend +#------------------------------------------------------------------------------ +FROM alpine:3 AS ultimate-webfrontend + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_FRONTEND +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME + +ENV ULTIMATE_FRONTEND_DEBUG="false" +ENV ULTIMATE_FRONTEND_MSG_ORIENTATION="left" + +ENV ULTIMATE_FRONTEND_PROTOCOL="http" +ENV ULTIMATE_FRONTEND_HOST="localhost" +ENV ULTIMATE_FRONTEND_PORT="80" +ENV ULTIMATE_FRONTEND_ROUTE="/website" + +ENV ULTIMATE_BACKEND_PROTOCOL="http" +ENV ULTIMATE_BACKEND_HOST="localhost" +ENV ULTIMATE_BACKEND_PORT=8080 +ENV ULTIMATE_BACKEND_ROUTE="/api" + +# install runtime dependencies for the Ultimate web frontend +RUN apk add --no-cache "gcc" \ + "g++" \ + "make" \ + "libc-dev" \ + "libc++-dev" \ + "linux-headers" \ + "ruby-full" \ + "ruby-dev" + +# install 'dockerize' for automatic configuration file creation +ENV DOCKERIZE_VERSION="v0.9.5" +RUN apk add --no-cache "wget" \ + "openssl" \ + "curl" && \ + wget -q -O - "https://github.com/jwilder/dockerize/releases/download/${DOCKERIZE_VERSION}/dockerize-alpine-linux-amd64-${DOCKERIZE_VERSION}.tar.gz" | tar xzf - -C "/usr/local/bin" && \ + apk del --no-cache "wget" + +# add the non-root user 'ultimate' for the Ultimate web frontend and prepare +# installation directory +RUN mkdir -p "${USER_HOME}" && \ + addgroup "${USER_GROUP}" && \ + adduser -G "${USER_GROUP}" -H -h "${USER_HOME}" -D "${USER_NAME}" && \ + chown -R "${USER_NAME}:${USER_GROUP}" "${USER_HOME}" +WORKDIR "${USER_HOME}" + +# install already built Ultimate web frontend +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-webfrontend "${DIR_OUTPUT_FRONTEND}" "${USER_HOME}" +ADD "config.js.tpl" "${USER_HOME}/config.js.tpl" + +# install Jekyll to serve the Ultimate web frontend +RUN bundle install + +# run the Ultimate web frontend as non-root user +USER "${USER_NAME}" + +# define health check to supervise the Ultimate web frontend's availability +HEALTHCHECK --interval=1m --timeout=10s --start-period=20s \ + CMD curl -f "${ULTIMATE_FRONTEND_PROTOCOL}://${ULTIMATE_FRONTEND_HOST}:${ULTIMATE_FRONTEND_PORT}${ULTIMATE_FRONTEND_ROUTE}/" || exit 1 + +# default entry point to serve the Ultimate web frontend +ENTRYPOINT dockerize -template "config.js.tpl:js/webinterface/config.js" \ + bundle exec jekyll serve --host "${ULTIMATE_FRONTEND_HOST}" \ + --port "${ULTIMATE_FRONTEND_PORT}" + #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate CLI #------------------------------------------------------------------------------ diff --git a/packaging/docker/README.md b/packaging/docker/README.md index b912243dc56..67d8c94ad0f 100644 --- a/packaging/docker/README.md +++ b/packaging/docker/README.md @@ -15,6 +15,7 @@ where `PRODUCT` is a placeholder for one of the products - `ultimate-deltadebugger` - `ultimate-eliminator` - `ultimate-webbackend` + - `ultimate-webfrontend` shipped with the Ultimate program analysis framework. @@ -49,6 +50,12 @@ The `XAUTHORITY` file is mounted into the container by Docker along with a tempo The Ultimate Debug UI application then uses this connection to render its graphical interface outside of the container on the host system. -## Configure Ultimate Webbackend +## Run Ultimate WebBackend and Frontend -The specific Ultimate `PRODUCT` called `ultimate-webbackend` requires an extensive and valid configuration for the Web service to start. +The specific Ultimate `PRODUCT`s called `ultimate-webbackend` and `ultimate-webfrontend` require an extensive and valid configuration for the Web service to start. +An example configuration is provided by a Docker Compose setup that can be configured by environemnt variables in the `ultimate-webbackend.env` and `ultimate-webfrontend.env` file. +After optional adjustment of the configuration, the setup can be provisioned using Docker Compose: +```shell +docker compose up +``` +The frontend of the Web service can be reached via the following URL in the web browser when using the example configuration: [http://localhost:80/website/](http://localhost:80/website/). diff --git a/packaging/docker/config.js.tpl b/packaging/docker/config.js.tpl new file mode 100644 index 00000000000..33ac9f79eb4 --- /dev/null +++ b/packaging/docker/config.js.tpl @@ -0,0 +1,31 @@ +/*----------------------------------------------------------------------------- + * Autogenerated Ultimate web frontend configuration. Do not edit! + *---------------------------------------------------------------------------*/ + +const _CONFIG = { + meta: { + // debug_mode: if set to true, `test/result.json` will be used as a response for fetching ultimate results. + debug_mode: {{ .Env.ULTIMATE_FRONTEND_DEBUG }}, + }, + backend: { + // web_bridge_url: URL to the WebBackend API. + web_bridge_url: '{{ .Env.ULTIMATE_BACKEND_PROTOCOL }}://{{ .Env.ULTIMATE_BACKEND_HOST }}:{{ .Env.ULTIMATE_BACKEND_PORT }}{{ .Env.ULTIMATE_BACKEND_ROUTE }}' + }, + editor: { + // Default content of the editor. + init_code: '// Enter code here ...', + // default_msg_orientation: one of ["bottom" | "left"], + // determines the ultimate response messages default orientation. + default_msg_orientation: "{{ .Env.ULTIMATE_FRONTEND_MSG_ORIENTATION }}" + }, + // code_file_extensions: Determines the file extension to be used as input for the ultimate tool. + // The key is the language of the tool in the frontend; + // The value is the file extension to be used by ultimate. + code_file_extensions: { + C: '.c', + Boogie: '.bpl', + C_pp: '.c', + automata_script: '.ats', + Smt: '.smt2' + } +}; diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index 504d59e4f93..34409f70dfa 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -1,12 +1,25 @@ version: "2" + services: ultimate-webbackend: build: dockerfile: "Dockerfile" target: "ultimate-webbackend" image: "ultimate-webbackend" - env_file: - - "ultimate-webbackend.env" + env_file: "ultimate-webbackend.env" ports: - "8080:8080" restart: "unless-stopped" + + ultimate-webfrontend: + build: + dockerfile: "Dockerfile" + target: "ultimate-webfrontend" + image: "ultimate-webfrontend" + env_file: "ultimate-webfrontend.env" + ports: + - "80:80" + restart: "unless-stopped" + depends_on: + ultimate-webbackend: + condition: service_healthy diff --git a/packaging/docker/ultimate-webfrontend.env b/packaging/docker/ultimate-webfrontend.env new file mode 100644 index 00000000000..4680448a1de --- /dev/null +++ b/packaging/docker/ultimate-webfrontend.env @@ -0,0 +1,18 @@ +############################################################################### +# Environment variables for 'ultimate-webfrontend' service in docker-compose.yml +############################################################################### + +# frontend settings +ULTIMATE_FRONTEND_DEBUG=false +ULTIMATE_FRONTEND_MSG_ORIENTATION=left + +ULTIMATE_FRONTEND_PROTOCOL=http +ULTIMATE_FRONTEND_HOST=0.0.0.0 +ULTIMATE_FRONTEND_PORT=80 +ULTIMATE_FRONTEND_ROUTE=/website + +# backend settings +ULTIMATE_BACKEND_PROTOCOL=http +ULTIMATE_BACKEND_HOST=localhost +ULTIMATE_BACKEND_PORT=8080 +ULTIMATE_BACKEND_ROUTE=/api From 2cb1621c90a4c4d763e5ae760c8b980bee044852 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 29 Jul 2025 20:10:48 +0200 Subject: [PATCH 09/38] Remove patch for Jekyll in Docker Web frontend image build The patch for the Jekyll installation is no longer necessary since the issue was fixed by updating Jekyll in commit c0f9255. --- packaging/docker/Dockerfile | 7 ------- 1 file changed, 7 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 5ec70973c99..85934c4c8ab 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -70,13 +70,6 @@ RUN apk add --no-cache "gcc" \ # build the Ultimate web frontend WORKDIR "${REPO_FRONTEND_ROOT}" - -# patch the Jekyll installation to work under Ruby 3.4+ -RUN echo -e "gem 'csv'\n" \ - "gem 'base64'\n" \ - "gem 'bigdecimal'\n" \ - "gem 'logger'" >> Gemfile - ENV PATH "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64:${PATH}" RUN python3 scripts/build.py From 9af11d84873e005c51904fcf5d33137219028c8b Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 29 Jul 2025 20:17:22 +0200 Subject: [PATCH 10/38] Run the Ultimate Debug UI in a Docker container as non-root user --- packaging/docker/Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 85934c4c8ab..b2043d92e40 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -233,7 +233,7 @@ COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/Debug-E4/l RUN ln -s "${USER_HOME}/UltimateDebug" "/usr/bin/UltimateDebug" # run the Ultimate Debug UI product as non-root user -#USER "${USER_NAME}" +USER "${USER_NAME}" # default entry point to print installed Ultimate version ENTRYPOINT ["/bin/sh", "-l"] From 39a443899189e125eff6f67d7fc7f4e1d50d71f6 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 29 Jul 2025 21:10:56 +0200 Subject: [PATCH 11/38] Make Jekyll baseurl option configurable for a Docker image build --- packaging/docker/Dockerfile | 4 +++- packaging/docker/docker-compose.yml | 2 ++ trunk/source/WebsiteStatic/scripts/build.py | 18 +++++++++++++----- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index b2043d92e40..9a56466d5b4 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -51,6 +51,8 @@ RUN mvn -f "${REPO_MAVEN_ROOT}" clean package -P materialize #------------------------------------------------------------------------------ FROM build AS build-webfrontend +ARG ULTIMATE_FRONTEND_BASEURL="/website" + ARG REPO_FRONTEND_ROOT ARG REPO_DIR_BUILD ARG DIR_BUILD @@ -71,7 +73,7 @@ RUN apk add --no-cache "gcc" \ # build the Ultimate web frontend WORKDIR "${REPO_FRONTEND_ROOT}" ENV PATH "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64:${PATH}" -RUN python3 scripts/build.py +RUN python3 scripts/build.py --baseurl "${ULTIMATE_FRONTEND_BASEURL}" #------------------------------------------------------------------------------ # 2nd build stage: package common Ultimate artifacts shared by all products diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index 34409f70dfa..d890c6c0172 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -15,6 +15,8 @@ services: build: dockerfile: "Dockerfile" target: "ultimate-webfrontend" + args: + ULTIMATE_FRONTEND_BASEURL: "/website" image: "ultimate-webfrontend" env_file: "ultimate-webfrontend.env" ports: diff --git a/trunk/source/WebsiteStatic/scripts/build.py b/trunk/source/WebsiteStatic/scripts/build.py index e1008c1b574..43d97d8cc08 100755 --- a/trunk/source/WebsiteStatic/scripts/build.py +++ b/trunk/source/WebsiteStatic/scripts/build.py @@ -28,16 +28,24 @@ def parse_args() -> argparse.Namespace: parser.add_argument( "--skip-settings", action="store_true", help="skip rebuilding settings (useful during debugging)" ) + parser.add_argument( + "--baseurl", action="store", type=str, help="set base URL for site (necessary when hosting the site in a sub-directory)" + ) return parser.parse_args() except argparse.ArgumentError as exc: print(exc.message + "\n" + exc.argument) sys.exit(1) -def run_jekyll(production_build=False): +def run_jekyll(production_build=False, baseurl=None): subprocess.run(get_jekyll_cli() + ["clean"], check=True) + baseurl_params = [] + + if production_build: + baseurl_params = ["--baseurl", "/"] + elif baseurl is not None: + baseurl_params = ["--baseurl", baseurl] - baseurl_params = ["--baseurl", "/"] if production_build else [] subprocess.run(get_jekyll_cli() + ["build", *baseurl_params], check=True) @@ -53,7 +61,7 @@ def copy_webinterface_config(production_build): shutil.copyfile(src, tgt) -def build(production_build=False, skip_settings=False): +def build(production_build=False, skip_settings=False, baseurl=None): # check if external tools are available if not skip_settings: get_ultimate_cli() @@ -70,7 +78,7 @@ def build(production_build=False, skip_settings=False): refresh_index() # build the static jekyll site - run_jekyll(production_build) + run_jekyll(production_build, baseurl) # copy the appropriate webinterface settings to _site/ copy_webinterface_config(production_build) @@ -78,4 +86,4 @@ def build(production_build=False, skip_settings=False): if __name__ == "__main__": args = parse_args() - build(args.production, args.skip_settings) + build(args.production, args.skip_settings, args.baseurl) From 335e81425f30803f27f756626b8ce60b4446825e Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 29 Jul 2025 22:36:16 +0200 Subject: [PATCH 12/38] Make Docker Compose setup of the Ultimate Web service configurable --- packaging/docker/Dockerfile | 14 ++++++---- packaging/docker/README.md | 4 +-- packaging/docker/docker-compose.yml | 28 +++++++++++++++---- packaging/docker/ultimate-webbackend.env | 22 --------------- ...ebfrontend.env => ultimate-webservice.env} | 12 ++++++-- 5 files changed, 42 insertions(+), 38 deletions(-) delete mode 100644 packaging/docker/ultimate-webbackend.env rename packaging/docker/{ultimate-webfrontend.env => ultimate-webservice.env} (61%) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 9a56466d5b4..3f835c19837 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -72,7 +72,7 @@ RUN apk add --no-cache "gcc" \ # build the Ultimate web frontend WORKDIR "${REPO_FRONTEND_ROOT}" -ENV PATH "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64:${PATH}" +ENV PATH="${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64:${PATH}" RUN python3 scripts/build.py --baseurl "${ULTIMATE_FRONTEND_BASEURL}" #------------------------------------------------------------------------------ @@ -330,17 +330,14 @@ ARG USER_HOME ARG REPO_DIR_WEBSITE_CONFIG="releaseScripts/website-config" ARG DIR_WEBSITE_CONFIG="${DIR_ULTIMATE}/${REPO_DIR_WEBSITE_CONFIG}" +ARG ULTIMATE_DIR_TMP="/tmp/ultimate" + ENV ULTIMATE_BACKEND_HOST="localhost" ENV ULTIMATE_BACKEND_PORT=8080 ENV ULTIMATE_BACKEND_ROUTE="/api" -ENV ULTIMATE_FRONTEND_SERVE="False" -ENV ULTIMATE_FRONTEND_PATH="/some/path" -ENV ULTIMATE_FRONTEND_ROUTE="/website" ENV ULTIMATE_LOG_PATH="/dev/stdout" ENV ULTIMATE_LOG_LEVEL="INFO" - -ENV ULTIMATE_DIR_TMP="/tmp/ultimate" ENV ULTIMATE_TIMEOUT=90 # create directory to store temporary files @@ -370,6 +367,11 @@ RUN rm -f "${USER_HOME}/WebBackend.ini" ENV ULTIMATE_BACKEND_SETTINGS_WHITELIST="${USER_HOME}/settings_whitelist.json" ENV ULTIMATE_BACKEND_SETTINGS_FILE="${USER_HOME}/web.config.properties" +# Serving the frontend from the backend is not supported by this Docker image +ENV ULTIMATE_FRONTEND_SERVE="False" +ENV ULTIMATE_FRONTEND_PATH="${USER_HOME}" +ENV ULTIMATE_FRONTEND_ROUTE="/website" + # expose communication port of the Webbackend EXPOSE "${ULTIMATE_BACKEND_PORT}" diff --git a/packaging/docker/README.md b/packaging/docker/README.md index 67d8c94ad0f..e9a5e416929 100644 --- a/packaging/docker/README.md +++ b/packaging/docker/README.md @@ -53,9 +53,9 @@ The Ultimate Debug UI application then uses this connection to render its graphi ## Run Ultimate WebBackend and Frontend The specific Ultimate `PRODUCT`s called `ultimate-webbackend` and `ultimate-webfrontend` require an extensive and valid configuration for the Web service to start. -An example configuration is provided by a Docker Compose setup that can be configured by environemnt variables in the `ultimate-webbackend.env` and `ultimate-webfrontend.env` file. +An example configuration is provided by a Docker Compose setup that can be configured by environemnt variables in the `ultimate-webservice.env` file. After optional adjustment of the configuration, the setup can be provisioned using Docker Compose: ```shell -docker compose up +docker compose --env-file ultimate-webservice.env up --build ``` The frontend of the Web service can be reached via the following URL in the web browser when using the example configuration: [http://localhost:80/website/](http://localhost:80/website/). diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index d890c6c0172..57661e78a57 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -5,10 +5,18 @@ services: build: dockerfile: "Dockerfile" target: "ultimate-webbackend" + args: + ULTIMATE_TMP_DIR: "${ULTIMATE_TMP_DIR-/tmp/ultimate}" image: "ultimate-webbackend" - env_file: "ultimate-webbackend.env" + environment: + ULTIMATE_BACKEND_HOST: "${ULTIMATE_BACKEND_HOST-localhost}" + ULTIMATE_BACKEND_PORT: ${ULTIMATE_BACKEND_PORT-8080} + ULTIMATE_BACKEND_ROUTE: "${ULTIMATE_BACKEND_ROUTE-/api}" + ULTIMATE_LOG_PATH: "${ULTIMATE_LOG_PATH-/dev/stdout}" + ULTIMATE_LOG_LEVEL: "${ULTIMATE_LOG_LEVEL-INFO}" + ULTIMATE_TIMEOUT: ${ULTIMATE_TIMEOUT-90} ports: - - "8080:8080" + - "8080:${ULTIMATE_BACKEND_PORT-8080}" restart: "unless-stopped" ultimate-webfrontend: @@ -16,11 +24,21 @@ services: dockerfile: "Dockerfile" target: "ultimate-webfrontend" args: - ULTIMATE_FRONTEND_BASEURL: "/website" + ULTIMATE_FRONTEND_BASEURL: "${ULTIMATE_FRONTEND_ROUTE-/website}" image: "ultimate-webfrontend" - env_file: "ultimate-webfrontend.env" + environment: + ULTIMATE_FRONTEND_DEBUG: "${ULTIMATE_FRONTEND_DEBUG-false}" + ULTIMATE_FRONTEND_MSG_ORIENTATION: "${ULTIMATE_FRONTEND_MSG_ORIENTATION-left}" + ULTIMATE_FRONTEND_PROTOCOL: "${ULTIMATE_FRONTEND_PROTOCOL-http}" + ULTIMATE_FRONTEND_HOST: "${ULTIMATE_FRONTEND_HOST-localhost}" + ULTIMATE_FRONTEND_PORT: ${ULTIMATE_FRONTEND_PORT-80} + ULTIMATE_FRONTEND_ROUTE: "${ULTIMATE_FRONTEND_ROUTE-/website}" + ULTIMATE_BACKEND_PROTOCOL: "${ULTIMATE_BACKEND_PROTOCOL-http}" + ULTIMATE_BACKEND_HOST: "${ULTIMATE_BACKEND_HOST-localhost}" + ULTIMATE_BACKEND_PORT: "${ULTIMATE_BACKEND_PORT-8080}" + ULTIMATE_BACKEND_ROUTE: "${ULTIMATE_BACKEND_ROUTE-/api}" ports: - - "80:80" + - "80:${ULTIMATE_FRONTEND_PORT-8080}" restart: "unless-stopped" depends_on: ultimate-webbackend: diff --git a/packaging/docker/ultimate-webbackend.env b/packaging/docker/ultimate-webbackend.env deleted file mode 100644 index 75cd655165e..00000000000 --- a/packaging/docker/ultimate-webbackend.env +++ /dev/null @@ -1,22 +0,0 @@ -############################################################################### -# Environment variables for 'ultimate-webbackend' service in docker-compose.yml -############################################################################### - -# backend settings -ULTIMATE_BACKEND_HOST=localhost -ULTIMATE_BACKEND_PORT=8080 -ULTIMATE_BACKEND_ROUTE=/api -ULTIMATE_BACKEND_START_TIMEOUT=30 - -# frontend settings -ULTIMATE_FRONTEND_SERVE=False -ULTIMATE_FRONTEND_PATH=/some/path -ULTIMATE_FRONTEND_ROUTE=/website - -# log settings -ULTIMATE_LOG_PATH=/dev/stdout -ULTIMATE_LOG_LEVEL=INFO - -# general settings -ULTIMATE_DIR_TMP=/tmp/ultimate -ULTIMATE_TIMEOUT=90 diff --git a/packaging/docker/ultimate-webfrontend.env b/packaging/docker/ultimate-webservice.env similarity index 61% rename from packaging/docker/ultimate-webfrontend.env rename to packaging/docker/ultimate-webservice.env index 4680448a1de..f7dba9579ad 100644 --- a/packaging/docker/ultimate-webfrontend.env +++ b/packaging/docker/ultimate-webservice.env @@ -1,6 +1,6 @@ -############################################################################### -# Environment variables for 'ultimate-webfrontend' service in docker-compose.yml -############################################################################### +########################################################################################################## +# Environment variables for 'ultimate-webfrontend' and 'ultimate-webbackend' service in docker-compose.yml +########################################################################################################## # frontend settings ULTIMATE_FRONTEND_DEBUG=false @@ -16,3 +16,9 @@ ULTIMATE_BACKEND_PROTOCOL=http ULTIMATE_BACKEND_HOST=localhost ULTIMATE_BACKEND_PORT=8080 ULTIMATE_BACKEND_ROUTE=/api + +ULTIMATE_LOG_PATH=/dev/stdout +ULTIMATE_LOG_LEVEL=INFO + +ULTIMATE_DIR_TMP=/tmp/ultimate +ULTIMATE_TIMEOUT=90 From 924d3e7243fe282342808ddc912087a50f6497cd Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 15 Aug 2025 20:39:48 +0200 Subject: [PATCH 13/38] Separate build of Ultimate products from creating ZIP archives This change introduces a new makeBuild.sh script that builds all Ultimate products and packages the products with the required configurations (toolchain and settings files), additional programs and files like solvers or licenses. This script is then used in the existing makeFresh.sh script for the common build steps to avoid duplicate script code. The functionality of the makeFresh.sh script remains unchanged. --- .gitignore | 7 +- .../default/createDeltaDebuggerDir.sh | 79 ---- releaseScripts/default/makeBuild.sh | 98 +++++ releaseScripts/default/makeFresh.sh | 106 +++--- releaseScripts/default/makePackageConfig.sh | 151 ++++++++ releaseScripts/default/makePackageReqCheck.sh | 106 ++++++ releaseScripts/default/makePackageSmall.sh | 95 +++++ releaseScripts/default/makeSettings.sh | 36 ++ releaseScripts/default/makeZip.sh | 164 ++------ releaseScripts/default/semver2.sh | 354 ++++++++++++++++++ 10 files changed, 910 insertions(+), 286 deletions(-) delete mode 100755 releaseScripts/default/createDeltaDebuggerDir.sh create mode 100755 releaseScripts/default/makeBuild.sh create mode 100755 releaseScripts/default/makePackageConfig.sh create mode 100644 releaseScripts/default/makePackageReqCheck.sh create mode 100755 releaseScripts/default/makePackageSmall.sh create mode 100755 releaseScripts/default/semver2.sh diff --git a/.gitignore b/.gitignore index 2cd55d48ec2..996a8c204fe 100644 --- a/.gitignore +++ b/.gitignore @@ -12,8 +12,8 @@ hs_err_pid* /packaging/docker/*.env -/releaseScripts/default/DeltaDebugger-linux/* -/releaseScripts/default/DeltaDebugger-win32/* +/releaseScripts/default/UDeltaDebugger-linux/* +/releaseScripts/default/UDeltaDebugger-win32/* /releaseScripts/default/UAutomizer-linux/* /releaseScripts/default/UAutomizer-win32/* /releaseScripts/default/UGemCutter-linux/* @@ -26,7 +26,8 @@ hs_err_pid* /releaseScripts/default/UTaipan-win32/* /releaseScripts/default/UTaipan-win32/ /releaseScripts/default/*.zip -/releaseScripts/default/WebBackend +/releaseScripts/default/UWebBackend-linux/* +/releaseScripts/default/UWebBackend-win32/* /releaseScripts/default/WebFrontend /releaseScripts/2018chccomp/Unihorn/StarExecArchive/* /releaseScripts/2018chccomp/Unihorn/StarExecArchive diff --git a/releaseScripts/default/createDeltaDebuggerDir.sh b/releaseScripts/default/createDeltaDebuggerDir.sh deleted file mode 100755 index 6f13056a638..00000000000 --- a/releaseScripts/default/createDeltaDebuggerDir.sh +++ /dev/null @@ -1,79 +0,0 @@ -#!/bin/bash -# This script generates a directory that contains the DeltaDebugger -# It takes additional binaries from the adds/ folder. Currently, we use z3, cvc4 and mathsat -# It also adds README, Ultimate.py, and various license files -# In contrast to createZip, it does not add toolchains or settings files and it does not generate a .zip, only the directory - -## Include the makeSettings shared functions -DIR="${BASH_SOURCE%/*}" -if [[ ! -d "$DIR" ]]; then DIR="$PWD"; fi -. "$DIR/makeSettings.sh" - - -if [ $# -le 0 ]; then - echo $# - echo "Not enough arguments supplied -- use arguments in the following order" - echo "1. 'linux' or 'win32' for the target platform" - exit 1 -fi - -TOOLNAME="DeltaDebugger" -LCTOOLNAME="$(echo $TOOLNAME | tr '[A-Z]' '[a-z]')" -echo "using $TOOLNAME ($LCTOOLNAME) as toolname" - - -if [ "$1" == "linux" ]; then - echo "Building .zip for linux..." - ARCH="linux" - ARCHPATH="products/DeltaDebugger/linux/gtk/x86_64" - Z3PATH="adds/z3" - CVC4PATH="adds/cvc4" - MATHSATPATH="adds/mathsat" -elif [ "$1" == "win32" ]; then - echo "Building .zip for win32..." - ARCH="win32" - ARCHPATH="products/DeltaDebugger/win32/win32/x86_64" - Z3PATH="adds/z3.exe" - CVC4PATH="adds/cvc4.exe" - MATHSATPATH="adds/mathsat.exe adds/mpir.dll adds/mathsat.dll" -else - echo "Wrong argument: ""$1"" -- use 'linux' or 'win32'" - exit 1 -fi - - -# set version -VERSION=`git rev-parse HEAD | cut -c1-8` -echo "Version is "$VERSION -TARGETDIR=${TOOLNAME}-${ARCH} -CONFIGDIR="$TARGETDIR"/config -DATADIR="$TARGETDIR"/data - -if [ -d "$TARGETDIR" ]; then - echo "Removing old ""$TARGETDIR" - rm -r "$TARGETDIR" -fi - -echo "Copying files" -mkdir "$TARGETDIR" -mkdir "$CONFIGDIR" -mkdir "$DATADIR" - -exit_on_fail cp -a ../../trunk/source/BA_SiteRepository/target/${ARCHPATH}/* "$TARGETDIR"/ -exit_on_fail cp adds/LICENSE* "$TARGETDIR"/ -exit_on_fail cp adds/*LICENSE "$TARGETDIR"/ -exit_on_fail cp adds/Ultimate.py "$TARGETDIR"/ -exit_on_fail cp adds/Ultimate.ini "$TARGETDIR"/ -exit_on_fail cp adds/README "$TARGETDIR"/ -exit_on_fail cp ${Z3PATH} "$TARGETDIR"/ -exit_on_fail cp ${CVC4PATH} "$TARGETDIR"/ -exit_on_fail cp ${MATHSATPATH} "$TARGETDIR"/ - -echo "Modifying Ultimate.py with version and toolname" -## replacing version value in Ultimate.py -exit_on_fail sed "s/version =.*/version = \'$VERSION\'/g" "$TARGETDIR"/Ultimate.py > "$TARGETDIR"/Ultimate.py.tmp && mv "$TARGETDIR"/Ultimate.py.tmp "$TARGETDIR"/Ultimate.py && chmod a+x "$TARGETDIR"/Ultimate.py - -## replacing toolname value in Ultimate.py -exit_on_fail sed "s/toolname =.*/toolname = \'$TOOLNAME\'/g" "$TARGETDIR"/Ultimate.py > "$TARGETDIR"/Ultimate.py.tmp && mv "$TARGETDIR"/Ultimate.py.tmp "$TARGETDIR"/Ultimate.py && chmod a+x "$TARGETDIR"/Ultimate.py - - diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh new file mode 100755 index 00000000000..1908833cdbe --- /dev/null +++ b/releaseScripts/default/makeBuild.sh @@ -0,0 +1,98 @@ +#!/bin/bash +#------------------------------------------------------------------------------- +# This script builds Ultimate with Maven and then creates all tools. +# Note that it does no longer build the website, as this requires Ruby and Jekyll. +# If you want to build the website, use 'makeWebsite.sh' after 'makeBuild.sh'. +#------------------------------------------------------------------------------- + +# Load shared functions and settings +DIR="${BASH_SOURCE%/*}" +if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi +source "${DIR}/makeSettings.sh" +source "${DIR}/semver2.sh" + +start() { + printf '▗▄▄▖ ▗▖ ▗▖▗▄▄▄▖▗▖ ▗▄▄▄ \n' + printf '▐▌ ▐▌▐▌ ▐▌ █ ▐▌ ▐▌ █\n' + printf '▐▛▀▚▖▐▌ ▐▌ █ ▐▌ ▐▌ █\n' + printf '▐▙▄▞▘▝▚▄▞▘▗▄█▄▖▐▙▄▄▖▐▙▄▄▀\n' + printf '┏━━━━━━━━━━━━━━━━━━━━━━━┓\n' + printf '┃ Ultimate Products ┃\n' + printf '┗━━━━━━━━━━━━━━━━━━━━━━━┛\n' + print_newline +} + +check() { + # Check if build tools are installed + test_if_cmd_is_available mvn + test_if_cmd_is_available java + test_if_cmd_is_available javac + # Retrieve build tool versions + VERS_MVN="$(get_cmd_version mvn --version)" + VERS_JVM="$(get_cmd_version java --version)" + VERS_JDK="$(get_cmd_version javac --version)" + # Check version of installed build tools + test_cmd_version_greater_equal "${VERS_MVN}" "3.9" "Maven" + test_cmd_version_greater_equal "${VERS_JVM}" "21.0" "Java Runtime" + test_cmd_version_greater_equal "${VERS_JDK}" "21.0" "Java Development Kit" +} + +build() { + spushd "../../trunk/source/BA_MavenParentUltimate/" + + print_heading "Using the build tools" + print_cmd_version "${VERS_MVN}" " Maven" + print_cmd_version "${VERS_JVM}" " Java Runtime" + print_cmd_version "${VERS_JDK}" "Java Development Kit" + print_newline + + print_heading "Start Ultimate build" + exit_on_fail mvn -T 1C clean install -Pmaterialize + print_newline + + spopd +} + +package() { + for platform in {linux,win32}; do + # makePackageConfig.sh + print_heading "Package Ultimate Taipan [${platform}]" + exit_on_fail bash makePackageConfig.sh "Taipan" "${platform}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + print_newline + + print_heading "Package Ultimate Automizer [${platform}]" + exit_on_fail bash makePackageConfig.sh "Automizer" "${platform}" "AutomizerCInline_WitnessPrinter.xml" "BuchiAutomizerCInline_WitnessPrinter.xml" "AutomizerCInline_IcfgBuilder.xml" "AutomizerCInline_WitnessPrinter.xml" "LTLAutomizerC.xml" "BuchiAutomizerCInline.xml" + print_newline + + print_heading "Package Ultimate Kojak [${platform}]" + exit_on_fail bash makePackageConfig.sh "Kojak" "${platform}" "KojakC_WitnessPrinter.xml" "NONE" "NONE" "KojakC_WitnessPrinter.xml" "NONE" "NONE" + print_newline + + print_heading "Package Ultimate GemCutter [${platform}]" + exit_on_fail bash makePackageConfig.sh "GemCutter" "${platform}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + print_newline + + print_heading "Package Ultimate Referee [${platform}]" + exit_on_fail bash makePackageConfig.sh "Referee" "${platform}" "RefereeCInline.xml" "NONE" "RefereeCInline_IcfgBuilder.xml" "NONE" "NONE" "NONE" + print_newline + + # makePackageSmall.sh + print_heading "Package Ultimate DeltaDebugger [${platform}]" + exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "${platform}" + print_newline + + print_heading "Package Ultimate WebBackend [${platform}]" + exit_on_fail bash makePackageSmall.sh "WebBackend" "${platform}" + print_newline + + # makePackageReqCheck.sh + print_heading "Package Ultimate ReqCheck [${platform}]" + exit_on_fail bash makePackageReqCheck.sh "ReqCheck" "${platform}" "ReqCheck.xml" "ReqCheck.xml" + print_newline + done +} + +start +check +build +package diff --git a/releaseScripts/default/makeFresh.sh b/releaseScripts/default/makeFresh.sh index 0491f1d9973..345d110a796 100755 --- a/releaseScripts/default/makeFresh.sh +++ b/releaseScripts/default/makeFresh.sh @@ -1,75 +1,53 @@ #!/bin/bash -# This script builds Ultimate with Maven and then creates deployable zip archives for -# all tools. +#------------------------------------------------------------------------------- +# This script builds Ultimate with Maven and then creates deployable zip archives for all tools. # Note that it does no longer build the website, as this requires Ruby and Jekyll. # If you want to build the website, use makeWebsite.sh after makeFresh.sh. +#------------------------------------------------------------------------------- - -# load shared functions and settings +# Load shared functions and settings DIR="${BASH_SOURCE%/*}" -if [[ ! -d "$DIR" ]]; then DIR="$PWD"; fi -. "$DIR/makeSettings.sh" - -verlte() { - printf '%s\n%s' "$1" "$2" | sort -C -V -} +if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi +source "${DIR}/makeSettings.sh" -build() { - spushd "../../trunk/source/BA_MavenParentUltimate/" - if ! command -v mvn &> /dev/null ; then - echo "Maven not found. Please install Maven and make sure it is in your PATH." - exit 1 - fi - mvn_version=$(mvn --version) - java_version=$(grep -oP 'Java version: \K.*?,' <<< "$mvn_version") - java_version=${java_version::-1} # remove , - if verlte "$java_version" "21.0.0"; then - echo "Java version $java_version is too old. Please install Java 21 or newer." - exit 1 - fi - printf 'Using the following versions:\n%s\n' "$mvn_version" - exit_on_fail mvn -T 1C clean install -Pmaterialize - spopd -} +# Load and execute all Ultimate build steps before archive function is called. +source "${DIR}/makeBuild.sh" -create_tool_zips() { +archive() { for platform in {linux,win32}; do - # makeZip - # Taipan - exit_on_fail bash makeZip.sh Taipan $platform AutomizerCInline_WitnessPrinter.xml NONE AutomizerCInline.xml AutomizerCInline_WitnessPrinter.xml NONE NONE - - # Automizer without separate blockencoding plugin - exit_on_fail bash makeZip.sh Automizer $platform AutomizerCInline_WitnessPrinter.xml BuchiAutomizerCInline_WitnessPrinter.xml AutomizerCInline_IcfgBuilder.xml AutomizerCInline_WitnessPrinter.xml LTLAutomizerC.xml BuchiAutomizerCInline.xml - - # Automizer with separate blockencoding plugin - #exit_on_fail bash makeZip.sh Automizer linux AutomizerC_BE_WitnessPrinter.xml BuchiAutomizerCInline_BE_WitnessPrinter.xml AutomizerC.xml AutomizerC_BE_WitnessPrinter.xml LTLAutomizerC.xml BuchiAutomizerCInline.xml - - # Kojak - exit_on_fail bash makeZip.sh Kojak $platform KojakC_WitnessPrinter.xml NONE NONE KojakC_WitnessPrinter.xml NONE NONE - - # GemCutter - exit_on_fail bash makeZip.sh GemCutter $platform AutomizerCInline_WitnessPrinter.xml NONE AutomizerCInline.xml AutomizerCInline_WitnessPrinter.xml NONE NONE - - # Referee - exit_on_fail bash makeZip.sh Referee $platform RefereeCInline.xml NONE RefereeCInline_IcfgBuilder.xml NONE NONE NONE - - # DeltaDebugger - exit_on_fail bash createDeltaDebuggerDir.sh $platform - - # ReqCheck - exit_on_fail bash createReqCheckZip.sh ReqCheck $platform ReqCheck.xml ReqCheck.xml + # makeZip.sh + print_heading "Archive Ultimate Taipan [${platform}]" + exit_on_fail bash makeZip.sh "Taipan" "${platform}" + print_newline + + print_heading "Archive Ultimate Automizer [${platform}]" + exit_on_fail bash makeZip.sh "Automizer" "${platform}" + print_newline + + print_heading "Archive Ultimate Kojak [${platform}]" + exit_on_fail bash makeZip.sh "Kojak" "${platform}" + print_newline + + print_heading "Archive Ultimate GemCutter [${platform}]" + exit_on_fail bash makeZip.sh "GemCutter" "${platform}" + print_newline + + print_heading "Archive Ultimate Referee [${platform}]" + exit_on_fail bash makeZip.sh "Referee" "${platform}" + print_newline + + print_heading "Archive Ultimate DeltaDebugger [${platform}]" + exit_on_fail bash makeZip.sh "DeltaDebugger" "${platform}" + print_newline + + print_heading "Archive Ultimate WebBackend [${platform}]" + exit_on_fail bash makeZip.sh "WebBackend" "${platform}" + print_newline + + print_heading "Archive Ultimate ReqCheck [${platform}]" + exit_on_fail bash makeZip.sh "ReqCheck" "${platform}" + print_newline done } -create_webbackend_dir() { - local source="../../trunk/source/BA_SiteRepository/target/products/WebBackend/linux/gtk/x86_64" - local target="$(readlink -f WebBackend)" - if [ -d "$target" ] ; then rm -r "$target" ; fi - mkdir "$target" - echo "Copying WebBackend" - cp -r "$source/"* "$target" -} - -build -create_tool_zips -create_webbackend_dir +archive diff --git a/releaseScripts/default/makePackageConfig.sh b/releaseScripts/default/makePackageConfig.sh new file mode 100755 index 00000000000..8d3ac0c8766 --- /dev/null +++ b/releaseScripts/default/makePackageConfig.sh @@ -0,0 +1,151 @@ +#!/bin/bash +#------------------------------------------------------------------------------- +# This script generates a package folder for an Ultimate tool that should be deployed. +# It takes additional binaries from the adds/ folder. Currently, we use z3, cvc4 and mathsat. +# It also adds README, Ultimate.py, and various license files. +#------------------------------------------------------------------------------- + +# Load shared functions and settings +DIR="${BASH_SOURCE%/*}" +if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi +source "${DIR}/makeSettings.sh" + +# Start the actual script +if [ "${#}" -le 2 ]; then + echo "Not enough arguments supplied -- use arguments in the following order" + echo "1. the toolname" + echo "2. 'linux' or 'win32' for the target platform" + echo "3. (optional) the reach toolchain (e.g., 'AutomizerC_WitnessPrinter.xml')" + echo "4. (optional) the termination toolchain or NONE" + echo "5. (optional) the witness validation toolchain or NONE" + echo "6. (optional) the memsafety deref and memtrack toolchain or NONE" + echo "7. (optional) the ltl toolchain or NONE" + echo "8. (optional) the termination witness validation toolchain or NONE" + exit 1 +fi + +TOOLNAME="${1}" +if [ -z "${TOOLNAME}" ]; then + echo "First argument (toolname) cannot be empty" + exit 1 +fi +LCTOOLNAME="$(echo "${TOOLNAME}" | tr '[A-Z]' '[a-z]')" +echo "Using ${TOOLNAME} (${LCTOOLNAME}) as toolname" + +# Additional files for all architectures +ADDS=( + "adds/LICENSE*" + "adds/z3-LICENSE" + "adds/cvc4-LICENSE" + "adds/mathsat-LICENSE" + "adds/ltl2ba-LICENSE" + "adds/Ultimate.py" + "adds/Ultimate.ini" + "adds/README" +) + +# Architecture-specific variables +if [ "${2}" == "linux" ]; then + echo "Packaging for linux..." + ARCH="linux" + ARCHPATH="products/CLI-E4/linux/gtk/x86_64" + ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba") +elif [ "${2}" == "win32" ]; then + echo "Packaging for win32..." + ARCH="win32" + ARCHPATH="products/CLI-E4/win32/win32/x86_64" + ADDS+=("adds/z3.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll" "adds/ltl2ba.exe") +else + echo "Wrong argument: ""${2}"" -- use 'linux' or 'win32'" + exit 1 +fi + +# Set version +VERSION="$(git rev-parse HEAD | cut -c1-8)" +echo "Version is ${VERSION}" + +TARGETDIR="U${TOOLNAME}-${ARCH}" +CONFIGDIR="${TARGETDIR}"/config +DATADIR="${TARGETDIR}"/data +SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" + +# Check all toolchain arguments +if [ -n "${3}" -a ! "NONE" = "${3}" ]; then + TOOLCHAIN=../../trunk/examples/toolchains/${3} +else + echo "No reach toolchain specified, ommitting..." + TOOLCHAIN= +fi + +if [ ! -z "${4}" -a ! "NONE" = "${4}" ]; then + TERMTOOLCHAIN=../../trunk/examples/toolchains/${4} +else + echo "No termination toolchain specified, ommitting..." + TERMTOOLCHAIN= +fi + +if [ ! -z "${5}" -a ! "NONE" = "${5}" ]; then + VALTOOLCHAIN=../../trunk/examples/toolchains/${5} +else + echo "No witness validation toolchain specified, ommitting..." + VALTOOLCHAIN= +fi + +if [ ! -z "${6}" -a ! "NONE" = "${6}" ]; then + MEMDEREFMEMTRACKTOOLCHAIN=../../trunk/examples/toolchains/${6} +else + echo "No memory deref toolchain specified, ommitting..." + MEMDEREFMEMTRACKTOOLCHAIN= +fi + +if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then + LTLTOOLCHAIN=../../trunk/examples/toolchains/${7} +else + echo "No LTL toolchain specified, ommitting..." + LTLTOOLCHAIN= +fi + +if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then + TERMVALTOOLCHAIN=../../trunk/examples/toolchains/${8} +else + echo "No termination witness validation toolchain specified, ommitting..." + TERMVALTOOLCHAIN= +fi + +# Removing files and dirs from previous deployments +if [ -d "${TARGETDIR}" ]; then + echo "Removing old ""${TARGETDIR}" + rm -r "${TARGETDIR}" +fi + +# Start copying files +echo "Copying files" +mkdir "${TARGETDIR}" +mkdir "${CONFIGDIR}" +mkdir "${DATADIR}" + +exit_on_fail cp -a ../../trunk/source/BA_SiteRepository/target/"${ARCHPATH}"/* "${TARGETDIR}/" +copy_if_non_empty "${TOOLCHAIN}" "${CONFIGDIR}/${TOOLNAME}Reach.xml" +copy_if_non_empty "${TERMTOOLCHAIN}" "${CONFIGDIR}/${TOOLNAME}Termination.xml" +copy_if_non_empty "${VALTOOLCHAIN}" "${CONFIGDIR}/${TOOLNAME}ReachWitnessValidation.xml" +copy_if_non_empty "${MEMDEREFMEMTRACKTOOLCHAIN}" "${CONFIGDIR}/${TOOLNAME}MemDerefMemtrack.xml" +copy_if_non_empty "${LTLTOOLCHAIN}" "${CONFIGDIR}/${TOOLNAME}LTL.xml" +copy_if_non_empty "${TERMVALTOOLCHAIN}" "${CONFIGDIR}/${TOOLNAME}TerminationWitnessValidation.xml" +exit_on_fail cp ${SETTINGS} "${CONFIGDIR}/." + +# Copy all adds to target dir +for add in "${ADDS[@]}" ; do + if ! readlink -fe ${add} > /dev/null ; then + echo "${add} does not exist, aborting..." + exit 1 + fi + exit_on_fail cp ${add} "${TARGETDIR}/" +done + +echo "Modifying Ultimate.py with version and toolname" +# Replacing version value in Ultimate.py +exit_on_fail sed -i "s/^version =.*$/version = \'${VERSION}\'/g" "${TARGETDIR}"/Ultimate.py +# Replacing toolname value in Ultimate.py +exit_on_fail sed -i "s/toolname =.*$/toolname = \'${TOOLNAME}\'/g" "${TARGETDIR}"/Ultimate.py +# Adjust permission to execute Ultimate.py +exit_on_fail chmod a+x "${TARGETDIR}"/Ultimate.py diff --git a/releaseScripts/default/makePackageReqCheck.sh b/releaseScripts/default/makePackageReqCheck.sh new file mode 100644 index 00000000000..936609a7da5 --- /dev/null +++ b/releaseScripts/default/makePackageReqCheck.sh @@ -0,0 +1,106 @@ +#!/bin/bash +#------------------------------------------------------------------------------- +# This script generates a package folder for the Ultimate ReqCheck product that should be deployed. +# It takes additional binaries from the adds/ folder. Currently, we use z3, cvc4 and mathsat. +# It also adds README, Ultimate.py, and various license files. +#------------------------------------------------------------------------------- + +# Load shared functions and settings +DIR="${BASH_SOURCE%/*}" +if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi +source "${DIR}/makeSettings.sh" + +# Start the actual script +if [ "${#}" -lt 4 ]; then + echo "Not enough arguments supplied -- use arguments in the following order" + echo "1. the toolname" + echo "2. 'linux' or 'win32' for the target platform" + echo "3. ReqCheck toolchain (e.g., 'ReqCheck.xml')" + echo "4. TestGen toolchain (e.g., 'ReqToTest.xml')" + exit 1 +fi + +TOOLNAME="${1}" +if [ -z "${TOOLNAME}" ]; then + echo "First argument (toolname) cannot be empty" + exit 1 +fi +LCTOOLNAME="$(echo ${TOOLNAME} | tr '[A-Z]' '[a-z]')" +echo "Using ${TOOLNAME} (${LCTOOLNAME}) as toolname" + +# Additional files for all architectures +ADDS=( + "adds/LICENSE*" + "adds/z3-LICENSE" + "adds/cvc4-LICENSE" + "adds/mathsat-LICENSE" + "adds/ltl2ba-LICENSE" + "adds/reqchecker/README" + "adds/reqchecker/run_complete_analysis.py" +) + +# Architecture-specific variables +if [ "${2}" == "linux" ]; then + echo "Packaging for linux..." + ARCH="linux" + ARCHPATH="products/CLI-E4/linux/gtk/x86_64" + ADDS+=("adds/z3" "adds/cvc4nyu" "adds/cvc4" "adds/mathsat") +elif [ "${2}" == "win32" ]; then + echo "Packaging for win32..." + ARCH="win32" + ARCHPATH="products/CLI-E4/win32/win32/x86_64" + ADDS+=("adds/z3.exe" "adds/cvc4nyu.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll") +else + echo "Wrong argument: ""${2}"" -- use 'linux' or 'win32'" + exit 1 +fi + +# Set version +VERSION="$(git rev-parse HEAD | cut -c1-8)" +echo "Version is ${VERSION}" + +TARGETDIR="U${TOOLNAME}-${ARCH}" +CONFIGDIR="${TARGETDIR}"/config +DATADIR="${TARGETDIR}"/data +SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" + +# Check toolchain argument +if [ ! -z "${3}" -a ! "NONE" = "${3}" ]; then + TOOLCHAIN=../../trunk/examples/toolchains/${3} +else + echo "No reach toolchain specified, ommitting..." + TOOLCHAIN= +fi + +if [ ! -z "${4}" -a ! "NONE" = "${4}" ]; then + TESTTOOLCHAIN=../../trunk/examples/toolchains/${4} +else + echo "No test toolchain specified, ommitting..." + TESTTOOLCHAIN= +fi + +# Removing files and dirs from previous deployments +if [ -d "${TARGETDIR}" ]; then + echo "Removing old ${TARGETDIR}" + rm -r "${TARGETDIR}" +fi + +# Start copying files +echo "Copying files" +mkdir "${TARGETDIR}" +mkdir "${CONFIGDIR}" +mkdir "${DATADIR}" + +exit_on_fail cp -a ../../trunk/source/BA_SiteRepository/target/"${ARCHPATH}"/* "${TARGETDIR}/" +copy_if_non_empty "${TOOLCHAIN}" "${CONFIGDIR}/ReqCheck.xml" +copy_if_non_empty "${TESTTOOLCHAIN}" "${CONFIGDIR}/ReqToTest.xml" +exit_on_fail cp ${SETTINGS} "${CONFIGDIR}"/. + +# Copy all adds to target dir +for add in "${ADDS[@]}" ; do + if ! readlink -fe ${add} > /dev/null ; then + echo "${add} does not exist, aborting..." + exit 1 + fi + exit_on_fail cp ${add} "${TARGETDIR}/" +done diff --git a/releaseScripts/default/makePackageSmall.sh b/releaseScripts/default/makePackageSmall.sh new file mode 100755 index 00000000000..7e272d45254 --- /dev/null +++ b/releaseScripts/default/makePackageSmall.sh @@ -0,0 +1,95 @@ +#!/bin/bash +#------------------------------------------------------------------------------- +# This script generates a package folder for an Ultimate product that should be deployed. +# It takes additional binaries from the adds/ folder. Currently, we use z3, cvc4 and mathsat. +# It also adds README, Ultimate.py, and various license files. +# It does not add toolchains or settings files, only the folder. +#------------------------------------------------------------------------------- + +# Load shared functions and settings +DIR="${BASH_SOURCE%/*}" +if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi +source "${DIR}/makeSettings.sh" + +# Start the actual script +if [ "${#}" -le 1 ]; then + echo "Not enough arguments supplied -- use arguments in the following order" + echo "1. the toolname" + echo "2. 'linux' or 'win32' for the target platform" + exit 1 +fi + +TOOLNAME="${1}" +if [ -z "${TOOLNAME}" ]; then + echo "First argument (toolname) cannot be empty" + exit 1 +fi +LCTOOLNAME="$(echo "${TOOLNAME}" | tr '[A-Z]' '[a-z]')" +echo "Using ${TOOLNAME} (${LCTOOLNAME}) as toolname" + +# Additional files for all architectures +ADDS=( + "adds/LICENSE*" + "adds/z3-LICENSE" + "adds/cvc4-LICENSE" + "adds/mathsat-LICENSE" + "adds/ltl2ba-LICENSE" + "adds/Ultimate.py" + "adds/Ultimate.ini" + "adds/README" +) + +# Architecture-specific variables +if [ "${2}" == "linux" ]; then + echo "Packaging for linux..." + ARCH="linux" + ARCHPATH="products/${TOOLNAME}/linux/gtk/x86_64" + ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba") +elif [ "${2}" == "win32" ]; then + echo "Packaging for win32..." + ARCH="win32" + ARCHPATH="products/${TOOLNAME}/win32/win32/x86_64" + ADDS+=("adds/z3.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll" "adds/ltl2ba.exe") +else + echo "Wrong argument: ""${2}"" -- use 'linux' or 'win32'" + exit 1 +fi + +# Set version +VERSION="$(git rev-parse HEAD | cut -c1-8)" +echo "Version is ${VERSION}" + +TARGETDIR="U${TOOLNAME}-${ARCH}" +CONFIGDIR="${TARGETDIR}"/config +DATADIR="${TARGETDIR}"/data + +# Removing files and dirs from previous deployments +if [ -d "${TARGETDIR}" ]; then + echo "Removing old ""${TARGETDIR}" + rm -r "${TARGETDIR}" +fi + +# Start copying files +echo "Copying files" +mkdir "${TARGETDIR}" +mkdir "${CONFIGDIR}" +mkdir "${DATADIR}" + +exit_on_fail cp -a ../../trunk/source/BA_SiteRepository/target/"${ARCHPATH}"/* "${TARGETDIR}/" + +# Copy all adds to target dir +for add in "${ADDS[@]}" ; do + if ! readlink -fe ${add} > /dev/null ; then + echo "${add} does not exist, aborting..." + exit 1 + fi + exit_on_fail cp ${add} "${TARGETDIR}/" +done + +echo "Modifying Ultimate.py with version and toolname" +# Replacing version value in Ultimate.py +exit_on_fail sed -i "s/^version =.*$/version = \'${VERSION}\'/g" "${TARGETDIR}"/Ultimate.py +# Replacing toolname value in Ultimate.py +exit_on_fail sed -i "s/toolname =.*$/toolname = \'${TOOLNAME}\'/g" "${TARGETDIR}"/Ultimate.py +# Adjust permission to execute Ultimate.py +exit_on_fail chmod a+x "${TARGETDIR}"/Ultimate.py diff --git a/releaseScripts/default/makeSettings.sh b/releaseScripts/default/makeSettings.sh index d27accf186f..f9a2578b31b 100755 --- a/releaseScripts/default/makeSettings.sh +++ b/releaseScripts/default/makeSettings.sh @@ -45,6 +45,42 @@ test_if_cmd_is_available() { fi } +test_cmd_version_greater_equal() { + local CMD_VERS_ACTUAL="${1}" + local CMD_VERS_EXPCTD="${2}" + local CMD_NAME="${3}" + + if [ "$(semver_compare ${CMD_VERS_ACTUAL} ${CMD_VERS_EXPCTD})" -eq -1 ]; then + printf '%s version %s is too old. ' "${CMD_NAME}" "${CMD_VERS_ACTUAL}" + printf 'Please install %s %s or newer.\n' "${CMD_NAME}" "${CMD_VERS_EXPCTD}" + exit 1 + fi +} + +get_cmd_version() { + ${@} | grep -m1 -Po "(\d+\.)+\d+" +} + +print_cmd_version() { + local CMD_VERS="${1}" + local CMD_NAME="${2}" + + printf '%s: %s\n' "${CMD_NAME}" "${CMD_VERS}" +} + +print_newline() { + printf '\n' +} + +print_heading() { + local HEADING_NAME="${1}" + local HEADING_LENGTH="${#HEADING_NAME}" + local HEADING_UNDERLINE="$(printf '━%.0s' $(seq 1 ${HEADING_LENGTH}))" + + printf '%s\n' "${HEADING_NAME}" + printf '%s\n' "${HEADING_UNDERLINE}" +} + spushd() { pushd "$1" > /dev/null || { echo "Could not change into $1" ; exit 1; } } diff --git a/releaseScripts/default/makeZip.sh b/releaseScripts/default/makeZip.sh index 30f194db952..db2b25090c7 100755 --- a/releaseScripts/default/makeZip.sh +++ b/releaseScripts/default/makeZip.sh @@ -1,166 +1,50 @@ #!/bin/bash -# This script generates a zip file for each Ultimate tool that should be deployed to GitHub or to some place else -# It takes additional binaries from the adds/ folder. Currently, we use z3, cvc4 and mathsat. -# It also adds README, Ultimate.py, and various license files +#------------------------------------------------------------------------------- +# This script generates a ZIP archive for an Ultimate product that should be deployed. +#------------------------------------------------------------------------------- - - -## include the makeSettings shared functions +# Load shared functions and settings DIR="${BASH_SOURCE%/*}" -if [[ ! -d "$DIR" ]]; then DIR="$PWD"; fi -. "$DIR/makeSettings.sh" +if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi +source "${DIR}/makeSettings.sh" - -## start the actual script -if [ $# -le 2 ]; then +# Start the actual script +if [ "${#}" -le 1 ]; then echo "Not enough arguments supplied -- use arguments in the following order" - echo "1. the toolname" + echo "1. the toolname" echo "2. 'linux' or 'win32' for the target platform" - echo "3. (optional) the reach toolchain (e.g., 'AutomizerC_WitnessPrinter.xml')" - echo "4. (optional) the termination toolchain or NONE" - echo "5. (optional) the witness validation toolchain or NONE" - echo "6. (optional) the memsafety deref and memtrack toolchain or NONE" - echo "7. (optional) the ltl toolchain or NONE" - echo "8. (optional) the termination witness validation toolchain or NONE" exit 1 fi -TOOLNAME="$1" -if [ -z "$TOOLNAME" ]; then +TOOLNAME="${1}" +if [ -z "${TOOLNAME}" ]; then echo "First argument (toolname) cannot be empty" exit 1 fi -LCTOOLNAME="$(echo "$TOOLNAME" | tr '[A-Z]' '[a-z]')" -echo "Using $TOOLNAME ($LCTOOLNAME) as toolname" - +LCTOOLNAME="$(echo "${TOOLNAME}" | tr '[A-Z]' '[a-z]')" +echo "Using ${TOOLNAME} (${LCTOOLNAME}) as toolname" -# additional files for all architectures -ADDS=( - "adds/LICENSE*" - "adds/z3-LICENSE" - "adds/cvc4-LICENSE" - "adds/mathsat-LICENSE" - "adds/ltl2ba-LICENSE" - "adds/Ultimate.py" - "adds/Ultimate.ini" - "adds/README" -) - -# architecture-specific variables -if [ "$2" == "linux" ]; then +# Architecture-specific variables +if [ "${2}" == "linux" ]; then echo "Building .zip for linux..." ARCH="linux" - ARCHPATH="products/CLI-E4/linux/gtk/x86_64" - ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba") -elif [ "$2" == "win32" ]; then +elif [ "${2}" == "win32" ]; then echo "Building .zip for win32..." ARCH="win32" - ARCHPATH="products/CLI-E4/win32/win32/x86_64" - ADDS+=("adds/z3.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll" "adds/ltl2ba.exe") else - echo "Wrong argument: ""$2"" -- use 'linux' or 'win32'" + echo "Wrong argument: ""${2}"" -- use 'linux' or 'win32'" exit 1 fi +TARGETDIR="U${TOOLNAME}-${ARCH}" +ZIPFILE="Ultimate${TOOLNAME}-${ARCH}.zip" -# set version -VERSION=$(git rev-parse HEAD | cut -c1-8) -echo "Version is $VERSION" - - -TARGETDIR=U${TOOLNAME}-${ARCH} -CONFIGDIR="$TARGETDIR"/config -DATADIR="$TARGETDIR"/data -ZIPFILE=Ultimate${TOOLNAME}-${ARCH}.zip -SETTINGS=../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}* - -# check all toolchain arguments -if [ -n "$3" -a ! "NONE" = "$3" ]; then - TOOLCHAIN=../../trunk/examples/toolchains/${3} -else - echo "No reach toolchain specified, ommitting..." - TOOLCHAIN= -fi - -if [ ! -z "$4" -a ! "NONE" = "$4" ]; then - TERMTOOLCHAIN=../../trunk/examples/toolchains/${4} -else - echo "No termination toolchain specified, ommitting..." - TERMTOOLCHAIN= -fi - -if [ ! -z "$5" -a ! "NONE" = "$5" ]; then - VALTOOLCHAIN=../../trunk/examples/toolchains/${5} -else - echo "No witness validation toolchain specified, ommitting..." - VALTOOLCHAIN= -fi - -if [ ! -z "$6" -a ! "NONE" = "$6" ]; then - MEMDEREFMEMTRACKTOOLCHAIN=../../trunk/examples/toolchains/${6} -else - echo "No memory deref toolchain specified, ommitting..." - MEMDEREFMEMTRACKTOOLCHAIN= -fi - -if [ ! -z "$7" -a ! "NONE" = "$7" ]; then - LTLTOOLCHAIN=../../trunk/examples/toolchains/${7} -else - echo "No LTL toolchain specified, ommitting..." - LTLTOOLCHAIN= -fi - -if [ ! -z "$8" -a ! "NONE" = "$8" ]; then - TERMVALTOOLCHAIN=../../trunk/examples/toolchains/${8} -else - echo "No termination witness validation toolchain specified, ommitting..." - TERMVALTOOLCHAIN= -fi - - -## removing files and dirs from previous deployments -if [ -d "$TARGETDIR" ]; then - echo "Removing old ""$TARGETDIR" - rm -r "$TARGETDIR" -fi +# Removing files and dirs from previous deployments if [ -f "${ZIPFILE}" ]; then - echo "Removing old .zip file ""${ZIPFILE}" + echo "Removing old ${ZIPFILE} file" rm "${ZIPFILE}" fi -## start copying files -echo "Copying files" -mkdir "$TARGETDIR" -mkdir "$CONFIGDIR" -mkdir "$DATADIR" - -exit_on_fail cp -a ../../trunk/source/BA_SiteRepository/target/${ARCHPATH}/* "$TARGETDIR"/ -copy_if_non_empty "$TOOLCHAIN" "$CONFIGDIR"/"$TOOLNAME"Reach.xml -copy_if_non_empty "$TERMTOOLCHAIN" "$CONFIGDIR"/"$TOOLNAME"Termination.xml -copy_if_non_empty "$VALTOOLCHAIN" "$CONFIGDIR"/"$TOOLNAME"ReachWitnessValidation.xml -copy_if_non_empty "$MEMDEREFMEMTRACKTOOLCHAIN" "$CONFIGDIR"/"$TOOLNAME"MemDerefMemtrack.xml -copy_if_non_empty "$LTLTOOLCHAIN" "$CONFIGDIR"/"$TOOLNAME"LTL.xml -copy_if_non_empty "$TERMVALTOOLCHAIN" "$CONFIGDIR"/"$TOOLNAME"TerminationWitnessValidation.xml -exit_on_fail cp ${SETTINGS} "$CONFIGDIR"/. - -## copy all adds to target dir -for add in "${ADDS[@]}" ; do - if ! readlink -fe $add > /dev/null ; then - echo "$add does not exist, aborting..." - exit 1 - fi - exit_on_fail cp $add "$TARGETDIR"/ -done - - -echo "Modifying Ultimate.py with version and toolname" -## replacing version value in Ultimate.py -exit_on_fail sed "s/^version =.*$/version = \'$VERSION\'/g" "$TARGETDIR"/Ultimate.py > "$TARGETDIR"/Ultimate.py.tmp && mv "$TARGETDIR"/Ultimate.py.tmp "$TARGETDIR"/Ultimate.py && chmod a+x "$TARGETDIR"/Ultimate.py - -## replacing toolname value in Ultimate.py -exit_on_fail sed "s/toolname =.*/toolname = \'$TOOLNAME\'/g" "$TARGETDIR"/Ultimate.py > "$TARGETDIR"/Ultimate.py.tmp && mv "$TARGETDIR"/Ultimate.py.tmp "$TARGETDIR"/Ultimate.py && chmod a+x "$TARGETDIR"/Ultimate.py - -## creating new zipfile -echo "Creating .zip" -exit_on_fail zip -q "${ZIPFILE}" -r "$TARGETDIR"/* - +# Creating ZIP archive +echo "Creating ${ZIPFILE} archive" +exit_on_fail zip -q "${ZIPFILE}" -r "${TARGETDIR}"/* diff --git a/releaseScripts/default/semver2.sh b/releaseScripts/default/semver2.sh new file mode 100755 index 00000000000..2463d4d8966 --- /dev/null +++ b/releaseScripts/default/semver2.sh @@ -0,0 +1,354 @@ +#!/bin/sh + +# POSIX SH portable semver 2.0 comparison tool. + +# This bash script compares pre-releases alphabetically as well (number < lowerCaseLetter < upperCaseLetter) +# +# returns 1 when A greater than B +# returns 0 when A equals B +# returns -1 when A lower than B +# +# Usage +# chmod +x semver2.sh +# ./semver2.sh 1.0.0-rc.0.a+metadata v1.0.0-rc.0+metadata +# --> 1 +# + +# This software was built with the help of the following sources: +# https://stackoverflow.com/a/58067270 +# https://www.unix.com/man-page/posix/1posix/cut/ +# https://stackoverflow.com/questions/51052475/how-to-iterate-over-the-characters-of-a-string-in-a-posix-shell-script + +set -eu + +debug() { + if [ "$debug" = "debug" ]; then printf "DEBUG: %s$1 \n"; fi +} + +# params char +# returns Integer +ord() { + printf '%d' "'$1" +} + + +isNumber() { + string=$1 + char="" + while true; do + substract="${string#?}" # All but the first character of the string + char="${string%"$substract"}" # Remove $rest, and you're left with the first character + string="$substract" + # no more chars to compare then success + if [ -z "$char" ]; then + printf "true" + return 1 + fi + # break if some of the chars is not a number + if [ "$(ord "$char")" -lt 48 ] || [ "$(ord "$char")" -gt 57 ]; then + printf "false" + return 0 + fi + done +} + +# params string {String}, Index {Number} +# returns char +getChar() { + string=$1 + index=$2 + cursor=-1 + char="" + while [ "$cursor" != "$index" ]; do + substract="${string#?}" # All but the first character of the string + char="${string%"$substract"}" # Remove $rest, and you're left with the first character + string="$substract" + cursor=$((cursor + 1)) + done + printf "%s$char" +} + +outcome() { + result=$1 + printf "%s$result\n" +} + + +compareNumber() { + if [ -z "$1" ] && [ -z "$2" ]; then + printf "%s" "0" + return + fi + + [ $(($2 - $1)) -gt 0 ] && printf "%s" "-1" + [ $(($2 - $1)) -lt 0 ] && printf "1" + [ $(($2 - $1)) = 0 ] && printf "0" +} + +compareString() { + result=false + index=0 + while true + do + a=$(getChar "$1" $index) + b=$(getChar "$2" $index) + + if [ -z "$a" ] && [ -z "$b" ] + then + printf "0" + return + fi + + ord_a=$(ord "$a") + ord_b=$(ord "$b") + + if [ "$(compareNumber "$ord_a" "$ord_b")" != "0" ]; then + printf "%s" "$(compareNumber "$ord_a" "$ord_b")" + return + fi + + index=$((index + 1)) + done +} + +includesString() { + string="$1" + substring="$2" + if [ "${string#*"$substring"}" != "$string" ] + then + printf "1" + return 1 # $substring is in $string + fi + printf "0" + return 0 # $substring is not in $string +} + +removeLeadingV() { + printf "%s${1#v}" +} + +# https://github.com/Ariel-Rodriguez/sh-semversion-2/pull/2 +# Spec #2 https://semver.org/#spec-item-2 +# MUST NOT contain leading zeroes +normalizeZero() { + next=$(printf %s "${1#0}") + if [ -z "$next" ]; then + printf %s "$1" + fi + printf %s "$next" +} + +semver_compare() { + firstParam=$1 #1.2.4-alpha.beta+METADATA + secondParam=$2 #1.2.4-alpha.beta.2+METADATA + debug=${3:-1} + verbose=${4:-1} + + [ "$verbose" = "verbose" ] && set -x + + version_a=$(printf %s "$firstParam" | cut -d'+' -f 1) + version_a=$(removeLeadingV "$version_a") + version_b=$(printf %s "$secondParam" | cut -d'+' -f 1) + version_b=$(removeLeadingV "$version_b") + + a_major=$(printf %s "$version_a" | cut -d'.' -f 1) + a_minor=$(printf %s "$version_a" | cut -d'.' -f 2) + a_patch=$(printf %s "$version_a" | cut -d'.' -f 3 | cut -d'-' -f 1) + a_pre="" + if [ "$(includesString "$version_a" -)" = 1 ]; then + a_pre=$(printf %s"${version_a#"$a_major.$a_minor.$a_patch-"}") + fi + + b_major=$(printf %s "$version_b" | cut -d'.' -f 1) + b_minor=$(printf %s "$version_b" | cut -d'.' -f 2) + b_patch=$(printf %s "$version_b" | cut -d'.' -f 3 | cut -d'-' -f 1) + b_pre="" + if [ "$(includesString "$version_b" -)" = 1 ]; then + b_pre=$(printf %s"${version_b#"$b_major.$b_minor.$b_patch-"}") + fi + + a_major=$(normalizeZero "$a_major") + a_minor=$(normalizeZero "$a_minor") + a_patch=$(normalizeZero "$a_patch") + b_major=$(normalizeZero "$b_major") + b_minor=$(normalizeZero "$b_minor") + b_patch=$(normalizeZero "$b_patch") + + unit_types="MAJOR MINOR PATCH" + a_normalized="$a_major $a_minor $a_patch" + b_normalized="$b_major $b_minor $b_patch" + + debug "Detected: $a_major $a_minor $a_patch identifiers: $a_pre" + debug "Detected: $b_major $b_minor $b_patch identifiers: $b_pre" + + ##### + # + # Find difference between Major Minor or Patch + # + + cursor=1 + while [ "$cursor" -lt 4 ] + do + a=$(printf %s "$a_normalized" | cut -d' ' -f $cursor) + b=$(printf %s "$b_normalized" | cut -d' ' -f $cursor) + if [ "$a" != "$b" ] + then + debug "$(printf %s "$unit_types" | cut -d' ' -f $cursor) is different" + outcome "$(compareNumber "$a" "$b")" + return + fi; + debug "$(printf "%s" "$unit_types" | cut -d' ' -f $cursor) are equal" + cursor=$((cursor + 1)) + done + + ##### + # + # Find difference between pre release identifiers + # + + if [ -z "$a_pre" ] && [ -z "$b_pre" ]; then + debug "Because both are equals" + outcome "0" + return + fi + + # Spec 11.3 a pre-release version has lower precedence than a normal version: + # 1.0.0 < 1.0.0-alpha + if [ -z "$a_pre" ]; then + debug "Because A is the stable release. Pre-release version has lower precedence than a released version" + outcome "1" + return + fi + # 1.0.0-alpha < 1.0.0 + if [ -z "$b_pre" ]; then + debug "Because B is the stable release. Pre-release version has lower precedence than a released version" + outcome "-1" + return + fi + + + isSingleIdentifier() { + substract="${2#?}" + if [ "${1%"$2"}" = "" ]; then + printf "true" + return 1; + fi + return 0 + } + + cursor=1 + while [ $cursor -lt 5 ] + do + a=$(printf %s "$a_pre" | cut -d'.' -f $cursor) + b=$(printf %s "$b_pre" | cut -d'.' -f $cursor) + + debug "Comparing identifier $a with $b" + + # Exit when there is nothing else to compare. + # Most likely because they are equals + if [ -z "$a" ] && [ -z "$b" ] + then + debug "are equals" + outcome "0" + return + fi; + + # Spec #11 https://semver.org/#spec-item-11 + # Precedence for two pre-release versions with the same major, minor, and patch version + # MUST be determined by comparing each dot separated identifier from left to right until a difference is found + + # Spec 11.4.4: A larger set of pre-release fields has a higher precedence than a smaller set, if all of the preceding identifiers are equal. + + if [ -n "$a" ] && [ -z "$b" ]; then + # When A is larger than B and preidentifiers are 1+n + # 1.0.0-alpha.beta.1 1.0.0-alpha.beta + # 1.0.0-alpha.beta.1.2 1.0.0-alpha.beta.1 + debug "Because A has larger set of pre-identifiers" + outcome "1" + return + fi + + # When A is shorter than B and preidentifiers are 1+n + # 1.0.0-alpha.beta 1.0.0-alpha.beta.d + # 1.0.0-alpha.beta 1.0.0-alpha.beta.1.2 + if [ -z "$a" ] && [ -n "$b" ]; then + debug "Because B has larger set of pre-identifiers" + outcome "-1" + return + fi + + # Spec #11.4.1 + # Identifiers consisting of only digits are compared numerically. + if [ "$(isNumber "$a")" = "true" ] || [ "$(isNumber "$b")" = "true" ]; then + + # if both identifiers are numbers, then compare and proceed + # 1.0.0-beta.3 1.0.0-beta.2 + if [ "$(isNumber "$a")" = "true" ] && [ "$(isNumber "$b")" = "true" ]; then + if [ "$(compareNumber "$a" "$b")" != "0" ]; then + debug "Number is not equal $(compareNumber "$a" "$b")" + outcome "$(compareNumber "$a" "$b")" + return + fi + fi + + # Spec 11.4.3 + # 1.0.0-alpha.1 1.0.0-alpha.beta.d + # 1.0.0-beta.3 1.0.0-1.2 + if [ "$(isNumber "$a")" = "false" ]; then + debug "Because Numeric identifiers always have lower precedence than non-numeric identifiers." + outcome "1" + return + fi + # 1.0.0-alpha.d 1.0.0-alpha.beta.1 + # 1.0.0-1.1 1.0.0-beta.1.2 + if [ "$(isNumber "$b")" = "false" ]; then + debug "Because Numeric identifiers always have lower precedence than non-numeric identifiers." + outcome "-1" + return + fi + else + # Spec 11.4.2 + # Identifiers with letters or hyphens are compared lexically in ASCII sort order. + # 1.0.0-alpha 1.0.0-beta.alpha + if [ "$(compareString "$a" "$b")" != "0" ]; then + debug "cardinal is not equal $(compareString a b)" + outcome "$(compareString "$a" "$b")" + return + fi + fi + + # Edge case when there is single identifier exaple: x.y.z-beta + if [ "$cursor" = 1 ]; then + + # When both versions are single return equals + # 1.0.0-alpha 1.0.0-alpha + if [ -n "$(isSingleIdentifier "$b_pre" "$b")" ] && [ -n "$(isSingleIdentifier "$a_pre" "$a")" ]; then + debug "Because both have single identifier" + outcome "0" + return + fi + + # Return greater when has more identifiers + # Spec 11.4.4: A larger set of pre-release fields has a higher precedence than a smaller set, if all of the preceding identifiers are equal. + + # When A is larger than B + # 1.0.0-alpha.beta 1.0.0-alpha + if [ -n "$(isSingleIdentifier "$b_pre" "$b")" ] && [ -z "$(isSingleIdentifier "$a_pre" "$a")" ]; then + debug "Because of single identifier, A has more pre-identifiers" + outcome "1" + return + fi + + # When A is shorter than B + # 1.0.0-alpha 1.0.0-alpha.beta + if [ -z "$(isSingleIdentifier "$b_pre" "$b")" ] && [ -n "$(isSingleIdentifier "$a_pre" "$a")" ]; then + debug "Because of single identifier, B has more pre-identifiers" + outcome "-1" + return + fi + fi + + # Proceed to the next identifier because previous comparition was equal. + cursor=$((cursor + 1)) + done +} From 464acfccdca6f1f497c531ecb8e33a959520c940 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Sun, 17 Aug 2025 18:00:41 +0200 Subject: [PATCH 14/38] Build and package Ultimate Eliminator as product --- .gitignore | 2 ++ releaseScripts/default/makeBuild.sh | 4 ++++ releaseScripts/default/makeFresh.sh | 4 ++++ .../{UltimateEliminator.product => Eliminator.product} | 2 +- trunk/source/BA_SiteRepository/pom.xml | 2 +- trunk/source/CoreRCP/plugin.xml | 4 ++-- 6 files changed, 14 insertions(+), 4 deletions(-) rename trunk/source/BA_SiteRepository/{UltimateEliminator.product => Eliminator.product} (93%) diff --git a/.gitignore b/.gitignore index 996a8c204fe..4bf8894d855 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,8 @@ hs_err_pid* /releaseScripts/default/UDeltaDebugger-win32/* /releaseScripts/default/UAutomizer-linux/* /releaseScripts/default/UAutomizer-win32/* +/releaseScripts/default/UEliminator-linux/* +/releaseScripts/default/UEliminator-win32/* /releaseScripts/default/UGemCutter-linux/* /releaseScripts/default/UGemCutter-win32/* /releaseScripts/default/UKojak-linux/* diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh index 1908833cdbe..e1d708fd979 100755 --- a/releaseScripts/default/makeBuild.sh +++ b/releaseScripts/default/makeBuild.sh @@ -81,6 +81,10 @@ package() { exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "${platform}" print_newline + print_heading "Package Ultimate Eliminator [${platform}]" + exit_on_fail bash makePackageSmall.sh "Eliminator" "${platform}" + print_newline + print_heading "Package Ultimate WebBackend [${platform}]" exit_on_fail bash makePackageSmall.sh "WebBackend" "${platform}" print_newline diff --git a/releaseScripts/default/makeFresh.sh b/releaseScripts/default/makeFresh.sh index 345d110a796..c76f2692156 100755 --- a/releaseScripts/default/makeFresh.sh +++ b/releaseScripts/default/makeFresh.sh @@ -40,6 +40,10 @@ archive() { exit_on_fail bash makeZip.sh "DeltaDebugger" "${platform}" print_newline + print_heading "Archive Ultimate Eliminator [${platform}]" + exit_on_fail bash makeZip.sh "Eliminator" "${platform}" + print_newline + print_heading "Archive Ultimate WebBackend [${platform}]" exit_on_fail bash makeZip.sh "WebBackend" "${platform}" print_newline diff --git a/trunk/source/BA_SiteRepository/UltimateEliminator.product b/trunk/source/BA_SiteRepository/Eliminator.product similarity index 93% rename from trunk/source/BA_SiteRepository/UltimateEliminator.product rename to trunk/source/BA_SiteRepository/Eliminator.product index 65a1b12a2b4..6904d9ae423 100644 --- a/trunk/source/BA_SiteRepository/UltimateEliminator.product +++ b/trunk/source/BA_SiteRepository/Eliminator.product @@ -1,7 +1,7 @@ - + diff --git a/trunk/source/BA_SiteRepository/pom.xml b/trunk/source/BA_SiteRepository/pom.xml index b809b9ff2d2..4c366b8291b 100644 --- a/trunk/source/BA_SiteRepository/pom.xml +++ b/trunk/source/BA_SiteRepository/pom.xml @@ -54,7 +54,7 @@ UltimateDeltaDebugger - UltimateEliminator + Eliminator UltimateEliminator diff --git a/trunk/source/CoreRCP/plugin.xml b/trunk/source/CoreRCP/plugin.xml index 275f9589b65..338ca1971bf 100644 --- a/trunk/source/CoreRCP/plugin.xml +++ b/trunk/source/CoreRCP/plugin.xml @@ -37,8 +37,8 @@ - - + + From 367f70ec4dfd5ad00a2e0d523c727bb2f96b30dc Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Sun, 17 Aug 2025 22:14:43 +0200 Subject: [PATCH 15/38] Build and package Ultimate CLI and Debug-UI --- .gitignore | 4 ++++ releaseScripts/default/makeBuild.sh | 8 ++++++++ releaseScripts/default/makeFresh.sh | 8 ++++++++ 3 files changed, 20 insertions(+) diff --git a/.gitignore b/.gitignore index 4bf8894d855..be1b4e39517 100644 --- a/.gitignore +++ b/.gitignore @@ -12,6 +12,10 @@ hs_err_pid* /packaging/docker/*.env +/releaseScripts/default/UCLI-E4-linux/* +/releaseScripts/default/UCLI-E4-win32/* +/releaseScripts/default/UDebug-E4-linux/* +/releaseScripts/default/UDebug-E4-win32/* /releaseScripts/default/UDeltaDebugger-linux/* /releaseScripts/default/UDeltaDebugger-win32/* /releaseScripts/default/UAutomizer-linux/* diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh index e1d708fd979..57da92d1957 100755 --- a/releaseScripts/default/makeBuild.sh +++ b/releaseScripts/default/makeBuild.sh @@ -77,6 +77,14 @@ package() { print_newline # makePackageSmall.sh + print_heading "Package Ultimate Command Line [${platform}]" + exit_on_fail bash makePackageSmall.sh "CLI-E4" "${platform}" + print_newline + + print_heading "Package Ultimate Debug UI [${platform}]" + exit_on_fail bash makePackageSmall.sh "Debug-E4" "${platform}" + print_newline + print_heading "Package Ultimate DeltaDebugger [${platform}]" exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "${platform}" print_newline diff --git a/releaseScripts/default/makeFresh.sh b/releaseScripts/default/makeFresh.sh index c76f2692156..67b74075a53 100755 --- a/releaseScripts/default/makeFresh.sh +++ b/releaseScripts/default/makeFresh.sh @@ -51,6 +51,14 @@ archive() { print_heading "Archive Ultimate ReqCheck [${platform}]" exit_on_fail bash makeZip.sh "ReqCheck" "${platform}" print_newline + + print_heading "Archive Ultimate Command Line [${platform}]" + exit_on_fail bash makeZip.sh "CLI-E4" "${platform}" + print_newline + + print_heading "Archive Ultimate Debug UI [${platform}]" + exit_on_fail bash makePackageSmall.sh "Debug-E4" "${platform}" + print_newline done } From 71a12db84ca5513a14daab0c1f2acbcd7da233a9 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Sun, 17 Aug 2025 23:19:59 +0200 Subject: [PATCH 16/38] Use build script to create Docker images with product-specific config --- packaging/docker/Dockerfile | 210 ++++++++++++++++++++++++++++-------- packaging/docker/README.md | 21 +++- packaging/docker/welcome.sh | 14 +++ 3 files changed, 194 insertions(+), 51 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 3f835c19837..e21c73b5d32 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -1,40 +1,39 @@ #------------------------------------------------------------------------------ -# Dockerfile: compile and package Ultimate toolchains +# Dockerfile: compile and package Ultimate products #------------------------------------------------------------------------------ # Author: Manuel Bentele # Copyright (c) 2023 #------------------------------------------------------------------------------ # common build arguments for multi-staged Docker build #------------------------------------------------------------------------------ -ARG REPO_MAVEN_ROOT="trunk/source/BA_MavenParentUltimate" -ARG REPO_FRONTEND_ROOT="trunk/source/WebsiteStatic" -ARG REPO_DIR_BUILD="trunk/source/BA_SiteRepository/target/products" +ARG REPO_DIR_FRONTEND="trunk/source/WebsiteStatic" +ARG REPO_DIR_BUILD="releaseScripts/default" ARG REPO_DIR_TOOLS="releaseScripts/default/adds" ARG DIR_BUILD="/home/build" ARG DIR_ULTIMATE="${DIR_BUILD}/ultimate" -ARG DIR_OUTPUT="${DIR_ULTIMATE}/${REPO_DIR_BUILD}" -ARG DIR_OUTPUT_FRONTEND="${DIR_ULTIMATE}/${REPO_FRONTEND_ROOT}" +ARG DIR_OUTPUT_BUILD="${DIR_ULTIMATE}/${REPO_DIR_BUILD}" +ARG DIR_OUTPUT_FRONTEND="${DIR_ULTIMATE}/${REPO_DIR_FRONTEND}" ARG DIR_TOOLS="${DIR_ULTIMATE}/${REPO_DIR_TOOLS}" ARG USER_NAME="ultimate" ARG USER_GROUP="ultimate" ARG USER_HOME="/home/${USER_NAME}" #------------------------------------------------------------------------------ -# 1st build stage: compile and materialize Ultimate +# 1st build stage: compile and build Ultimate products #------------------------------------------------------------------------------ -FROM alpine:3 AS build +FROM alpine:3 AS build-products ARG REPO_URL="https://github.com/ultimate-pa/ultimate.git" ARG REPO_BRANCH="dev" -ARG REPO_MAVEN_ROOT ARG REPO_DIR_BUILD ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD # install build dependencies for an entire Ultimate build -RUN apk add --no-cache "git" \ +RUN apk add --no-cache "bash" \ + "git" \ "maven" \ "openjdk21" @@ -44,20 +43,20 @@ RUN mkdir -p "${DIR_BUILD}" && \ # build all Ultimate products WORKDIR "${DIR_ULTIMATE}" -RUN mvn -f "${REPO_MAVEN_ROOT}" clean package -P materialize +RUN cd "${DIR_OUTPUT_BUILD}" && bash makeBuild.sh #------------------------------------------------------------------------------ # 2nd build stage: compile and build the Ultimate web interface #------------------------------------------------------------------------------ -FROM build AS build-webfrontend +FROM build-products AS build-webfrontend ARG ULTIMATE_FRONTEND_BASEURL="/website" -ARG REPO_FRONTEND_ROOT +ARG REPO_DIR_FRONTEND ARG REPO_DIR_BUILD ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD # install build dependencies for building the Ultimate web frontend RUN apk add --no-cache "gcc" \ @@ -71,8 +70,8 @@ RUN apk add --no-cache "gcc" \ "ruby-dev" # build the Ultimate web frontend -WORKDIR "${REPO_FRONTEND_ROOT}" -ENV PATH="${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64:${PATH}" +WORKDIR "${REPO_DIR_FRONTEND}" +ENV PATH="${DIR_OUTPUT_BUILD}/CLI-E4/linux/gtk/x86_64:${PATH}" RUN python3 scripts/build.py --baseurl "${ULTIMATE_FRONTEND_BASEURL}" #------------------------------------------------------------------------------ @@ -84,7 +83,7 @@ ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD ARG DIR_TOOLS ARG USER_NAME ARG USER_GROUP @@ -102,11 +101,8 @@ RUN mkdir -p "${USER_HOME}" && \ chown -R "${USER_NAME}:${USER_GROUP}" "${USER_HOME}" WORKDIR "${USER_HOME}" -# install alread compiled tools for all Ultimate products -COPY --from=build "${DIR_TOOLS}/cvc4" "/usr/bin/cvc4" -COPY --from=build "${DIR_TOOLS}/ltl2ba" "/usr/bin/ltl2ba" -COPY --from=build "${DIR_TOOLS}/mathsat" "/usr/bin/mathsat" -COPY --from=build "${DIR_TOOLS}/z3" "/usr/bin/z3" +# make Ultimate executable, scripts, and solvers available +ENV PATH="${USER_HOME}:${PATH}" # add Welcome script to print Ultimate version ADD "welcome.sh" "/etc/profile.d/welcome.sh" @@ -192,15 +188,14 @@ ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD ARG DIR_TOOLS ARG USER_NAME ARG USER_GROUP ARG USER_HOME # install already built Ultimate CLI product -COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/CLI-E4/linux/gtk/x86_64" "${USER_HOME}" -RUN ln -s "${USER_HOME}/Ultimate" "/usr/bin/Ultimate" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UCLI-E4-linux" "${USER_HOME}" # run the Ultimate CLI product as non-root user USER "${USER_NAME}" @@ -217,7 +212,7 @@ ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD ARG DIR_TOOLS ARG USER_NAME ARG USER_GROUP @@ -231,8 +226,7 @@ RUN apk add --no-cache "openjdk21-jre" \ "xauth" # install already built Ultimate Debug UI product -COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/Debug-E4/linux/gtk/x86_64" "${USER_HOME}" -RUN ln -s "${USER_HOME}/UltimateDebug" "/usr/bin/UltimateDebug" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UDebug-E4-linux" "${USER_HOME}" # run the Ultimate Debug UI product as non-root user USER "${USER_NAME}" @@ -241,25 +235,25 @@ USER "${USER_NAME}" ENTRYPOINT ["/bin/sh", "-l"] #------------------------------------------------------------------------------ -# 3rd build stage: package Ultimate ReqAnalyzer +# 3rd build stage: package Ultimate Automizer #------------------------------------------------------------------------------ -FROM ultimate-common AS ultimate-reqanalyzer +FROM ultimate-common AS ultimate-automizer ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD ARG DIR_TOOLS ARG USER_NAME ARG USER_GROUP ARG USER_HOME -# install already built Ultimate ReqAnalyzer product -COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/ReqAnalyzer/linux/gtk/x86_64" "${USER_HOME}" -RUN ln -s "${USER_HOME}/ReqAnalyzer" "/usr/bin/ReqAnalyzer" +# install already built Ultimate Automizer product +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UAutomizer-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/Automizer" -# run the Ultimate ReqAnalyzer product as non-root user +# run the Ultimate Automizer product as non-root user USER "${USER_NAME}" # default entry point to print installed Ultimate version @@ -274,15 +268,15 @@ ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD ARG DIR_TOOLS ARG USER_NAME ARG USER_GROUP ARG USER_HOME # install already built Ultimate DeltaDebugger product -COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/DeltaDebugger/linux/gtk/x86_64" "${USER_HOME}" -RUN ln -s "${USER_HOME}/Ultimate" "/usr/bin/Ultimate" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UDeltaDebugger-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/DeltaDebugger" # default entry point to print installed Ultimate version ENTRYPOINT ["/bin/sh", "-l"] @@ -296,15 +290,15 @@ ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD ARG DIR_TOOLS ARG USER_NAME ARG USER_GROUP ARG USER_HOME # install already built Ultimate Eliminator product -COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/UltimateEliminator/linux/gtk/x86_64" "${USER_HOME}" -RUN ln -s "${USER_HOME}/Ultimate" "/usr/bin/Ultimate" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UEliminator-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/Eliminator" # run the Ultimate Eliminator product as non-root user USER "${USER_NAME}" @@ -312,6 +306,131 @@ USER "${USER_NAME}" # default entry point to print installed Ultimate version ENTRYPOINT ["/bin/sh", "-l"] +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate GemCutter +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-gemcutter + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_BUILD +ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME + +# install already built Ultimate GemCutter product +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UGemCutter-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/GemCutter" + +# run the Ultimate GemCutter product as non-root user +USER "${USER_NAME}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] + +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate Kojak +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-kojak + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_BUILD +ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME + +# install already built Ultimate Kojak product +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UKojak-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/Kojak" + +# run the Ultimate Kojak product as non-root user +USER "${USER_NAME}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] + +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate Referee +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-referee + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_BUILD +ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME + +# install already built Ultimate Referee product +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UReferee-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/Referee" + +# run the Ultimate Referee product as non-root user +USER "${USER_NAME}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] + +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate ReqAnalyzer +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-reqanalyzer + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_BUILD +ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME + +# install already built Ultimate ReqAnalyzer product +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UReqCheck-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/ReqAnalyzer" + +# run the Ultimate ReqAnalyzer product as non-root user +USER "${USER_NAME}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] + +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate Taipan +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-taipan + +ARG REPO_DIR_BUILD +ARG REPO_DIR_TOOLS +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_BUILD +ARG DIR_TOOLS +ARG USER_NAME +ARG USER_GROUP +ARG USER_HOME + +# install already built Ultimate Taipan product +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UTaipan-linux" "${USER_HOME}" +RUN ln -s "${USER_HOME}/Ultimate" "${USER_HOME}/Taipan" + +# run the Ultimate Taipan product as non-root user +USER "${USER_NAME}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] + #------------------------------------------------------------------------------ # 3rd build stage: package Ultimate WebBackend #------------------------------------------------------------------------------ @@ -321,7 +440,7 @@ ARG REPO_DIR_BUILD ARG REPO_DIR_TOOLS ARG DIR_BUILD ARG DIR_ULTIMATE -ARG DIR_OUTPUT +ARG DIR_OUTPUT_BUILD ARG DIR_TOOLS ARG USER_NAME ARG USER_GROUP @@ -352,14 +471,13 @@ RUN apk add --no-cache "wget" \ apk del --no-cache "wget" # install already built Ultimate WebBackend product -COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_OUTPUT}/WebBackend/linux/gtk/x86_64" "${USER_HOME}" -RUN ln -s "${USER_HOME}/WebBackend" "/usr/bin/WebBackend" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_OUTPUT_BUILD}/UWebBackend-linux" "${USER_HOME}" # run the Ultimate WebBackend product as non-root user USER "${USER_NAME}" # add configuration files and templates for 'dockerize' and Ultimate -COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build "${DIR_WEBSITE_CONFIG}/backend/settings_whitelist.json" "${USER_HOME}/settings_whitelist.json" +COPY --chown="${USER_NAME}:${USER_GROUP}" --from=build-products "${DIR_WEBSITE_CONFIG}/backend/settings_whitelist.json" "${USER_HOME}/settings_whitelist.json" ADD "web.config.properties.tpl" "${USER_HOME}/web.config.properties.tpl" ADD "WebBackend.ini.tpl" "${USER_HOME}/WebBackend.ini.tpl" RUN rm -f "${USER_HOME}/WebBackend.ini" diff --git a/packaging/docker/README.md b/packaging/docker/README.md index e9a5e416929..3f6578ccc36 100644 --- a/packaging/docker/README.md +++ b/packaging/docker/README.md @@ -7,16 +7,24 @@ An Ultimate `PRODUCT` can be built with the following Docker call docker build -t --target . ``` -where `PRODUCT` is a placeholder for one of the products +where `PRODUCT` is a placeholder for one of the pre-configured products - - `ultimate-cli` - - `ultimate-debug` - - `ultimate-reqanalyzer` + - `ultimate-automizer` - `ultimate-deltadebugger` - `ultimate-eliminator` + - `ultimate-gemcutter` + - `ultimate-kojak` + - `ultimate-referee` + - `ultimate-reqanalyzer` + - `ultimate-taipan` - `ultimate-webbackend` - `ultimate-webfrontend` +or one of the basic products without any configuration (e.g., for your own Docker images or for debugging and development) + + - `ultimate-cli` + - `ultimate-debug` + shipped with the Ultimate program analysis framework. For validating the built Ultimate `PRODUCT` image, you can create and run a Docker container based on this image with the following Docker call. @@ -33,7 +41,10 @@ If you want to run Ultimate interactively for any verification input, you can sp docker run -it /bin/bash -tc -s -i ``` -Calling the Ultimate `PRODUCT` within the container then follows as usual, where a `TOOLCHAIN`, `SETTINGS`, and `PROGRAM` file path should be specified for a verification run. +Calling the Ultimate `PRODUCT` within the container then follows as usual, where a `TOOLCHAIN`, `SETTINGS`, and `PROGRAM` file should be specified for a verification run. +The pre-configured products are already provided with the appropriate tool-specific configuration files (toolchain and setting files). +You can access the configuration directory within a Docker container via the environment variable `ULTIMATE\_CONFIG\_PATH`. + An exception is a start of the graphical Ultimate Debug UI. To do this, a graphic connection to the host system must be established via the X11 protocol, which can be done with the following Docker call. ```shell diff --git a/packaging/docker/welcome.sh b/packaging/docker/welcome.sh index 21d6f3541dc..335342867dd 100755 --- a/packaging/docker/welcome.sh +++ b/packaging/docker/welcome.sh @@ -1,5 +1,7 @@ #!/bin/sh +ULTIMATE_CONFIG_PATH="config" + check_and_print_version() { for cmd in "${@}"; do if command -v "${cmd}" >/dev/null 2>&1; then @@ -9,6 +11,16 @@ check_and_print_version() { done } +check_and_print_config() { + if [ -d "${ULTIMATE_CONFIG_PATH}" ] && [ "$(ls -A "${ULTIMATE_CONFIG_PATH}")" ]; then + export ULTIMATE_CONFIG_PATH="${ULTIMATE_CONFIG_PATH}" + echo "Product-specific toolchain and setting files for Ultimate are available at: ${PWD}/${ULTIMATE_CONFIG_PATH}" + echo "You can access the configuration directory via the environment variable 'ULTIMATE_CONFIG_PATH'." + else + echo "Product-specific toolchain and setting files for Ultimate are not part of this installation." + fi +} + echo "▗▖ ▗▖▗▖ ▗▄▄▄▖▗▄▄▄▖▗▖ ▗▖ ▗▄▖▗▄▄▄▖▗▄▄▄▖" echo "▐▌ ▐▌▐▌ █ █ ▐▛▚▞▜▌▐▌ ▐▌ █ ▐▌ " echo "▐▌ ▐▌▐▌ █ █ ▐▌ ▐▌▐▛▀▜▌ █ ▐▛▀▀▘" @@ -18,3 +30,5 @@ echo "┃ Program Analysis Framework ┃" echo "┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛" check_and_print_version "Ultimate" "UltimateDebug" "ReqAnalyzer" "WebBackend" echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━" +check_and_print_config +echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━" From e3bfd2a90f102c95e79d1fd04b840d30c37f379a Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Mon, 18 Aug 2025 11:51:42 +0200 Subject: [PATCH 17/38] Indicate archive step after build with separate heading --- releaseScripts/default/makeBuild.sh | 16 ++++++++-------- releaseScripts/default/makeFresh.sh | 16 ++++++++++++++-- 2 files changed, 22 insertions(+), 10 deletions(-) diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh index 57da92d1957..1da57adf99d 100755 --- a/releaseScripts/default/makeBuild.sh +++ b/releaseScripts/default/makeBuild.sh @@ -11,7 +11,7 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" source "${DIR}/semver2.sh" -start() { +build_init() { printf '▗▄▄▖ ▗▖ ▗▖▗▄▄▄▖▗▖ ▗▄▄▄ \n' printf '▐▌ ▐▌▐▌ ▐▌ █ ▐▌ ▐▌ █\n' printf '▐▛▀▚▖▐▌ ▐▌ █ ▐▌ ▐▌ █\n' @@ -22,7 +22,7 @@ start() { print_newline } -check() { +build_check() { # Check if build tools are installed test_if_cmd_is_available mvn test_if_cmd_is_available java @@ -37,7 +37,7 @@ check() { test_cmd_version_greater_equal "${VERS_JDK}" "21.0" "Java Development Kit" } -build() { +build_run() { spushd "../../trunk/source/BA_MavenParentUltimate/" print_heading "Using the build tools" @@ -53,7 +53,7 @@ build() { spopd } -package() { +build_package() { for platform in {linux,win32}; do # makePackageConfig.sh print_heading "Package Ultimate Taipan [${platform}]" @@ -104,7 +104,7 @@ package() { done } -start -check -build -package +build_init +build_check +build_run +build_package diff --git a/releaseScripts/default/makeFresh.sh b/releaseScripts/default/makeFresh.sh index 67b74075a53..a657cd7cc86 100755 --- a/releaseScripts/default/makeFresh.sh +++ b/releaseScripts/default/makeFresh.sh @@ -13,7 +13,18 @@ source "${DIR}/makeSettings.sh" # Load and execute all Ultimate build steps before archive function is called. source "${DIR}/makeBuild.sh" -archive() { +archive_init() { + printf ' ▗▄▖ ▗▄▄▖ ▗▄▄▖▗▖ ▗▖▗▄▄▄▖▗▖ ▗▖▗▄▄▄▖\n' + printf '▐▌ ▐▌▐▌ ▐▌▐▌ ▐▌ ▐▌ █ ▐▌ ▐▌▐▌ \n' + printf '▐▛▀▜▌▐▛▀▚▖▐▌ ▐▛▀▜▌ █ ▐▌ ▐▌▐▛▀▀▘\n' + printf '▐▌ ▐▌▐▌ ▐▌▝▚▄▄▖▐▌ ▐▌▗▄█▄▖ ▝▚▞▘ ▐▙▄▄▖\n' + printf '┏━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓\n' + printf '┃ Ultimate Products ┃\n' + printf '┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛\n' + print_newline +} + +archive_run() { for platform in {linux,win32}; do # makeZip.sh print_heading "Archive Ultimate Taipan [${platform}]" @@ -62,4 +73,5 @@ archive() { done } -archive +archive_init +archive_run From abc7f78e0e159b465388300b615ade7132fc03eb Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Mon, 18 Aug 2025 22:55:53 +0200 Subject: [PATCH 18/38] Add parameter to build script to restrict platforms --- packaging/docker/Dockerfile | 2 +- releaseScripts/default/makeBuild.sh | 97 ++++++++++++++++++++++------- releaseScripts/default/makeFresh.sh | 46 +++++++------- 3 files changed, 98 insertions(+), 47 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index e21c73b5d32..5ce0ca32928 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -43,7 +43,7 @@ RUN mkdir -p "${DIR_BUILD}" && \ # build all Ultimate products WORKDIR "${DIR_ULTIMATE}" -RUN cd "${DIR_OUTPUT_BUILD}" && bash makeBuild.sh +RUN cd "${DIR_OUTPUT_BUILD}" && bash makeBuild.sh -p linux #------------------------------------------------------------------------------ # 2nd build stage: compile and build the Ultimate web interface diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh index 1da57adf99d..551d68a16d3 100755 --- a/releaseScripts/default/makeBuild.sh +++ b/releaseScripts/default/makeBuild.sh @@ -11,6 +11,56 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" source "${DIR}/semver2.sh" +# Default platforms for the build of Ultimate +PLATFORMS=("linux" "win32") + +build_printhelp() { + printf 'Usage: %s [-o all|linux|win32]\n' "${0}" + print_newline + printf 'Options:\n' + printf ' -p Specify platforms to build for:\n' + printf ' all build for Linux and Windows [default]\n' + printf ' linux build only for Linux\n' + printf ' win32 build only for Windows\n' + printf ' -h Show this help message\n' +} + +build_parseopts() { + while getopts "p:h" OPT; do + case "${OPT}" in + p) + case "${OPTARG}" in + all) + # Use all platforms by default + ;; + linux) + PLATFORMS=("linux") + ;; + windows) + PLATFORMS=("win32") + ;; + *) + printf '%s: invalid option for -p -- %s\n' "${0}" "${OPTARG}" + print_newline + build_printhelp + exit 1 + ;; + esac + ;; + h) + print_newline + build_printhelp + exit 1 + ;; + *) + print_newline + build_printhelp + exit 1 + ;; + esac + done +} + build_init() { printf '▗▄▄▖ ▗▖ ▗▖▗▄▄▄▖▗▖ ▗▄▄▄ \n' printf '▐▌ ▐▌▐▌ ▐▌ █ ▐▌ ▐▌ █\n' @@ -54,56 +104,57 @@ build_run() { } build_package() { - for platform in {linux,win32}; do + for PLATFORM in "${PLATFORMS[@]}"; do # makePackageConfig.sh - print_heading "Package Ultimate Taipan [${platform}]" - exit_on_fail bash makePackageConfig.sh "Taipan" "${platform}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + print_heading "Package Ultimate Taipan [${PLATFORM}]" + exit_on_fail bash makePackageConfig.sh "Taipan" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" print_newline - print_heading "Package Ultimate Automizer [${platform}]" - exit_on_fail bash makePackageConfig.sh "Automizer" "${platform}" "AutomizerCInline_WitnessPrinter.xml" "BuchiAutomizerCInline_WitnessPrinter.xml" "AutomizerCInline_IcfgBuilder.xml" "AutomizerCInline_WitnessPrinter.xml" "LTLAutomizerC.xml" "BuchiAutomizerCInline.xml" + print_heading "Package Ultimate Automizer [${PLATFORM}]" + exit_on_fail bash makePackageConfig.sh "Automizer" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "BuchiAutomizerCInline_WitnessPrinter.xml" "AutomizerCInline_IcfgBuilder.xml" "AutomizerCInline_WitnessPrinter.xml" "LTLAutomizerC.xml" "BuchiAutomizerCInline.xml" print_newline - print_heading "Package Ultimate Kojak [${platform}]" - exit_on_fail bash makePackageConfig.sh "Kojak" "${platform}" "KojakC_WitnessPrinter.xml" "NONE" "NONE" "KojakC_WitnessPrinter.xml" "NONE" "NONE" + print_heading "Package Ultimate Kojak [${PLATFORM}]" + exit_on_fail bash makePackageConfig.sh "Kojak" "${PLATFORM}" "KojakC_WitnessPrinter.xml" "NONE" "NONE" "KojakC_WitnessPrinter.xml" "NONE" "NONE" print_newline - print_heading "Package Ultimate GemCutter [${platform}]" - exit_on_fail bash makePackageConfig.sh "GemCutter" "${platform}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + print_heading "Package Ultimate GemCutter [${PLATFORM}]" + exit_on_fail bash makePackageConfig.sh "GemCutter" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" print_newline - print_heading "Package Ultimate Referee [${platform}]" - exit_on_fail bash makePackageConfig.sh "Referee" "${platform}" "RefereeCInline.xml" "NONE" "RefereeCInline_IcfgBuilder.xml" "NONE" "NONE" "NONE" + print_heading "Package Ultimate Referee [${PLATFORM}]" + exit_on_fail bash makePackageConfig.sh "Referee" "${PLATFORM}" "RefereeCInline.xml" "NONE" "RefereeCInline_IcfgBuilder.xml" "NONE" "NONE" "NONE" print_newline # makePackageSmall.sh - print_heading "Package Ultimate Command Line [${platform}]" - exit_on_fail bash makePackageSmall.sh "CLI-E4" "${platform}" + print_heading "Package Ultimate Command Line [${PLATFORM}]" + exit_on_fail bash makePackageSmall.sh "CLI-E4" "${PLATFORM}" print_newline - print_heading "Package Ultimate Debug UI [${platform}]" - exit_on_fail bash makePackageSmall.sh "Debug-E4" "${platform}" + print_heading "Package Ultimate Debug UI [${PLATFORM}]" + exit_on_fail bash makePackageSmall.sh "Debug-E4" "${PLATFORM}" print_newline - print_heading "Package Ultimate DeltaDebugger [${platform}]" - exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "${platform}" + print_heading "Package Ultimate DeltaDebugger [${PLATFORM}]" + exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "${PLATFORM}" print_newline - print_heading "Package Ultimate Eliminator [${platform}]" - exit_on_fail bash makePackageSmall.sh "Eliminator" "${platform}" + print_heading "Package Ultimate Eliminator [${PLATFORM}]" + exit_on_fail bash makePackageSmall.sh "Eliminator" "${PLATFORM}" print_newline - print_heading "Package Ultimate WebBackend [${platform}]" - exit_on_fail bash makePackageSmall.sh "WebBackend" "${platform}" + print_heading "Package Ultimate WebBackend [${PLATFORM}]" + exit_on_fail bash makePackageSmall.sh "WebBackend" "${PLATFORM}" print_newline # makePackageReqCheck.sh - print_heading "Package Ultimate ReqCheck [${platform}]" - exit_on_fail bash makePackageReqCheck.sh "ReqCheck" "${platform}" "ReqCheck.xml" "ReqCheck.xml" + print_heading "Package Ultimate ReqCheck [${PLATFORM}]" + exit_on_fail bash makePackageReqCheck.sh "ReqCheck" "${PLATFORM}" "ReqCheck.xml" "ReqCheck.xml" print_newline done } +build_parseopts "${@}" build_init build_check build_run diff --git a/releaseScripts/default/makeFresh.sh b/releaseScripts/default/makeFresh.sh index a657cd7cc86..93d93b76793 100755 --- a/releaseScripts/default/makeFresh.sh +++ b/releaseScripts/default/makeFresh.sh @@ -25,50 +25,50 @@ archive_init() { } archive_run() { - for platform in {linux,win32}; do + for PLATFORM in "${PLATFORMS[@]}"; do # makeZip.sh - print_heading "Archive Ultimate Taipan [${platform}]" - exit_on_fail bash makeZip.sh "Taipan" "${platform}" + print_heading "Archive Ultimate Taipan [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Taipan" "${PLATFORM}" print_newline - print_heading "Archive Ultimate Automizer [${platform}]" - exit_on_fail bash makeZip.sh "Automizer" "${platform}" + print_heading "Archive Ultimate Automizer [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Automizer" "${PLATFORM}" print_newline - print_heading "Archive Ultimate Kojak [${platform}]" - exit_on_fail bash makeZip.sh "Kojak" "${platform}" + print_heading "Archive Ultimate Kojak [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Kojak" "${PLATFORM}" print_newline - print_heading "Archive Ultimate GemCutter [${platform}]" - exit_on_fail bash makeZip.sh "GemCutter" "${platform}" + print_heading "Archive Ultimate GemCutter [${PLATFORM}]" + exit_on_fail bash makeZip.sh "GemCutter" "${PLATFORM}" print_newline - print_heading "Archive Ultimate Referee [${platform}]" - exit_on_fail bash makeZip.sh "Referee" "${platform}" + print_heading "Archive Ultimate Referee [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Referee" "${PLATFORM}" print_newline - print_heading "Archive Ultimate DeltaDebugger [${platform}]" - exit_on_fail bash makeZip.sh "DeltaDebugger" "${platform}" + print_heading "Archive Ultimate DeltaDebugger [${PLATFORM}]" + exit_on_fail bash makeZip.sh "DeltaDebugger" "${PLATFORM}" print_newline - print_heading "Archive Ultimate Eliminator [${platform}]" - exit_on_fail bash makeZip.sh "Eliminator" "${platform}" + print_heading "Archive Ultimate Eliminator [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Eliminator" "${PLATFORM}" print_newline - print_heading "Archive Ultimate WebBackend [${platform}]" - exit_on_fail bash makeZip.sh "WebBackend" "${platform}" + print_heading "Archive Ultimate WebBackend [${PLATFORM}]" + exit_on_fail bash makeZip.sh "WebBackend" "${PLATFORM}" print_newline - print_heading "Archive Ultimate ReqCheck [${platform}]" - exit_on_fail bash makeZip.sh "ReqCheck" "${platform}" + print_heading "Archive Ultimate ReqCheck [${PLATFORM}]" + exit_on_fail bash makeZip.sh "ReqCheck" "${PLATFORM}" print_newline - print_heading "Archive Ultimate Command Line [${platform}]" - exit_on_fail bash makeZip.sh "CLI-E4" "${platform}" + print_heading "Archive Ultimate Command Line [${PLATFORM}]" + exit_on_fail bash makeZip.sh "CLI-E4" "${PLATFORM}" print_newline - print_heading "Archive Ultimate Debug UI [${platform}]" - exit_on_fail bash makePackageSmall.sh "Debug-E4" "${platform}" + print_heading "Archive Ultimate Debug UI [${PLATFORM}]" + exit_on_fail bash makePackageSmall.sh "Debug-E4" "${PLATFORM}" print_newline done } From 00c1d8914e970b6054444e5e12a62b47e3d684cb Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 19 Aug 2025 00:17:05 +0200 Subject: [PATCH 19/38] Add notes and restrictions to Docker packaging README --- packaging/docker/README.md | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/packaging/docker/README.md b/packaging/docker/README.md index 3f6578ccc36..ffe8ad70c44 100644 --- a/packaging/docker/README.md +++ b/packaging/docker/README.md @@ -1,10 +1,11 @@ -# Package Ultimate for Docker +# Docker Packaging and Deployment of Ultimate Products ## Build Ultimate Docker images + An Ultimate `PRODUCT` can be built with the following Docker call ```shell -docker build -t --target . +docker build --platform linux/amd64 --tag --target . ``` where `PRODUCT` is a placeholder for one of the pre-configured products @@ -27,6 +28,10 @@ or one of the basic products without any configuration (e.g., for your own Docke shipped with the Ultimate program analysis framework. +> [!NOTE] +> Building the Ultimate product images is currently limited to the Docker target platform `linux/amd64` (Linux containers for the 64-bit x86 architecture). +> However, these images can still be used on a Windows system with [Docker Desktop](https://docs.docker.com/desktop/setup/install/windows-install/) configured with the WSL2 or Hyper-V backend in order to create and run Linux containers on a Windows system. + For validating the built Ultimate `PRODUCT` image, you can create and run a Docker container based on this image with the following Docker call. ```shell docker run -it @@ -42,8 +47,10 @@ docker run -it /bin/bash -tc -s -i ``` Calling the Ultimate `PRODUCT` within the container then follows as usual, where a `TOOLCHAIN`, `SETTINGS`, and `PROGRAM` file should be specified for a verification run. -The pre-configured products are already provided with the appropriate tool-specific configuration files (toolchain and setting files). -You can access the configuration directory within a Docker container via the environment variable `ULTIMATE\_CONFIG\_PATH`. + +> [!NOTE] +> The pre-configured products are already provided with the appropriate configuration (toolchain and setting files). +> You can access the configuration directory within a Docker container via the environment variable `ULTIMATE_CONFIG_PATH`. An exception is a start of the graphical Ultimate Debug UI. To do this, a graphic connection to the host system must be established via the X11 protocol, which can be done with the following Docker call. From 2cd3962e6b027f630450fb1c33ae08a2b6581ba9 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 19 Aug 2025 21:51:19 +0200 Subject: [PATCH 20/38] Fix Docker run command for Ultimate images --- packaging/docker/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packaging/docker/README.md b/packaging/docker/README.md index ffe8ad70c44..ba6670b9d3c 100644 --- a/packaging/docker/README.md +++ b/packaging/docker/README.md @@ -43,7 +43,7 @@ As an expected result, you should then receive the Ultimate version output from If you want to run Ultimate interactively for any verification input, you can spwan a bash in a created and started Ultimate `PRODUCT` container as follows. ```shell -docker run -it /bin/bash +docker run -it -tc -s -i ``` Calling the Ultimate `PRODUCT` within the container then follows as usual, where a `TOOLCHAIN`, `SETTINGS`, and `PROGRAM` file should be specified for a verification run. From 244a448c4acff4be1615bc42b962a27fe815e943 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Tue, 19 Aug 2025 23:19:29 +0200 Subject: [PATCH 21/38] Replace Perl Regex with Extended Regex to support non-GNU grep --- releaseScripts/default/makeSettings.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/releaseScripts/default/makeSettings.sh b/releaseScripts/default/makeSettings.sh index f9a2578b31b..5630b580a22 100755 --- a/releaseScripts/default/makeSettings.sh +++ b/releaseScripts/default/makeSettings.sh @@ -58,7 +58,7 @@ test_cmd_version_greater_equal() { } get_cmd_version() { - ${@} | grep -m1 -Po "(\d+\.)+\d+" + ${@} | grep -m1 -Eo "([[:digit:]]+\.)+[[:digit:]]+" } print_cmd_version() { From e0aae9979f50e9595ae9313105aeb38d10d2c424 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 00:12:18 +0200 Subject: [PATCH 22/38] Replace GNU readlink in build scripts --- releaseScripts/default/makePackageConfig.sh | 10 ++++------ releaseScripts/default/makePackageReqCheck.sh | 10 ++++------ releaseScripts/default/makePackageSmall.sh | 10 ++++------ 3 files changed, 12 insertions(+), 18 deletions(-) diff --git a/releaseScripts/default/makePackageConfig.sh b/releaseScripts/default/makePackageConfig.sh index 8d3ac0c8766..90226517f66 100755 --- a/releaseScripts/default/makePackageConfig.sh +++ b/releaseScripts/default/makePackageConfig.sh @@ -34,7 +34,9 @@ echo "Using ${TOOLNAME} (${LCTOOLNAME}) as toolname" # Additional files for all architectures ADDS=( - "adds/LICENSE*" + "adds/LICENSE" + "adds/LICENSE.GPL" + "adds/LICENSE.GPL.LESSER" "adds/z3-LICENSE" "adds/cvc4-LICENSE" "adds/mathsat-LICENSE" @@ -135,11 +137,7 @@ exit_on_fail cp ${SETTINGS} "${CONFIGDIR}/." # Copy all adds to target dir for add in "${ADDS[@]}" ; do - if ! readlink -fe ${add} > /dev/null ; then - echo "${add} does not exist, aborting..." - exit 1 - fi - exit_on_fail cp ${add} "${TARGETDIR}/" + exit_on_fail cp "${add}" "${TARGETDIR}/" done echo "Modifying Ultimate.py with version and toolname" diff --git a/releaseScripts/default/makePackageReqCheck.sh b/releaseScripts/default/makePackageReqCheck.sh index 936609a7da5..6da48e01352 100644 --- a/releaseScripts/default/makePackageReqCheck.sh +++ b/releaseScripts/default/makePackageReqCheck.sh @@ -30,7 +30,9 @@ echo "Using ${TOOLNAME} (${LCTOOLNAME}) as toolname" # Additional files for all architectures ADDS=( - "adds/LICENSE*" + "adds/LICENSE" + "adds/LICENSE.GPL" + "adds/LICENSE.GPL.LESSER" "adds/z3-LICENSE" "adds/cvc4-LICENSE" "adds/mathsat-LICENSE" @@ -98,9 +100,5 @@ exit_on_fail cp ${SETTINGS} "${CONFIGDIR}"/. # Copy all adds to target dir for add in "${ADDS[@]}" ; do - if ! readlink -fe ${add} > /dev/null ; then - echo "${add} does not exist, aborting..." - exit 1 - fi - exit_on_fail cp ${add} "${TARGETDIR}/" + exit_on_fail cp "${add}" "${TARGETDIR}/" done diff --git a/releaseScripts/default/makePackageSmall.sh b/releaseScripts/default/makePackageSmall.sh index 7e272d45254..08a6b111061 100755 --- a/releaseScripts/default/makePackageSmall.sh +++ b/releaseScripts/default/makePackageSmall.sh @@ -29,7 +29,9 @@ echo "Using ${TOOLNAME} (${LCTOOLNAME}) as toolname" # Additional files for all architectures ADDS=( - "adds/LICENSE*" + "adds/LICENSE" + "adds/LICENSE.GPL" + "adds/LICENSE.GPL.LESSER" "adds/z3-LICENSE" "adds/cvc4-LICENSE" "adds/mathsat-LICENSE" @@ -79,11 +81,7 @@ exit_on_fail cp -a ../../trunk/source/BA_SiteRepository/target/"${ARCHPATH}"/* " # Copy all adds to target dir for add in "${ADDS[@]}" ; do - if ! readlink -fe ${add} > /dev/null ; then - echo "${add} does not exist, aborting..." - exit 1 - fi - exit_on_fail cp ${add} "${TARGETDIR}/" + exit_on_fail cp "${add}" "${TARGETDIR}/" done echo "Modifying Ultimate.py with version and toolname" From c1c43ece65c8e66ded8f26122542745263916fdf Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 00:42:25 +0200 Subject: [PATCH 23/38] Fix quoting in build scripts --- releaseScripts/default/makePackageConfig.sh | 24 +++++++++---------- releaseScripts/default/makePackageReqCheck.sh | 6 ++--- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/releaseScripts/default/makePackageConfig.sh b/releaseScripts/default/makePackageConfig.sh index 90226517f66..807c16bb5c3 100755 --- a/releaseScripts/default/makePackageConfig.sh +++ b/releaseScripts/default/makePackageConfig.sh @@ -73,45 +73,45 @@ SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" # Check all toolchain arguments if [ -n "${3}" -a ! "NONE" = "${3}" ]; then - TOOLCHAIN=../../trunk/examples/toolchains/${3} + TOOLCHAIN="../../trunk/examples/toolchains/${3}" else echo "No reach toolchain specified, ommitting..." - TOOLCHAIN= + TOOLCHAIN="" fi if [ ! -z "${4}" -a ! "NONE" = "${4}" ]; then - TERMTOOLCHAIN=../../trunk/examples/toolchains/${4} + TERMTOOLCHAIN="../../trunk/examples/toolchains/${4}" else echo "No termination toolchain specified, ommitting..." - TERMTOOLCHAIN= + TERMTOOLCHAIN="" fi if [ ! -z "${5}" -a ! "NONE" = "${5}" ]; then - VALTOOLCHAIN=../../trunk/examples/toolchains/${5} + VALTOOLCHAIN="../../trunk/examples/toolchains/${5}" else echo "No witness validation toolchain specified, ommitting..." - VALTOOLCHAIN= + VALTOOLCHAIN="" fi if [ ! -z "${6}" -a ! "NONE" = "${6}" ]; then - MEMDEREFMEMTRACKTOOLCHAIN=../../trunk/examples/toolchains/${6} + MEMDEREFMEMTRACKTOOLCHAIN="../../trunk/examples/toolchains/${6}" else echo "No memory deref toolchain specified, ommitting..." - MEMDEREFMEMTRACKTOOLCHAIN= + MEMDEREFMEMTRACKTOOLCHAIN="" fi if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then - LTLTOOLCHAIN=../../trunk/examples/toolchains/${7} + LTLTOOLCHAIN="../../trunk/examples/toolchains/${7}" else echo "No LTL toolchain specified, ommitting..." - LTLTOOLCHAIN= + LTLTOOLCHAIN="" fi if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then - TERMVALTOOLCHAIN=../../trunk/examples/toolchains/${8} + TERMVALTOOLCHAIN="../../trunk/examples/toolchains/${8}" else echo "No termination witness validation toolchain specified, ommitting..." - TERMVALTOOLCHAIN= + TERMVALTOOLCHAIN="" fi # Removing files and dirs from previous deployments diff --git a/releaseScripts/default/makePackageReqCheck.sh b/releaseScripts/default/makePackageReqCheck.sh index 6da48e01352..edfa537e26f 100644 --- a/releaseScripts/default/makePackageReqCheck.sh +++ b/releaseScripts/default/makePackageReqCheck.sh @@ -68,17 +68,17 @@ SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" # Check toolchain argument if [ ! -z "${3}" -a ! "NONE" = "${3}" ]; then - TOOLCHAIN=../../trunk/examples/toolchains/${3} + TOOLCHAIN="../../trunk/examples/toolchains/${3}" else echo "No reach toolchain specified, ommitting..." TOOLCHAIN= fi if [ ! -z "${4}" -a ! "NONE" = "${4}" ]; then - TESTTOOLCHAIN=../../trunk/examples/toolchains/${4} + TESTTOOLCHAIN="../../trunk/examples/toolchains/${4}" else echo "No test toolchain specified, ommitting..." - TESTTOOLCHAIN= + TESTTOOLCHAIN="" fi # Removing files and dirs from previous deployments From 27e6a0f84c4ad22cca0a2c881c7a81f4c0b29aff Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 01:02:46 +0200 Subject: [PATCH 24/38] Fix invalid path to Ultimate product in Dockerfile --- packaging/docker/Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 5ce0ca32928..ac52aecf956 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -71,7 +71,7 @@ RUN apk add --no-cache "gcc" \ # build the Ultimate web frontend WORKDIR "${REPO_DIR_FRONTEND}" -ENV PATH="${DIR_OUTPUT_BUILD}/CLI-E4/linux/gtk/x86_64:${PATH}" +ENV PATH="${DIR_OUTPUT_BUILD}/UCLI-E4-linux:${PATH}" RUN python3 scripts/build.py --baseurl "${ULTIMATE_FRONTEND_BASEURL}" #------------------------------------------------------------------------------ From 99fc96adf12e3615736ff06e72600379009c57d9 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 02:01:30 +0200 Subject: [PATCH 25/38] Enable colorized promt in Docker container --- packaging/docker/Dockerfile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index ac52aecf956..b9341872af8 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -104,6 +104,9 @@ WORKDIR "${USER_HOME}" # make Ultimate executable, scripts, and solvers available ENV PATH="${USER_HOME}:${PATH}" +# enable colorized prompt +RUN ln -s /etc/profile.d/color_prompt.sh.disabled /etc/profile.d/color_prompt.sh + # add Welcome script to print Ultimate version ADD "welcome.sh" "/etc/profile.d/welcome.sh" From a4565e532381472841ecf1dc94aa57f494d42f99 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 02:02:33 +0200 Subject: [PATCH 26/38] Make Ultimate executable, scripts, and solvers in Docker image available --- packaging/docker/Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index b9341872af8..f5c826e715f 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -102,7 +102,7 @@ RUN mkdir -p "${USER_HOME}" && \ WORKDIR "${USER_HOME}" # make Ultimate executable, scripts, and solvers available -ENV PATH="${USER_HOME}:${PATH}" +RUN echo "export PATH=\"${USER_HOME}:${PATH}\"" > /etc/profile.d/ultimate_path.sh # enable colorized prompt RUN ln -s /etc/profile.d/color_prompt.sh.disabled /etc/profile.d/color_prompt.sh From 8f7271fdd96ed823078785ea0152aaf31a776c3b Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 02:03:17 +0200 Subject: [PATCH 27/38] Adjust Ultimate configuration path variable in Docker container --- packaging/docker/welcome.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/packaging/docker/welcome.sh b/packaging/docker/welcome.sh index 335342867dd..3bb187ef2f4 100755 --- a/packaging/docker/welcome.sh +++ b/packaging/docker/welcome.sh @@ -1,6 +1,6 @@ #!/bin/sh -ULTIMATE_CONFIG_PATH="config" +ULTIMATE_CONFIG_PATH="/home/ultimate/config" check_and_print_version() { for cmd in "${@}"; do @@ -14,7 +14,7 @@ check_and_print_version() { check_and_print_config() { if [ -d "${ULTIMATE_CONFIG_PATH}" ] && [ "$(ls -A "${ULTIMATE_CONFIG_PATH}")" ]; then export ULTIMATE_CONFIG_PATH="${ULTIMATE_CONFIG_PATH}" - echo "Product-specific toolchain and setting files for Ultimate are available at: ${PWD}/${ULTIMATE_CONFIG_PATH}" + echo "Product-specific toolchain and setting files for Ultimate are available at: ${ULTIMATE_CONFIG_PATH}" echo "You can access the configuration directory via the environment variable 'ULTIMATE_CONFIG_PATH'." else echo "Product-specific toolchain and setting files for Ultimate are not part of this installation." From 82216522021dfa772c26fc6aa206fe7608c509a8 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 16:20:55 +0200 Subject: [PATCH 28/38] Make maximum heap and stack size configurable for Ultimate products --- releaseScripts/default/adds/Ultimate.ini | 9 --- releaseScripts/default/makeBuild.sh | 76 +++++++++++++------ releaseScripts/default/makePackageConfig.sh | 61 +++++++-------- releaseScripts/default/makePackageReqCheck.sh | 28 ++++--- releaseScripts/default/makePackageSmall.sh | 23 +++--- releaseScripts/default/makeSettings.sh | 45 +++++++++++ 6 files changed, 155 insertions(+), 87 deletions(-) delete mode 100644 releaseScripts/default/adds/Ultimate.ini diff --git a/releaseScripts/default/adds/Ultimate.ini b/releaseScripts/default/adds/Ultimate.ini deleted file mode 100644 index adcf0ff3b0d..00000000000 --- a/releaseScripts/default/adds/Ultimate.ini +++ /dev/null @@ -1,9 +0,0 @@ ---launcher.suppressErrors --nosplash --consoleLog ---console --data -@user.home/.ultimate --vmargs --Xmx12G --Xms512M diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh index 551d68a16d3..c086f1c866f 100755 --- a/releaseScripts/default/makeBuild.sh +++ b/releaseScripts/default/makeBuild.sh @@ -13,21 +13,48 @@ source "${DIR}/semver2.sh" # Default platforms for the build of Ultimate PLATFORMS=("linux" "win32") +# Default maximum heap memory size for Ultimate products +MEM_HEAP_MAX_SIZE="12G" +# Default maximum stack memory size for Ultimate products +MEM_STACK_MAX_SIZE="512M" -build_printhelp() { - printf 'Usage: %s [-o all|linux|win32]\n' "${0}" +_print_help() { + printf 'Usage: %s [-m ] [-s ] [-p all|linux|win32] [-h]\n' "${0}" print_newline printf 'Options:\n' + printf ' -m Set maximum heap memory size for Ultimate products (default: %s)\n' "${MEM_HEAP_MAX_SIZE}" + printf ' -s Set maximum stack memory size for Ultimate products (default: %s)\n' "${MEM_STACK_MAX_SIZE}" printf ' -p Specify platforms to build for:\n' - printf ' all build for Linux and Windows [default]\n' + printf ' all build for Linux and Windows (default)\n' printf ' linux build only for Linux\n' printf ' win32 build only for Windows\n' printf ' -h Show this help message\n' } +_validate_memory_size() { + local MEM_OPT="${1}" + local MEM_SIZE="${2}" + + # Check if memory size is valid (e.g., 512, 1024K, 2MB, 4GB, etc.) + if [[ ! "${MEM_SIZE}" =~ ^[0-9]+[KMG]$ ]]; then + printf '%s: invalid value for %s -- %s\n' "${0}" "${MEM_OPT}" "${MEM_SIZE}" + print_newline + _print_help + exit 1 + fi +} + build_parseopts() { - while getopts "p:h" OPT; do + while getopts "m:s:p:h" OPT; do case "${OPT}" in + m) + _validate_memory_size "-m" "${OPTARG}" + MEM_HEAP_MAX_SIZE="${OPTARG}" + ;; + s) + _validate_memory_size "-s" "${OPTARG}" + MEM_STACK_MAX_SIZE="${OPTARG}" + ;; p) case "${OPTARG}" in all) @@ -42,19 +69,19 @@ build_parseopts() { *) printf '%s: invalid option for -p -- %s\n' "${0}" "${OPTARG}" print_newline - build_printhelp + _print_help exit 1 ;; esac ;; h) print_newline - build_printhelp - exit 1 + _print_help + exit 0 ;; *) print_newline - build_printhelp + _print_help exit 1 ;; esac @@ -96,6 +123,11 @@ build_run() { print_cmd_version "${VERS_JDK}" "Java Development Kit" print_newline + print_heading "Using the configuration for Ultimate" + print_memory_size "${MEM_HEAP_MAX_SIZE}" "Maximum memory heap size" + print_memory_size "${MEM_STACK_MAX_SIZE}" "Maximum memory stack size" + print_newline + print_heading "Start Ultimate build" exit_on_fail mvn -T 1C clean install -Pmaterialize print_newline @@ -105,51 +137,51 @@ build_run() { build_package() { for PLATFORM in "${PLATFORMS[@]}"; do - # makePackageConfig.sh + # makePackageConfig.sh print_heading "Package Ultimate Taipan [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Taipan" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "Taipan" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" print_newline print_heading "Package Ultimate Automizer [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Automizer" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "BuchiAutomizerCInline_WitnessPrinter.xml" "AutomizerCInline_IcfgBuilder.xml" "AutomizerCInline_WitnessPrinter.xml" "LTLAutomizerC.xml" "BuchiAutomizerCInline.xml" + exit_on_fail bash makePackageConfig.sh "Automizer" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "BuchiAutomizerCInline_WitnessPrinter.xml" "AutomizerCInline_IcfgBuilder.xml" "AutomizerCInline_WitnessPrinter.xml" "LTLAutomizerC.xml" "BuchiAutomizerCInline.xml" print_newline print_heading "Package Ultimate Kojak [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Kojak" "${PLATFORM}" "KojakC_WitnessPrinter.xml" "NONE" "NONE" "KojakC_WitnessPrinter.xml" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "Kojak" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "KojakC_WitnessPrinter.xml" "NONE" "NONE" "KojakC_WitnessPrinter.xml" "NONE" "NONE" print_newline print_heading "Package Ultimate GemCutter [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "GemCutter" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "GemCutter" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" print_newline print_heading "Package Ultimate Referee [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Referee" "${PLATFORM}" "RefereeCInline.xml" "NONE" "RefereeCInline_IcfgBuilder.xml" "NONE" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "Referee" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "RefereeCInline.xml" "NONE" "RefereeCInline_IcfgBuilder.xml" "NONE" "NONE" "NONE" print_newline - # makePackageSmall.sh + # makePackageSmall.sh print_heading "Package Ultimate Command Line [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "CLI-E4" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "CLI-E4" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate Debug UI [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "Debug-E4" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "Debug-E4" "UltimateDebug" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate DeltaDebugger [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate Eliminator [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "Eliminator" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "Eliminator" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate WebBackend [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "WebBackend" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "WebBackend" "WebBackend" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline - # makePackageReqCheck.sh + # makePackageReqCheck.sh print_heading "Package Ultimate ReqCheck [${PLATFORM}]" - exit_on_fail bash makePackageReqCheck.sh "ReqCheck" "${PLATFORM}" "ReqCheck.xml" "ReqCheck.xml" + exit_on_fail bash makePackageReqCheck.sh "ReqCheck" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "ReqCheck.xml" "ReqCheck.xml" print_newline done } diff --git a/releaseScripts/default/makePackageConfig.sh b/releaseScripts/default/makePackageConfig.sh index 807c16bb5c3..55fc228674a 100755 --- a/releaseScripts/default/makePackageConfig.sh +++ b/releaseScripts/default/makePackageConfig.sh @@ -11,16 +11,19 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" # Start the actual script -if [ "${#}" -le 2 ]; then +if [ "${#}" -le 5 ]; then echo "Not enough arguments supplied -- use arguments in the following order" - echo "1. the toolname" - echo "2. 'linux' or 'win32' for the target platform" - echo "3. (optional) the reach toolchain (e.g., 'AutomizerC_WitnessPrinter.xml')" - echo "4. (optional) the termination toolchain or NONE" - echo "5. (optional) the witness validation toolchain or NONE" - echo "6. (optional) the memsafety deref and memtrack toolchain or NONE" - echo "7. (optional) the ltl toolchain or NONE" - echo "8. (optional) the termination witness validation toolchain or NONE" + echo " 1. the toolname" + echo " 2. the launcher name" + echo " 3. the maximum heap memory size" + echo " 4. the maximum stack memory size" + echo " 5. 'linux' or 'win32' for the target platform" + echo " 6. (optional) the reach toolchain (e.g., 'AutomizerC_WitnessPrinter.xml')" + echo " 7. (optional) the termination toolchain or NONE" + echo " 8. (optional) the witness validation toolchain or NONE" + echo " 9. (optional) the memsafety deref and memtrack toolchain or NONE" + echo "10. (optional) the ltl toolchain or NONE" + echo "11. (optional) the termination witness validation toolchain or NONE" exit 1 fi @@ -42,23 +45,22 @@ ADDS=( "adds/mathsat-LICENSE" "adds/ltl2ba-LICENSE" "adds/Ultimate.py" - "adds/Ultimate.ini" "adds/README" ) # Architecture-specific variables -if [ "${2}" == "linux" ]; then +if [ "${5}" == "linux" ]; then echo "Packaging for linux..." ARCH="linux" ARCHPATH="products/CLI-E4/linux/gtk/x86_64" ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba") -elif [ "${2}" == "win32" ]; then +elif [ "${5}" == "win32" ]; then echo "Packaging for win32..." ARCH="win32" ARCHPATH="products/CLI-E4/win32/win32/x86_64" ADDS+=("adds/z3.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll" "adds/ltl2ba.exe") else - echo "Wrong argument: ""${2}"" -- use 'linux' or 'win32'" + echo "Wrong argument: ""${5}"" -- use 'linux' or 'win32'" exit 1 fi @@ -72,43 +74,43 @@ DATADIR="${TARGETDIR}"/data SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" # Check all toolchain arguments -if [ -n "${3}" -a ! "NONE" = "${3}" ]; then - TOOLCHAIN="../../trunk/examples/toolchains/${3}" +if [ -n "${6}" -a ! "NONE" = "${6}" ]; then + TOOLCHAIN="../../trunk/examples/toolchains/${6}" else echo "No reach toolchain specified, ommitting..." TOOLCHAIN="" fi -if [ ! -z "${4}" -a ! "NONE" = "${4}" ]; then - TERMTOOLCHAIN="../../trunk/examples/toolchains/${4}" +if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then + TERMTOOLCHAIN="../../trunk/examples/toolchains/${7}" else echo "No termination toolchain specified, ommitting..." TERMTOOLCHAIN="" fi -if [ ! -z "${5}" -a ! "NONE" = "${5}" ]; then - VALTOOLCHAIN="../../trunk/examples/toolchains/${5}" +if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then + VALTOOLCHAIN="../../trunk/examples/toolchains/${8}" else echo "No witness validation toolchain specified, ommitting..." VALTOOLCHAIN="" fi -if [ ! -z "${6}" -a ! "NONE" = "${6}" ]; then - MEMDEREFMEMTRACKTOOLCHAIN="../../trunk/examples/toolchains/${6}" +if [ ! -z "${9}" -a ! "NONE" = "${9}" ]; then + MEMDEREFMEMTRACKTOOLCHAIN="../../trunk/examples/toolchains/${9}" else echo "No memory deref toolchain specified, ommitting..." MEMDEREFMEMTRACKTOOLCHAIN="" fi -if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then - LTLTOOLCHAIN="../../trunk/examples/toolchains/${7}" +if [ ! -z "${10}" -a ! "NONE" = "${10}" ]; then + LTLTOOLCHAIN="../../trunk/examples/toolchains/${10}" else echo "No LTL toolchain specified, ommitting..." LTLTOOLCHAIN="" fi -if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then - TERMVALTOOLCHAIN="../../trunk/examples/toolchains/${8}" +if [ ! -z "${11}" -a ! "NONE" = "${11}" ]; then + TERMVALTOOLCHAIN="../../trunk/examples/toolchains/${11}" else echo "No termination witness validation toolchain specified, ommitting..." TERMVALTOOLCHAIN="" @@ -140,10 +142,5 @@ for add in "${ADDS[@]}" ; do exit_on_fail cp "${add}" "${TARGETDIR}/" done -echo "Modifying Ultimate.py with version and toolname" -# Replacing version value in Ultimate.py -exit_on_fail sed -i "s/^version =.*$/version = \'${VERSION}\'/g" "${TARGETDIR}"/Ultimate.py -# Replacing toolname value in Ultimate.py -exit_on_fail sed -i "s/toolname =.*$/toolname = \'${TOOLNAME}\'/g" "${TARGETDIR}"/Ultimate.py -# Adjust permission to execute Ultimate.py -exit_on_fail chmod a+x "${TARGETDIR}"/Ultimate.py +setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" diff --git a/releaseScripts/default/makePackageReqCheck.sh b/releaseScripts/default/makePackageReqCheck.sh index edfa537e26f..5772ce142c4 100644 --- a/releaseScripts/default/makePackageReqCheck.sh +++ b/releaseScripts/default/makePackageReqCheck.sh @@ -11,12 +11,15 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" # Start the actual script -if [ "${#}" -lt 4 ]; then +if [ "${#}" -lt 7 ]; then echo "Not enough arguments supplied -- use arguments in the following order" echo "1. the toolname" - echo "2. 'linux' or 'win32' for the target platform" - echo "3. ReqCheck toolchain (e.g., 'ReqCheck.xml')" - echo "4. TestGen toolchain (e.g., 'ReqToTest.xml')" + echo "2. the launcher name" + echo "3. the maximum heap memory size" + echo "4. the maximum stack memory size" + echo "5. 'linux' or 'win32' for the target platform" + echo "6. ReqCheck toolchain (e.g., 'ReqCheck.xml')" + echo "7. TestGen toolchain (e.g., 'ReqToTest.xml')" exit 1 fi @@ -42,18 +45,18 @@ ADDS=( ) # Architecture-specific variables -if [ "${2}" == "linux" ]; then +if [ "${5}" == "linux" ]; then echo "Packaging for linux..." ARCH="linux" ARCHPATH="products/CLI-E4/linux/gtk/x86_64" ADDS+=("adds/z3" "adds/cvc4nyu" "adds/cvc4" "adds/mathsat") -elif [ "${2}" == "win32" ]; then +elif [ "${5}" == "win32" ]; then echo "Packaging for win32..." ARCH="win32" ARCHPATH="products/CLI-E4/win32/win32/x86_64" ADDS+=("adds/z3.exe" "adds/cvc4nyu.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll") else - echo "Wrong argument: ""${2}"" -- use 'linux' or 'win32'" + echo "Wrong argument: ""${5}"" -- use 'linux' or 'win32'" exit 1 fi @@ -67,15 +70,15 @@ DATADIR="${TARGETDIR}"/data SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" # Check toolchain argument -if [ ! -z "${3}" -a ! "NONE" = "${3}" ]; then - TOOLCHAIN="../../trunk/examples/toolchains/${3}" +if [ ! -z "${6}" -a ! "NONE" = "${6}" ]; then + TOOLCHAIN="../../trunk/examples/toolchains/${6}" else echo "No reach toolchain specified, ommitting..." TOOLCHAIN= fi -if [ ! -z "${4}" -a ! "NONE" = "${4}" ]; then - TESTTOOLCHAIN="../../trunk/examples/toolchains/${4}" +if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then + TESTTOOLCHAIN="../../trunk/examples/toolchains/${7}" else echo "No test toolchain specified, ommitting..." TESTTOOLCHAIN="" @@ -102,3 +105,6 @@ exit_on_fail cp ${SETTINGS} "${CONFIGDIR}"/. for add in "${ADDS[@]}" ; do exit_on_fail cp "${add}" "${TARGETDIR}/" done + +setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" diff --git a/releaseScripts/default/makePackageSmall.sh b/releaseScripts/default/makePackageSmall.sh index 08a6b111061..d89d3e9c251 100755 --- a/releaseScripts/default/makePackageSmall.sh +++ b/releaseScripts/default/makePackageSmall.sh @@ -12,10 +12,13 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" # Start the actual script -if [ "${#}" -le 1 ]; then +if [ "${#}" -lt 5 ]; then echo "Not enough arguments supplied -- use arguments in the following order" echo "1. the toolname" - echo "2. 'linux' or 'win32' for the target platform" + echo "2. the launcher name" + echo "3. the maximum heap memory size" + echo "4. the maximum stack memory size" + echo "5. 'linux' or 'win32' for the target platform" exit 1 fi @@ -37,23 +40,22 @@ ADDS=( "adds/mathsat-LICENSE" "adds/ltl2ba-LICENSE" "adds/Ultimate.py" - "adds/Ultimate.ini" "adds/README" ) # Architecture-specific variables -if [ "${2}" == "linux" ]; then +if [ "${5}" == "linux" ]; then echo "Packaging for linux..." ARCH="linux" ARCHPATH="products/${TOOLNAME}/linux/gtk/x86_64" ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba") -elif [ "${2}" == "win32" ]; then +elif [ "${5}" == "win32" ]; then echo "Packaging for win32..." ARCH="win32" ARCHPATH="products/${TOOLNAME}/win32/win32/x86_64" ADDS+=("adds/z3.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll" "adds/ltl2ba.exe") else - echo "Wrong argument: ""${2}"" -- use 'linux' or 'win32'" + echo "Wrong argument: ""${5}"" -- use 'linux' or 'win32'" exit 1 fi @@ -84,10 +86,5 @@ for add in "${ADDS[@]}" ; do exit_on_fail cp "${add}" "${TARGETDIR}/" done -echo "Modifying Ultimate.py with version and toolname" -# Replacing version value in Ultimate.py -exit_on_fail sed -i "s/^version =.*$/version = \'${VERSION}\'/g" "${TARGETDIR}"/Ultimate.py -# Replacing toolname value in Ultimate.py -exit_on_fail sed -i "s/toolname =.*$/toolname = \'${TOOLNAME}\'/g" "${TARGETDIR}"/Ultimate.py -# Adjust permission to execute Ultimate.py -exit_on_fail chmod a+x "${TARGETDIR}"/Ultimate.py +setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" diff --git a/releaseScripts/default/makeSettings.sh b/releaseScripts/default/makeSettings.sh index 5630b580a22..7abaefe023e 100755 --- a/releaseScripts/default/makeSettings.sh +++ b/releaseScripts/default/makeSettings.sh @@ -57,6 +57,44 @@ test_cmd_version_greater_equal() { fi } +setup_ultimate_product_info() { + local PRODUCT_PATH="${1}" + local PRODUCT_LAUNCHER="${2}" + local PRODUCT_NAME="${3}" + local PRODUCT_VERSION="${4}" + + if [[ -f "${PRODUCT_PATH}/Ultimate.py" ]]; then + echo "Setup version and toolname for Ultimate.py" + # Replacing toolname value in Ultimate.py + exit_on_fail sed -i "s/^toolname =.*$/toolname = \'${PRODUCT_NAME}\'/g" "${PRODUCT_PATH}/Ultimate.py" + # Replacing version value in Ultimate.py + exit_on_fail sed -i "s/^version =.*$/version = \'${PRODUCT_VERSION}\'/g" "${PRODUCT_PATH}/Ultimate.py" + # Adjust permission to execute Ultimate.py + exit_on_fail chmod a+x "${PRODUCT_PATH}/Ultimate.py" + fi + + if [[ -f "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}" ]]; then + echo "Change permissions to run ${PRODUCT_LAUNCHER}" + # Adjust permission to execute product launcher (e.g., 'Ultimate' launcher executable) + exit_on_fail chmod a+x "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}" + fi +} + +setup_ultimate_product_memory() { + local PRODUCT_PATH="${1}" + local PRODUCT_LAUNCHER="${2}" + local PRODUCT_MEM_HEAP_MAX="${3}" + local PRODUCT_MEM_STACK_MAX="${4}" + + if [[ -f "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" ]]; then + echo "Setup maximum stack and heap size for ${PRODUCT_LAUNCHER}" + # Replacing maximum heap memory value in *.ini + exit_on_fail sed -i "s/^-Xmx.*$/-Xmx${PRODUCT_MEM_HEAP_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" + # Replacing maximum stack memory value in *.ini + exit_on_fail sed -i "s/^-Xms.*$/-Xms${PRODUCT_MEM_STACK_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" + fi +} + get_cmd_version() { ${@} | grep -m1 -Eo "([[:digit:]]+\.)+[[:digit:]]+" } @@ -68,6 +106,13 @@ print_cmd_version() { printf '%s: %s\n' "${CMD_NAME}" "${CMD_VERS}" } +print_memory_size() { + local MEM_SIZE="${1}" + local MEM_NAME="${2}" + + printf '%s: %s\n' "${MEM_NAME}" "${MEM_SIZE}" +} + print_newline() { printf '\n' } From 997682eb698b93356e643ac76db646055cf702c5 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 23:11:20 +0200 Subject: [PATCH 29/38] Fix invalid Docker compose build argument for the Webbackend image --- packaging/docker/docker-compose.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index 57661e78a57..fa29a79b289 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -6,7 +6,7 @@ services: dockerfile: "Dockerfile" target: "ultimate-webbackend" args: - ULTIMATE_TMP_DIR: "${ULTIMATE_TMP_DIR-/tmp/ultimate}" + ULTIMATE_DIR_TMP: "${ULTIMATE_DIR_TMP-/tmp/ultimate}" image: "ultimate-webbackend" environment: ULTIMATE_BACKEND_HOST: "${ULTIMATE_BACKEND_HOST-localhost}" From 4205eaf95f7d00a826b869fc3c452002be7d14c4 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Wed, 20 Aug 2025 23:31:09 +0200 Subject: [PATCH 30/38] Make maximum heap and stack size configurable in Docker compose setup --- packaging/docker/Dockerfile | 5 ++++- packaging/docker/docker-compose.yml | 4 ++++ packaging/docker/ultimate-webservice.env | 3 +++ 3 files changed, 11 insertions(+), 1 deletion(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index f5c826e715f..89fb6f37e61 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -26,6 +26,9 @@ FROM alpine:3 AS build-products ARG REPO_URL="https://github.com/ultimate-pa/ultimate.git" ARG REPO_BRANCH="dev" +ARG ULTIMATE_MEMORY_HEAP_MAX="12G" +ARG ULTIMATE_MEMORY_STACK_MAX="512M" + ARG REPO_DIR_BUILD ARG DIR_BUILD ARG DIR_ULTIMATE @@ -43,7 +46,7 @@ RUN mkdir -p "${DIR_BUILD}" && \ # build all Ultimate products WORKDIR "${DIR_ULTIMATE}" -RUN cd "${DIR_OUTPUT_BUILD}" && bash makeBuild.sh -p linux +RUN cd "${DIR_OUTPUT_BUILD}" && bash makeBuild.sh -m "${ULTIMATE_MEMORY_HEAP_MAX}" -s "${ULTIMATE_MEMORY_STACK_MAX}" -p linux #------------------------------------------------------------------------------ # 2nd build stage: compile and build the Ultimate web interface diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index fa29a79b289..0b6f649a214 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -7,6 +7,8 @@ services: target: "ultimate-webbackend" args: ULTIMATE_DIR_TMP: "${ULTIMATE_DIR_TMP-/tmp/ultimate}" + ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-12G}" + ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-512M}" image: "ultimate-webbackend" environment: ULTIMATE_BACKEND_HOST: "${ULTIMATE_BACKEND_HOST-localhost}" @@ -25,6 +27,8 @@ services: target: "ultimate-webfrontend" args: ULTIMATE_FRONTEND_BASEURL: "${ULTIMATE_FRONTEND_ROUTE-/website}" + ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-12G}" + ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-512M}" image: "ultimate-webfrontend" environment: ULTIMATE_FRONTEND_DEBUG: "${ULTIMATE_FRONTEND_DEBUG-false}" diff --git a/packaging/docker/ultimate-webservice.env b/packaging/docker/ultimate-webservice.env index f7dba9579ad..646dab54ff8 100644 --- a/packaging/docker/ultimate-webservice.env +++ b/packaging/docker/ultimate-webservice.env @@ -22,3 +22,6 @@ ULTIMATE_LOG_LEVEL=INFO ULTIMATE_DIR_TMP=/tmp/ultimate ULTIMATE_TIMEOUT=90 + +ULTIMATE_MEMORY_HEAP_MAX=12G +ULTIMATE_MEMORY_STACK_MAX=512M From e194cd4d23a4e3b495e5382c24a2488d97ef68e1 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Thu, 21 Aug 2025 01:41:17 +0200 Subject: [PATCH 31/38] Add GCC as syntax checker to Docker image of WebBackend --- packaging/docker/Dockerfile | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 89fb6f37e61..59d50b2dafb 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -468,6 +468,10 @@ ENV ULTIMATE_TIMEOUT=90 # create directory to store temporary files RUN mkdir -p "${ULTIMATE_DIR_TMP}" +# install runtime dependencies for the WebBackend +RUN apk add --no-cache "gcc" \ + "libc-dev" + # install 'dockerize' for automatic configuration file creation ENV DOCKERIZE_VERSION="v0.9.5" RUN apk add --no-cache "wget" \ From a221748e6e9bab564912c0b410fdf512b518feac Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Thu, 21 Aug 2025 01:45:49 +0200 Subject: [PATCH 32/38] Fix invalid Docker defaults for the Ultimate Webservices --- packaging/docker/Dockerfile | 9 ++++++--- packaging/docker/docker-compose.yml | 4 ++-- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 59d50b2dafb..02984b981b1 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -500,14 +500,17 @@ ENV ULTIMATE_FRONTEND_SERVE="False" ENV ULTIMATE_FRONTEND_PATH="${USER_HOME}" ENV ULTIMATE_FRONTEND_ROUTE="/website" -# expose communication port of the Webbackend +# expose communication port of the WebBackend EXPOSE "${ULTIMATE_BACKEND_PORT}" -# define health check to supervise the Ultimate Webbackend's availability +# define health check to supervise the Ultimate WebBackend's availability HEALTHCHECK --interval=1m --timeout=10s --start-period=20s \ CMD curl -f "http://${ULTIMATE_BACKEND_HOST}:${ULTIMATE_BACKEND_PORT}${ULTIMATE_BACKEND_ROUTE}" || exit 1 -# default entry point to automatically configure and start the Ultimate Webbackend product +# append WebBackend executable and solvers directory to the PATH environment variable to ensure they are accessible by the Docker entrypoint command +ENV PATH="${USER_HOME}:${PATH}" + +# default entry point to automatically configure and start the Ultimate WebBackend product ENTRYPOINT ["dockerize", "-template", "web.config.properties.tpl:web.config.properties", \ "-template", "WebBackend.ini.tpl:WebBackend.ini", \ "WebBackend"] diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index 0b6f649a214..5017ac211d9 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -34,7 +34,7 @@ services: ULTIMATE_FRONTEND_DEBUG: "${ULTIMATE_FRONTEND_DEBUG-false}" ULTIMATE_FRONTEND_MSG_ORIENTATION: "${ULTIMATE_FRONTEND_MSG_ORIENTATION-left}" ULTIMATE_FRONTEND_PROTOCOL: "${ULTIMATE_FRONTEND_PROTOCOL-http}" - ULTIMATE_FRONTEND_HOST: "${ULTIMATE_FRONTEND_HOST-localhost}" + ULTIMATE_FRONTEND_HOST: "${ULTIMATE_FRONTEND_HOST-0.0.0.0}" ULTIMATE_FRONTEND_PORT: ${ULTIMATE_FRONTEND_PORT-80} ULTIMATE_FRONTEND_ROUTE: "${ULTIMATE_FRONTEND_ROUTE-/website}" ULTIMATE_BACKEND_PROTOCOL: "${ULTIMATE_BACKEND_PROTOCOL-http}" @@ -42,7 +42,7 @@ services: ULTIMATE_BACKEND_PORT: "${ULTIMATE_BACKEND_PORT-8080}" ULTIMATE_BACKEND_ROUTE: "${ULTIMATE_BACKEND_ROUTE-/api}" ports: - - "80:${ULTIMATE_FRONTEND_PORT-8080}" + - "80:${ULTIMATE_FRONTEND_PORT-80}" restart: "unless-stopped" depends_on: ultimate-webbackend: From 154fa5dd510dd55b7077a13ee1c505ac1ca5961b Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Thu, 21 Aug 2025 21:41:24 +0200 Subject: [PATCH 33/38] Fix issue when archiving the Ultimate Debug UI product --- releaseScripts/default/makeFresh.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/releaseScripts/default/makeFresh.sh b/releaseScripts/default/makeFresh.sh index 93d93b76793..7fd3c02a0a3 100755 --- a/releaseScripts/default/makeFresh.sh +++ b/releaseScripts/default/makeFresh.sh @@ -68,7 +68,7 @@ archive_run() { print_newline print_heading "Archive Ultimate Debug UI [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "Debug-E4" "${PLATFORM}" + exit_on_fail bash makeZip.sh "Debug-E4" "${PLATFORM}" print_newline done } From 748fbc2ec265621557a6df9a18bbdfb9061fdbe1 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 22 Aug 2025 14:03:47 +0200 Subject: [PATCH 34/38] Make maximum heap and stack size configurable in Ultimate.py --- releaseScripts/default/adds/Ultimate.py | 6 ++++-- releaseScripts/default/makeSettings.sh | 12 ++++++++++-- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/releaseScripts/default/adds/Ultimate.py b/releaseScripts/default/adds/Ultimate.py index e21fa8ac790..b1fd4c25ba6 100755 --- a/releaseScripts/default/adds/Ultimate.py +++ b/releaseScripts/default/adds/Ultimate.py @@ -20,6 +20,8 @@ # fmt: off version = '4f54f8f5' toolname = 'Automizer' +memory_heap_size_max = '12G' +memory_stack_size_max = '512M' # fmt: on write_ultimate_output_to_file = True @@ -281,8 +283,8 @@ def create_ultimate_base_call(): ultimate_bin = [ get_java(), "-Dosgi.configuration.area=" + os.path.join(datadir, "config"), - "-Xmx15G", - "-Xms4m", + "-Xmx" + memory_heap_size_max, + "-Xms" + memory_stack_size_max, ] if enable_assertions: diff --git a/releaseScripts/default/makeSettings.sh b/releaseScripts/default/makeSettings.sh index 7abaefe023e..206495a6672 100755 --- a/releaseScripts/default/makeSettings.sh +++ b/releaseScripts/default/makeSettings.sh @@ -88,11 +88,19 @@ setup_ultimate_product_memory() { if [[ -f "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" ]]; then echo "Setup maximum stack and heap size for ${PRODUCT_LAUNCHER}" - # Replacing maximum heap memory value in *.ini + # Replacing maximum heap memory size in *.ini exit_on_fail sed -i "s/^-Xmx.*$/-Xmx${PRODUCT_MEM_HEAP_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" - # Replacing maximum stack memory value in *.ini + # Replacing maximum stack memory size in *.ini exit_on_fail sed -i "s/^-Xms.*$/-Xms${PRODUCT_MEM_STACK_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" fi + + if [[ -f "${PRODUCT_PATH}/Ultimate.py" ]]; then + echo "Setup maximum stack and heap size in Ultimate.py" + # Replacing maximum heap memory size in Ultimate.py + exit_on_fail sed -i "s/^memory_heap_size_max =.*$/memory_heap_size_max = \'${PRODUCT_MEM_HEAP_MAX}\'/g" "${PRODUCT_PATH}/Ultimate.py" + # Replacing maximum stack memory size in Ultimate.py + exit_on_fail sed -i "s/^memory_stack_size_max =.*$/memory_stack_size_max = \'${PRODUCT_MEM_STACK_MAX}\'/g" "${PRODUCT_PATH}/Ultimate.py" + fi } get_cmd_version() { From 47edf2538d1f57e349c38890e62c340e7a61008c Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 22 Aug 2025 14:09:12 +0200 Subject: [PATCH 35/38] Fix invalid build argument in Docker compose setup --- packaging/docker/docker-compose.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index 5017ac211d9..c8549baf97b 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -28,7 +28,7 @@ services: args: ULTIMATE_FRONTEND_BASEURL: "${ULTIMATE_FRONTEND_ROUTE-/website}" ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-12G}" - ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-512M}" + ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-512M}" image: "ultimate-webfrontend" environment: ULTIMATE_FRONTEND_DEBUG: "${ULTIMATE_FRONTEND_DEBUG-false}" From 798d4ab8e3eb8d7f88bc9b491f59b12f87f0f8c7 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 22 Aug 2025 14:57:35 +0200 Subject: [PATCH 36/38] Fix incorrect handling of memory settings for Ultimate products --- packaging/docker/Dockerfile | 4 +- packaging/docker/docker-compose.yml | 2 + packaging/docker/ultimate-webservice.env | 1 + releaseScripts/default/adds/Ultimate.py | 4 +- releaseScripts/default/makeBuild.sh | 44 ++++++++------- releaseScripts/default/makePackageConfig.sh | 53 ++++++++++--------- releaseScripts/default/makePackageReqCheck.sh | 29 +++++----- releaseScripts/default/makePackageSmall.sh | 17 +++--- releaseScripts/default/makeSettings.sh | 15 ++++-- trunk/source/BA_SiteRepository/CLI-E4.product | 2 +- .../source/BA_SiteRepository/Debug-E4.product | 2 +- .../BA_SiteRepository/DeltaDebugger.product | 2 +- .../BA_SiteRepository/Eliminator.product | 2 +- .../BA_SiteRepository/ReqAnalyzer.product | 2 +- .../Ultimate_E4.32_Java21.target | 2 +- .../Ultimate_E4.32_Java21_Linux.target | 2 +- .../Ultimate_E4.32_Java21_MacOS.target | 2 +- .../Ultimate_E4.32_Java21_Win32.target | 2 +- .../BA_SiteRepository/WebBackend.product | 4 +- 19 files changed, 106 insertions(+), 85 deletions(-) diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 02984b981b1..8f467173c0e 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -26,6 +26,7 @@ FROM alpine:3 AS build-products ARG REPO_URL="https://github.com/ultimate-pa/ultimate.git" ARG REPO_BRANCH="dev" +ARG ULTIMATE_MEMORY_HEAP_INIT="4M" ARG ULTIMATE_MEMORY_HEAP_MAX="12G" ARG ULTIMATE_MEMORY_STACK_MAX="512M" @@ -46,7 +47,8 @@ RUN mkdir -p "${DIR_BUILD}" && \ # build all Ultimate products WORKDIR "${DIR_ULTIMATE}" -RUN cd "${DIR_OUTPUT_BUILD}" && bash makeBuild.sh -m "${ULTIMATE_MEMORY_HEAP_MAX}" -s "${ULTIMATE_MEMORY_STACK_MAX}" -p linux +RUN cd "${DIR_OUTPUT_BUILD}" && \ + bash makeBuild.sh -i "${ULTIMATE_MEMORY_HEAP_INIT}" -m "${ULTIMATE_MEMORY_HEAP_MAX}" -s "${ULTIMATE_MEMORY_STACK_MAX}" -p linux #------------------------------------------------------------------------------ # 2nd build stage: compile and build the Ultimate web interface diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index c8549baf97b..e44136a3818 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -7,6 +7,7 @@ services: target: "ultimate-webbackend" args: ULTIMATE_DIR_TMP: "${ULTIMATE_DIR_TMP-/tmp/ultimate}" + ULTIMATE_MEMORY_HEAP_INIT: ${ULTIMATE_MEMORY_HEAP_INIT-4M} ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-12G}" ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-512M}" image: "ultimate-webbackend" @@ -27,6 +28,7 @@ services: target: "ultimate-webfrontend" args: ULTIMATE_FRONTEND_BASEURL: "${ULTIMATE_FRONTEND_ROUTE-/website}" + ULTIMATE_MEMORY_HEAP_INIT: ${ULTIMATE_MEMORY_HEAP_INIT-4M} ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-12G}" ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-512M}" image: "ultimate-webfrontend" diff --git a/packaging/docker/ultimate-webservice.env b/packaging/docker/ultimate-webservice.env index 646dab54ff8..bf06d173927 100644 --- a/packaging/docker/ultimate-webservice.env +++ b/packaging/docker/ultimate-webservice.env @@ -23,5 +23,6 @@ ULTIMATE_LOG_LEVEL=INFO ULTIMATE_DIR_TMP=/tmp/ultimate ULTIMATE_TIMEOUT=90 +ULTIMATE_MEMORY_HEAP_INIT=4M ULTIMATE_MEMORY_HEAP_MAX=12G ULTIMATE_MEMORY_STACK_MAX=512M diff --git a/releaseScripts/default/adds/Ultimate.py b/releaseScripts/default/adds/Ultimate.py index b1fd4c25ba6..80aca83e45e 100755 --- a/releaseScripts/default/adds/Ultimate.py +++ b/releaseScripts/default/adds/Ultimate.py @@ -20,6 +20,7 @@ # fmt: off version = '4f54f8f5' toolname = 'Automizer' +memory_heap_size_init = '4M' memory_heap_size_max = '12G' memory_stack_size_max = '512M' # fmt: on @@ -283,8 +284,9 @@ def create_ultimate_base_call(): ultimate_bin = [ get_java(), "-Dosgi.configuration.area=" + os.path.join(datadir, "config"), + "-Xms" + memory_heap_size_init, "-Xmx" + memory_heap_size_max, - "-Xms" + memory_stack_size_max, + "-Xss" + memory_stack_size_max, ] if enable_assertions: diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh index c086f1c866f..4be701771d5 100755 --- a/releaseScripts/default/makeBuild.sh +++ b/releaseScripts/default/makeBuild.sh @@ -13,15 +13,18 @@ source "${DIR}/semver2.sh" # Default platforms for the build of Ultimate PLATFORMS=("linux" "win32") +# Default initial heap memory size for Ultimate products +MEM_HEAP_INIT_SIZE="4M" # Default maximum heap memory size for Ultimate products MEM_HEAP_MAX_SIZE="12G" # Default maximum stack memory size for Ultimate products MEM_STACK_MAX_SIZE="512M" _print_help() { - printf 'Usage: %s [-m ] [-s ] [-p all|linux|win32] [-h]\n' "${0}" + printf 'Usage: %s [-i ] [-m ] [-s ] [-p all|linux|win32] [-h]\n' "${0}" print_newline printf 'Options:\n' + printf ' -i Set initial heap memory size for Ultimate products (default: %s)\n' "${MEM_HEAP_INIT_SIZE}" printf ' -m Set maximum heap memory size for Ultimate products (default: %s)\n' "${MEM_HEAP_MAX_SIZE}" printf ' -s Set maximum stack memory size for Ultimate products (default: %s)\n' "${MEM_STACK_MAX_SIZE}" printf ' -p Specify platforms to build for:\n' @@ -45,8 +48,12 @@ _validate_memory_size() { } build_parseopts() { - while getopts "m:s:p:h" OPT; do + while getopts "i:m:s:p:h" OPT; do case "${OPT}" in + i) + _validate_memory_size "-i" "${OPTARG}" + MEM_HEAP_INIT_SIZE="${OPTARG}" + ;; m) _validate_memory_size "-m" "${OPTARG}" MEM_HEAP_MAX_SIZE="${OPTARG}" @@ -124,8 +131,9 @@ build_run() { print_newline print_heading "Using the configuration for Ultimate" - print_memory_size "${MEM_HEAP_MAX_SIZE}" "Maximum memory heap size" - print_memory_size "${MEM_STACK_MAX_SIZE}" "Maximum memory stack size" + print_memory_size "${MEM_HEAP_INIT_SIZE}" "Initial heap memory size" + print_memory_size "${MEM_HEAP_MAX_SIZE}" "Maximum heap memory size" + print_memory_size "${MEM_STACK_MAX_SIZE}" "Maximum stack memory size" print_newline print_heading "Start Ultimate build" @@ -137,51 +145,51 @@ build_run() { build_package() { for PLATFORM in "${PLATFORMS[@]}"; do - # makePackageConfig.sh + # makePackageConfig.sh print_heading "Package Ultimate Taipan [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Taipan" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "Taipan" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" print_newline print_heading "Package Ultimate Automizer [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Automizer" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "BuchiAutomizerCInline_WitnessPrinter.xml" "AutomizerCInline_IcfgBuilder.xml" "AutomizerCInline_WitnessPrinter.xml" "LTLAutomizerC.xml" "BuchiAutomizerCInline.xml" + exit_on_fail bash makePackageConfig.sh "Automizer" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "BuchiAutomizerCInline_WitnessPrinter.xml" "AutomizerCInline_IcfgBuilder.xml" "AutomizerCInline_WitnessPrinter.xml" "LTLAutomizerC.xml" "BuchiAutomizerCInline.xml" print_newline print_heading "Package Ultimate Kojak [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Kojak" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "KojakC_WitnessPrinter.xml" "NONE" "NONE" "KojakC_WitnessPrinter.xml" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "Kojak" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "KojakC_WitnessPrinter.xml" "NONE" "NONE" "KojakC_WitnessPrinter.xml" "NONE" "NONE" print_newline print_heading "Package Ultimate GemCutter [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "GemCutter" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "GemCutter" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "AutomizerCInline_WitnessPrinter.xml" "NONE" "AutomizerCInline.xml" "AutomizerCInline_WitnessPrinter.xml" "NONE" "NONE" print_newline print_heading "Package Ultimate Referee [${PLATFORM}]" - exit_on_fail bash makePackageConfig.sh "Referee" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "RefereeCInline.xml" "NONE" "RefereeCInline_IcfgBuilder.xml" "NONE" "NONE" "NONE" + exit_on_fail bash makePackageConfig.sh "Referee" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "RefereeCInline.xml" "NONE" "RefereeCInline_IcfgBuilder.xml" "NONE" "NONE" "NONE" print_newline - # makePackageSmall.sh + # makePackageSmall.sh print_heading "Package Ultimate Command Line [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "CLI-E4" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "CLI-E4" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate Debug UI [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "Debug-E4" "UltimateDebug" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "Debug-E4" "UltimateDebug" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate DeltaDebugger [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "DeltaDebugger" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate Eliminator [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "Eliminator" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "Eliminator" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline print_heading "Package Ultimate WebBackend [${PLATFORM}]" - exit_on_fail bash makePackageSmall.sh "WebBackend" "WebBackend" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" + exit_on_fail bash makePackageSmall.sh "WebBackend" "WebBackend" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" print_newline - # makePackageReqCheck.sh + # makePackageReqCheck.sh print_heading "Package Ultimate ReqCheck [${PLATFORM}]" - exit_on_fail bash makePackageReqCheck.sh "ReqCheck" "Ultimate" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "ReqCheck.xml" "ReqCheck.xml" + exit_on_fail bash makePackageReqCheck.sh "ReqCheck" "Ultimate" "${MEM_HEAP_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" "ReqCheck.xml" "ReqCheck.xml" print_newline done } diff --git a/releaseScripts/default/makePackageConfig.sh b/releaseScripts/default/makePackageConfig.sh index 55fc228674a..6994aac0952 100755 --- a/releaseScripts/default/makePackageConfig.sh +++ b/releaseScripts/default/makePackageConfig.sh @@ -11,19 +11,20 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" # Start the actual script -if [ "${#}" -le 5 ]; then +if [ "${#}" -le 6 ]; then echo "Not enough arguments supplied -- use arguments in the following order" echo " 1. the toolname" echo " 2. the launcher name" - echo " 3. the maximum heap memory size" - echo " 4. the maximum stack memory size" - echo " 5. 'linux' or 'win32' for the target platform" - echo " 6. (optional) the reach toolchain (e.g., 'AutomizerC_WitnessPrinter.xml')" - echo " 7. (optional) the termination toolchain or NONE" - echo " 8. (optional) the witness validation toolchain or NONE" - echo " 9. (optional) the memsafety deref and memtrack toolchain or NONE" - echo "10. (optional) the ltl toolchain or NONE" - echo "11. (optional) the termination witness validation toolchain or NONE" + echo " 3. the initial heap memory size" + echo " 4. the maximum heap memory size" + echo " 5. the maximum stack memory size" + echo " 6. 'linux' or 'win32' for the target platform" + echo " 7. (optional) the reach toolchain (e.g., 'AutomizerC_WitnessPrinter.xml')" + echo " 8. (optional) the termination toolchain or NONE" + echo " 9. (optional) the witness validation toolchain or NONE" + echo "10. (optional) the memsafety deref and memtrack toolchain or NONE" + echo "11. (optional) the ltl toolchain or NONE" + echo "12. (optional) the termination witness validation toolchain or NONE" exit 1 fi @@ -49,18 +50,18 @@ ADDS=( ) # Architecture-specific variables -if [ "${5}" == "linux" ]; then +if [ "${6}" == "linux" ]; then echo "Packaging for linux..." ARCH="linux" ARCHPATH="products/CLI-E4/linux/gtk/x86_64" ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba") -elif [ "${5}" == "win32" ]; then +elif [ "${6}" == "win32" ]; then echo "Packaging for win32..." ARCH="win32" ARCHPATH="products/CLI-E4/win32/win32/x86_64" ADDS+=("adds/z3.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll" "adds/ltl2ba.exe") else - echo "Wrong argument: ""${5}"" -- use 'linux' or 'win32'" + echo "Wrong argument: ""${6}"" -- use 'linux' or 'win32'" exit 1 fi @@ -74,43 +75,43 @@ DATADIR="${TARGETDIR}"/data SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" # Check all toolchain arguments -if [ -n "${6}" -a ! "NONE" = "${6}" ]; then - TOOLCHAIN="../../trunk/examples/toolchains/${6}" +if [ -n "${7}" -a ! "NONE" = "${7}" ]; then + TOOLCHAIN="../../trunk/examples/toolchains/${7}" else echo "No reach toolchain specified, ommitting..." TOOLCHAIN="" fi -if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then - TERMTOOLCHAIN="../../trunk/examples/toolchains/${7}" +if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then + TERMTOOLCHAIN="../../trunk/examples/toolchains/${8}" else echo "No termination toolchain specified, ommitting..." TERMTOOLCHAIN="" fi -if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then - VALTOOLCHAIN="../../trunk/examples/toolchains/${8}" +if [ ! -z "${9}" -a ! "NONE" = "${9}" ]; then + VALTOOLCHAIN="../../trunk/examples/toolchains/${9}" else echo "No witness validation toolchain specified, ommitting..." VALTOOLCHAIN="" fi -if [ ! -z "${9}" -a ! "NONE" = "${9}" ]; then - MEMDEREFMEMTRACKTOOLCHAIN="../../trunk/examples/toolchains/${9}" +if [ ! -z "${10}" -a ! "NONE" = "${10}" ]; then + MEMDEREFMEMTRACKTOOLCHAIN="../../trunk/examples/toolchains/${10}" else echo "No memory deref toolchain specified, ommitting..." MEMDEREFMEMTRACKTOOLCHAIN="" fi -if [ ! -z "${10}" -a ! "NONE" = "${10}" ]; then - LTLTOOLCHAIN="../../trunk/examples/toolchains/${10}" +if [ ! -z "${11}" -a ! "NONE" = "${11}" ]; then + LTLTOOLCHAIN="../../trunk/examples/toolchains/${11}" else echo "No LTL toolchain specified, ommitting..." LTLTOOLCHAIN="" fi -if [ ! -z "${11}" -a ! "NONE" = "${11}" ]; then - TERMVALTOOLCHAIN="../../trunk/examples/toolchains/${11}" +if [ ! -z "${12}" -a ! "NONE" = "${12}" ]; then + TERMVALTOOLCHAIN="../../trunk/examples/toolchains/${12}" else echo "No termination witness validation toolchain specified, ommitting..." TERMVALTOOLCHAIN="" @@ -143,4 +144,4 @@ for add in "${ADDS[@]}" ; do done setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" -setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" "${5}" diff --git a/releaseScripts/default/makePackageReqCheck.sh b/releaseScripts/default/makePackageReqCheck.sh index 5772ce142c4..59da159114f 100644 --- a/releaseScripts/default/makePackageReqCheck.sh +++ b/releaseScripts/default/makePackageReqCheck.sh @@ -11,15 +11,16 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" # Start the actual script -if [ "${#}" -lt 7 ]; then +if [ "${#}" -lt 8 ]; then echo "Not enough arguments supplied -- use arguments in the following order" echo "1. the toolname" echo "2. the launcher name" - echo "3. the maximum heap memory size" - echo "4. the maximum stack memory size" - echo "5. 'linux' or 'win32' for the target platform" - echo "6. ReqCheck toolchain (e.g., 'ReqCheck.xml')" - echo "7. TestGen toolchain (e.g., 'ReqToTest.xml')" + echo "3. the initial heap memory size" + echo "4. the maximum heap memory size" + echo "5. the maximum stack memory size" + echo "6. 'linux' or 'win32' for the target platform" + echo "7. ReqCheck toolchain (e.g., 'ReqCheck.xml')" + echo "8. TestGen toolchain (e.g., 'ReqToTest.xml')" exit 1 fi @@ -45,18 +46,18 @@ ADDS=( ) # Architecture-specific variables -if [ "${5}" == "linux" ]; then +if [ "${6}" == "linux" ]; then echo "Packaging for linux..." ARCH="linux" ARCHPATH="products/CLI-E4/linux/gtk/x86_64" ADDS+=("adds/z3" "adds/cvc4nyu" "adds/cvc4" "adds/mathsat") -elif [ "${5}" == "win32" ]; then +elif [ "${6}" == "win32" ]; then echo "Packaging for win32..." ARCH="win32" ARCHPATH="products/CLI-E4/win32/win32/x86_64" ADDS+=("adds/z3.exe" "adds/cvc4nyu.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll") else - echo "Wrong argument: ""${5}"" -- use 'linux' or 'win32'" + echo "Wrong argument: ""${6}"" -- use 'linux' or 'win32'" exit 1 fi @@ -70,15 +71,15 @@ DATADIR="${TARGETDIR}"/data SETTINGS="../../trunk/examples/settings/default/${LCTOOLNAME}/*${TOOLNAME}*" # Check toolchain argument -if [ ! -z "${6}" -a ! "NONE" = "${6}" ]; then - TOOLCHAIN="../../trunk/examples/toolchains/${6}" +if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then + TOOLCHAIN="../../trunk/examples/toolchains/${7}" else echo "No reach toolchain specified, ommitting..." TOOLCHAIN= fi -if [ ! -z "${7}" -a ! "NONE" = "${7}" ]; then - TESTTOOLCHAIN="../../trunk/examples/toolchains/${7}" +if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then + TESTTOOLCHAIN="../../trunk/examples/toolchains/${8}" else echo "No test toolchain specified, ommitting..." TESTTOOLCHAIN="" @@ -107,4 +108,4 @@ for add in "${ADDS[@]}" ; do done setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" -setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" "${5}" diff --git a/releaseScripts/default/makePackageSmall.sh b/releaseScripts/default/makePackageSmall.sh index d89d3e9c251..886ad59d003 100755 --- a/releaseScripts/default/makePackageSmall.sh +++ b/releaseScripts/default/makePackageSmall.sh @@ -12,13 +12,14 @@ if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi source "${DIR}/makeSettings.sh" # Start the actual script -if [ "${#}" -lt 5 ]; then +if [ "${#}" -lt 6 ]; then echo "Not enough arguments supplied -- use arguments in the following order" echo "1. the toolname" echo "2. the launcher name" - echo "3. the maximum heap memory size" - echo "4. the maximum stack memory size" - echo "5. 'linux' or 'win32' for the target platform" + echo "3. the initial heap memory size" + echo "4. the maximum heap memory size" + echo "5. the maximum stack memory size" + echo "6. 'linux' or 'win32' for the target platform" exit 1 fi @@ -44,18 +45,18 @@ ADDS=( ) # Architecture-specific variables -if [ "${5}" == "linux" ]; then +if [ "${6}" == "linux" ]; then echo "Packaging for linux..." ARCH="linux" ARCHPATH="products/${TOOLNAME}/linux/gtk/x86_64" ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba") -elif [ "${5}" == "win32" ]; then +elif [ "${6}" == "win32" ]; then echo "Packaging for win32..." ARCH="win32" ARCHPATH="products/${TOOLNAME}/win32/win32/x86_64" ADDS+=("adds/z3.exe" "adds/cvc4.exe" "adds/mathsat.exe" "adds/mpir.dll" "adds/mathsat.dll" "adds/ltl2ba.exe") else - echo "Wrong argument: ""${5}"" -- use 'linux' or 'win32'" + echo "Wrong argument: ""${6}"" -- use 'linux' or 'win32'" exit 1 fi @@ -87,4 +88,4 @@ for add in "${ADDS[@]}" ; do done setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" -setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" "${5}" diff --git a/releaseScripts/default/makeSettings.sh b/releaseScripts/default/makeSettings.sh index 206495a6672..a57572ca53c 100755 --- a/releaseScripts/default/makeSettings.sh +++ b/releaseScripts/default/makeSettings.sh @@ -83,21 +83,26 @@ setup_ultimate_product_info() { setup_ultimate_product_memory() { local PRODUCT_PATH="${1}" local PRODUCT_LAUNCHER="${2}" - local PRODUCT_MEM_HEAP_MAX="${3}" - local PRODUCT_MEM_STACK_MAX="${4}" + local PRODUCT_MEM_HEAP_INIT="${3}" + local PRODUCT_MEM_HEAP_MAX="${4}" + local PRODUCT_MEM_STACK_MAX="${5}" if [[ -f "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" ]]; then - echo "Setup maximum stack and heap size for ${PRODUCT_LAUNCHER}" + echo "Setup stack and heap sizes for ${PRODUCT_LAUNCHER}" # Replacing maximum heap memory size in *.ini exit_on_fail sed -i "s/^-Xmx.*$/-Xmx${PRODUCT_MEM_HEAP_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" + # Replacing initial heap memory size in *.ini + exit_on_fail sed -i "s/^-Xms.*$/-Xms${PRODUCT_MEM_HEAP_INIT}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" # Replacing maximum stack memory size in *.ini - exit_on_fail sed -i "s/^-Xms.*$/-Xms${PRODUCT_MEM_STACK_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" + exit_on_fail sed -i "s/^-Xss.*$/-Xss${PRODUCT_MEM_STACK_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" fi if [[ -f "${PRODUCT_PATH}/Ultimate.py" ]]; then - echo "Setup maximum stack and heap size in Ultimate.py" + echo "Setup stack and heap sizes in Ultimate.py" # Replacing maximum heap memory size in Ultimate.py exit_on_fail sed -i "s/^memory_heap_size_max =.*$/memory_heap_size_max = \'${PRODUCT_MEM_HEAP_MAX}\'/g" "${PRODUCT_PATH}/Ultimate.py" + # Replacing initial heap memory size in Ultimate.py + exit_on_fail sed -i "s/^memory_heap_size_init =.*$/memory_heap_size_init = \'${PRODUCT_MEM_HEAP_INIT}\'/g" "${PRODUCT_PATH}/Ultimate.py" # Replacing maximum stack memory size in Ultimate.py exit_on_fail sed -i "s/^memory_stack_size_max =.*$/memory_stack_size_max = \'${PRODUCT_MEM_STACK_MAX}\'/g" "${PRODUCT_PATH}/Ultimate.py" fi diff --git a/trunk/source/BA_SiteRepository/CLI-E4.product b/trunk/source/BA_SiteRepository/CLI-E4.product index 303f35d6bd7..b4459d0e1db 100644 --- a/trunk/source/BA_SiteRepository/CLI-E4.product +++ b/trunk/source/BA_SiteRepository/CLI-E4.product @@ -21,7 +21,7 @@ -data @user.home\ultimate-data - -Xmx4g -Xms4M -Dequinox.resolver.revision.batch.size=1 + -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Debug-E4.product b/trunk/source/BA_SiteRepository/Debug-E4.product index 0923608b9ef..09408842b33 100644 --- a/trunk/source/BA_SiteRepository/Debug-E4.product +++ b/trunk/source/BA_SiteRepository/Debug-E4.product @@ -22,7 +22,7 @@ -data @user.home\ultimate-data - -Xmx4g -Xms4M -Dequinox.resolver.revision.batch.size=1 + -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/DeltaDebugger.product b/trunk/source/BA_SiteRepository/DeltaDebugger.product index 32a6f122c07..47c00c20963 100644 --- a/trunk/source/BA_SiteRepository/DeltaDebugger.product +++ b/trunk/source/BA_SiteRepository/DeltaDebugger.product @@ -21,7 +21,7 @@ -data @user.home\ultimate-data - -Xmx4g -Xms4M -Dequinox.resolver.revision.batch.size=1 + -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Eliminator.product b/trunk/source/BA_SiteRepository/Eliminator.product index 6904d9ae423..7c821ddde48 100644 --- a/trunk/source/BA_SiteRepository/Eliminator.product +++ b/trunk/source/BA_SiteRepository/Eliminator.product @@ -21,7 +21,7 @@ -data @user.home\ultimate-data - -Xmx4g -Xms4m -Dequinox.resolver.revision.batch.size=1 + -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/ReqAnalyzer.product b/trunk/source/BA_SiteRepository/ReqAnalyzer.product index 02ea03770e4..964705d89cb 100644 --- a/trunk/source/BA_SiteRepository/ReqAnalyzer.product +++ b/trunk/source/BA_SiteRepository/ReqAnalyzer.product @@ -22,7 +22,7 @@ -data @user.home\ultimate-data - -Xmx4g -Xms4M -Dequinox.resolver.revision.batch.size=1 + -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target index b42d05618f0..617fd810699 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G + -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target index 7abfdfb0392..ae08f77f8bb 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G + -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 linux diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target index 36df46fafbf..a41fac3d1c8 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G + -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 macosx diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target index 35a2c5c381a..7fdfa4662e8 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G + -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 win32 diff --git a/trunk/source/BA_SiteRepository/WebBackend.product b/trunk/source/BA_SiteRepository/WebBackend.product index aeb388260d4..ec133cbd988 100644 --- a/trunk/source/BA_SiteRepository/WebBackend.product +++ b/trunk/source/BA_SiteRepository/WebBackend.product @@ -9,9 +9,7 @@ -nosplash -consoleLog - -Dosgi.noShutdown=true -Dequinox.resolver.revision.batch.size=1 --Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog --DWebBackend.SETTINGS_FILE=\path\to\web.config.properties.dist + -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 -Dosgi.noShutdown=true -Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog -DWebBackend.SETTINGS_FILE=\path\to\web.config.properties.dist From dca7cf6fc9e54832da6cb071e25f9f3d6153f287 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 22 Aug 2025 15:22:04 +0200 Subject: [PATCH 37/38] Make maximum heap and stack size configurable in run_complete_analysis.py --- .../adds/reqchecker/run_complete_analysis.py | 13 +++++++++++-- releaseScripts/default/makeSettings.sh | 12 +++++++++++- 2 files changed, 22 insertions(+), 3 deletions(-) diff --git a/releaseScripts/default/adds/reqchecker/run_complete_analysis.py b/releaseScripts/default/adds/reqchecker/run_complete_analysis.py index bbc3edbc8b4..34b69b94900 100755 --- a/releaseScripts/default/adds/reqchecker/run_complete_analysis.py +++ b/releaseScripts/default/adds/reqchecker/run_complete_analysis.py @@ -18,6 +18,14 @@ from tqdm import tqdm +# quoting style is important here +# fmt: off +memory_heap_size_init = '4M' +memory_heap_size_max = '12G' +memory_stack_size_max = '2M' +# fmt: on + + class _ExitCode: """ Specify a named exit code for global usage. @@ -716,8 +724,9 @@ def create_common_ultimate_cli_args(args, toolchain, settings, input_file): return [ "java", "-Dosgi.configuration.area=config/", - "-Xmx100G", - "-Xss4m", + "-Xms" + memory_heap_size_init, + "-Xmx" + memory_heap_size_max, + "-Xss" + memory_stack_size_max, "-jar", "plugins/org.eclipse.equinox.launcher_1.6.800.v20240513-1750.jar", "-tc", diff --git a/releaseScripts/default/makeSettings.sh b/releaseScripts/default/makeSettings.sh index a57572ca53c..0bfda13c6d4 100755 --- a/releaseScripts/default/makeSettings.sh +++ b/releaseScripts/default/makeSettings.sh @@ -106,6 +106,16 @@ setup_ultimate_product_memory() { # Replacing maximum stack memory size in Ultimate.py exit_on_fail sed -i "s/^memory_stack_size_max =.*$/memory_stack_size_max = \'${PRODUCT_MEM_STACK_MAX}\'/g" "${PRODUCT_PATH}/Ultimate.py" fi + + if [[ -f "${PRODUCT_PATH}/run_complete_analysis.py" ]]; then + echo "Setup stack and heap sizes in run_complete_analysis.py" + # Replacing maximum heap memory size in reqchecker/run_complete_analysis.py + exit_on_fail sed -i "s/^memory_heap_size_max =.*$/memory_heap_size_max = \'${PRODUCT_MEM_HEAP_MAX}\'/g" "${PRODUCT_PATH}/run_complete_analysis.py" + # Replacing initial heap memory size in reqchecker/run_complete_analysis.py + exit_on_fail sed -i "s/^memory_heap_size_init =.*$/memory_heap_size_init = \'${PRODUCT_MEM_HEAP_INIT}\'/g" "${PRODUCT_PATH}/run_complete_analysis.py" + # Replacing maximum stack memory size in reqchecker/run_complete_analysis.py + exit_on_fail sed -i "s/^memory_stack_size_max =.*$/memory_stack_size_max = \'${PRODUCT_MEM_STACK_MAX}\'/g" "${PRODUCT_PATH}/run_complete_analysis.py" + fi } get_cmd_version() { @@ -215,4 +225,4 @@ get_ult_version(){ exit 1 fi spopd -} \ No newline at end of file +} From d98f0337f7427344e0babeb60d4c5a09c426c2c9 Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 22 Aug 2025 15:39:53 +0200 Subject: [PATCH 38/38] Change the default memory sizes of the Java Runtime for Ultimate products The standard memory sizes of the Java Runtime for Ultimate products are uniformly set to the following values: - Initial heap memory size: 2M - Maximum heap memory size: 4G - Maximum stack memory size: 1M If other memory sizes are required, these can be configured for each build of Ultimate products. The Ultimate products for the SV-COMP should be built with the following settings: ./makeBuild.sh -i 2M -m 15G -s 1M On the other hand, the ReqCheck product for analyzing large requirement sets should be built with the following settings: ./makeBuild.sh -i 2M -m 100G -s 4M --- Jenkinsfile.nightly | 8 ++++---- packaging/docker/Dockerfile | 6 +++--- packaging/docker/docker-compose.yml | 12 ++++++------ packaging/docker/ultimate-webservice.env | 6 +++--- releaseScripts/default/adds/UltDelta.py | 5 +++-- releaseScripts/default/adds/Ultimate.py | 6 +++--- .../default/adds/reqchecker/run_complete_analysis.py | 6 +++--- releaseScripts/default/adds/run-ultimate.sh | 5 +++-- releaseScripts/default/makeBuild.sh | 6 +++--- trunk/source/BA_MavenParentUltimate/pom.xml | 6 +++--- trunk/source/BA_SiteRepository/CLI-E4.product | 2 +- trunk/source/BA_SiteRepository/Debug-E4.product | 2 +- trunk/source/BA_SiteRepository/DeltaDebugger.product | 2 +- trunk/source/BA_SiteRepository/Eliminator.product | 2 +- trunk/source/BA_SiteRepository/ReqAnalyzer.product | 2 +- .../BA_SiteRepository/Ultimate_E4.32_Java21.target | 2 +- .../Ultimate_E4.32_Java21_Linux.target | 2 +- .../Ultimate_E4.32_Java21_MacOS.target | 2 +- .../Ultimate_E4.32_Java21_Win32.target | 2 +- trunk/source/BA_SiteRepository/WebBackend.product | 2 +- .../source/BA_SiteRepository/nodeploy/CDT-E4.product | 2 +- trunk/source/WebsiteStatic/_tools/ltl_automizer.html | 4 ++-- 22 files changed, 47 insertions(+), 45 deletions(-) diff --git a/Jenkinsfile.nightly b/Jenkinsfile.nightly index 01ed0e08e75..5f6bb31639c 100644 --- a/Jenkinsfile.nightly +++ b/Jenkinsfile.nightly @@ -85,11 +85,11 @@ pipeline { } } steps { - withMaven(mavenOpts: '-Xmx4g -Xss4m -ea', options: [artifactsPublisher(disabled: true), junitPublisher(healthScaleFactor: 1.0, keepLongStdio: true, skipPublishingChecks: false)]) { + withMaven(mavenOpts: '-Xmx4G -Xss4M -ea', options: [artifactsPublisher(disabled: true), junitPublisher(healthScaleFactor: 1.0, keepLongStdio: true, skipPublishingChecks: false)]) { sh 'cd trunk/source/BA_MavenParentUltimate && mvn -T 1C clean install -Pcoverage -Dmaven.test.failure.ignore=true -DexcludedGroups=de.uni_freiburg.informatik.ultimate.test.junitextension.categories.NoRegression' } // TODO: Fix Jenkins coverage - // withEnv(['JAVA_ARGS="-Xmx4g"']) { + // withEnv(['JAVA_ARGS="-Xmx4G"']) { // recordCoverage(tools: [[parser: 'JACOCO', pattern: '**/target/site/jacoco-aggregate/jacoco.xml']]) // } } @@ -117,7 +117,7 @@ pipeline { } steps { withCredentials([string(credentialsId: 'SonarTokenJenkinsPipeline', variable: 'SONAR_TOKEN')]) { - withMaven(mavenOpts: '-Xmx4g -Xss4m', publisherStrategy: 'EXPLICIT', traceability: true) { + withMaven(mavenOpts: '-Xmx4G -Xss4M', publisherStrategy: 'EXPLICIT', traceability: true) { sh 'cd trunk/source/BA_MavenParentUltimate && mvn install -Psonar -Dsonar.host.url=https://sonar.sopranium.de -Dsonar.token=$SONAR_TOKEN' } } @@ -132,7 +132,7 @@ pipeline { } } steps { - withMaven(mavenOpts: '-Xmx4g -Xss4m', publisherStrategy: 'EXPLICIT') { + withMaven(mavenOpts: '-Xmx4G -Xss4M', publisherStrategy: 'EXPLICIT') { sh 'cd releaseScripts/default && ./makeFresh.sh' } sshagent(credentials: ['jenkins-deploy']) { diff --git a/packaging/docker/Dockerfile b/packaging/docker/Dockerfile index 8f467173c0e..20ff026a9d5 100644 --- a/packaging/docker/Dockerfile +++ b/packaging/docker/Dockerfile @@ -26,9 +26,9 @@ FROM alpine:3 AS build-products ARG REPO_URL="https://github.com/ultimate-pa/ultimate.git" ARG REPO_BRANCH="dev" -ARG ULTIMATE_MEMORY_HEAP_INIT="4M" -ARG ULTIMATE_MEMORY_HEAP_MAX="12G" -ARG ULTIMATE_MEMORY_STACK_MAX="512M" +ARG ULTIMATE_MEMORY_HEAP_INIT="2M" +ARG ULTIMATE_MEMORY_HEAP_MAX="4G" +ARG ULTIMATE_MEMORY_STACK_MAX="1M" ARG REPO_DIR_BUILD ARG DIR_BUILD diff --git a/packaging/docker/docker-compose.yml b/packaging/docker/docker-compose.yml index e44136a3818..1c9f132adcb 100644 --- a/packaging/docker/docker-compose.yml +++ b/packaging/docker/docker-compose.yml @@ -7,9 +7,9 @@ services: target: "ultimate-webbackend" args: ULTIMATE_DIR_TMP: "${ULTIMATE_DIR_TMP-/tmp/ultimate}" - ULTIMATE_MEMORY_HEAP_INIT: ${ULTIMATE_MEMORY_HEAP_INIT-4M} - ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-12G}" - ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-512M}" + ULTIMATE_MEMORY_HEAP_INIT: ${ULTIMATE_MEMORY_HEAP_INIT-2M} + ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-4G}" + ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-1M}" image: "ultimate-webbackend" environment: ULTIMATE_BACKEND_HOST: "${ULTIMATE_BACKEND_HOST-localhost}" @@ -28,9 +28,9 @@ services: target: "ultimate-webfrontend" args: ULTIMATE_FRONTEND_BASEURL: "${ULTIMATE_FRONTEND_ROUTE-/website}" - ULTIMATE_MEMORY_HEAP_INIT: ${ULTIMATE_MEMORY_HEAP_INIT-4M} - ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-12G}" - ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-512M}" + ULTIMATE_MEMORY_HEAP_INIT: ${ULTIMATE_MEMORY_HEAP_INIT-2M} + ULTIMATE_MEMORY_HEAP_MAX: "${ULTIMATE_MEMORY_HEAP_MAX-4G}" + ULTIMATE_MEMORY_STACK_MAX: "${ULTIMATE_MEMORY_STACK_MAX-1M}" image: "ultimate-webfrontend" environment: ULTIMATE_FRONTEND_DEBUG: "${ULTIMATE_FRONTEND_DEBUG-false}" diff --git a/packaging/docker/ultimate-webservice.env b/packaging/docker/ultimate-webservice.env index bf06d173927..0918a0ef094 100644 --- a/packaging/docker/ultimate-webservice.env +++ b/packaging/docker/ultimate-webservice.env @@ -23,6 +23,6 @@ ULTIMATE_LOG_LEVEL=INFO ULTIMATE_DIR_TMP=/tmp/ultimate ULTIMATE_TIMEOUT=90 -ULTIMATE_MEMORY_HEAP_INIT=4M -ULTIMATE_MEMORY_HEAP_MAX=12G -ULTIMATE_MEMORY_STACK_MAX=512M +ULTIMATE_MEMORY_HEAP_INIT=2M +ULTIMATE_MEMORY_HEAP_MAX=4G +ULTIMATE_MEMORY_STACK_MAX=1M diff --git a/releaseScripts/default/adds/UltDelta.py b/releaseScripts/default/adds/UltDelta.py index e9329f91d46..7972119b763 100755 --- a/releaseScripts/default/adds/UltDelta.py +++ b/releaseScripts/default/adds/UltDelta.py @@ -56,8 +56,9 @@ def get_binary(): ultimate_bin = [ "java", "-Dosgi.configuration.area=" + os.path.join(datadir, "config"), - "-Xmx12G", - "-Xms4m", + "-Xms2M", + "-Xmx4G", + "-Xms1M", ] if enable_assertions: diff --git a/releaseScripts/default/adds/Ultimate.py b/releaseScripts/default/adds/Ultimate.py index 80aca83e45e..d9d4eb29772 100755 --- a/releaseScripts/default/adds/Ultimate.py +++ b/releaseScripts/default/adds/Ultimate.py @@ -20,9 +20,9 @@ # fmt: off version = '4f54f8f5' toolname = 'Automizer' -memory_heap_size_init = '4M' -memory_heap_size_max = '12G' -memory_stack_size_max = '512M' +memory_heap_size_init = '2M' +memory_heap_size_max = '4G' +memory_stack_size_max = '1M' # fmt: on write_ultimate_output_to_file = True diff --git a/releaseScripts/default/adds/reqchecker/run_complete_analysis.py b/releaseScripts/default/adds/reqchecker/run_complete_analysis.py index 34b69b94900..ebec1901590 100755 --- a/releaseScripts/default/adds/reqchecker/run_complete_analysis.py +++ b/releaseScripts/default/adds/reqchecker/run_complete_analysis.py @@ -20,9 +20,9 @@ # quoting style is important here # fmt: off -memory_heap_size_init = '4M' -memory_heap_size_max = '12G' -memory_stack_size_max = '2M' +memory_heap_size_init = '2M' +memory_heap_size_max = '4G' +memory_stack_size_max = '1M' # fmt: on diff --git a/releaseScripts/default/adds/run-ultimate.sh b/releaseScripts/default/adds/run-ultimate.sh index 68b1460b339..f70dccaf5ae 100755 --- a/releaseScripts/default/adds/run-ultimate.sh +++ b/releaseScripts/default/adds/run-ultimate.sh @@ -2,8 +2,9 @@ # small script to wrap common Ultimate startup things java \ -Dosgi.configuration.area=config/ \ --Xmx10G \ --Xss4m \ +-Xms2M \ +-Xmx4G \ +-Xss1M \ -jar plugins/org.eclipse.equinox.launcher_1.6.800.v20240513-1750.jar \ -data config/data \ "$@" diff --git a/releaseScripts/default/makeBuild.sh b/releaseScripts/default/makeBuild.sh index 4be701771d5..1b5ae4c83d6 100755 --- a/releaseScripts/default/makeBuild.sh +++ b/releaseScripts/default/makeBuild.sh @@ -14,11 +14,11 @@ source "${DIR}/semver2.sh" # Default platforms for the build of Ultimate PLATFORMS=("linux" "win32") # Default initial heap memory size for Ultimate products -MEM_HEAP_INIT_SIZE="4M" +MEM_HEAP_INIT_SIZE="2M" # Default maximum heap memory size for Ultimate products -MEM_HEAP_MAX_SIZE="12G" +MEM_HEAP_MAX_SIZE="4G" # Default maximum stack memory size for Ultimate products -MEM_STACK_MAX_SIZE="512M" +MEM_STACK_MAX_SIZE="1M" _print_help() { printf 'Usage: %s [-i ] [-m ] [-s ] [-p all|linux|win32] [-h]\n' "${0}" diff --git a/trunk/source/BA_MavenParentUltimate/pom.xml b/trunk/source/BA_MavenParentUltimate/pom.xml index 89202f598bd..ad72d232383 100644 --- a/trunk/source/BA_MavenParentUltimate/pom.xml +++ b/trunk/source/BA_MavenParentUltimate/pom.xml @@ -164,8 +164,8 @@ - -Xmx4g - -Xmx4g -ea + -Xmx4G + -Xmx4G -ea @@ -604,4 +604,4 @@ - \ No newline at end of file + diff --git a/trunk/source/BA_SiteRepository/CLI-E4.product b/trunk/source/BA_SiteRepository/CLI-E4.product index b4459d0e1db..a84438febd5 100644 --- a/trunk/source/BA_SiteRepository/CLI-E4.product +++ b/trunk/source/BA_SiteRepository/CLI-E4.product @@ -21,7 +21,7 @@ -data @user.home\ultimate-data - -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Debug-E4.product b/trunk/source/BA_SiteRepository/Debug-E4.product index 09408842b33..10f8249396d 100644 --- a/trunk/source/BA_SiteRepository/Debug-E4.product +++ b/trunk/source/BA_SiteRepository/Debug-E4.product @@ -22,7 +22,7 @@ -data @user.home\ultimate-data - -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/DeltaDebugger.product b/trunk/source/BA_SiteRepository/DeltaDebugger.product index 47c00c20963..3689c4fd5c5 100644 --- a/trunk/source/BA_SiteRepository/DeltaDebugger.product +++ b/trunk/source/BA_SiteRepository/DeltaDebugger.product @@ -21,7 +21,7 @@ -data @user.home\ultimate-data - -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Eliminator.product b/trunk/source/BA_SiteRepository/Eliminator.product index 7c821ddde48..c2319a7a5a9 100644 --- a/trunk/source/BA_SiteRepository/Eliminator.product +++ b/trunk/source/BA_SiteRepository/Eliminator.product @@ -21,7 +21,7 @@ -data @user.home\ultimate-data - -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/ReqAnalyzer.product b/trunk/source/BA_SiteRepository/ReqAnalyzer.product index 964705d89cb..0e6dad57a6c 100644 --- a/trunk/source/BA_SiteRepository/ReqAnalyzer.product +++ b/trunk/source/BA_SiteRepository/ReqAnalyzer.product @@ -22,7 +22,7 @@ -data @user.home\ultimate-data - -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target index 617fd810699..acfb6357729 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -ea -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target index ae08f77f8bb..263e4a327a8 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Linux.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -ea -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 linux diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target index a41fac3d1c8..141bc4ead0c 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_MacOS.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -ea -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 macosx diff --git a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target index 7fdfa4662e8..d467b1d9114 100644 --- a/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target +++ b/trunk/source/BA_SiteRepository/Ultimate_E4.32_Java21_Win32.target @@ -2,7 +2,7 @@ - -ea -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 + -ea -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 win32 diff --git a/trunk/source/BA_SiteRepository/WebBackend.product b/trunk/source/BA_SiteRepository/WebBackend.product index ec133cbd988..0ddb4d48ab9 100644 --- a/trunk/source/BA_SiteRepository/WebBackend.product +++ b/trunk/source/BA_SiteRepository/WebBackend.product @@ -9,7 +9,7 @@ -nosplash -consoleLog - -Xms4M -Xmx4G -Xss2M -Dequinox.resolver.revision.batch.size=1 -Dosgi.noShutdown=true -Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog -DWebBackend.SETTINGS_FILE=\path\to\web.config.properties.dist + -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 -Dosgi.noShutdown=true -Dorg.eclipse.jetty.util.log.class=org.eclipse.jetty.util.log.StdErrLog -DWebBackend.SETTINGS_FILE=\path\to\web.config.properties.dist diff --git a/trunk/source/BA_SiteRepository/nodeploy/CDT-E4.product b/trunk/source/BA_SiteRepository/nodeploy/CDT-E4.product index 7504e7fe71d..67bde1fb706 100644 --- a/trunk/source/BA_SiteRepository/nodeploy/CDT-E4.product +++ b/trunk/source/BA_SiteRepository/nodeploy/CDT-E4.product @@ -16,7 +16,7 @@ -consoleLog -nosplash - -Xms256m -Xmx1024m + -Xms2M -Xmx4G -Xss1M diff --git a/trunk/source/WebsiteStatic/_tools/ltl_automizer.html b/trunk/source/WebsiteStatic/_tools/ltl_automizer.html index 862d40e26df..5b70f477989 100644 --- a/trunk/source/WebsiteStatic/_tools/ltl_automizer.html +++ b/trunk/source/WebsiteStatic/_tools/ltl_automizer.html @@ -97,9 +97,9 @@

Interpreting results

The results under Results from de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer: contain the actual result, i.e. in this example, Büchi Automizer proved that the LTL property F(G(A)) holds says that the property was proven successfully.

Changing time and memory limits

-

This version of LTL Automizer comes with a pre-set timeout of 20 minutes and Java heap space set to 8GB.
+

This version of LTL Automizer comes with a pre-set timeout of 20 minutes and Java heap space set to 4GB.
If you wish to change the timeout, you must edit Default.epf, search the line /instance/UltimateCore/Toolchain\ timeout\ in\ seconds=1200 and change the 1200 to something else. 0 disables the timeout.
-If you want to change the heap space limit, you must edit Ultimate.ini and change the line -Xmx8g to something more appropriate. +If you want to change the heap space limit, you must edit Ultimate.ini and change the line -Xmx4G to something more appropriate.