Change the .stats format into sqlite3

Improves querying of the .stats file, reduces its size, speeds up reads and
writes and has better defined fail behaviour.

6 files changed, 196 insertions, 82 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);
diff --git a/scripts/build/p-klee-linux-ubuntu-16.04.inc b/scripts/build/p-klee-linux-ubuntu-16.04.inc
index b4ba3f33..40582be5 100644
--- a/scripts/build/p-klee-linux-ubuntu-16.04.inc
+++ b/scripts/build/p-klee-linux-ubuntu-16.04.inc
@@ -4,11 +4,13 @@ install_build_dependencies_klee() {
   dependencies=(
     build-essential
     cmake
+    libsqlite3-dev
     python-pip #for lit
     python-setuptools #for lit
     python-wheel #for lit
     zlib1g-dev
     python3
+    python3-pip
   )
 
   if [[ $(to_bool "${COVERAGE}") -eq 1 ]]; then
@@ -18,4 +20,5 @@ install_build_dependencies_klee() {
   apt -y --no-install-recommends install "${dependencies[@]}"
 
   pip install lit
+  pip3 install tabulate --user
 }
\ No newline at end of file
diff --git a/test/regression/2017-03-23-early-exit-log-stats.c b/test/regression/2017-03-23-early-exit-log-stats.c
index 4de3aa3d..3a76b9f8 100644
--- a/test/regression/2017-03-23-early-exit-log-stats.c
+++ b/test/regression/2017-03-23-early-exit-log-stats.c
@@ -1,9 +1,10 @@
 // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // Delay writing instructions so that we ensure on exit that flush happens
-// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 %t.bc 2> %t.log
+// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 -stats-commit-after=1 %t.bc 2> %t.log
+// RUN: klee-stats -to-csv %t.klee-out > %t.stats.csv
 // RUN: FileCheck -check-prefix=CHECK-KLEE -input-file=%t.log %s
-// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.klee-out/run.stats %s
+// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats.csv %s
 #include "klee/klee.h"
 #include <stdlib.h>
 int main(){
@@ -17,6 +18,6 @@ int main(){
   return 0;
 }
 // First check we find a line with the expected format
-// CHECK-STATS:{{^\('Instructions'}}
+// CHECK-STATS:{{^Instructions}}
 // Now check that we eventually get a line where a non zero amount of instructions were executed
-// CHECK-STATS:{{^\([ ]*([1-9]|([1-9]+)[0-9])}}
+// CHECK-STATS:{{^\([ ]*[1-9]|([1-9]+)[0-9]}}
diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats
index 7989459f..ebe48753 100755
--- a/tools/klee-stats/klee-stats
+++ b/tools/klee-stats/klee-stats
@@ -20,6 +20,7 @@ import os
 import re
 import sys
 import argparse
+import sqlite3
 
 from operator import itemgetter
 try:
@@ -65,14 +66,27 @@ def getLogFile(path):
 
 class LazyEvalList:
     """Store all the lines in run.stats and eval() when needed."""
-    def __init__(self, lines):
+    def __init__(self, fileName):
         # The first line in the records contains headers.
-        self.lines = lines[1:]
+      #  self.lines = lines[1:]
+      self.conn = sqlite3.connect(fileName);
+      self.c = self.conn.cursor()
+      self.c.execute("SELECT * FROM stats ORDER BY Instructions DESC LIMIT 1")
+      self.lines = self.c.fetchone()
+
+    def aggregateRecords(self):
+        memC = self.conn.cursor()
+        memC.execute("SELECT max(MallocUsage) / 1024 / 1024, avg(MallocUsage) / 1024 / 1024 from stats")
+        maxMem, avgMem = memC.fetchone()
+
+        stateC = self.conn.cursor()
+        stateC.execute("SELECT max(NumStates), avg(NumStates) from stats")
+        maxStates, avgStates = stateC.fetchone()
+        return (maxMem, avgMem, maxStates, avgStates)
+
 
     def __getitem__(self, index):
-        if isinstance(self.lines[index], str):
-            self.lines[index] = eval(self.lines[index])
-        return self.lines[index]
+        return self.lines
 
     def __len__(self):
         return len(self.lines)
@@ -92,23 +106,6 @@ def getMatchedRecordIndex(records, column, target):
     return lo
 
 
-def aggregateRecords(records):
-    # index for memUsage and stateCount in run.stats
-    memIndex = 6
-    stateIndex = 5
-
-    # maximum and average memory usage
-    memValues = list(map(itemgetter(memIndex), records))
-    maxMem = max(memValues) / 1024 / 1024
-    avgMem = sum(memValues) / len(memValues) / 1024 / 1024
-
-    # maximum and average number of states
-    stateValues = list(map(itemgetter(stateIndex), records))
-    maxStates = max(stateValues)
-    avgStates = sum(stateValues) / len(stateValues)
-
-    return (maxMem, avgMem, maxStates, avgStates)
-
 
 def stripCommonPathPrefix(paths):
     paths = map(os.path.normpath, paths)
@@ -296,6 +293,9 @@ def main():
                         type=isPositiveInt, default='10', metavar='n',
                         help='Sample a data point every n lines for a '
                         'run.stats (default: 10)')
+    parser.add_argument('-to-csv',
+                          action='store_true', dest='toCsv',
+                          help='Dump run.stats to STDOUT in CSV format')
 
     # argument group for controlling output verboseness
     pControl = parser.add_mutually_exclusive_group(required=False)
@@ -343,6 +343,7 @@ def main():
 
     args = parser.parse_args()
 
+
     # get print controls
     pr = 'NONE'
     if args.pAll:
@@ -359,7 +360,21 @@ def main():
         print('no klee output dir found', file=sys.stderr)
         exit(1)
     # read contents from every run.stats file into LazyEvalList
-    data = [LazyEvalList(list(open(getLogFile(d)))) for d in dirs]
+    data = [LazyEvalList(getLogFile(d)) for d in dirs]
+
+    if args.toCsv:
+        import csv
+        data = data[0]
+        c = data.conn.cursor()
+        sql3_cursor = c.execute("SELECT * FROM stats")
+        csv_out = csv.writer(sys.stdout)
+        # write header                        
+        csv_out.writerow([d[0] for d in sql3_cursor.description])
+        # write data                          
+        for result in sql3_cursor:
+          csv_out.writerow(result)
+ 
+        return
     if len(data) > 1:
         dirs = stripCommonPathPrefix(dirs)
     # attach the stripped path
@@ -392,12 +407,12 @@ def main():
         if args.compBy:
             matchIndex = getMatchedRecordIndex(
                 records, itemgetter(compIndex), refValue)
-            stats = aggregateRecords(LazyEvalList(records[:matchIndex + 1]))
+            stats = recrods.aggregateRecords() # aggregateRecords(LazyEvalList(records[:matchIndex + 1]))
             totStats.append(stats)
             row.extend(getRow(records[matchIndex], stats, pr))
             totRecords.append(records[matchIndex])
         else:
-            stats = aggregateRecords(records)
+            stats = records.aggregateRecords()
             totStats.append(stats)
             row.extend(getRow(records[-1], stats, pr))
             totRecords.append(records[-1])