about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2020-12-22 19:52:12 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2021-04-20 11:42:23 +0100
commitc8ef08267fd5e67f40defac1ae692e8ec906fa3f (patch)
treefa09f1ffa7bac2b2a75b6e32c67dd7cf904bce02 /lib/Core
parent88893697f6630f0d281d21be6362489e616bca2f (diff)
downloadklee-c8ef08267fd5e67f40defac1ae692e8ec906fa3f.tar.gz
Added -max-static-pct-check-delay to replace the hardcoded delay after which the MaxStatic*Pct checks are performed.
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp12
-rw-r--r--lib/Core/Executor.h3
2 files changed, 14 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index cea7f173..cc3ac50f 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -365,6 +365,12 @@ cl::opt<double> MaxStaticCPSolvePct(
              "instructions (default=1.0 (always))"),
     cl::cat(TerminationCat));
 
+cl::opt<std::string> MaxStaticPctCheckDelay(
+    "max-static-pct-check-delay",
+    cl::desc("Time after which the --max-static-*-pct checks are enforced (default=60s)"),
+    cl::init("60s"),
+    cl::cat(TerminationCat));
+
 cl::opt<std::string> TimerInterval(
     "timer-interval",
     cl::desc("Minimum interval to check timers. "
@@ -485,6 +491,8 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
   this->solver = new TimingSolver(solver, EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
 
+  maxStaticPctCheckDelay = time::Span{MaxStaticPctCheckDelay};
+
   initializeSearchOptions();
 
   if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats())
@@ -971,7 +979,9 @@ ref<Expr> Executor::maxStaticPctChecks(ExecutionState &current,
       MaxStaticCPForkPct == 1. && MaxStaticCPSolvePct == 1.)
     return condition;
 
-  if (statsTracker->elapsed() <= time::seconds(60))
+  // these checks are performed only after MaxStaticPctCheckDelay time has
+  // passed since execution started
+  if (statsTracker->elapsed() <= maxStaticPctCheckDelay)
     return condition;
 
   StatisticManager &sm = *theStatisticManager;
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index ae960731..db8e508c 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -205,6 +205,9 @@ private:
   /// Maximum time to allow for a single instruction.
   time::Span maxInstructionTime;
 
+  /// Time after which the --max-static-*-pct checks are enforced
+  time::Span maxStaticPctCheckDelay;
+
   /// Assumes ownership of the created array objects
   ArrayCache arrayCache;