From 47539fc43316fcd57e148473a408a255bc8edd03 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Sat, 20 Feb 2021 23:45:21 +0000 Subject: [PATCH 1/3] Remove extraneous files and folders from .github We have changed our implementation of package building in CI, and some of the original implementation files are no longer relevant. --- .github/workflows/TODO.md | 18 -- .../debian/64bit_regression_tests.patch | 30 -- .github/workflows/debian/Makefile | 281 ------------------ .github/workflows/debian/README.md | 14 - .github/workflows/debian/changelog | 6 - .github/workflows/debian/surefire | 35 --- .github/workflows/macos15/Makefile | 69 ----- .github/workflows/version.py | 26 -- 8 files changed, 479 deletions(-) delete mode 100644 .github/workflows/TODO.md delete mode 100644 .github/workflows/debian/64bit_regression_tests.patch delete mode 100644 .github/workflows/debian/Makefile delete mode 100644 .github/workflows/debian/README.md delete mode 100644 .github/workflows/debian/changelog delete mode 100644 .github/workflows/debian/surefire delete mode 100644 .github/workflows/macos15/Makefile delete mode 100755 .github/workflows/version.py diff --git a/.github/workflows/TODO.md b/.github/workflows/TODO.md deleted file mode 100644 index db96e2243fb..00000000000 --- a/.github/workflows/TODO.md +++ /dev/null @@ -1,18 +0,0 @@ -Left to do: -* Make the Debian builds run the full debian package flow. -* Refactor the workflow to invoke a makefile that can be invoked either from - the workflow or from a command line to build the package. -* Make the workflow distinguish between stable versions and latest versions - Stable versions should write into cbmc (or bin) and latest versions - should write into cbmc-latest (so they can exist side-by-side). Windows - packages will have to have different product guids for stable and latest. -* Transform version numbers from 5.12 to 5.12.0.id where id is some value - that increments with each build. A good candidate is `github.run_id` or - `github.run_num`. -* Can we automate the generation of repository packages (eg, homebrew)? - -Plans: -* Wait for Michael's Debian builds and fit them into the workflow -* Refactor the workflow to invoke Makefiles -* Prepare PR -* Do remaining items as PR refinements. diff --git a/.github/workflows/debian/64bit_regression_tests.patch b/.github/workflows/debian/64bit_regression_tests.patch deleted file mode 100644 index 1aded21ab91..00000000000 --- a/.github/workflows/debian/64bit_regression_tests.patch +++ /dev/null @@ -1,30 +0,0 @@ ---- /tmp/64bit_regression_tests 2020-07-24 18:34:51.811830486 +0000 -+++ 64bit_regression_tests 2020-07-24 18:36:44.827779374 +0000 -@@ -87,7 +87,7 @@ - union myunion - -byte_extract_little_endian\(u, 0ll?, .*int.*\) - +byte_extract_little_endian\(u, 0l?l?, .*int.*\) -- \d+ll? -+ \d+ll? - \{ \.i=\d+ll? \} - - --- cbmc-5.12.orig/regression/cbmc/byte_update11/main.c -@@ -147,14 +147,14 @@ - --harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz - ^EXIT=0$ - ^SIGNAL=0$ ---\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS ---\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS -+-\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS -+-\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS - -\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS - -\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS - -\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS - -\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS --+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS --+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[(\(signed( long)* int\))?i\]: SUCCESS -++\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[(\(signed( long)* int\))?i\]: SUCCESS -++\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS - +\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[(\(signed( long)* int\))?i\]: SUCCESS - +\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[(\(signed( long)* int\))?i\]: SUCCESS - +\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[(\(signed( long)* int\))?i\]: SUCCESS diff --git a/.github/workflows/debian/Makefile b/.github/workflows/debian/Makefile deleted file mode 100644 index fc86d02df18..00000000000 --- a/.github/workflows/debian/Makefile +++ /dev/null @@ -1,281 +0,0 @@ -################################################################ -# Configuration - -# CBMC -# -# CBMC name: The stable package will be $(CBMC_NAME) and the develop -# package will be $(CBMC_NAME)-latest. -# -# CBMC version: The version number returned by `cbmc --version`. - -CBMC_NAME = cbmc -CBMC_VERSION = 5.12 - -# Builds -# -# GITHUB: Build using a clone of the GitHub repository if GITHUB is -# nonempty, and build by downloading tarballs if it is not. If GITHUB -# is nonempty, the GitHub repository must be a subdirectory of the -# directory containing this Makefile, and it must be named -# $(CBMC_NAME)-$(CBMC_VERSION). -# -# STABLE: When GITHUB is not nonempty and we are downloading tarballs, -# download the tagged commit $(CBMC_NAME)-$(CBMC_VERSION) if STABLE is -# nonempty and download the tip of the develop branch if it is not. -# Regardless of whether GITHUB is nonempty or not, install into -# /usr/bin if STABLE is nonempty and into /usr/local/cbmc-latest/bin if -# it is not. - -STABLE= -GITHUB= - -# Packages -# -# PKG_NAME: The name of the package, typically cbmc or cbmc-latest -# PKG_VERSION: The version of the package, typically 5.12-1 -# PKG_OS: The Ubuntu code name, typically xenial or bionic or focal -# -# The name defaults to cbmc or cbmc-latest. The version defaults to a -# value computed from the most recent package, but is typically given -# on the command line when building from GitHub. The os defaults to -# the value given in /etc/os-release. -# -# Package version used in changelog: $(PKG_VERSION)~$(PKG_OS) -# Package name: $(PKG_NAME)_$(PKG_VERSION)~$(PKG_OS)_amd64.deb - -ifneq ($(STABLE),) -PKG_NAME = $(CBMC_NAME) -else -PKG_NAME = $(CBMC_NAME)-latest -endif - -#PKG_VERSION = - -PKG_OS = `lsb_release -c | awk '{ print $$2 }'` - -# Debian packaging -# -# DEBIAN_BASE: The Debian version to fetch the debian folder from. -# This Makefile downloads cbmc_$(DEBIAN_BASE).debian.tar.xz from -# Debian and uses its contents as the starting point for the debian -# folder for this package. - -DEBIAN_BASE=5.12-5 - -################################################################ - -default: build - -SRCDIR=$(CBMC_NAME)-$(CBMC_VERSION) - -################################################################ -# Assemble the source tree in $(SRCDIR) -# - -ifeq ($(GITHUB),) -# GITHUB is empty, so assemble the source tree from tarballs - -## Download the source tree -$(CBMC_NAME)_$(CBMC_VERSION).orig.tar.gz: -ifneq ($(STABLE),) - # For the stable release, download the tagged commit - curl -o $@ -L \ - https://github.com/diffblue/cbmc/archive/cbmc-$(CBMC_VERSION).tar.gz -else - # For the latest release, download latest commit on the develop branch - curl -o $@ -L \ - https://github.com/diffblue/cbmc/tarball/develop -endif - -## Download the java models library submoduled into the cbmc repository -$(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz: - curl -o $@ -L \ - https://github.com/diffblue/java-models-library/archive/master.tar.gz - -## Extract the source tree -$(SRCDIR): $(CBMC_NAME)_$(CBMC_VERSION).orig.tar.gz - tar xzf $< -ifneq ($(STABLE),) - mv cbmc-cbmc-$(CBMC_VERSION) $@ -else - mv diffblue-cbmc-* $@ -endif - -## Extract the java models library. The Debian patch files expect this -## library to be at the top level and not under src/jbmc where it is -## submoduled into the cbmc repository. -$(SRCDIR)/java-models-library: \ - $(SRCDIR) \ - $(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz - cd $< && tar xzf ../$(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz - mv $> $(SRCDIR)/debian/changelog - $(RM) $(SRCDIR)/debian/changelog.orig - -# Patch the debian control files. -# In particular, install cbmc-latest into /usr/local/cbmc-latest/bin and -# use locally-installed versions of debhelper and maven plug-in. -patch-debian-files: -ifeq ($(STABLE),) - # Install cbmc-latest in /usr/local/cbmc-latest/bin (cbmc in /usr/bin) - sed -i "s/^Package: cbmc.*/Package: $(PKG_NAME)/" $(SRCDIR)/debian/control - sed -i "s#usr/bin#usr/local/$(PKG_NAME)/bin#g" $(SRCDIR)/debian/dirs - sed -i "s#usr/bin#usr/local/$(PKG_NAME)/bin#g" $(SRCDIR)/debian/install - sed -i "s#usr/bin#usr/local/$(PKG_NAME)/bin#g" $(SRCDIR)/debian/links - echo "override_dh_usrlocal:" >> $(SRCDIR)/debian/rules - echo "\ttrue" >> $(SRCDIR)/debian/rules - echo "override_dh_dwz:" >> $(SRCDIR)/debian/rules - echo "\ttrue" >> $(SRCDIR)/debian/rules - $(RM) $(SRCDIR)/debian/manpages - sed -i "/share\/man\/man1/d" $(SRCDIR)/debian/links -endif - # Patch debhelper version - DEBHELPER_VERSION=`dpkg -l debhelper | tail -n1 | awk '{print $$3}' | cut -f1 -d.` && \ - echo Found debhelper version $$DEBHELPER_VERSION && \ - echo $$DEBHELPER_VERSION > $(SRCDIR)/debian/compat && \ - if [ $$DEBHELPER_VERSION -lt 10 ] ; then \ - sed -i 's/^\tdh $$@/\tdh $$@ --parallel/' $(SRCDIR)/debian/rules ; \ - fi - sed -i "s/debhelper-compat *([<>=]* *[0-9]*),//" $(SRCDIR)/debian/control - -# Update the debian path files. -# Changes in the source code may cause old patches to apply only with -# fuzz, and Debian package building does not allow fuzz. -patch-debian-patches: $(SRCDIR)/debian - - # Repair the maven patch on xenial: Add back the version number the patch deletes - if [ "$(PKG_OS)" = "xenial" ] ; then \ - sed -i "s/@@ -32,7 +32,6 @@/@@ -32,7 +32,7 @@/" $(SRCDIR)/debian/patches/maven* && \ - sed -i "/^-[[:space:]]*.*<\/version>/ a + VERSION<\/version>" \ - $(SRCDIR)/debian/patches/maven* ; \ - fi - - # Repair the maven patch: update the version number - PLUGIN_VERSION=`dpkg -l libmaven-compiler-plugin-java | tail -n1 | awk '{print $$3}' | cut -f1 -d-` && \ - sed -i "s/^\(+[[:space:]]*\).*<\/version>/\1$$PLUGIN_VERSION<\/version>/" \ - $(SRCDIR)/debian/patches/maven* - - # Add a surefire patch to supply a version number - cp surefire $(SRCDIR)/debian/patches - echo "surefire" >> $(SRCDIR)/debian/patches/series - SUREFIRE_VERSION=`dpkg -l libsurefire-java | tail -n1 | awk '{print $$3}' | cut -f1 -d-` && \ - sed -i "s/SUREFIRE<\/version>/$$SUREFIRE_VERSION<\/version>/" \ - $(SRCDIR)/debian/patches/surefire - - # Patch 64bit_regression_tests patch - cd $(SRCDIR)/debian/patches && patch < ../../../64bit_regression_tests.patch - - # Refresh all patches with quilt - sudo apt-get -y install quilt - cd $(SRCDIR) && export QUILT_PATCHES=debian/patches && \ - while quilt push; do quilt refresh; done && quilt pop -a - $(RM) $(SRCDIR)/debian/patches/*~ - -# Patch the debian rules to build cbmc concurrently. -# See also the --parallel option added to dh above for early debhelper versions. -# This should really become part of the standard Debian build rules. -patch-debian-concurrency: - sed -i '11s/^$$/parallel = $$(patsubst parallel=\%,\%,$$(filter parallel=\%,$$(DEB_BUILD_OPTIONS)))/' \ - $(SRCDIR)/debian/rules - sed -i 's/$$(MAKE)/$$(MAKE) -j$$(parallel)/' $(SRCDIR)/debian/rules - -# -# End Assemble the debian directory -################################################################ - -build: $(SRCDIR) $(SRCDIR)/debian $(SRCDIR)/java-models-library - sudo apt-get -y install \ - debhelper minisat zlib1g-dev flex bison default-jdk-headless \ - maven maven-repo-helper maven-debian-helper \ - libmaven-compiler-plugin-java \ - gdb - $(MAKE) patch-debian-patches - $(MAKE) patch-debian-changelog - $(MAKE) patch-debian-files - $(MAKE) patch-debian-concurrency - cd $(SRCDIR) && dpkg-buildpackage -b -Jauto -uc -d - # upload new artifacts - -clean: - $(RM) -r $(SRCDIR) - $(RM) $(CBMC_NAME)_$(CBMC_VERSION).orig.tar.gz - $(RM) $(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz - -.PHONY: default build clean -.PHONY: patch-debian-changelog patch-debian-files patch-debian-concurrency -.PHONY: patch-debian-patches diff --git a/.github/workflows/debian/README.md b/.github/workflows/debian/README.md deleted file mode 100644 index ec7bbd15ad0..00000000000 --- a/.github/workflows/debian/README.md +++ /dev/null @@ -1,14 +0,0 @@ -# CBMC Debian package - -This builds the Debian package for CBMC, using an auto-generated changelog. - -* Run `make` to - * clone the latest release and build CBMC, and - * create a Debian package `cbmc__.deb` for that latest - release. - -Install with `sudo dpkg -i `cbmc__.deb`. - -Remove with `sudo dpkg -r cbmc`. - -Read the Makefile for the API. diff --git a/.github/workflows/debian/changelog b/.github/workflows/debian/changelog deleted file mode 100644 index a2dac58bbd6..00000000000 --- a/.github/workflows/debian/changelog +++ /dev/null @@ -1,6 +0,0 @@ -cbmc (#VERSION#) unstable; urgency=low - - * Auto-build - - -- Builder #DATE# - diff --git a/.github/workflows/debian/surefire b/.github/workflows/debian/surefire deleted file mode 100644 index 37f413c926b..00000000000 --- a/.github/workflows/debian/surefire +++ /dev/null @@ -1,35 +0,0 @@ -Description: Use maven-repo-helper - . - cbmc (5.10-1) unstable; urgency=low - . - * New upstream release - * Updated Standards version to 4.2.1 (no changes required) -Author: Michael Tautschnig - ---- -The information above should follow the Patch Tagging Guidelines, please -checkout http://dep.debian.net/deps/dep3/ to learn about the format. Here -are templates for supplementary fields that you might want to add: - -Origin: , -Bug: -Bug-Debian: https://bugs.debian.org/ -Bug-Ubuntu: https://launchpad.net/bugs/ -Forwarded: -Reviewed-By: -Last-Update: 2018-09-27 - ---- cbmc-5.10.orig/java-models-library/pom.xml -+++ cbmc-5.10/java-models-library/pom.xml -@@ -43,6 +43,11 @@ - - - org.apache.maven.plugins -+ maven-surefire-plugin -+ 2.17 -+ -+ -+ org.apache.maven.plugins - maven-javadoc-plugin - 3.0.0-M1 - diff --git a/.github/workflows/macos15/Makefile b/.github/workflows/macos15/Makefile deleted file mode 100644 index 08c66fa99b7..00000000000 --- a/.github/workflows/macos15/Makefile +++ /dev/null @@ -1,69 +0,0 @@ -PKG_STABLE_NAME = cbmc -PKG_LATEST_NAME = cbmc-latest -PKG_STABLE_TAR = $(PKG_STABLE_NAME).tar.gz -PKG_LATEST_TAR = $(PKG_LATEST_NAME).tar.gz - -REPODIR ?= . - -default: stable latest - -stable: $(PKG_STABLE_TAR) - -latest: $(PKG_LATEST_TAR) - -$(REPODIR)/build/bin/cbmc: - brew install cmake ninja openjdk maven - # See https://github.com/diffblue/cbmc/issues/4956 for clang issue - cd $(REPODIR) && cmake -S. -Bbuild -DCMAKE_C_COMPILER=/usr/bin/clang -DWITH_JBMC=YES -GNinja - cd $(REPODIR) && cmake --build build - -$(PKG_STABLE_TAR): $(REPODIR)/build/bin/cbmc - $(RM) -r ${PKG_STABLE_NAME} - - mkdir -p ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/cbmc ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/goto-analyzer ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/goto-cc ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/goto-diff ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/goto-gcc ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/goto-harness ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/goto-instrument ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/goto-ld ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/janalyzer ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/java-unit ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/jbmc ${PKG_STABLE_NAME}/bin - cp $(REPODIR)/build/bin/jdiff ${PKG_STABLE_NAME}/bin - - mkdir -p ${PKG_STABLE_NAME}/share/man/man1 - cp $(REPODIR)/doc/man/cbmc.1 ${PKG_STABLE_NAME}/share/man/man1 - - tar fcz ${PKG_STABLE_TAR} ${PKG_STABLE_NAME} - -$(PKG_LATEST_TAR): $(REPODIR)/build/bin/cbmc - $(RM) -r ${PKG_LATEST_NAME} - - mkdir -p ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/cbmc ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/goto-analyzer ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/goto-cc ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/goto-diff ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/goto-gcc ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/goto-harness ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/goto-instrument ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/goto-ld ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/janalyzer ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/java-unit ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/jbmc ${PKG_LATEST_NAME}/bin - cp $(REPODIR)/build/bin/jdiff ${PKG_LATEST_NAME}/bin - - mkdir -p ${PKG_LATEST_NAME}/share/man/man1 - cp $(REPODIR)/doc/man/cbmc.1 ${PKG_LATEST_NAME}/share/man/man1 - - tar fcz ${PKG_LATEST_TAR} ${PKG_LATEST_NAME} - -clean: - $(RM) *~ - $(RM) -r $(PKG_STABLE_TAR) $(PKG_STABLE_NAME) - $(RM) -r $(PKG_LATEST_TAR) $(PKG_LATEST_NAME) - -.PHONY: default stable latest clean diff --git a/.github/workflows/version.py b/.github/workflows/version.py deleted file mode 100755 index 1ab62964007..00000000000 --- a/.github/workflows/version.py +++ /dev/null @@ -1,26 +0,0 @@ -#!/usr/bin/env python3 - -import sys - -def debian_number(major='0', minor='0', patch='0', build='0'): - """Generate a Debian package version number from components.""" - return "{}.{}.{}-{}".format(major, minor, patch, build) - -def version_number(version, build="0"): - """Generate a Debian package version number.""" - - parts = version.split('.') - if len(parts) > 3: - raise UserWarning("Version number {} contains {} components, " - "expected at most 3".format(version, len(parts))) - - major, minor, patch = (parts + ["0", "0", "0"])[:3] - return debian_number(major, minor, patch, build) - -def main(): - version = sys.argv[1] if len(sys.argv) > 1 else "0" - build = sys.argv[2] if len(sys.argv) > 2 else "0" - print(version_number(version, build)) - -if __name__ == "__main__": - main() From 725682172e15e7d7fc8387568da0c780bc68a5e4 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Sat, 20 Feb 2021 23:58:22 +0000 Subject: [PATCH 2/3] Update github actions readme file. The original readme.md file is no longer corresponding to the current implementation of CI we have, so this is bringing it more in line with the current state. --- .github/workflows/README.md | 78 +++++++++++-------------------------- 1 file changed, 22 insertions(+), 56 deletions(-) diff --git a/.github/workflows/README.md b/.github/workflows/README.md index 95d5ec21cc1..0fcc02faffc 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -1,56 +1,22 @@ -# CBMC packages - -This project builds installation packages for the tip of the develop -branch for MacOS, Windows, and Ubuntu. - -There exist installation packages for the latest stable releases of -CBMC on MacOS and Ubuntu. - -On MacOS: -* brew install cbmc - -On Ubuntu: -* sudo apt-get install software-properties-common -* sudo add-apt-repository ppa:mt-debian/cbmc-backports -* sudo apt-get update -* sudo apt-get install cbmc - -This project uses GitHub Actions to build installation packages for -the tip of the develop branch for MacOS, Windows, and Ubuntu each time -new commits is added to develop. The packages reside on GitHub as -artifacts that can be listed using the GitHub Actions API. - -A separate project implements a web page hosted on GitHub Pages that makes -it easy to find the installation package for the tip of develop. - -The stable installation packages describe above for MacOS and Ubuntu -install into the local operating system's equivalent of -/usr/local/bin. -This project builds two kinds of packages: -* cbmc installs into the equvalent of /usr/local/bin -* cbmc-latest installs into the equivalent of /usr/local/cbmc-latest/bin, - and makes it possible to have two copies of cbmc --- a stable release - and a tip of develop --- side-by-side on the same machine. - -For each operatin system: -* The MacOS package is just a tar file of a directory containing the - binaries. The directory should be unpacked and placed in the search - path. Using Homebrew, "brew install cbmc" will install the latest - stable release. These tar files are intended only to distribute the - development versions between stable releases (Homebrew repository - updates of the stable versions are quick). - -* The Windows package is an Microsoft Installer (msi) for Windows 10 - with Visual Studio 2019. It can be installed by double-clicking on the - installer or runnin `msexec /i `. - -* The Ubuntu package is a Debian package that can be installed with - `dpkg -i `. There are packages for Ubuntu 18 and Ubuntu 16. - These packages are intended to distribute the development versions - between stable releases, but also to produce the stable packages uploaded - to a Debian or Ubuntu PPA. - -The file packages.yaml defines the workflow for GitHub Actions to build the -packages. Each package is defined by a job that runs in its own -container. The subdirectories contain files and data needed to build -each of the packages. +# CBMC CI infrastructure + +This folder contains implementation and configuration files for +our CI infrastructure on top of Github Actions. Aside from CI, +it also contains packaging and automated release scripts. + +The files in this folder correspond to: + +* `build-and-test-Xen.yaml` -> Build Xen using CBMC tools. +* `csmith.yaml` -> Run 10 randomly generated CSmith tests per Pull Request. +* `doxygen-check.yaml` -> Build project doxygen documentation per Pull Request. +* `pull-request-check-cpplint.sh` -> Script that's called per Pull Request to execute + `cpplint` over changes. +* `pull-request-check-clang-format.sh` -> Script that's called per Pull Request + to execute `clang-format` over changes. +* `pull-request-checks.yaml` -> Configuration file for the Github Actions CI jobs + for the various platforms. +* `regular-release.yaml` -> Configuration file for performing an automated release + every time a tag of a specific form (`cbmc-x.y.z`) is pushed. +* `release-packages.yaml` -> Configuration file for performing building of build + artifacts that are attached to release when it's being made. Invoked when a + regular release is performed. From 4daa686780917f1af78cc6029797d6aa02b020ff Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 23 Feb 2021 17:24:25 +0000 Subject: [PATCH 3/3] Rename some actions and add information on the CI platforms. Add some information to the readme with regard to the main platforms we are building/testing CBMC on Github Actions. --- .github/workflows/README.md | 26 ++++++++++++++++++++++ .github/workflows/doxygen-check.yaml | 2 +- .github/workflows/pull-request-checks.yaml | 2 +- 3 files changed, 28 insertions(+), 2 deletions(-) diff --git a/.github/workflows/README.md b/.github/workflows/README.md index 0fcc02faffc..91b7ec31229 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -20,3 +20,29 @@ The files in this folder correspond to: * `release-packages.yaml` -> Configuration file for performing building of build artifacts that are attached to release when it's being made. Invoked when a regular release is performed. + +## CI Platforms + +We are currently building and testing CBMC under the following configurations: + +* `make` * `gcc` * `linux` (ubuntu 20.04) +* `make` * `clang` * `linux` (ubuntu 20.04) +* `cmake` * `gcc` * `linux` (ubuntu 20.04) +* `make` * `clang` * `macos` (10.15) +* `cmake` * `clang` * `macos` (10.15) +* `cmake` * `vs` * `windows` (vs2019) + +Aside from the main platform builds for testing, we are also performing +some auxiliary builds that test packaging support to be up-to-date. We +do that for: + +* a `docker` image +* an `ubuntu-20.04` package +* an `ubuntu-18.04` package +* a `windows-msi` installer package + +Last but not least, we are also performing a coverage statistics collection +job, which builds CBMC with coverage information on, and then runs the tests, +finally uploading the results to [Codecov](https://about.codecov.io) which +then updates pull request with coverage statistics after the job has finished +running. diff --git a/.github/workflows/doxygen-check.yaml b/.github/workflows/doxygen-check.yaml index 5cf84913b51..cfd2a96dd84 100644 --- a/.github/workflows/doxygen-check.yaml +++ b/.github/workflows/doxygen-check.yaml @@ -1,4 +1,4 @@ -name: doxygen-check +name: Build Doxygen Documentation on: pull_request: branches: [ develop ] diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index ddd699c7658..b2a203c6349 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -1,4 +1,4 @@ -name: pull-request-checks +name: Build and Test CBMC on: pull_request: branches: [ develop ]