Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update KLEE #688

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/matrix.json
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{
"include": [
{
"DOCKER_TAG": "2024.03.0",
"DOCKER_TAG": "2024.08.0",
"OPERATING_SYSTEM_TAG": "20.04",
"LLVM_VERSION_MAJOR": "14"
}
Expand Down
4 changes: 3 additions & 1 deletion docker/Dockerfile_base
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ WORKDIR docker
# Install required system packages
RUN apt update
RUN DEBIAN_FRONTEND=noninteractive apt install -y --no-install-recommends sudo file python3-dateutil wget fakeroot libssl-dev build-essential \
software-properties-common
software-properties-common pkg-config
RUN echo "check_certificate = off" > /etc/wgetrc

# We use C++ 17 for UnitTestBot, it is available in gcc-9; default gcc for ubuntu:18.04 is gcc-7
Expand Down Expand Up @@ -217,6 +217,8 @@ RUN ./configure --make-llvm-lib && make -j`nproc`

# Download library for access private members
RUN git clone https://github.com/martong/access_private.git $UTBOT_ALL/access_private
RUN git clone https://github.com/arximboldi/immer.git $UTBOT_ALL/immer
RUN git clone https://github.com/nlohmann/json.git $UTBOT_ALL/json

RUN apt autoclean

Expand Down
10 changes: 5 additions & 5 deletions server/src/KleeRunner.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,9 +58,9 @@ void KleeRunner::runKlee(const std::vector<tests::TestMethod> &testMethods,
LOG_SCOPE_FUNCTION(DEBUG);

fs::path kleeOutDir = Paths::getKleeOutDir(projectContext);
if (fs::exists(kleeOutDir)) {
FileSystemUtils::removeAll(kleeOutDir);
}
// if (fs::exists(kleeOutDir)) {
// FileSystemUtils::removeAll(kleeOutDir);
// }
fs::create_directories(kleeOutDir);
CollectionUtils::MapFileTo<std::vector<TestMethod>> fileToMethods;
for (const auto &method : testMethods) {
Expand Down Expand Up @@ -219,9 +219,9 @@ KleeRunner::createKleeParams(const tests::TestMethod &testMethod,

std::vector<std::string> argvData = {
"klee",
"--entry-point=" + KleeUtils::entryPointFunction(tests, testMethod.methodName, true),
"--entry-points=" + KleeUtils::entryPointFunction(tests, testMethod.methodName, true),
"--libc=klee",
"--utbot",
// "--utbot",
"--posix-runtime",
"--skip-not-lazy-initialized",
"--min-number-elements-li=1",
Expand Down
3 changes: 2 additions & 1 deletion server/src/Server.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -312,7 +312,8 @@ Status Server::TestsGenServiceImpl::ProcessBaseTestRequest(BaseTestGen &testGen,
fetcher.getStructsToDeclare(), testGen.serverBuildDir, typesHandler)
.generateTestHeaders(testGen.tests, stubGen, selectedTargets, testGen.progressWriter);
KleeRunner kleeRunner{testGen.projectContext, testGen.settingsContext};
bool interactiveMode = (dynamic_cast<ProjectTestGen *>(&testGen) != nullptr);
// bool interactiveMode = (dynamic_cast<ProjectTestGen *>(&testGen) != nullptr);
bool interactiveMode = false;
auto generationStartTime = std::chrono::steady_clock::now();
StatsUtils::TestsGenerationStatsFileMap generationStatsMap(testGen.projectContext,
std::chrono::duration_cast<std::chrono::milliseconds>(
Expand Down
3 changes: 3 additions & 0 deletions submodules/build-klee.sh
Original file line number Diff line number Diff line change
Expand Up @@ -21,13 +21,16 @@ $UTBOT_CMAKE_BINARY -G Ninja \
-DENABLE_SYSTEM_TESTS=TRUE \
-DGTEST_SRC_DIR=$UTBOT_ALL/gtest \
-DGTEST_INCLUDE_DIR=$UTBOT_ALL/gtest/googletest/include \
-DJSON_SRC_DIR=$UTBOT_ALL/json \
-DIMMER_SRC_DIR=$UTBOT_ALL/immer \
-DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/klee \
-DENABLE_KLEE_LIBCXX=TRUE \
-DKLEE_LIBCXX_DIR=$UTBOT_ALL/libcxx/install \
-DKLEE_LIBCXX_INCLUDE_DIR=$UTBOT_ALL/libcxx/install/include/c++/v1 \
-DENABLE_KLEE_EH_CXX=TRUE \
-DKLEE_LIBCXXABI_SRC_DIR=$UTBOT_ALL/libcxx/libcxxabi \
-DCMAKE_BUILD_TYPE=RelWithDebInfo \
-DWARNINGS_AS_ERRORS=OFF \
..

$UTBOT_CMAKE_BINARY --build .
Expand Down
2 changes: 1 addition & 1 deletion submodules/klee
Submodule klee updated 568 files
Loading