Skip to content
This repository was archived by the owner on Apr 3, 2023. It is now read-only.

Commit 66531fb

Browse files
author
Vlastimil Zeman
authored
Merge pull request #1 from diffblue/feature/alpine-debian-image
Alpine and Ubuntu image for cbmc-builder
2 parents 3fa2b06 + 04b81a9 commit 66531fb

File tree

10 files changed

+325
-6
lines changed

10 files changed

+325
-6
lines changed

.gitignore

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
.dobi
2+
alpine-dist
3+
alpine-tmp
4+
ubuntu-dist
5+
ubuntu-tmp

.gitmodules

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
[submodule "cbmc"]
2+
path = cbmc
3+
url = https://github.com/diffblue/cbmc.git

.travis.yml

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
language: cpp
2+
3+
os: linux
4+
5+
sudo: required
6+
7+
services:
8+
- docker
9+
10+
before_install:
11+
# Download dobi binary and save it in the current folder
12+
- curl -L https://github.com/dnephin/dobi/releases/download/v0.9/dobi-linux >dobi
13+
# Make that binary executable
14+
- chmod u+x ./dobi
15+
# Pull to be sure that we get all git tags
16+
- git pull --depth=2000
17+
18+
- |
19+
# If this is PR then CBMC submodule should refer to diffblue/cbmc repository
20+
if [[ "${TRAVIS_PULL_REQUEST}" == "true" && \
21+
$(git config --get --file=.gitmodules submodule.cbmc.url) != "https://github.com/diffblue/cbmc.git" ]]
22+
then
23+
echo "This is pull request. Set CBMC submodule URL to diffblue/cbmc repository."
24+
echo "git config --file=.gitmodules submodule.cbmc.url https://github.com/diffblue/cbmc.git"
25+
exit 1
26+
fi
27+
28+
# Build cbmc-builder and try to build & test cbmc in it. Run in parallel for
29+
# each distro.
30+
env:
31+
- DISTRO="alpine"
32+
- DISTRO="ubuntu"
33+
34+
script:
35+
- BUILDER_TAG=$(git describe) ./dobi ${DISTRO}-test

README.md

Lines changed: 47 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,59 @@
1+
# CBMC Builder Docker Images [![Build Status](https://travis-ci.org/diffblue/cbmc-builder.svg?branch=master)](https://travis-ci.org/diffblue/cbmc-builder)
2+
13
This is the Git repo of the Docker images for building
2-
[CBMC](https://github.com/diffblue/cbmc) in/for different operating systems.
4+
[CBMC](https://github.com/diffblue/cbmc) in/for different operating systems.
5+
6+
Builders exist for two OS:
7+
- alpine in [alpine/Dockerfile](alpine/Dockerfile) referenced as
8+
`diffblue/cbmc-builder:alpine`,
9+
`diffblue/cbmc-builder:alpine-0.0.1`
10+
- ubuntu in [ubuntu/Dockerfile](ubuntu/Dockerfile) referenced as
11+
`diffblue/cbmc-builder:latest`,
12+
`diffblue/cbmc-builder:xenial`,
13+
`diffblue/cbmc-builder:xenial-0.0.1`
14+
15+
## To compile CBMC source manually
316

4-
To compile `CBMC` source
17+
Set path to your cloned CBMC source
18+
19+
```bash
20+
CBMC_PATH=~/git/cbmc
21+
```
22+
23+
To run compilation [instructions](https://github.com/diffblue/cbmc/blob/master/COMPILING)
24+
in container
525

626
```bash
7-
CBMC_PATH=~/Workspace/cbmc-git
827
docker run --rm -v ${CBMC_PATH}:/cbmc diffblue/cbmc-builder make -C src minisat2-download
9-
docker run --rm -v ${CBMC_PATH}:/cbmc diffblue/cbmc-builder make -C src libzip-download zlib-download
10-
docker run --rm -v ${CBMC_PATH}:/cbmc diffblue/cbmc-builder make -C src libzip-build
11-
docker run --rm -v ${CBMC_PATH}:/cbmc diffblue/cbmc-builder make -C src -j2
28+
docker run --rm -v ${CBMC_PATH}:/cbmc diffblue/cbmc-builder make -C src -j$(getconf _NPROCESSORS_ONLN)
1229
```
1330

1431
To run tests afterwards
1532

1633
```bash
1734
docker run --rm -v ${CBMC_PATH}:/cbmc diffblue/cbmc-builder make -C regression test
1835
```
36+
37+
## To compile CBMC source using *dobi*
38+
39+
Install [dobi](https://github.com/dnephin/dobi/) and add it to your `PATH`.
40+
41+
Enter to folder with `dobi.yml` (root of this repository).
42+
43+
To run all tasks
44+
45+
```bash
46+
BUILD_TAG=$(git describe) dobi
47+
```
48+
49+
To run all tests
50+
51+
```bash
52+
BUILD_TAG=$(git describe) dobi test
53+
```
54+
55+
Remove all temporary files
56+
57+
```bash
58+
BUILD_TAG=$(git describe) dobi clean
59+
```

alpine/Dockerfile

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FROM alpine:3.5
2+
3+
LABEL maintainer="DiffBlue Ltd."
4+
5+
RUN apk add --no-cache gcc g++ make ccache bison flex perl-libwww bash
6+
7+
# Will be mounted to source during run
8+
WORKDIR /cbmc

alpine/Dockerfile.distro

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
FROM alpine:3.5
2+
3+
LABEL maintainer="DiffBlue Ltd."
4+
5+
RUN apk add --no-cache libgcc libstdc++
6+
7+
COPY alpine-dist /usr/bin

cbmc

Submodule cbmc added at 610e9e4

dobi.yaml

Lines changed: 203 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,203 @@
1+
#
2+
# dobi.yaml - resources for building and testing docker images
3+
#
4+
5+
meta:
6+
project: cbmc
7+
default: distros
8+
9+
#
10+
# Mounts
11+
#
12+
13+
mount=source:
14+
bind: ./cbmc/
15+
path: /src/cbmc/
16+
17+
## Alpine Mounts
18+
19+
mount=alpine-tmp:
20+
bind: ./alpine-tmp
21+
path: /tmp/projects
22+
23+
mount=alpine-dist:
24+
bind: ./alpine-dist/
25+
path: /dist/
26+
27+
## Ubuntu Mounts
28+
29+
mount=ubuntu-tmp:
30+
bind: ./ubuntu-tmp
31+
path: /tmp/projects
32+
33+
mount=ubuntu-dist:
34+
bind: ./ubuntu-dist/
35+
path: /dist/
36+
37+
#
38+
# Images
39+
#
40+
41+
## Alpine Images
42+
43+
image=alpine-builder:
44+
image: diffblue/cbmc-builder
45+
context: alpine/
46+
dockerfile: Dockerfile
47+
tags:
48+
- 'alpine'
49+
- 'alpine-{env.BUILDER_TAG}'
50+
51+
image=alpine-distro:
52+
image: diffblue/cbmc
53+
dockerfile: alpine/Dockerfile.distro
54+
depends: ["alpine-copy-binaries"]
55+
description: "Build the distribution image"
56+
tags:
57+
- 'alpine'
58+
- 'alpine-{env.BUILDER_TAG}'
59+
60+
## Ubuntu Images
61+
62+
image=ubuntu-builder:
63+
image: diffblue/cbmc-builder
64+
context: ubuntu/
65+
dockerfile: Dockerfile
66+
tags:
67+
- 'latest'
68+
- 'xenial'
69+
- 'xenial-{env.BUILDER_TAG}'
70+
71+
image=ubuntu-distro:
72+
image: diffblue/cbmc
73+
dockerfile: ubuntu/Dockerfile.distro
74+
depends: ["ubuntu-copy-binaries"]
75+
description: "Build the distribution image"
76+
tags:
77+
- 'latest'
78+
- 'xenial'
79+
- 'xenial-{env.BUILDER_TAG}'
80+
81+
#
82+
# Jobs
83+
#
84+
85+
## Alpine Jobs
86+
87+
job=alpine-copy-src:
88+
use: alpine-builder
89+
mounts: [source, alpine-tmp]
90+
artifact: alpine-tmp/cbmc
91+
command: "bash -c \"cp -r /src/cbmc /tmp/projects/\""
92+
description: "Copy source to temporary folder."
93+
94+
job=alpine-prebuild:
95+
use: alpine-builder
96+
depends: ["alpine-copy-src"]
97+
mounts: [alpine-tmp]
98+
artifact: alpine-tmp/cbmc/minisat-2.2.1
99+
command: "bash -c \"make -C /tmp/projects/cbmc/src minisat2-download\""
100+
description: "Do make prebuild actions."
101+
102+
job=alpine-build:
103+
use: alpine-builder
104+
depends: ["alpine-prebuild"]
105+
mounts: [alpine-tmp]
106+
artifact: alpine-tmp/cbmc/src/cbmc/cbmc
107+
command: "bash -c \"make -C /tmp/projects/cbmc/src -j$(getconf _NPROCESSORS_ONLN)\""
108+
description: "Do make build."
109+
110+
job=alpine-test:
111+
use: alpine-builder
112+
depends: ["alpine-build"]
113+
mounts: [alpine-tmp]
114+
command: "bash -c \"make -C /tmp/projects/cbmc/regression test\""
115+
description: "Do make tests."
116+
117+
job=alpine-copy-binaries:
118+
use: alpine-builder
119+
depends: ["alpine-build"]
120+
mounts: [alpine-tmp, alpine-dist]
121+
artifact: alpine-dist/bin
122+
command: "bash -c \"mkdir -p /dist/bin && cp -r /tmp/projects/cbmc/src/cbmc/cbmc /dist/bin/ && cp -r /tmp/projects/cbmc/src/goto-*/goto-* /dist/bin/ && rm /dist/bin/*.a\""
123+
description: "Copy binaries to dist folder."
124+
125+
job=alpine-clean:
126+
use: alpine-builder
127+
mounts: [alpine-tmp, alpine-dist]
128+
command: "bash -c \"rm -rf /tmp/projects/* && rm -rf /dist/*\""
129+
description: "Delete temporary files and binaries"
130+
131+
## Ubuntu Jobs
132+
133+
job=ubuntu-copy-src:
134+
use: ubuntu-builder
135+
mounts: [source, ubuntu-tmp]
136+
artifact: ubuntu-tmp/cbmc
137+
command: "bash -c \"cp -r /src/cbmc /tmp/projects/\""
138+
description: "Copy source to temporary folder."
139+
140+
job=ubuntu-prebuild:
141+
use: ubuntu-builder
142+
depends: ["ubuntu-copy-src"]
143+
mounts: [ubuntu-tmp]
144+
artifact: ubuntu-tmp/cbmc/minisat-2.2.1
145+
command: "bash -c \"make -C /tmp/projects/cbmc/src minisat2-download\""
146+
description: "Do make prebuild actions."
147+
148+
job=ubuntu-build:
149+
use: ubuntu-builder
150+
depends: ["ubuntu-prebuild"]
151+
mounts: [ubuntu-tmp]
152+
artifact: ubuntu-tmp/cbmc/src/cbmc/cbmc
153+
command: "bash -c \"make -C /tmp/projects/cbmc/src -j$(getconf _NPROCESSORS_ONLN)\""
154+
description: "Do make build."
155+
156+
job=ubuntu-test:
157+
use: ubuntu-builder
158+
depends: ["ubuntu-build"]
159+
mounts: [ubuntu-tmp]
160+
command: "bash -c \"make -C /tmp/projects/cbmc/regression test\""
161+
description: "Do make tests."
162+
163+
job=ubuntu-copy-binaries:
164+
use: ubuntu-builder
165+
depends: ["ubuntu-build"]
166+
mounts: [ubuntu-tmp, ubuntu-dist]
167+
artifact: ubuntu-dist/bin
168+
command: "bash -c \"mkdir -p /dist/bin && cp -r /tmp/projects/cbmc/src/cbmc/cbmc /dist/bin/ && cp -r /tmp/projects/cbmc/src/goto-*/goto-* /dist/bin/ && rm /dist/bin/*.a\""
169+
description: "Copy binaries to dist folder."
170+
171+
job=ubuntu-clean:
172+
use: ubuntu-builder
173+
mounts: [ubuntu-tmp, ubuntu-dist]
174+
command: "bash -c \"rm -rf /tmp/projects/* && rm -rf /dist/*\""
175+
description: "Delete temporary files and binaries"
176+
177+
#
178+
# Aliases
179+
#
180+
181+
alias=alpine:
182+
tasks: [alpine-copy-src, alpine-prebuild, alpine-build, alpine-test, alpine-copy-binaries]
183+
description: "Run all containers and jobs for Alpine"
184+
185+
alias=ubuntu:
186+
tasks: [ubuntu-copy-src, ubuntu-prebuild, ubuntu-build, ubuntu-test, ubuntu-copy-binaries]
187+
description: "Run all containers and jobs for Ubuntu"
188+
189+
alias=test:
190+
tasks: [alpine-test, ubuntu-test]
191+
description: "Run all tests for all distros."
192+
193+
alias=distros:
194+
tasks: [alpine-distro, ubuntu-distro]
195+
description: "Create all distro images."
196+
197+
alias=clean:
198+
tasks: [alpine-clean, ubuntu-clean]
199+
description: "Delete temporary files and binaries for all distros."
200+
201+
alias=all:
202+
tasks: [alpine, ubuntu]
203+
description: "Run all jobs for all distros."

ubuntu/Dockerfile

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
FROM ubuntu:16.04
2+
3+
LABEL maintainer="DiffBlue Ltd."
4+
5+
RUN apt-get update \
6+
&& apt-get install -y --no-install-recommends \
7+
g++ gcc make ccache bison flex libwww-perl patch \
8+
&& rm -rf /var/lib/apt/lists/*
9+
10+
# Will be mounted to source during run
11+
WORKDIR /cbmc

ubuntu/Dockerfile.distro

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
FROM ubuntu:16.04
2+
3+
LABEL maintainer="DiffBlue Ltd."
4+
5+
COPY ubuntu-dist /usr/bin

0 commit comments

Comments
 (0)