Skip to content

Commit

Permalink
Clean klee-stats, StatsTracker and cmake
Browse files Browse the repository at this point in the history
  • Loading branch information
@kren1 @MartinNowack
kren1 authored and MartinNowack committed Apr 4, 2019
1 parent b1f34f8 commit 572d644
Show file tree
Hide file tree
Showing 6 changed files with 262 additions and 236 deletions.
10 changes: 10 additions & 0 deletions CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -415,6 +415,16 @@ else()
message(STATUS "TCMalloc support disabled")
endif()

################################################################################
# Detect SQLite3
################################################################################
find_package(SQLite3)
if (SQLITE3_FOUND)
include_directories(${SQLITE3_INCLUDE_DIRS})
else()
message( FATAL_ERROR "SQLite3 not found, please install" )
endif()

################################################################################
# Detect libcap
################################################################################
Expand Down
37 changes: 37 additions & 0 deletions cmake/modules/FindSQLite3.cmake
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
# Copyright (C) 2007-2009 LuaDist.
# Created by Peter Kapec <kapecp@gmail.com>
# Redistribution and use of this file is allowed according to the terms of the MIT license.
# For details see the COPYRIGHT file distributed with LuaDist.
# Note:
# Searching headers and libraries is very simple and is NOT as powerful as scripts
# distributed with CMake, because LuaDist defines directories to search for.
# Everyone is encouraged to contact the author with improvements. Maybe this file
# becomes part of CMake distribution sometimes.

# - Find sqlite3
# Find the native SQLITE3 headers and libraries.
#
# SQLITE3_INCLUDE_DIRS - where to find sqlite3.h, etc.
# SQLITE3_LIBRARIES - List of libraries when using sqlite.
# SQLITE3_FOUND - True if sqlite found.

# Look for the header file.
FIND_PATH(SQLITE3_INCLUDE_DIR NAMES sqlite3.h)

# Look for the library.
FIND_LIBRARY(SQLITE3_LIBRARY NAMES sqlite3)

# Handle the QUIETLY and REQUIRED arguments and set SQLITE3_FOUND to TRUE if all listed variables are TRUE.
INCLUDE(FindPackageHandleStandardArgs)
FIND_PACKAGE_HANDLE_STANDARD_ARGS(SQLITE3 DEFAULT_MSG SQLITE3_LIBRARY SQLITE3_INCLUDE_DIR)

# Copy the results to the output variables.
IF(SQLITE3_FOUND)
SET(SQLITE3_LIBRARIES ${SQLITE3_LIBRARY})
SET(SQLITE3_INCLUDE_DIRS ${SQLITE3_INCLUDE_DIR})
ELSE(SQLITE3_FOUND)
SET(SQLITE3_LIBRARIES)
SET(SQLITE3_INCLUDE_DIRS)
ENDIF(SQLITE3_FOUND)

MARK_AS_ADVANCED(SQLITE3_INCLUDE_DIRS SQLITE3_LIBRARIES)
2 changes: 1 addition & 1 deletion lib/Core/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ set(LLVM_COMPONENTS
)

klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
target_link_libraries(kleeCore PUBLIC ${LLVM_LIBS} sqlite3)
target_link_libraries(kleeCore PUBLIC ${LLVM_LIBS} ${SQLITE3_LIBRARIES})
target_link_libraries(kleeCore PRIVATE
kleeBasic
kleeModule
Expand Down
256 changes: 132 additions & 124 deletions lib/Core/StatsTracker.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,12 +80,12 @@ cl::opt<unsigned> StatsWriteAfterInstructions(
"Write statistics after each n instructions, 0 to disable (default=0)"),
cl::cat(StatsCat));

cl::opt<unsigned> CommitEvery(
"stats-commit-after", cl::init(0),
cl::desc("Commit the statistics every N writes. Setting to 0 commits every "
"write in interval mode (default) or every 1000 writes in write after "
"N instructions (default=0)"),
cl::cat(StatsCat));
cl::opt<unsigned> CommitEvery(
"stats-commit-after", cl::init(0),
cl::desc("Commit the statistics every N writes. By default commit every "
"write with -stats-write-interval or every 1000 writes with "
"-stats-write-after-instructions. (default=0)"),
cl::cat(StatsCat));

cl::opt<std::string> IStatsWriteInterval(
"istats-write-interval", cl::init("10s"),
Expand Down Expand Up @@ -205,13 +205,11 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,

KModule *km = executor.kmodule.get();
if(CommitEvery > 0) {
commitEvery = CommitEvery.getValue();
statsCommitEvery = CommitEvery;
} else {
commitEvery = StatsWriteInterval > 0 ? 1 : 1000;
statsCommitEvery = StatsWriteInterval > 0 ? 1 : 1000;
}



if (!sys::path::is_absolute(objectFilename)) {
SmallString<128> current(objectFilename);
if(sys::fs::make_absolute(current)) {
Expand Down Expand Up @@ -248,11 +246,12 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
}

if (OutputStats) {
if(sqlite3_open(executor.interpreterHandler->getOutputFilename("run.stats").c_str(), &statsFile)){
std::stringstream error_s;
error_s << "Can't open database: " << sqlite3_errmsg(statsFile);
sqlite3_close(statsFile);
klee_error("%s", error_s.str().c_str());
auto db_filename = executor.interpreterHandler->getOutputFilename("run.stats");
if(sqlite3_open(db_filename.c_str(), &statsFile) != SQLITE_OK){
std::ostringstream errorstream;
errorstream << "Can't open database: " << sqlite3_errmsg(statsFile);
sqlite3_close(statsFile);
klee_error("%s",errorstream.str().c_str());
} else {
writeStatsHeader();
writeStatsLine();
Expand Down Expand Up @@ -280,8 +279,7 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
}

StatsTracker::~StatsTracker() {
char *zErrMsg;
sqlite3_exec(statsFile, "END TRANSACTION", NULL, NULL, &zErrMsg);
sqlite3_exec(statsFile, "END TRANSACTION", nullptr, nullptr, nullptr);
sqlite3_finalize(insertStmt);
sqlite3_close(statsFile);
}
Expand Down Expand Up @@ -387,6 +385,12 @@ void StatsTracker::framePopped(ExecutionState &es) {
// XXX remove me?
}

std::string sqlite3ErrToStringAndFree(const std::string& prefix , char* sqlite3ErrMsg) {
std::ostringstream sstream;
sstream << prefix << sqlite3ErrMsg;
sqlite3_free(sqlite3ErrMsg);
return sstream.str();
}

void StatsTracker::markBranchVisited(ExecutionState *visitedTrue,
ExecutionState *visitedFalse) {
Expand All @@ -413,130 +417,134 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue,
}

void StatsTracker::writeStatsHeader() {
std::stringstream create, insert;
std::ostringstream create, insert;
create << "CREATE TABLE stats ";
create << "(Instructions int,"
<< "FullBranches int,"
<< "PartialBranches int,"
<< "NumBranches int,"
<< "UserTime int,"
<< "NumStates int,"
<< "MallocUsage int,"
<< "NumQueries int,"
<< "NumQueryConstructs int,"
<< "NumObjects int,"
<< "WallTime int,"
<< "CoveredInstructions int,"
<< "UncoveredInstructions int,"
<< "QueryTime int,"
<< "SolverTime int,"
<< "CexCacheTime int,"
<< "ForkTime int,"
<< "ResolveTime int,"
<< "QueryCexCacheMisses int,"
create << "(Instructions INTEGER,"
<< "FullBranches INTEGER,"
<< "PartialBranches INTEGER,"
<< "NumBranches INTEGER,"
<< "UserTime REAL,"
<< "NumStates INTEGER,"
<< "MallocUsage INTEGER,"
<< "NumQueries INTEGER,"
<< "NumQueryConstructs INTEGER,"
<< "NumObjects INTEGER,"
<< "WallTime REAL,"
<< "CoveredInstructions INTEGER,"
<< "UncoveredInstructions INTEGER,"
<< "QueryTime INTEGER,"
<< "SolverTime INTEGER,"
<< "CexCacheTime INTEGER,"
<< "ForkTime INTEGER,"
<< "ResolveTime INTEGER,"
<< "QueryCexCacheMisses INTEGER,"
#ifdef KLEE_ARRAY_DEBUG
<< "ArrayHashTime int,"
<< "ArrayHashTime INTEGER,"
#endif
<< "QueryCexCacheHits int"
<< "QueryCexCacheHits INTEGER"
<< ")";
char *zErrMsg = 0;
if(sqlite3_exec(statsFile, create.str().c_str(), NULL, NULL, &zErrMsg)) {
klee_error("ERROR creating table: %s", zErrMsg);
return;
}
insert << "INSERT INTO stats ( "
<< "Instructions ,"
<< "FullBranches ,"
<< "PartialBranches ,"
<< "NumBranches ,"
<< "UserTime ,"
<< "NumStates ,"
<< "MallocUsage ,"
<< "NumQueries ,"
<< "NumQueryConstructs ,"
<< "NumObjects ,"
<< "WallTime ,"
<< "CoveredInstructions ,"
<< "UncoveredInstructions ,"
<< "QueryTime ,"
<< "SolverTime ,"
<< "CexCacheTime ,"
<< "ForkTime ,"
<< "ResolveTime ,"
<< "QueryCexCacheMisses ,"
char *zErrMsg = nullptr;
if(sqlite3_exec(statsFile, create.str().c_str(), nullptr, nullptr, &zErrMsg)) {
klee_error("%s", sqlite3ErrToStringAndFree("ERROR creating table: ", zErrMsg).c_str());
return;
}
insert << "INSERT INTO stats ( "
<< "Instructions ,"
<< "FullBranches ,"
<< "PartialBranches ,"
<< "NumBranches ,"
<< "UserTime ,"
<< "NumStates ,"
<< "MallocUsage ,"
<< "NumQueries ,"
<< "NumQueryConstructs ,"
<< "NumObjects ,"
<< "WallTime ,"
<< "CoveredInstructions ,"
<< "UncoveredInstructions ,"
<< "QueryTime ,"
<< "SolverTime ,"
<< "CexCacheTime ,"
<< "ForkTime ,"
<< "ResolveTime ,"
<< "QueryCexCacheMisses ,"
#ifdef KLEE_ARRAY_DEBUG
<< "ArrayHashTime,"
<< "ArrayHashTime,"
#endif
<< "QueryCexCacheHits "
<< ") VALUES ( "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "QueryCexCacheHits "
<< ") VALUES ( "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
<< "?, "
#ifdef KLEE_ARRAY_DEBUG
<< "?, "
<< "?, "
#endif
<< "? "
<< ")";
if(sqlite3_prepare_v2(statsFile, insert.str().c_str(), -1, &insertStmt, 0)) {
klee_error("Cannot create prepared statement! %s", sqlite3_errmsg(statsFile));
return;
}
sqlite3_exec(statsFile, "PRAGMA synchronous = OFF", NULL, NULL, &zErrMsg);
sqlite3_exec(statsFile, "BEGIN TRANSACTION", NULL, NULL, &zErrMsg);
<< "? "
<< ")";
if(sqlite3_prepare_v2(statsFile, insert.str().c_str(), -1, &insertStmt, nullptr) != SQLITE_OK) {
klee_error("Cannot create prepared statement! %s", sqlite3_errmsg(statsFile));
return;
}
sqlite3_exec(statsFile, "PRAGMA synchronous = OFF", nullptr, nullptr, nullptr);
sqlite3_exec(statsFile, "BEGIN TRANSACTION", nullptr, nullptr, nullptr);
}

time::Span StatsTracker::elapsed() {
return time::getWallTime() - startWallTime;
}

void StatsTracker::writeStatsLine() {
sqlite3_bind_int64(insertStmt, 1, stats::instructions);
sqlite3_bind_int64(insertStmt, 2, fullBranches);
sqlite3_bind_int64(insertStmt, 3, partialBranches);
sqlite3_bind_int64(insertStmt, 4, numBranches);
sqlite3_bind_int64(insertStmt, 5, time::getUserTime().toMicroseconds());
sqlite3_bind_int64(insertStmt, 6, executor.states.size());
sqlite3_bind_int64(insertStmt, 7, util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize());
sqlite3_bind_int64(insertStmt, 8, stats::queries);
sqlite3_bind_int64(insertStmt, 9, stats::queryConstructs);
sqlite3_bind_int64(insertStmt, 10, 0); // was numObjects
sqlite3_bind_int64(insertStmt, 11, elapsed().toMicroseconds());
sqlite3_bind_int64(insertStmt, 12, stats::coveredInstructions);
sqlite3_bind_int64(insertStmt, 13, stats::uncoveredInstructions);
sqlite3_bind_int64(insertStmt, 14, stats::queryTime);
sqlite3_bind_int64(insertStmt, 15, stats::solverTime);
sqlite3_bind_int64(insertStmt, 16, stats::cexCacheTime);
sqlite3_bind_int64(insertStmt, 17, stats::forkTime);
sqlite3_bind_int64(insertStmt, 18, stats::resolveTime);
sqlite3_bind_int64(insertStmt, 19, stats::queryCexCacheMisses);
sqlite3_bind_int64(insertStmt, 20, stats::queryCexCacheHits);
sqlite3_bind_int64(insertStmt, 1, stats::instructions);
sqlite3_bind_int64(insertStmt, 2, fullBranches);
sqlite3_bind_int64(insertStmt, 3, partialBranches);
sqlite3_bind_int64(insertStmt, 4, numBranches);
sqlite3_bind_int64(insertStmt, 5, time::getUserTime().toMicroseconds());
sqlite3_bind_int64(insertStmt, 6, executor.states.size());
sqlite3_bind_int64(insertStmt, 7, util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize());
sqlite3_bind_int64(insertStmt, 8, stats::queries);
sqlite3_bind_int64(insertStmt, 9, stats::queryConstructs);
sqlite3_bind_int64(insertStmt, 10, 0); // was numObjects
sqlite3_bind_int64(insertStmt, 11, elapsed().toMicroseconds());
sqlite3_bind_int64(insertStmt, 12, stats::coveredInstructions);
sqlite3_bind_int64(insertStmt, 13, stats::uncoveredInstructions);
sqlite3_bind_int64(insertStmt, 14, stats::queryTime);
sqlite3_bind_int64(insertStmt, 15, stats::solverTime);
sqlite3_bind_int64(insertStmt, 16, stats::cexCacheTime);
sqlite3_bind_int64(insertStmt, 17, stats::forkTime);
sqlite3_bind_int64(insertStmt, 18, stats::resolveTime);
sqlite3_bind_int64(insertStmt, 19, stats::queryCexCacheMisses);
sqlite3_bind_int64(insertStmt, 20, stats::queryCexCacheHits);
#ifdef KLEE_ARRAY_DEBUG
sqlite3_bind_int64(insertStmt, 21, stats::arrayHashTime);
sqlite3_bind_int64(insertStmt, 21, stats::arrayHashTime);
#endif
sqlite3_step(insertStmt);
sqlite3_reset(insertStmt);
if(writeCount % commitEvery == 0 ) {
char *zErrMsg = 0;
sqlite3_exec(statsFile, "END TRANSACTION", NULL, NULL, &zErrMsg);
sqlite3_exec(statsFile, "BEGIN TRANSACTION", NULL, NULL, &zErrMsg);
}
writeCount++;
int errCode = sqlite3_step(insertStmt);
if(errCode != SQLITE_DONE) klee_error("Error %d in sqlite3_step function", errCode);

errCode = sqlite3_reset(insertStmt);
if(errCode != SQLITE_OK) klee_error("Error %d in sqlite3_reset function", errCode);

if(statsWriteCount == statsCommitEvery) {
sqlite3_exec(statsFile, "END TRANSACTION", nullptr, nullptr, nullptr);
sqlite3_exec(statsFile, "BEGIN TRANSACTION", nullptr, nullptr, nullptr);
statsWriteCount = 0;
}
statsWriteCount++;
}

void StatsTracker::updateStateStatistics(uint64_t addend) {
Expand Down
8 changes: 4 additions & 4 deletions lib/Core/StatsTracker.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,10 +40,10 @@ namespace klee {
std::string objectFilename;

std::unique_ptr<llvm::raw_fd_ostream> istatsFile;
sqlite3 *statsFile;
sqlite3_stmt *insertStmt;
unsigned writeCount;
unsigned commitEvery;
sqlite3 *statsFile = nullptr;
sqlite3_stmt *insertStmt = nullptr;
std::uint32_t statsCommitEvery;
std::uint32_t statsWriteCount = 0;
time::Point startWallTime;

unsigned numBranches;
Expand Down
Loading

0 comments on commit 572d644

Please sign in to comment.