From 118584898dee525fa16da09aad8a037c45fcd540 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 13 Jan 2015 14:40:05 -0500 Subject: [PATCH] Fix a memory issue in ResourceManager on 32-bit (resolves bug #606). --- src/smt/smt_engine.cpp | 1 + src/util/resource_manager.cpp | 26 +++++++++---------- src/util/resource_manager.h | 48 +++++++++++++++++------------------ 3 files changed, 38 insertions(+), 37 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d039377a1..ee09359ad 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -303,6 +303,7 @@ struct SmtEngineStatistics { */ class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; + /** * Manager for limiting time and abstract resource usage. */ diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 7aeb2fc0f..6d32120d9 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -23,7 +23,7 @@ using namespace CVC4; using namespace std; -void Timer::set(unsigned long millis, bool wallTime) { +void Timer::set(uint64_t millis, bool wallTime) { d_ms = millis; Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; // keep track of when it was set, even if it's disabled (i.e. == 0) @@ -47,7 +47,7 @@ void Timer::set(unsigned long millis, bool wallTime) { } /** Return the milliseconds elapsed since last set(). */ -unsigned long Timer::elapsedWall() const { +uint64_t Timer::elapsedWall() const { Assert (d_wall_time); timeval tv; gettimeofday(&tv, NULL); @@ -58,14 +58,14 @@ unsigned long Timer::elapsedWall() const { return tv.tv_sec * 1000 + tv.tv_usec / 1000; } -unsigned long Timer::elapsedCPU() const { +uint64_t Timer::elapsedCPU() const { Assert (!d_wall_time); clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time; Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <= d_thisCallTimeBudget) return 0; return d_thisCallTimeBudget - time_passed; @@ -239,7 +239,7 @@ void ResourceManager::beginCall() { } void ResourceManager::endCall() { - unsigned long usedInCall = d_perCallTimer.elapsed(); + uint64_t usedInCall = d_perCallTimer.elapsed(); d_perCallTimer.set(0); d_cumulativeTimeUsed += usedInCall; } diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 94e7dbba2..d1ec0456a 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -33,7 +33,7 @@ namespace CVC4 { */ class CVC4_PUBLIC Timer { - unsigned long d_ms; + uint64_t d_ms; timeval d_wall_limit; clock_t d_cpu_start_time; clock_t d_cpu_limit; @@ -41,9 +41,9 @@ class CVC4_PUBLIC Timer { bool d_wall_time; /** Return the milliseconds elapsed since last set() cpu time. */ - unsigned long elapsedCPU() const; + uint64_t elapsedCPU() const; /** Return the milliseconds elapsed since last set() wall time. */ - unsigned long elapsedWall() const; + uint64_t elapsedWall() const; public: @@ -61,10 +61,10 @@ public: } /** Set a millisecond timer (0==off). */ - void set(unsigned long millis, bool wall_time = true); + void set(uint64_t millis, bool wall_time = true); /** Return the milliseconds elapsed since last set() wall/cpu time depending on d_wall_time*/ - unsigned long elapsed() const; + uint64_t elapsed() const; bool expired() const; };/* class Timer */ @@ -76,36 +76,36 @@ class CVC4_PUBLIC ResourceManager { Timer d_perCallTimer; /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */ - unsigned long d_timeBudgetCumulative; + uint64_t d_timeBudgetCumulative; /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ - unsigned long d_timeBudgetPerCall; + uint64_t d_timeBudgetPerCall; /** A user-imposed cumulative resource budget. 0 = no limit. */ - unsigned long d_resourceBudgetCumulative; + uint64_t d_resourceBudgetCumulative; /** A user-imposed per-call resource budget. 0 = no limit. */ - unsigned long d_resourceBudgetPerCall; + uint64_t d_resourceBudgetPerCall; /** The number of milliseconds used. */ - unsigned long d_cumulativeTimeUsed; + uint64_t d_cumulativeTimeUsed; /** The amount of resource used. */ - unsigned long d_cumulativeResourceUsed; + uint64_t d_cumulativeResourceUsed; /** The ammount of resource used during this call. */ - unsigned long d_thisCallResourceUsed; + uint64_t d_thisCallResourceUsed; /** * The ammount of resource budget for this call (min between per call * budget and left-over cumulative budget. */ - unsigned long d_thisCallTimeBudget; - unsigned long d_thisCallResourceBudget; + uint64_t d_thisCallTimeBudget; + uint64_t d_thisCallResourceBudget; bool d_isHardLimit; bool d_on; bool d_cpuTime; - unsigned long d_spendResourceCalls; + uint64_t d_spendResourceCalls; /** Counter indicating how often to check resource manager in loops */ - static const unsigned long s_resourceCount; + static const uint64_t s_resourceCount; public: @@ -119,20 +119,20 @@ public: bool outOfTime() const; bool out() const { return d_on && (outOfResources() || outOfTime()); } - unsigned long getResourceUsage() const; - unsigned long getTimeUsage() const; - unsigned long getResourceRemaining() const; - unsigned long getTimeRemaining() const; + uint64_t getResourceUsage() const; + uint64_t getTimeUsage() const; + uint64_t getResourceRemaining() const; + uint64_t getTimeRemaining() const; - unsigned long getResourceBudgetForThisCall() { + uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; } void spendResource() throw(UnsafeInterruptException); void setHardLimit(bool value); - void setResourceLimit(unsigned long units, bool cumulative = false); - void setTimeLimit(unsigned long millis, bool cumulative = false); + void setResourceLimit(uint64_t units, bool cumulative = false); + void setTimeLimit(uint64_t millis, bool cumulative = false); void useCPUTime(bool cpu); void enable(bool on); @@ -149,7 +149,7 @@ public: */ void endCall(); - static unsigned long getFrequencyCount() { return s_resourceCount; } + static uint64_t getFrequencyCount() { return s_resourceCount; } friend class SmtEngine; };/* class ResourceManager */ -- 2.30.2