StatsTracker: remove NumObjects, fix assignment of and always write ArrayHashTime

* fix binding order for assignments when KLEE_ARRAY_DEBUG enabled
* always write ArrayHashTime column to run.stats, assign -1 when KLEE_ARRAY_DEBUG disabled
* remove unused NumObjects column from run.stats
* remove NumObjects panel from Grafana

2 files changed, 73 insertions, 249 deletions

diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 20944061..0c2886b8 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -432,8 +432,8 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue,
 
 void StatsTracker::writeStatsHeader() {
   std::ostringstream create, insert;
-  create << "CREATE TABLE stats ";
-  create     << "(Instructions INTEGER,"
+  create << "CREATE TABLE stats ("
+             << "Instructions INTEGER,"
              << "FullBranches INTEGER,"
              << "PartialBranches INTEGER,"
              << "NumBranches INTEGER,"
@@ -442,7 +442,6 @@ void StatsTracker::writeStatsHeader() {
              << "MallocUsage INTEGER,"
              << "NumQueries INTEGER,"
              << "NumQueryConstructs INTEGER,"
-             << "NumObjects INTEGER,"
              << "WallTime REAL,"
              << "CoveredInstructions INTEGER,"
              << "UncoveredInstructions INTEGER,"
@@ -452,11 +451,9 @@ void StatsTracker::writeStatsHeader() {
              << "ForkTime INTEGER,"
              << "ResolveTime INTEGER,"
              << "QueryCexCacheMisses INTEGER,"
-#ifdef KLEE_ARRAY_DEBUG
-	           << "ArrayHashTime INTEGER,"
-#endif
-             << "QueryCexCacheHits INTEGER"
-             << ")";
+             << "QueryCexCacheHits INTEGER,"
+             << "ArrayHashTime INTEGER"
+         << ')';
   char *zErrMsg = nullptr;
   if(sqlite3_exec(statsFile, create.str().c_str(), nullptr, nullptr, &zErrMsg)) {
     klee_error("%s", sqlite3ErrToStringAndFree("ERROR creating table: ", zErrMsg).c_str());
@@ -468,55 +465,49 @@ void StatsTracker::writeStatsHeader() {
    * happen, but if it does this statement will fail with SQLITE_CONSTRAINT error. If this happens you should either
    * remove the constraints or consider using `IGNORE` mode.
    */
-  insert << "INSERT OR FAIL 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,"
-#endif
-             << "QueryCexCacheHits "
-             << ") VALUES ( "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-             << "?, "
-#ifdef KLEE_ARRAY_DEBUG
-             << "?, "
-#endif
+  insert << "INSERT OR FAIL INTO stats ("
+             << "Instructions,"
+             << "FullBranches,"
+             << "PartialBranches,"
+             << "NumBranches,"
+             << "UserTime,"
+             << "NumStates,"
+             << "MallocUsage,"
+             << "NumQueries,"
+             << "NumQueryConstructs,"
+             << "WallTime,"
+             << "CoveredInstructions,"
+             << "UncoveredInstructions,"
+             << "QueryTime,"
+             << "SolverTime,"
+             << "CexCacheTime,"
+             << "ForkTime,"
+             << "ResolveTime,"
+             << "QueryCexCacheMisses,"
+             << "QueryCexCacheHits,"
+             << "ArrayHashTime"
+         << ") VALUES ("
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
+             << "?,"
              << "? "
-             << ")";
+         << ')';
 
   if(sqlite3_prepare_v2(statsFile, insert.str().c_str(), -1, &insertStmt, nullptr) != SQLITE_OK) {
     klee_error("Cannot create prepared statement: %s", sqlite3_errmsg(statsFile));
@@ -537,19 +528,20 @@ void StatsTracker::writeStatsLine() {
   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, 10, elapsed().toMicroseconds());
+  sqlite3_bind_int64(insertStmt, 11, stats::coveredInstructions);
+  sqlite3_bind_int64(insertStmt, 12, stats::uncoveredInstructions);
+  sqlite3_bind_int64(insertStmt, 13, stats::queryTime);
+  sqlite3_bind_int64(insertStmt, 14, stats::solverTime);
+  sqlite3_bind_int64(insertStmt, 15, stats::cexCacheTime);
+  sqlite3_bind_int64(insertStmt, 16, stats::forkTime);
+  sqlite3_bind_int64(insertStmt, 17, stats::resolveTime);
+  sqlite3_bind_int64(insertStmt, 18, stats::queryCexCacheMisses);
+  sqlite3_bind_int64(insertStmt, 19, stats::queryCexCacheHits);
 #ifdef KLEE_ARRAY_DEBUG
-  sqlite3_bind_int64(insertStmt, 21, stats::arrayHashTime);
+  sqlite3_bind_int64(insertStmt, 20, stats::arrayHashTime);
+#else
+  sqlite3_bind_int64(insertStmt, 20, -1LL);
 #endif
   int errCode = sqlite3_step(insertStmt);
   if(errCode != SQLITE_DONE) klee_error("Error writing stats data: %s", sqlite3_errmsg(statsFile));
diff --git a/utils/grafana/klee_dashboard.json b/utils/grafana/klee_dashboard.json
index c895dce0..3b653bab 100644
--- a/utils/grafana/klee_dashboard.json
+++ b/utils/grafana/klee_dashboard.json
@@ -1885,174 +1885,6 @@
         "x": 0,
         "y": 79
       },
-      "id": 50,
-      "interval": null,
-      "links": [],
-      "mappingType": 1,
-      "mappingTypes": [
-        {
-          "name": "value to text",
-          "value": 1
-        },
-        {
-          "name": "range to text",
-          "value": 2
-        }
-      ],
-      "maxDataPoints": 100,
-      "nullPointMode": "connected",
-      "nullText": null,
-      "options": {},
-      "postfix": "",
-      "postfixFontSize": "50%",
-      "prefix": "",
-      "prefixFontSize": "50%",
-      "rangeMaps": [
-        {
-          "from": "null",
-          "text": "N/A",
-          "to": "null"
-        }
-      ],
-      "sparkline": {
-        "fillColor": "rgba(31, 118, 189, 0.18)",
-        "full": false,
-        "lineColor": "rgb(31, 120, 193)",
-        "show": false,
-        "ymax": null,
-        "ymin": null
-      },
-      "tableColumn": "",
-      "targets": [
-        {
-          "refId": "A",
-          "target": "NumObjects",
-          "type": "timeserie"
-        }
-      ],
-      "thresholds": "",
-      "timeFrom": null,
-      "timeShift": null,
-      "title": "Num Objects ",
-      "type": "singlestat",
-      "valueFontSize": "80%",
-      "valueMaps": [
-        {
-          "op": "=",
-          "text": "N/A",
-          "value": "null"
-        }
-      ],
-      "valueName": "current"
-    },
-    {
-      "aliasColors": {},
-      "bars": false,
-      "dashLength": 10,
-      "dashes": false,
-      "fill": 1,
-      "fillGradient": 0,
-      "gridPos": {
-        "h": 8,
-        "w": 15,
-        "x": 7,
-        "y": 79
-      },
-      "id": 48,
-      "legend": {
-        "avg": false,
-        "current": false,
-        "max": false,
-        "min": false,
-        "show": true,
-        "total": false,
-        "values": false
-      },
-      "lines": true,
-      "linewidth": 1,
-      "nullPointMode": "null",
-      "options": {
-        "dataLinks": []
-      },
-      "percentage": false,
-      "pointradius": 2,
-      "points": false,
-      "renderer": "flot",
-      "seriesOverrides": [],
-      "spaceLength": 10,
-      "stack": false,
-      "steppedLine": false,
-      "targets": [
-        {
-          "refId": "A",
-          "target": "NumObjects",
-          "type": "timeserie"
-        }
-      ],
-      "thresholds": [],
-      "timeFrom": null,
-      "timeRegions": [],
-      "timeShift": null,
-      "title": "Num Objects",
-      "tooltip": {
-        "shared": true,
-        "sort": 0,
-        "value_type": "individual"
-      },
-      "type": "graph",
-      "xaxis": {
-        "buckets": null,
-        "mode": "time",
-        "name": null,
-        "show": true,
-        "values": []
-      },
-      "yaxes": [
-        {
-          "format": "short",
-          "label": null,
-          "logBase": 1,
-          "max": null,
-          "min": null,
-          "show": true
-        },
-        {
-          "format": "short",
-          "label": null,
-          "logBase": 1,
-          "max": null,
-          "min": null,
-          "show": true
-        }
-      ],
-      "yaxis": {
-        "align": false,
-        "alignLevel": null
-      }
-    },
-    {
-      "cacheTimeout": null,
-      "colorBackground": true,
-      "colorValue": false,
-      "colors": [
-        "#3274D9",
-        "#3274D9",
-        "#d44a3a"
-      ],
-      "format": "locale",
-      "gauge": {
-        "maxValue": 100,
-        "minValue": 0,
-        "show": false,
-        "thresholdLabels": false,
-        "thresholdMarkers": true
-      },
-      "gridPos": {
-        "h": 8,
-        "w": 7,
-        "x": 0,
-        "y": 87
-      },
       "id": 64,
       "interval": null,
       "links": [],
@@ -2124,7 +1956,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 87
+        "y": 79
       },
       "id": 62,
       "legend": {
@@ -2219,7 +2051,7 @@
         "h": 8,
         "w": 7,
         "x": 0,
-        "y": 95
+        "y": 87
       },
       "id": 66,
       "interval": null,
@@ -2290,7 +2122,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 95
+        "y": 87
       },
       "id": 60,
       "legend": {
@@ -2385,7 +2217,7 @@
         "h": 8,
         "w": 7,
         "x": 0,
-        "y": 103
+        "y": 95
       },
       "id": 68,
       "interval": null,
@@ -2456,7 +2288,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 103
+        "y": 95
       },
       "id": 58,
       "legend": {
@@ -2551,7 +2383,7 @@
         "h": 7,
         "w": 7,
         "x": 0,
-        "y": 111
+        "y": 103
       },
       "id": 70,
       "interval": null,
@@ -2622,7 +2454,7 @@
         "h": 7,
         "w": 15,
         "x": 7,
-        "y": 111
+        "y": 103
       },
       "id": 56,
       "legend": {
@@ -2718,7 +2550,7 @@
         "h": 8,
         "w": 7,
         "x": 0,
-        "y": 118
+        "y": 110
       },
       "id": 72,
       "interval": null,
@@ -2789,7 +2621,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 118
+        "y": 110
       },
       "id": 52,
       "legend": {
@@ -2886,7 +2718,7 @@
         "h": 7,
         "w": 7,
         "x": 0,
-        "y": 126
+        "y": 118
       },
       "id": 74,
       "interval": null,
@@ -2957,7 +2789,7 @@
         "h": 7,
         "w": 15,
         "x": 7,
-        "y": 126
+        "y": 118
       },
       "id": 54,
       "legend": {
@@ -3052,7 +2884,7 @@
         "h": 7,
         "w": 7,
         "x": 0,
-        "y": 133
+        "y": 125
       },
       "id": 76,
       "interval": null,
@@ -3123,7 +2955,7 @@
         "h": 7,
         "w": 15,
         "x": 7,
-        "y": 133
+        "y": 125
       },
       "id": 34,
       "legend": {