-
Notifications
You must be signed in to change notification settings - Fork 3
155 lines (134 loc) · 6.08 KB
/
continuous_integration.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
name: Continuous integration
on:
push:
branches: [main]
pull_request:
branches: [main]
workflow_dispatch:
jobs:
format:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- run: cargo fmt --check
clippy:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- run: cargo clippy -- -D warnings
test:
# will wait for new cache on push to main branch, otherwise will run straight away with existing cache
needs: generate_log
if: ${{ always() && !failure() && !cancelled() }}
strategy:
fail-fast: false
matrix:
z3version: ['4.8.7', '4.8.17', '4.11.2', '4.12.2', '4.12.4']
# Linux, Processor (CPU): 4, Memory (RAM): 16 GB, Storage (SSD): 14 GB
# https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners/about-github-hosted-runners#supported-runners-and-hardware-resources
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- id: configure-z3-id
run: echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT
- name: Cache cargo
uses: Swatinem/rust-cache@v2
with:
shared-key: "shared"
- uses: actions/cache/restore@v3
with:
path: logs
key: use-restore-key-instead
restore-keys: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-
- id: check-logs-cached
run: ls -la logs
- run: cargo version && SLP_MEMORY_LIMIT_GB=16 cargo test --workspace -- --nocapture
# Failure
- run: tar -czf failing_logs.tar.bz2 logs/
if: failure()
- uses: actions/[email protected]
if: failure()
with:
name: "logs_z3_v${{ matrix.z3version }}"
path: failing_logs.tar.bz2
retention-days: 1
generate_log:
# only run this job on push to main branch
if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch'
strategy:
fail-fast: false
matrix:
z3version: ['4.8.7', '4.8.17', '4.11.2', '4.12.2', '4.12.4']
# for versions of Z3 at least 4.9.0 we need v1.3 of the GitHub action, for older versions of Z3, 1.2.2
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install Z3 for older version
uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3"
if: ${{ matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9' }}
with:
version: ${{ matrix.z3version }}
- name: Install Z3 for newer version
uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3"
if: ${{ !(matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9') }}
with:
version: ${{ matrix.z3version }}
- name: Configure Z3 version environment variable
id: configure-z3-id
run: |
# Generate filename comaptible version: 4.8.7 -> 4_8_7
echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT
# Generate regex compatible version: 4.8.7 -> 4\.8\.7
echo "z3_v_regex=$(echo "${{ matrix.z3version }}" | sed 's/\./\\./g')" >> $GITHUB_OUTPUT
- name: Cache log files
id: cache-log
uses: actions/cache@v3
with:
path: logs
key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ hashFiles('smt-problems/**/*.smt2') }}
restore-keys: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-
- name: Run Z3 solver on changed smt2 files and compress
id: run_z3_and_upload
run: |
# Create the 'logs' directory
test -d "logs" || mkdir "logs"
# Loop through all files and check that log exists
for file in smt-problems/**/*.smt2; do
test -f "$file" || break
# Skip if the file if the first line is a comment with
[ "$(sed -n '/^;[^\n]*${{ steps.configure-z3-id.outputs.z3_v_regex }}/p;q' $file)" ] && echo "Skipping $file since the first line contains \"${{ matrix.z3version }}\"" && continue || true
# Get the file hash
file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1)
# Get the filename without extension
base_name=$(basename "${file%.*}")
# Log file name
log_file_name="logs/${base_name}_fHash_${file_hash}.log"
# Skip if log file exists and is not empty
test -s "${log_file_name}" && continue || true
rm -f "logs/${base_name}_fHash_*.log"
echo "Processing \"$file\" to \"$log_file_name\""
# Run Z3 solver for the file and save the log in the 'logs' directory.
# The memory limit is set to 15.5GB and the timeout is set to 30 seconds
# (this limits the log file size to roughly <=4GB). We redirect
# the output so that it doesn't get printed and listen for a
# timeout message in which case we remove the last line of the log
# file since it may be incomplete (and cause parsing errors).
z3 trace=true proof=true -memory:15872 -T:10 trace-file-name=${log_file_name} ./$file \
> >(grep -q "timeout" && echo "[Timeout] Removing last line of logfile" && tail -n 1 "${log_file_name}" | wc -c | xargs -I {} truncate -s -{} "${log_file_name}") \
|| echo "!!! Error processing \"$file\""
test -s "${log_file_name}" || echo "!!! Log file not created for \"$file\""
done
# TODO: not enough permission for this.
# - name: Delete old cache
# run: |
# echo "Fetching list of cache key"
# cacheKeys=$(gh cache list -R $REPO | cut -f 1)
# ## Setting this to not fail the workflow while deleting cache keys.
# set +e
# for cacheKey in $cacheKeys; do
# echo "Deleting $cacheKey"
# gh cache delete $cacheKey -R $REPO
# done
# env:
# GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
# REPO: ${{ github.repository }}