Skip to content

Commit a568133

Browse files
metametamoonmetametamoon
committed
tmp: debug ci macos
1 parent d9cce39 commit a568133

4 files changed

Lines changed: 156 additions & 154 deletions

File tree

‎.github/workflows/build.yaml‎

Lines changed: 149 additions & 149 deletions
Original file line numberDiff line numberDiff line change
@@ -43,118 +43,118 @@ env:
4343
IMMER_VERSION: v0.8.1
4444

4545
jobs:
46-
Linux:
47-
runs-on: ubuntu-22.04
48-
strategy:
49-
matrix:
50-
name: [
51-
"LLVM 16",
52-
"LLVM 15",
53-
"LLVM 14",
54-
"LLVM 13",
55-
"LLVM 12",
56-
"LLVM 11, Doxygen",
57-
"ASan",
58-
"UBSan",
59-
"MSan",
60-
"Z3 only",
61-
"metaSMT",
62-
"STP master",
63-
"Bitwuzla only",
64-
"Latest klee-uclibc",
65-
"Asserts disabled",
66-
"No TCMalloc, optimised runtime",
67-
]
68-
include:
69-
- name: "LLVM 16"
70-
env:
71-
LLVM_VERSION: 16
72-
- name: "LLVM 15"
73-
env:
74-
LLVM_VERSION: 15
75-
- name: "LLVM 14"
76-
env:
77-
LLVM_VERSION: 14
78-
- name: "LLVM 13"
79-
env:
80-
LLVM_VERSION: 13
81-
- name: "LLVM 12"
82-
env:
83-
LLVM_VERSION: 12
84-
- name: "LLVM 11, Doxygen"
85-
env:
86-
LLVM_VERSION: 11
87-
ENABLE_DOXYGEN: 1
88-
# Sanitizer builds. Do unoptimized build otherwise the optimizer
89-
# might remove problematic code
90-
- name: "ASan"
91-
env:
92-
SANITIZER_BUILD: address
93-
ENABLE_OPTIMIZED: 0
94-
USE_TCMALLOC: 0
95-
SANITIZER_LLVM_VERSION: 12
96-
- name: "UBSan"
97-
env:
98-
SANITIZER_BUILD: undefined
99-
ENABLE_OPTIMIZED: 0
100-
USE_TCMALLOC: 0
101-
SANITIZER_LLVM_VERSION: 12
102-
- name: "MSan"
103-
env:
104-
SANITIZER_BUILD: memory
105-
ENABLE_OPTIMIZED: 0
106-
USE_TCMALLOC: 0
107-
SOLVERS: STP
108-
SANITIZER_LLVM_VERSION: 14
109-
# Test just using Z3 only
110-
- name: "Z3 only"
111-
env:
112-
SOLVERS: Z3
113-
# Test just using metaSMT
114-
- name: "metaSMT"
115-
env:
116-
METASMT_VERSION: qf_abv
117-
SOLVERS: metaSMT
118-
METASMT_DEFAULT: STP
119-
REQUIRES_RTTI: 1
120-
# Test we can build against STP master
121-
- name: "STP master"
122-
env:
123-
SOLVERS: STP
124-
STP_VERSION: master
125-
# Test just using Bitwuzla only
126-
- name: "Bitwuzla only"
127-
env:
128-
SOLVERS: BITWUZLA
129-
# Check we can build latest klee-uclibc branch
130-
- name: "Latest klee-uclibc"
131-
env:
132-
UCLIBC_VERSION: klee_0_9_29
133-
# Check at least one build with Asserts disabled.
134-
- name: "Asserts disabled"
135-
env:
136-
DISABLE_ASSERTIONS: 1
137-
# Check without TCMALLOC and with an optimised runtime library
138-
- name: "No TCMalloc, optimised runtime"
139-
env:
140-
SOLVERS: STP
141-
USE_TCMALLOC: 0
142-
KLEE_RUNTIME_BUILD: "Release+Debug+Asserts"
143-
steps:
144-
- name: Checkout KLEE source code
145-
uses: actions/checkout@v3
146-
with:
147-
submodules: recursive
148-
- name: Memory layout fix for old clang
149-
run: |
150-
# TODO remove this once upstream fix is available
151-
sudo sysctl -w vm.mmap_rnd_bits=28
152-
- name: Build KLEE
153-
env: ${{ matrix.env }}
154-
run: scripts/build/build.sh klee --docker --create-final-image
155-
- name: Run tests
156-
env: ${{ matrix.env }}
157-
run: scripts/build/run-tests.sh --run-docker --debug
46+
# Linux:
47+
# runs-on: ubuntu-22.04
48+
# strategy:
49+
# matrix:
50+
# name: [
51+
# "LLVM 16",
52+
# "LLVM 15",
53+
# "LLVM 14",
54+
# "LLVM 13",
55+
# "LLVM 12",
56+
# "LLVM 11, Doxygen",
57+
# "ASan",
58+
# "UBSan",
59+
# "MSan",
60+
# "Z3 only",
61+
# "metaSMT",
62+
# "STP master",
63+
# "Bitwuzla only",
64+
# "Latest klee-uclibc",
65+
# "Asserts disabled",
66+
# "No TCMalloc, optimised runtime",
67+
# ]
68+
# include:
69+
# - name: "LLVM 16"
70+
# env:
71+
# LLVM_VERSION: 16
72+
# - name: "LLVM 15"
73+
# env:
74+
# LLVM_VERSION: 15
75+
# - name: "LLVM 14"
76+
# env:
77+
# LLVM_VERSION: 14
78+
# - name: "LLVM 13"
79+
# env:
80+
# LLVM_VERSION: 13
81+
# - name: "LLVM 12"
82+
# env:
83+
# LLVM_VERSION: 12
84+
# - name: "LLVM 11, Doxygen"
85+
# env:
86+
# LLVM_VERSION: 11
87+
# ENABLE_DOXYGEN: 1
88+
# # Sanitizer builds. Do unoptimized build otherwise the optimizer
89+
# # might remove problematic code
90+
# - name: "ASan"
91+
# env:
92+
# SANITIZER_BUILD: address
93+
# ENABLE_OPTIMIZED: 0
94+
# USE_TCMALLOC: 0
95+
# SANITIZER_LLVM_VERSION: 12
96+
# - name: "UBSan"
97+
# env:
98+
# SANITIZER_BUILD: undefined
99+
# ENABLE_OPTIMIZED: 0
100+
# USE_TCMALLOC: 0
101+
# SANITIZER_LLVM_VERSION: 12
102+
# - name: "MSan"
103+
# env:
104+
# SANITIZER_BUILD: memory
105+
# ENABLE_OPTIMIZED: 0
106+
# USE_TCMALLOC: 0
107+
# SOLVERS: STP
108+
# SANITIZER_LLVM_VERSION: 14
109+
# # Test just using Z3 only
110+
# - name: "Z3 only"
111+
# env:
112+
# SOLVERS: Z3
113+
# # Test just using metaSMT
114+
# - name: "metaSMT"
115+
# env:
116+
# METASMT_VERSION: qf_abv
117+
# SOLVERS: metaSMT
118+
# METASMT_DEFAULT: STP
119+
# REQUIRES_RTTI: 1
120+
# # Test we can build against STP master
121+
# - name: "STP master"
122+
# env:
123+
# SOLVERS: STP
124+
# STP_VERSION: master
125+
# # Test just using Bitwuzla only
126+
# - name: "Bitwuzla only"
127+
# env:
128+
# SOLVERS: BITWUZLA
129+
# # Check we can build latest klee-uclibc branch
130+
# - name: "Latest klee-uclibc"
131+
# env:
132+
# UCLIBC_VERSION: klee_0_9_29
133+
# # Check at least one build with Asserts disabled.
134+
# - name: "Asserts disabled"
135+
# env:
136+
# DISABLE_ASSERTIONS: 1
137+
# # Check without TCMALLOC and with an optimised runtime library
138+
# - name: "No TCMalloc, optimised runtime"
139+
# env:
140+
# SOLVERS: STP
141+
# USE_TCMALLOC: 0
142+
# KLEE_RUNTIME_BUILD: "Release+Debug+Asserts"
143+
# steps:
144+
# - name: Checkout KLEE source code
145+
# uses: actions/checkout@v3
146+
# with:
147+
# submodules: recursive
148+
# - name: Memory layout fix for old clang
149+
# run: |
150+
# # TODO remove this once upstream fix is available
151+
# sudo sysctl -w vm.mmap_rnd_bits=28
152+
# - name: Build KLEE
153+
# env: ${{ matrix.env }}
154+
# run: scripts/build/build.sh klee --docker --create-final-image
155+
# - name: Run tests
156+
# env: ${{ matrix.env }}
157+
# run: scripts/build/run-tests.sh --run-docker --debug
158158

159159

160160
macOS:
@@ -190,43 +190,43 @@ jobs:
190190
- name: Build Docker image
191191
run: docker build .
192192

193-
Coverage:
194-
runs-on: ubuntu-latest
195-
strategy:
196-
matrix:
197-
name: [
198-
"STP",
199-
"Z3",
200-
"Bitwuzla",
201-
]
202-
include:
203-
- name: "STP"
204-
env:
205-
SOLVERS: STP
206-
- name: "Z3"
207-
env:
208-
SOLVERS: Z3:STP
209-
- name: "Bitwuzla"
210-
env:
211-
SOLVERS: BITWUZLA:Z3
212-
env:
213-
ENABLE_OPTIMIZED: 0
214-
COVERAGE: 1
215-
steps:
216-
- name: Checkout KLEE source code
217-
uses: actions/checkout@v3
218-
with:
219-
# Codecov may run into "Issue detecting commit SHA. Please run
220-
# actions/checkout with fetch-depth > 1 or set to 0" when uploading.
221-
# See also https://github.com/codecov/codecov-action/issues/190
222-
fetch-depth: 2
223-
submodules: recursive
224-
- name: Build KLEE
225-
env: ${{ matrix.env }}
226-
run: scripts/build/build.sh klee --docker --create-final-image
227-
- name: Run tests
228-
env: ${{ matrix.env }}
229-
run: scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug
193+
# Coverage:
194+
# runs-on: ubuntu-latest
195+
# strategy:
196+
# matrix:
197+
# name: [
198+
# "STP",
199+
# "Z3",
200+
# "Bitwuzla",
201+
# ]
202+
# include:
203+
# - name: "STP"
204+
# env:
205+
# SOLVERS: STP
206+
# - name: "Z3"
207+
# env:
208+
# SOLVERS: Z3:STP
209+
# - name: "Bitwuzla"
210+
# env:
211+
# SOLVERS: BITWUZLA:Z3
212+
# env:
213+
# ENABLE_OPTIMIZED: 0
214+
# COVERAGE: 1
215+
# steps:
216+
# - name: Checkout KLEE source code
217+
# uses: actions/checkout@v3
218+
# with:
219+
# # Codecov may run into "Issue detecting commit SHA. Please run
220+
# # actions/checkout with fetch-depth > 1 or set to 0" when uploading.
221+
# # See also https://github.com/codecov/codecov-action/issues/190
222+
# fetch-depth: 2
223+
# submodules: recursive
224+
# - name: Build KLEE
225+
# env: ${{ matrix.env }}
226+
# run: scripts/build/build.sh klee --docker --create-final-image
227+
# - name: Run tests
228+
# env: ${{ matrix.env }}
229+
# run: scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug
230230

231231
clang-format:
232232
runs-on: ubuntu-latest

‎build.sh‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ ENABLE_WARNINGS_AS_ERRORS=0
3636

3737
## Solvers Required options
3838
# SOLVERS=STP
39-
SOLVERS=BITWUZLA:Z3:STP
39+
SOLVERS=metaSMT
4040

4141
## Google Test Required options
4242
GTEST_VERSION=1.16.0
@@ -58,6 +58,8 @@ STP_VERSION=2.3.3
5858
MINISAT_VERSION=master
5959

6060
BITWUZLA_VERSION=0.7.0
61+
METASMT_VERSION=qf_abv
62+
METASMT_DEFAULT=STP
6163

6264
KEEP_PARSE="true"
6365
while [ $KEEP_PARSE = "true" ]; do
@@ -72,4 +74,4 @@ else
7274
fi
7375
done
7476

75-
BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME ./scripts/build/build.sh klee --install-system-deps
77+
BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME METASMT_VERSION=$METASMT_VERSION METASMT_DEFAULT=$METASMT_DEFAULT ./scripts/build/build.sh klee --install-system-deps

‎lib/Solver/Z3CoreBuilder.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref<Expr> e, int *width_out) {
206206
switch (e->getKind()) {
207207
case Expr::Pointer:
208208
case Expr::ConstantPointer: {
209-
assert(0 && "unreachable");
209+
return constructActual(e->getValue(), width_out);
210210
}
211211

212212
case Expr::Constant: {

‎test/Bidirectional/Memory/cond-function-pointer-change.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc
22
// RUN: rm -rf %t.klee-out
3-
// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log
4-
// RUN: FileCheck %s -input-file=%t.log
3+
// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log || echo "ok"
4+
// RUN: FileCheck %s -input-file=%t.log --dump-input-filter=all
55

66
#include "klee/klee.h"
77
#include <assert.h>

0 commit comments

Comments
 (0)