[Solver] Optionally dump kqueries which cost more time than previous …

…queries Note: Statistic QueryTimeMaxOnce is useless before this commit.
efeslab · Mar 3, 2021 · 0e02437 · 0e02437
1 parent 0f82e73
commit 0e02437
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 1 deletion.
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
@@ -16,7 +16,9 @@
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/ExprDebugHelper.h"
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/Internal/Support/MiscCmdLine.h"
 #include "klee/OptionCategories.h"
 #include "klee/Solver/SolverImpl.h"
 
@@ -333,7 +335,7 @@ bool STPSolverImpl::computeInitialValues(
     const Query &query, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char>> &values, bool &hasSolution) {
   runStatusCode = SOLVER_RUN_STATUS_FAILURE;
-  TimerStatIncrementer t(stats::queryTime);
+  TimerStatIncrementerWithMax t(stats::queryTime, stats::queryTimeMaxOnce);
 
   vc_push(vc);
 
@@ -365,6 +367,14 @@ bool STPSolverImpl::computeInitialValues(
     success = true;
   }
 
+  time::Span queryTimeOnce = t.check();
+  if (t.isMaxUpdated() && DebugDumpKQuery) {
+    char dumpfilename[128];
+    snprintf(dumpfilename, sizeof(dumpfilename), "queryTimeMaxOnce_%lu.kquery",
+             queryTimeOnce.toMicroseconds());
+    debugDumpConstraintsImpl(query.constraints, objects, dumpfilename);
+  }
+
   if (success) {
     if (hasSolution)
       ++stats::queriesInvalid;

diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
@@ -10,6 +10,7 @@
 #include "klee/Config/config.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Internal/Support/FileHandling.h"
+#include "klee/Internal/Support/MiscCmdLine.h"
 #include "klee/OptionCategories.h"
 
 #ifdef ENABLE_Z3
@@ -20,6 +21,7 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/ExprDebugHelper.h"
 #include "klee/Solver/Solver.h"
 #include "klee/Solver/SolverImpl.h"
 #include "llvm/Support/CommandLine.h"
@@ -326,6 +328,18 @@ bool Z3SolverImpl::internalRunSolver(
   // ``builder->construct()``.
   builder->clearConstructCache();
 
+  time::Span queryTimeOnce = t.check();
+  if (t.isMaxUpdated() && DebugDumpKQuery) {
+    if (objects) {
+      char dumpfilename[128];
+      snprintf(dumpfilename, sizeof(dumpfilename),
+               "queryTimeMaxOnce_%lu.kquery", queryTimeOnce.toMicroseconds());
+      debugDumpConstraintsImpl(query.constraints, *objects, dumpfilename);
+    } else {
+      klee_warning("queryTimeMaxOnce Updated but objects is NULL");
+    }
+  }
+
   if (runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE ||
       runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE) {
     if (hasSolution) {