diff --git a/.gitignore b/.gitignore index 62178d2fecb..be1b4e39517 100644 --- a/.gitignore +++ b/.gitignore @@ -10,10 +10,18 @@ hs_err_pid* *.md.backup -/releaseScripts/default/DeltaDebugger-linux/* -/releaseScripts/default/DeltaDebugger-win32/* +/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/* /releaseScripts/default/UAutomizer-win32/* +/releaseScripts/default/UEliminator-linux/* +/releaseScripts/default/UEliminator-win32/* /releaseScripts/default/UGemCutter-linux/* /releaseScripts/default/UGemCutter-win32/* /releaseScripts/default/UKojak-linux/* @@ -24,7 +32,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/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 new file mode 100644 index 00000000000..20ff026a9d5 --- /dev/null +++ b/packaging/docker/Dockerfile @@ -0,0 +1,518 @@ +#------------------------------------------------------------------------------ +# Dockerfile: compile and package Ultimate products +#------------------------------------------------------------------------------ +# Author: Manuel Bentele +# Copyright (c) 2023 +#------------------------------------------------------------------------------ +# common build arguments for multi-staged Docker build +#------------------------------------------------------------------------------ +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_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 build Ultimate products +#------------------------------------------------------------------------------ +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="2M" +ARG ULTIMATE_MEMORY_HEAP_MAX="4G" +ARG ULTIMATE_MEMORY_STACK_MAX="1M" + +ARG REPO_DIR_BUILD +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_BUILD + +# install build dependencies for an entire Ultimate build +RUN apk add --no-cache "bash" \ + "git" \ + "maven" \ + "openjdk21" + +# 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 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 +#------------------------------------------------------------------------------ +FROM build-products AS build-webfrontend + +ARG ULTIMATE_FRONTEND_BASEURL="/website" + +ARG REPO_DIR_FRONTEND +ARG REPO_DIR_BUILD +ARG DIR_BUILD +ARG DIR_ULTIMATE +ARG DIR_OUTPUT_BUILD + +# 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_DIR_FRONTEND}" +ENV PATH="${DIR_OUTPUT_BUILD}/UCLI-E4-linux:${PATH}" +RUN python3 scripts/build.py --baseurl "${ULTIMATE_FRONTEND_BASEURL}" + +#------------------------------------------------------------------------------ +# 2nd build stage: package common Ultimate artifacts shared by all products +#------------------------------------------------------------------------------ +FROM alpine:3 AS ultimate-common + +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 runtime dependencies for all Ultimate products +RUN apk add --no-cache "libc6-compat" \ + "openjdk21-jre-headless" + +# 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}" + +# make Ultimate executable, scripts, and solvers available +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 + +# 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 +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-cli + +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 CLI product +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}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] + +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate Debug UI +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-debug + +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 graphical dependencies for Ultimate Debug UI product +RUN apk add --no-cache "openjdk21-jre" \ + "libcanberra-gtk3" \ + "dbus-x11" \ + "ttf-freefont" \ + "xauth" + +# install already built Ultimate Debug UI product +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}" + +# default entry point to print installed Ultimate version +ENTRYPOINT ["/bin/sh", "-l"] + +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate Automizer +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-automizer + +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 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 Automizer 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 DeltaDebugger +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-deltadebugger + +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 DeltaDebugger product +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"] + +#------------------------------------------------------------------------------ +# 3rd build stage: package Ultimate Eliminator +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-eliminator + +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 Eliminator product +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}" + +# 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 +#------------------------------------------------------------------------------ +FROM ultimate-common AS ultimate-webbackend + +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 + +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_LOG_PATH="/dev/stdout" +ENV ULTIMATE_LOG_LEVEL="INFO" +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" \ + "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" + +# install already built Ultimate WebBackend product +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-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" + +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}" + +# 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 + +# 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/README.md b/packaging/docker/README.md new file mode 100644 index 00000000000..ba6670b9d3c --- /dev/null +++ b/packaging/docker/README.md @@ -0,0 +1,79 @@ +# 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 --platform linux/amd64 --tag --target . +``` + +where `PRODUCT` is a placeholder for one of the pre-configured products + + - `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. + +> [!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 +``` +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 + -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. + +> [!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. +```shell +docker run -it --network host \ + -e DISPLAY=$DISPLAY \ + -v :/home/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. + + +## 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-webservice.env` file. +After optional adjustment of the configuration, the setup can be provisioned using Docker Compose: +```shell +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/WebBackend.ini.tpl b/packaging/docker/WebBackend.ini.tpl new file mode 100644 index 00000000000..56505c71540 --- /dev/null +++ b/packaging/docker/WebBackend.ini.tpl @@ -0,0 +1,10 @@ +-startup +plugins/org.eclipse.equinox.launcher_1.6.800.v20240513-1750.jar +--launcher.library +plugins/org.eclipse.equinox.launcher.gtk.linux.x86_64_1.2.1000.v20240506-2123 +-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/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 new file mode 100644 index 00000000000..1c9f132adcb --- /dev/null +++ b/packaging/docker/docker-compose.yml @@ -0,0 +1,51 @@ +version: "2" + +services: + ultimate-webbackend: + build: + dockerfile: "Dockerfile" + target: "ultimate-webbackend" + args: + ULTIMATE_DIR_TMP: "${ULTIMATE_DIR_TMP-/tmp/ultimate}" + 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}" + 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:${ULTIMATE_BACKEND_PORT-8080}" + restart: "unless-stopped" + + ultimate-webfrontend: + build: + dockerfile: "Dockerfile" + target: "ultimate-webfrontend" + args: + ULTIMATE_FRONTEND_BASEURL: "${ULTIMATE_FRONTEND_ROUTE-/website}" + 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}" + ULTIMATE_FRONTEND_MSG_ORIENTATION: "${ULTIMATE_FRONTEND_MSG_ORIENTATION-left}" + ULTIMATE_FRONTEND_PROTOCOL: "${ULTIMATE_FRONTEND_PROTOCOL-http}" + 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}" + ULTIMATE_BACKEND_HOST: "${ULTIMATE_BACKEND_HOST-localhost}" + ULTIMATE_BACKEND_PORT: "${ULTIMATE_BACKEND_PORT-8080}" + ULTIMATE_BACKEND_ROUTE: "${ULTIMATE_BACKEND_ROUTE-/api}" + ports: + - "80:${ULTIMATE_FRONTEND_PORT-80}" + restart: "unless-stopped" + depends_on: + ultimate-webbackend: + condition: service_healthy diff --git a/packaging/docker/ultimate-webservice.env b/packaging/docker/ultimate-webservice.env new file mode 100644 index 00000000000..0918a0ef094 --- /dev/null +++ b/packaging/docker/ultimate-webservice.env @@ -0,0 +1,28 @@ +########################################################################################################## +# Environment variables for 'ultimate-webfrontend' and 'ultimate-webbackend' 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 + +ULTIMATE_LOG_PATH=/dev/stdout +ULTIMATE_LOG_LEVEL=INFO + +ULTIMATE_DIR_TMP=/tmp/ultimate +ULTIMATE_TIMEOUT=90 + +ULTIMATE_MEMORY_HEAP_INIT=2M +ULTIMATE_MEMORY_HEAP_MAX=4G +ULTIMATE_MEMORY_STACK_MAX=1M 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 }} diff --git a/packaging/docker/welcome.sh b/packaging/docker/welcome.sh new file mode 100755 index 00000000000..3bb187ef2f4 --- /dev/null +++ b/packaging/docker/welcome.sh @@ -0,0 +1,34 @@ +#!/bin/sh + +ULTIMATE_CONFIG_PATH="/home/ultimate/config" + +check_and_print_version() { + for cmd in "${@}"; do + if command -v "${cmd}" >/dev/null 2>&1; then + "${cmd}" --version + return + fi + 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: ${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 "▐▌ ▐▌▐▌ █ █ ▐▌ ▐▌▐▛▀▜▌ █ ▐▛▀▀▘" +echo "▝▚▄▞▘▐▙▄▄▖█ ▗▄█▄▖▐▌ ▐▌▐▌ ▐▌ █ ▐▙▄▄▖" +echo "┏━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓" +echo "┃ Program Analysis Framework ┃" +echo "┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛" +check_and_print_version "Ultimate" "UltimateDebug" "ReqAnalyzer" "WebBackend" +echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━" +check_and_print_config +echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━" 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.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/adds/Ultimate.py b/releaseScripts/default/adds/Ultimate.py index e21fa8ac790..d9d4eb29772 100755 --- a/releaseScripts/default/adds/Ultimate.py +++ b/releaseScripts/default/adds/Ultimate.py @@ -20,6 +20,9 @@ # fmt: off version = '4f54f8f5' toolname = 'Automizer' +memory_heap_size_init = '2M' +memory_heap_size_max = '4G' +memory_stack_size_max = '1M' # fmt: on write_ultimate_output_to_file = True @@ -281,8 +284,9 @@ def create_ultimate_base_call(): ultimate_bin = [ get_java(), "-Dosgi.configuration.area=" + os.path.join(datadir, "config"), - "-Xmx15G", - "-Xms4m", + "-Xms" + memory_heap_size_init, + "-Xmx" + memory_heap_size_max, + "-Xss" + memory_stack_size_max, ] if enable_assertions: diff --git a/releaseScripts/default/adds/reqchecker/run_complete_analysis.py b/releaseScripts/default/adds/reqchecker/run_complete_analysis.py index bbc3edbc8b4..ebec1901590 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 = '2M' +memory_heap_size_max = '4G' +memory_stack_size_max = '1M' +# 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/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/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..1b5ae4c83d6 --- /dev/null +++ b/releaseScripts/default/makeBuild.sh @@ -0,0 +1,201 @@ +#!/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" + +# Default platforms for the build of Ultimate +PLATFORMS=("linux" "win32") +# Default initial heap memory size for Ultimate products +MEM_HEAP_INIT_SIZE="2M" +# Default maximum heap memory size for Ultimate products +MEM_HEAP_MAX_SIZE="4G" +# Default maximum stack memory size for Ultimate products +MEM_STACK_MAX_SIZE="1M" + +_print_help() { + 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' + 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 "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}" + ;; + s) + _validate_memory_size "-s" "${OPTARG}" + MEM_STACK_MAX_SIZE="${OPTARG}" + ;; + 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 + _print_help + exit 1 + ;; + esac + ;; + h) + print_newline + _print_help + exit 0 + ;; + *) + print_newline + _print_help + exit 1 + ;; + esac + done +} + +build_init() { + printf '▗▄▄▖ ▗▖ ▗▖▗▄▄▄▖▗▖ ▗▄▄▄ \n' + printf '▐▌ ▐▌▐▌ ▐▌ █ ▐▌ ▐▌ █\n' + printf '▐▛▀▚▖▐▌ ▐▌ █ ▐▌ ▐▌ █\n' + printf '▐▙▄▞▘▝▚▄▞▘▗▄█▄▖▐▙▄▄▖▐▙▄▄▀\n' + printf '┏━━━━━━━━━━━━━━━━━━━━━━━┓\n' + printf '┃ Ultimate Products ┃\n' + printf '┗━━━━━━━━━━━━━━━━━━━━━━━┛\n' + print_newline +} + +build_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_run() { + 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 "Using the configuration for Ultimate" + 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" + exit_on_fail mvn -T 1C clean install -Pmaterialize + print_newline + + spopd +} + +build_package() { + for PLATFORM in "${PLATFORMS[@]}"; do + # makePackageConfig.sh + print_heading "Package Ultimate Taipan [${PLATFORM}]" + 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_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_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_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_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${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" "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_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_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_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_INIT_SIZE}" "${MEM_HEAP_MAX_SIZE}" "${MEM_STACK_MAX_SIZE}" "${PLATFORM}" + print_newline + + # makePackageReqCheck.sh + print_heading "Package Ultimate ReqCheck [${PLATFORM}]" + 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 +} + +build_parseopts "${@}" +build_init +build_check +build_run +build_package diff --git a/releaseScripts/default/makeFresh.sh b/releaseScripts/default/makeFresh.sh index 0491f1d9973..7fd3c02a0a3 100755 --- a/releaseScripts/default/makeFresh.sh +++ b/releaseScripts/default/makeFresh.sh @@ -1,75 +1,77 @@ #!/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" +if [[ ! -d "${DIR}" ]]; then DIR="${PWD}"; fi +source "${DIR}/makeSettings.sh" -verlte() { - printf '%s\n%s' "$1" "$2" | sort -C -V -} +# Load and execute all Ultimate build steps before archive function is called. +source "${DIR}/makeBuild.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 +archive_init() { + printf ' ▗▄▖ ▗▄▄▖ ▗▄▄▖▗▖ ▗▖▗▄▄▄▖▗▖ ▗▖▗▄▄▄▖\n' + printf '▐▌ ▐▌▐▌ ▐▌▐▌ ▐▌ ▐▌ █ ▐▌ ▐▌▐▌ \n' + printf '▐▛▀▜▌▐▛▀▚▖▐▌ ▐▛▀▜▌ █ ▐▌ ▐▌▐▛▀▀▘\n' + printf '▐▌ ▐▌▐▌ ▐▌▝▚▄▄▖▐▌ ▐▌▗▄█▄▖ ▝▚▞▘ ▐▙▄▄▖\n' + printf '┏━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓\n' + printf '┃ Ultimate Products ┃\n' + printf '┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛\n' + print_newline } -create_tool_zips() { - 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 +archive_run() { + for PLATFORM in "${PLATFORMS[@]}"; do + # makeZip.sh + print_heading "Archive Ultimate Taipan [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Taipan" "${PLATFORM}" + print_newline - # 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 + print_heading "Archive Ultimate Automizer [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Automizer" "${PLATFORM}" + print_newline - # 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 + print_heading "Archive Ultimate Kojak [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Kojak" "${PLATFORM}" + print_newline - # Kojak - exit_on_fail bash makeZip.sh Kojak $platform KojakC_WitnessPrinter.xml NONE NONE KojakC_WitnessPrinter.xml NONE NONE + print_heading "Archive Ultimate GemCutter [${PLATFORM}]" + exit_on_fail bash makeZip.sh "GemCutter" "${PLATFORM}" + print_newline - # GemCutter - exit_on_fail bash makeZip.sh GemCutter $platform AutomizerCInline_WitnessPrinter.xml NONE AutomizerCInline.xml AutomizerCInline_WitnessPrinter.xml NONE NONE + print_heading "Archive Ultimate Referee [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Referee" "${PLATFORM}" + print_newline - # Referee - exit_on_fail bash makeZip.sh Referee $platform RefereeCInline.xml NONE RefereeCInline_IcfgBuilder.xml NONE NONE NONE + print_heading "Archive Ultimate DeltaDebugger [${PLATFORM}]" + exit_on_fail bash makeZip.sh "DeltaDebugger" "${PLATFORM}" + print_newline - # DeltaDebugger - exit_on_fail bash createDeltaDebuggerDir.sh $platform + print_heading "Archive Ultimate Eliminator [${PLATFORM}]" + exit_on_fail bash makeZip.sh "Eliminator" "${PLATFORM}" + print_newline - # ReqCheck - exit_on_fail bash createReqCheckZip.sh ReqCheck $platform ReqCheck.xml ReqCheck.xml - done -} + print_heading "Archive Ultimate WebBackend [${PLATFORM}]" + exit_on_fail bash makeZip.sh "WebBackend" "${PLATFORM}" + print_newline -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" + 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 makeZip.sh "Debug-E4" "${PLATFORM}" + print_newline + done } -build -create_tool_zips -create_webbackend_dir +archive_init +archive_run diff --git a/releaseScripts/default/makePackageConfig.sh b/releaseScripts/default/makePackageConfig.sh new file mode 100755 index 00000000000..6994aac0952 --- /dev/null +++ b/releaseScripts/default/makePackageConfig.sh @@ -0,0 +1,147 @@ +#!/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 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 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 + +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/LICENSE.GPL" + "adds/LICENSE.GPL.LESSER" + "adds/z3-LICENSE" + "adds/cvc4-LICENSE" + "adds/mathsat-LICENSE" + "adds/ltl2ba-LICENSE" + "adds/Ultimate.py" + "adds/README" +) + +# Architecture-specific variables +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 [ "${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: ""${6}"" -- 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 "${7}" -a ! "NONE" = "${7}" ]; then + TOOLCHAIN="../../trunk/examples/toolchains/${7}" +else + echo "No reach toolchain specified, ommitting..." + TOOLCHAIN="" +fi + +if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then + TERMTOOLCHAIN="../../trunk/examples/toolchains/${8}" +else + echo "No termination toolchain specified, ommitting..." + TERMTOOLCHAIN="" +fi + +if [ ! -z "${9}" -a ! "NONE" = "${9}" ]; then + VALTOOLCHAIN="../../trunk/examples/toolchains/${9}" +else + echo "No witness validation toolchain specified, ommitting..." + VALTOOLCHAIN="" +fi + +if [ ! -z "${10}" -a ! "NONE" = "${10}" ]; then + MEMDEREFMEMTRACKTOOLCHAIN="../../trunk/examples/toolchains/${10}" +else + echo "No memory deref toolchain specified, ommitting..." + MEMDEREFMEMTRACKTOOLCHAIN="" +fi + +if [ ! -z "${11}" -a ! "NONE" = "${11}" ]; then + LTLTOOLCHAIN="../../trunk/examples/toolchains/${11}" +else + echo "No LTL toolchain specified, ommitting..." + LTLTOOLCHAIN="" +fi + +if [ ! -z "${12}" -a ! "NONE" = "${12}" ]; then + TERMVALTOOLCHAIN="../../trunk/examples/toolchains/${12}" +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 + exit_on_fail cp "${add}" "${TARGETDIR}/" +done + +setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" "${5}" diff --git a/releaseScripts/default/makePackageReqCheck.sh b/releaseScripts/default/makePackageReqCheck.sh new file mode 100644 index 00000000000..59da159114f --- /dev/null +++ b/releaseScripts/default/makePackageReqCheck.sh @@ -0,0 +1,111 @@ +#!/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 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 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 + +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/LICENSE.GPL" + "adds/LICENSE.GPL.LESSER" + "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 [ "${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 [ "${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: ""${6}"" -- 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 "${7}" -a ! "NONE" = "${7}" ]; then + TOOLCHAIN="../../trunk/examples/toolchains/${7}" +else + echo "No reach toolchain specified, ommitting..." + TOOLCHAIN= +fi + +if [ ! -z "${8}" -a ! "NONE" = "${8}" ]; then + TESTTOOLCHAIN="../../trunk/examples/toolchains/${8}" +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 + exit_on_fail cp "${add}" "${TARGETDIR}/" +done + +setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" "${5}" diff --git a/releaseScripts/default/makePackageSmall.sh b/releaseScripts/default/makePackageSmall.sh new file mode 100755 index 00000000000..886ad59d003 --- /dev/null +++ b/releaseScripts/default/makePackageSmall.sh @@ -0,0 +1,91 @@ +#!/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 [ "${#}" -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 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 + +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/LICENSE.GPL" + "adds/LICENSE.GPL.LESSER" + "adds/z3-LICENSE" + "adds/cvc4-LICENSE" + "adds/mathsat-LICENSE" + "adds/ltl2ba-LICENSE" + "adds/Ultimate.py" + "adds/README" +) + +# Architecture-specific variables +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 [ "${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: ""${6}"" -- 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 + exit_on_fail cp "${add}" "${TARGETDIR}/" +done + +setup_ultimate_product_info "${TARGETDIR}" "${2}" "${TOOLNAME}" "${VERSION}" +setup_ultimate_product_memory "${TARGETDIR}" "${2}" "${3}" "${4}" "${5}" diff --git a/releaseScripts/default/makeSettings.sh b/releaseScripts/default/makeSettings.sh index d27accf186f..0bfda13c6d4 100755 --- a/releaseScripts/default/makeSettings.sh +++ b/releaseScripts/default/makeSettings.sh @@ -45,6 +45,110 @@ 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 +} + +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_INIT="${3}" + local PRODUCT_MEM_HEAP_MAX="${4}" + local PRODUCT_MEM_STACK_MAX="${5}" + + if [[ -f "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" ]]; then + 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/^-Xss.*$/-Xss${PRODUCT_MEM_STACK_MAX}/g" "${PRODUCT_PATH}/${PRODUCT_LAUNCHER}.ini" + fi + + if [[ -f "${PRODUCT_PATH}/Ultimate.py" ]]; then + 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 + + 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() { + ${@} | grep -m1 -Eo "([[:digit:]]+\.)+[[:digit:]]+" +} + +print_cmd_version() { + local CMD_VERS="${1}" + local CMD_NAME="${2}" + + 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' +} + +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; } } @@ -121,4 +225,4 @@ get_ult_version(){ exit 1 fi spopd -} \ No newline at end of file +} 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 +} 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 303f35d6bd7..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 - -Xmx4g -Xms4M -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 0923608b9ef..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 - -Xmx4g -Xms4M -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 32a6f122c07..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 - -Xmx4g -Xms4M -Dequinox.resolver.revision.batch.size=1 + -Xms2M -Xmx4G -Xss1M -Dequinox.resolver.revision.batch.size=1 diff --git a/trunk/source/BA_SiteRepository/UltimateEliminator.product b/trunk/source/BA_SiteRepository/Eliminator.product similarity index 92% rename from trunk/source/BA_SiteRepository/UltimateEliminator.product rename to trunk/source/BA_SiteRepository/Eliminator.product index 65a1b12a2b4..c2319a7a5a9 100644 --- a/trunk/source/BA_SiteRepository/UltimateEliminator.product +++ b/trunk/source/BA_SiteRepository/Eliminator.product @@ -1,7 +1,7 @@ - + @@ -21,7 +21,7 @@ -data @user.home\ultimate-data - -Xmx4g -Xms4m -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 02ea03770e4..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 - -Xmx4g -Xms4M -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 b42d05618f0..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 + -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 7abfdfb0392..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 + -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 36df46fafbf..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 + -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 35a2c5c381a..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 + -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 aeb388260d4..0ddb4d48ab9 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 + -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/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 @@ - - + + 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.

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)