Skip to content

Commit

Permalink
Added -max-static-pct-check-delay to replace the hardcoded delay afte…
Browse files Browse the repository at this point in the history
…r which the MaxStatic*Pct checks are performed.
  • Loading branch information
ccadar authored and MartinNowack committed Apr 20, 2021
1 parent 8889369 commit c8ef082
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 1 deletion.
12 changes: 11 additions & 1 deletion lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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. "
Expand Down Expand Up @@ -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())
Expand Down Expand Up @@ -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;
Expand Down
3 changes: 3 additions & 0 deletions lib/Core/Executor.h
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,9 @@ class Executor : public Interpreter {
/// 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;

Expand Down

0 comments on commit c8ef082

Please sign in to comment.