about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/CMakeLists.txt2
-rw-r--r--lib/Core/StatsTracker.cpp190
-rw-r--r--lib/Core/StatsTracker.h9
3 files changed, 148 insertions, 53 deletions
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 83a6e001..4d0ec635 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -40,7 +40,7 @@ set(LLVM_COMPONENTS
 )
 
 klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
-target_link_libraries(kleeCore PUBLIC ${LLVM_LIBS})
+target_link_libraries(kleeCore PUBLIC ${LLVM_LIBS} sqlite3)
 target_link_libraries(kleeCore PRIVATE
   kleeBasic
   kleeModule
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index dac18370..4b557df2 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -80,6 +80,13 @@ 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<std::string> IStatsWriteInterval(
     "istats-write-interval", cl::init("10s"),
     cl::desc(
@@ -197,6 +204,13 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
         "time.");
 
   KModule *km = executor.kmodule.get();
+  if(CommitEvery > 0) {
+      commitEvery = CommitEvery.getValue();
+  } else {
+      commitEvery = StatsWriteInterval > 0 ? 1 : 1000;
+  }
+
+
 
   if (!sys::path::is_absolute(objectFilename)) {
     SmallString<128> current(objectFilename);
@@ -234,15 +248,17 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
   }
 
   if (OutputStats) {
-    statsFile = executor.interpreterHandler->openOutputFile("run.stats");
-    if (statsFile) {
+    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());
+    } else {
       writeStatsHeader();
       writeStatsLine();
 
       if (statsWriteInterval)
         executor.addTimer(new WriteStatsTimer(this), statsWriteInterval);
-    } else {
-      klee_error("Unable to open statistics trace file (run.stats).");
     }
   }
 
@@ -263,6 +279,13 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
   }
 }
 
+StatsTracker::~StatsTracker() {
+  char *zErrMsg;
+  sqlite3_exec(statsFile, "END TRANSACTION", NULL, NULL, &zErrMsg);
+  sqlite3_finalize(insertStmt);
+  sqlite3_close(statsFile);
+}
+
 void StatsTracker::done() {
   if (statsFile)
     writeStatsLine();
@@ -390,31 +413,92 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue,
 }
 
 void StatsTracker::writeStatsHeader() {
-  *statsFile << "('Instructions',"
-             << "'FullBranches',"
-             << "'PartialBranches',"
-             << "'NumBranches',"
-             << "'UserTime',"
-             << "'NumStates',"
-             << "'MallocUsage',"
-             << "'NumQueries',"
-             << "'NumQueryConstructs',"
-             << "'NumObjects',"
-             << "'WallTime',"
-             << "'CoveredInstructions',"
-             << "'UncoveredInstructions',"
-             << "'QueryTime',"
-             << "'SolverTime',"
-             << "'CexCacheTime',"
-             << "'ForkTime',"
-             << "'ResolveTime',"
-             << "'QueryCexCacheMisses',"
-             << "'QueryCexCacheHits',"
+  std::stringstream 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,"
+#ifdef KLEE_ARRAY_DEBUG
+	     << "ArrayHashTime int,"
+#endif
+             << "QueryCexCacheHits int"
+             << ")";
+       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 ,"
 #ifdef KLEE_ARRAY_DEBUG
-	     << "'ArrayHashTime',"
+              << "ArrayHashTime,"
 #endif
-             << ")\n";
-  statsFile->flush();
+              << "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);
 }
 
 time::Span StatsTracker::elapsed() {
@@ -422,31 +506,37 @@ time::Span StatsTracker::elapsed() {
 }
 
 void StatsTracker::writeStatsLine() {
-  *statsFile << "(" << stats::instructions
-             << "," << fullBranches
-             << "," << partialBranches
-             << "," << numBranches
-             << "," << time::getUserTime().toSeconds()
-             << "," << executor.states.size()
-             << "," << util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize()
-             << "," << stats::queries
-             << "," << stats::queryConstructs
-             << "," << 0 // was numObjects
-             << "," << elapsed().toSeconds()
-             << "," << stats::coveredInstructions
-             << "," << stats::uncoveredInstructions
-             << "," << time::microseconds(stats::queryTime).toSeconds()
-             << "," << time::microseconds(stats::solverTime).toSeconds()
-             << "," << time::microseconds(stats::cexCacheTime).toSeconds()
-             << "," << time::microseconds(stats::forkTime).toSeconds()
-             << "," << time::microseconds(stats::resolveTime).toSeconds()
-             << "," << stats::queryCexCacheMisses
-             << "," << 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
-             << "," << time::microseconds(stats::arrayHashTime).toSeconds()
+             sqlite3_bind_int64(insertStmt, 21, stats::arrayHashTime);
 #endif
-             << ")\n";
-  statsFile->flush();
+             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++;
 }
 
 void StatsTracker::updateStateStatistics(uint64_t addend) {
diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h
index 88e4cf30..f09f7638 100644
--- a/lib/Core/StatsTracker.h
+++ b/lib/Core/StatsTracker.h
@@ -15,6 +15,7 @@
 
 #include <memory>
 #include <set>
+#include <sqlite3.h>
 
 namespace llvm {
   class BranchInst;
@@ -38,7 +39,11 @@ namespace klee {
     Executor &executor;
     std::string objectFilename;
 
-    std::unique_ptr<llvm::raw_fd_ostream> statsFile, istatsFile;
+    std::unique_ptr<llvm::raw_fd_ostream> istatsFile;
+    sqlite3 *statsFile;
+    sqlite3_stmt *insertStmt;
+    unsigned writeCount;
+    unsigned commitEvery;
     time::Point startWallTime;
 
     unsigned numBranches;
@@ -61,7 +66,7 @@ namespace klee {
   public:
     StatsTracker(Executor &_executor, std::string _objectFilename,
                  bool _updateMinDistToUncovered);
-    ~StatsTracker() = default;
+    ~StatsTracker();
 
     // called after a new StackFrame has been pushed (for callpath tracing)
     void framePushed(ExecutionState &es, StackFrame *parentFrame);
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-29 10:35:54 +0000