Skip to content

Commit 7697748

Browse files
danpoedanpoe
authored
Merge pull request #5347 from markrtuttle/github-actions2
GitHub Actions to build installation packages
2 parents 0c08382 + faae0fe commit 7697748

17 files changed

+1272
-0
lines changed

‎.github/workflows/README.md

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
# CBMC packages
2+
3+
This project builds installation packages for the tip of the develop
4+
branch for MacOS, Windows, and Ubuntu.
5+
6+
There exist installation packages for the latest stable releases of
7+
CBMC on MacOS and Ubuntu.
8+
9+
On MacOS:
10+
* brew install cbmc
11+
12+
On Ubuntu:
13+
* sudo apt-get install software-properties-common
14+
* sudo add-apt-repository ppa:mt-debian/cbmc-backports
15+
* sudo apt-get update
16+
* sudo apt-get install cbmc
17+
18+
This project uses GitHub Actions to build installation packages for
19+
the tip of the develop branch for MacOS, Windows, and Ubuntu each time
20+
new commits is added to develop. The packages reside on GitHub as
21+
artifacts that can be listed using the GitHub Actions API.
22+
23+
A separate project implements a web page hosted on GitHub Pages that makes
24+
it easy to find the installation package for the tip of develop.
25+
26+
The stable installation packages describe above for MacOS and Ubuntu
27+
install into the local operating system's equivalent of
28+
/usr/local/bin.
29+
This project builds two kinds of packages:
30+
* cbmc installs into the equvalent of /usr/local/bin
31+
* cbmc-latest installs into the equivalent of /usr/local/cbmc-latest/bin,
32+
and makes it possible to have two copies of cbmc --- a stable release
33+
and a tip of develop --- side-by-side on the same machine.
34+
35+
For each operatin system:
36+
* The MacOS package is just a tar file of a directory containing the
37+
binaries. The directory should be unpacked and placed in the search
38+
path. Using Homebrew, "brew install cbmc" will install the latest
39+
stable release. These tar files are intended only to distribute the
40+
development versions between stable releases (Homebrew repository
41+
updates of the stable versions are quick).
42+
43+
* The Windows package is an Microsoft Installer (msi) for Windows 10
44+
with Visual Studio 2019. It can be installed by double-clicking on the
45+
installer or runnin `msexec /i <filename>`.
46+
47+
* The Ubuntu package is a Debian package that can be installed with
48+
`dpkg -i <filename>`. There are packages for Ubuntu 18 and Ubuntu 16.
49+
These packages are intended to distribute the development versions
50+
between stable releases, but also to produce the stable packages uploaded
51+
to a Debian or Ubuntu PPA.
52+
53+
The file packages.yaml defines the workflow for GitHub Actions to build the
54+
packages. Each package is defined by a job that runs in its own
55+
container. The subdirectories contain files and data needed to build
56+
each of the packages.

‎.github/workflows/TODO.md

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
Left to do:
2+
* Make the Debian builds run the full debian package flow.
3+
* Refactor the workflow to invoke a makefile that can be invoked either from
4+
the workflow or from a command line to build the package.
5+
* Make the workflow distinguish between stable versions and latest versions
6+
Stable versions should write into cbmc (or bin) and latest versions
7+
should write into cbmc-latest (so they can exist side-by-side). Windows
8+
packages will have to have different product guids for stable and latest.
9+
* Transform version numbers from 5.12 to 5.12.0.id where id is some value
10+
that increments with each build. A good candidate is `github.run_id` or
11+
`github.run_num`.
12+
* Can we automate the generation of repository packages (eg, homebrew)?
13+
14+
Plans:
15+
* Wait for Michael's Debian builds and fit them into the workflow
16+
* Refactor the workflow to invoke Makefiles
17+
* Prepare PR
18+
* Do remaining items as PR refinements.

‎.github/workflows/debian/64bit_regression_tests.patch

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
--- 64bit_regression_tests 2020-06-19 16:40:45.963502746 +0000
2+
+++ 64bit_regression_tests_patch 2020-06-19 16:42:12.338994730 +0000
3+
@@ -147,14 +147,14 @@
4+
--harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
8+
--\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
9+
+-\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
10+
+-\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
11+
-\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
12+
-\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
13+
-\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
14+
-\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
15+
-+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS
16+
-+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[(\(signed( long)* int\))?i\]: SUCCESS
17+
++\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[(\(signed( long)* int\))?i\]: SUCCESS
18+
++\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS
19+
+\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[(\(signed( long)* int\))?i\]: SUCCESS
20+
+\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[(\(signed( long)* int\))?i\]: SUCCESS
21+
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[(\(signed( long)* int\))?i\]: SUCCESS

‎.github/workflows/debian/Makefile

Lines changed: 281 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,281 @@
1+
################################################################
2+
# Configuration
3+
4+
# CBMC
5+
#
6+
# CBMC name: The stable package will be $(CBMC_NAME) and the develop
7+
# package will be $(CBMC_NAME)-latest.
8+
#
9+
# CBMC version: The version number returned by `cbmc --version`.
10+
11+
CBMC_NAME = cbmc
12+
CBMC_VERSION = 5.12
13+
14+
# Builds
15+
#
16+
# GITHUB: Build using a clone of the GitHub repository if GITHUB is
17+
# nonempty, and build by downloading tarballs if it is not. If GITHUB
18+
# is nonempty, the GitHub repository must be a subdirectory of the
19+
# directory containing this Makefile, and it must be named
20+
# $(CBMC_NAME)-$(CBMC_VERSION).
21+
#
22+
# STABLE: When GITHUB is not nonempty and we are downloading tarballs,
23+
# download the tagged commit $(CBMC_NAME)-$(CBMC_VERSION) if STABLE is
24+
# nonempty and download the tip of the develop branch if it is not.
25+
# Regardless of whether GITHUB is nonempty or not, install into
26+
# /usr/bin if STABLE is nonempty and into /usr/local/cbmc-latest/bin if
27+
# it is not.
28+
29+
STABLE=
30+
GITHUB=
31+
32+
# Packages
33+
#
34+
# PKG_NAME: The name of the package, typically cbmc or cbmc-latest
35+
# PKG_VERSION: The version of the package, typically 5.12-1
36+
# PKG_OS: The Ubuntu code name, typically xenial or bionic or focal
37+
#
38+
# The name defaults to cbmc or cbmc-latest. The version defaults to a
39+
# value computed from the most recent package, but is typically given
40+
# on the command line when building from GitHub. The os defaults to
41+
# the value given in /etc/os-release.
42+
#
43+
# Package version used in changelog: $(PKG_VERSION)~$(PKG_OS)
44+
# Package name: $(PKG_NAME)_$(PKG_VERSION)~$(PKG_OS)_amd64.deb
45+
46+
ifneq ($(STABLE),)
47+
PKG_NAME = $(CBMC_NAME)
48+
else
49+
PKG_NAME = $(CBMC_NAME)-latest
50+
endif
51+
52+
#PKG_VERSION =
53+
54+
PKG_OS = `lsb_release -c | awk '{ print $$2 }'`
55+
56+
# Debian packaging
57+
#
58+
# DEBIAN_BASE: The Debian version to fetch the debian folder from.
59+
# This Makefile downloads cbmc_$(DEBIAN_BASE).debian.tar.xz from
60+
# Debian and uses its contents as the starting point for the debian
61+
# folder for this package.
62+
63+
DEBIAN_BASE=5.12-5
64+
65+
################################################################
66+
67+
default: build
68+
69+
SRCDIR=$(CBMC_NAME)-$(CBMC_VERSION)
70+
71+
################################################################
72+
# Assemble the source tree in $(SRCDIR)
73+
#
74+
75+
ifeq ($(GITHUB),)
76+
# GITHUB is empty, so assemble the source tree from tarballs
77+
78+
## Download the source tree
79+
$(CBMC_NAME)_$(CBMC_VERSION).orig.tar.gz:
80+
ifneq ($(STABLE),)
81+
# For the stable release, download the tagged commit
82+
curl -o $@ -L \
83+
https://github.com/diffblue/cbmc/archive/cbmc-$(CBMC_VERSION).tar.gz
84+
else
85+
# For the latest release, download latest commit on the develop branch
86+
curl -o $@ -L \
87+
https://github.com/diffblue/cbmc/tarball/develop
88+
endif
89+
90+
## Download the java models library submoduled into the cbmc repository
91+
$(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz:
92+
curl -o $@ -L \
93+
https://github.com/diffblue/java-models-library/archive/master.tar.gz
94+
95+
## Extract the source tree
96+
$(SRCDIR): $(CBMC_NAME)_$(CBMC_VERSION).orig.tar.gz
97+
tar xzf $<
98+
ifneq ($(STABLE),)
99+
mv cbmc-cbmc-$(CBMC_VERSION) $@
100+
else
101+
mv diffblue-cbmc-* $@
102+
endif
103+
104+
## Extract the java models library. The Debian patch files expect this
105+
## library to be at the top level and not under src/jbmc where it is
106+
## submoduled into the cbmc repository.
107+
$(SRCDIR)/java-models-library: \
108+
$(SRCDIR) \
109+
$(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz
110+
cd $< && tar xzf ../$(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz
111+
mv $</java-models-library-master $</java-models-library
112+
113+
else
114+
# GITHUB is nonempty, so use the GitHub repository in $(SRCDIR).
115+
116+
## Create source tarball for Debian from the repository
117+
$(CBMC_NAME)_$(CBMC_VERSION).orig.tar.gz:
118+
tar fcz $@ $(SRCDIR) \
119+
--exclude java-models-library --exclude debian \
120+
--exclude-vcs --exclude-vcs-ignores --exclude .github
121+
122+
## Move the java models library to where the Debian patch files expect
123+
## to find them.
124+
$(SRCDIR)/java-models-library:
125+
mv $(SRCDIR)/jbmc/lib/java-models-library $@
126+
127+
endif
128+
129+
#
130+
# End Assemble the source tree
131+
################################################################
132+
133+
################################################################
134+
# Assemble the debian directory
135+
#
136+
137+
# We download the debian directory from the debian repository, but
138+
# Ubuntu16 requires the use of clang due to some unicode bugs in
139+
# libraries with the default gcc.
140+
#
141+
# NOTE: We should use existing artifacts instead.
142+
143+
DEBIAN_TARBALL=http://deb.debian.org/debian/pool/main/c/cbmc/cbmc_$(DEBIAN_BASE).debian.tar.xz
144+
XENIAL_TARBALL=https://launchpad.net/~mt-debian/+archive/ubuntu/cbmc-backports/+sourcefiles/cbmc/5.12-5~xenial10/cbmc_5.12-5~xenial10.debian.tar.xz
145+
146+
# Download the debian directory.
147+
$(SRCDIR)/debian: $(SRCDIR)
148+
echo Found PKG_OS=$(PKG_OS)
149+
if [ "$(PKG_OS)" = "xenial" ] ; then \
150+
echo Downloading $(XENIAL_TARBALL); \
151+
curl -L -o debian.tar.xz $(XENIAL_TARBALL); \
152+
sudo apt-get -y install clang-3.8 libc++-dev libc++abi-dev; \
153+
else \
154+
echo Downloading $(DEBIAN_TARBALL); \
155+
curl -L -o debian.tar.xz $(DEBIAN_TARBALL); \
156+
fi
157+
cd $< && tar xJf ../debian.tar.xz
158+
$(RM) debian.tar.xz
159+
160+
# Update the debian changelog.
161+
patch-debian-changelog:
162+
echo Found PKG_VERSION=$(PKG_VERSION)
163+
if [ "$(PKG_VERSION)" != "" ]; then \
164+
NEW_VERSION=$(PKG_VERSION); \
165+
else \
166+
OLD_VERSION=`cd $(SRCDIR) && dpkg-parsechangelog -S Version` && \
167+
echo Found OLD_VERSION=$${OLD_VERSION} && \
168+
if dpkg --compare-versions "$${OLD_VERSION}" lt $(CBMC_VERSION) ; then \
169+
NEW_VERSION=$(CBMC_VERSION)-1 ; \
170+
else \
171+
MINOR=`echo $${OLD_VERSION} | cut -f2 -d- | cut -f1 -d. | cut -f1 -d~` && \
172+
echo Found MINOR=$${MINOR} && \
173+
NEW_VERSION=$(CBMC_VERSION)-`expr $${MINOR} + 1` ; \
174+
fi \
175+
fi && \
176+
echo Found NEW_VERSION=$${NEW_VERSION} && \
177+
NEW_VERSION=`echo $${NEW_VERSION} | cut -f1 -d~` && \
178+
echo Updated NEW_VERSION=$${NEW_VERSION} && \
179+
mv $(SRCDIR)/debian/changelog $(SRCDIR)/debian/changelog.orig && \
180+
cp changelog $(SRCDIR)/debian/changelog && \
181+
sed -i "s/#VERSION#/$${NEW_VERSION}~$(PKG_OS)/" $(SRCDIR)/debian/changelog
182+
sed -i "s/#DATE#/`date -R`/" $(SRCDIR)/debian/changelog
183+
# Use "unstable" for Debian distribution; use Ubunu code name for Ubuntu
184+
if [[ `lsb_release -d` == *Ubuntu* ]]; then \
185+
sed -i "s/unstable/$(PKG_OS)/" $(SRCDIR)/debian/changelog; \
186+
fi
187+
cat $(SRCDIR)/debian/changelog.orig >> $(SRCDIR)/debian/changelog
188+
$(RM) $(SRCDIR)/debian/changelog.orig
189+
190+
# Patch the debian control files.
191+
# In particular, install cbmc-latest into /usr/local/cbmc-latest/bin and
192+
# use locally-installed versions of debhelper and maven plug-in.
193+
patch-debian-files:
194+
ifeq ($(STABLE),)
195+
# Install cbmc-latest in /usr/local/cbmc-latest/bin (cbmc in /usr/bin)
196+
sed -i "s/^Package: cbmc.*/Package: $(PKG_NAME)/" $(SRCDIR)/debian/control
197+
sed -i "s#usr/bin#usr/local/$(PKG_NAME)/bin#g" $(SRCDIR)/debian/dirs
198+
sed -i "s#usr/bin#usr/local/$(PKG_NAME)/bin#g" $(SRCDIR)/debian/install
199+
sed -i "s#usr/bin#usr/local/$(PKG_NAME)/bin#g" $(SRCDIR)/debian/links
200+
echo "override_dh_usrlocal:" >> $(SRCDIR)/debian/rules
201+
echo "\ttrue" >> $(SRCDIR)/debian/rules
202+
echo "override_dh_dwz:" >> $(SRCDIR)/debian/rules
203+
echo "\ttrue" >> $(SRCDIR)/debian/rules
204+
$(RM) $(SRCDIR)/debian/manpages
205+
sed -i "/share\/man\/man1/d" $(SRCDIR)/debian/links
206+
endif
207+
# Patch debhelper version
208+
DEBHELPER_VERSION=`dpkg -l debhelper | tail -n1 | awk '{print $$3}' | cut -f1 -d.` && \
209+
echo Found debhelper version $$DEBHELPER_VERSION && \
210+
echo $$DEBHELPER_VERSION > $(SRCDIR)/debian/compat && \
211+
if [ $$DEBHELPER_VERSION -lt 10 ] ; then \
212+
sed -i 's/^\tdh $$@/\tdh $$@ --parallel/' $(SRCDIR)/debian/rules ; \
213+
fi
214+
sed -i "s/debhelper-compat *([<>=]* *[0-9]*),//" $(SRCDIR)/debian/control
215+
216+
# Update the debian path files.
217+
# Changes in the source code may cause old patches to apply only with
218+
# fuzz, and Debian package building does not allow fuzz.
219+
patch-debian-patches: $(SRCDIR)/debian
220+
221+
# Repair the maven patch on xenial: Add back the version number the patch deletes
222+
if [ "$(PKG_OS)" = "xenial" ] ; then \
223+
sed -i "s/@@ -32,7 +32,6 @@/@@ -32,7 +32,7 @@/" $(SRCDIR)/debian/patches/maven* && \
224+
sed -i "/^-[[:space:]]*<version>.*<\/version>/ a + <version>VERSION<\/version>" \
225+
$(SRCDIR)/debian/patches/maven* ; \
226+
fi
227+
228+
# Repair the maven patch: update the version number
229+
PLUGIN_VERSION=`dpkg -l libmaven-compiler-plugin-java | tail -n1 | awk '{print $$3}' | cut -f1 -d-` && \
230+
sed -i "s/^\(+[[:space:]]*<version>\).*<\/version>/\1$$PLUGIN_VERSION<\/version>/" \
231+
$(SRCDIR)/debian/patches/maven*
232+
233+
# Add a surefire patch to supply a version number
234+
cp surefire $(SRCDIR)/debian/patches
235+
echo "surefire" >> $(SRCDIR)/debian/patches/series
236+
SUREFIRE_VERSION=`dpkg -l libsurefire-java | tail -n1 | awk '{print $$3}' | cut -f1 -d-` && \
237+
sed -i "s/<version>SUREFIRE<\/version>/<version>$$SUREFIRE_VERSION<\/version>/" \
238+
$(SRCDIR)/debian/patches/surefire
239+
240+
# Patch 64bit_regression_tests patch
241+
cd $(SRCDIR)/debian/patches && patch < ../../../64bit_regression_tests.patch
242+
243+
# Refresh all patches with quilt
244+
sudo apt-get -y install quilt
245+
cd $(SRCDIR) && export QUILT_PATCHES=debian/patches && \
246+
while quilt push; do quilt refresh; done && quilt pop -a
247+
$(RM) $(SRCDIR)/debian/patches/*~
248+
249+
# Patch the debian rules to build cbmc concurrently.
250+
# See also the --parallel option added to dh above for early debhelper versions.
251+
# This should really become part of the standard Debian build rules.
252+
patch-debian-concurrency:
253+
sed -i '11s/^$$/parallel = $$(patsubst parallel=\%,\%,$$(filter parallel=\%,$$(DEB_BUILD_OPTIONS)))/' \
254+
$(SRCDIR)/debian/rules
255+
sed -i 's/$$(MAKE)/$$(MAKE) -j$$(parallel)/' $(SRCDIR)/debian/rules
256+
257+
#
258+
# End Assemble the debian directory
259+
################################################################
260+
261+
build: $(SRCDIR) $(SRCDIR)/debian $(SRCDIR)/java-models-library
262+
sudo apt-get -y install \
263+
debhelper minisat zlib1g-dev flex bison default-jdk-headless \
264+
maven maven-repo-helper maven-debian-helper \
265+
libmaven-compiler-plugin-java \
266+
gdb
267+
$(MAKE) patch-debian-patches
268+
$(MAKE) patch-debian-changelog
269+
$(MAKE) patch-debian-files
270+
$(MAKE) patch-debian-concurrency
271+
cd $(SRCDIR) && dpkg-buildpackage -b -Jauto -uc -d
272+
# upload new artifacts
273+
274+
clean:
275+
$(RM) -r $(SRCDIR)
276+
$(RM) $(CBMC_NAME)_$(CBMC_VERSION).orig.tar.gz
277+
$(RM) $(CBMC_NAME)_$(CBMC_VERSION).orig-java-models-library.tar.gz
278+
279+
.PHONY: default build clean
280+
.PHONY: patch-debian-changelog patch-debian-files patch-debian-concurrency
281+
.PHONY: patch-debian-patches

‎.github/workflows/debian/README.md

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# CBMC Debian package
2+
3+
This builds the Debian package for CBMC, using an auto-generated changelog.
4+
5+
* Run `make` to
6+
* clone the latest release and build CBMC, and
7+
* create a Debian package `cbmc_<RELEASE>_<ARCHITECTURE>.deb` for that latest
8+
release.
9+
10+
Install with `sudo dpkg -i `cbmc_<RELEASE>_<ARCHITECTURE>.deb`.
11+
12+
Remove with `sudo dpkg -r cbmc`.
13+
14+
Read the Makefile for the API.

0 commit comments

Comments
 (0)