max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(util/debug): add version of lean_assert that also works in non-debug builds

Browse source
This commit is contained in:
Gabriel Ebner 2017-02-28 14:31:49 +01:00
parent 52bcfb713f
commit d22bfbd12a
3 changed files with 19 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/mt_task_queue.cpp
View file

@ -61,7 +61,7 @@ void mt_task_queue::notify_queue_changed() {
constexpr chrono::milliseconds g_worker_max_idle_time = chrono::milliseconds(1000);
void mt_task_queue::spawn_worker() {
lean_assert(!m_shutting_down);
lean_always_assert(!m_shutting_down);
auto this_worker = std::make_shared<worker_info>();
m_workers.push_back(this_worker);
m_required_workers--;
@ -120,8 +120,8 @@ void mt_task_queue::spawn_worker() {
}
void mt_task_queue::handle_finished(gtask const & t) {
lean_assert(get_state(t).load() > task_state::Running);
lean_assert(get_data(t));
lean_always_assert(get_state(t).load() > task_state::Running);
lean_always_assert(get_data(t));
if (!get_data(t)->m_sched_info)
return; // task has never been submitted
@ -135,7 +135,7 @@ void mt_task_queue::handle_finished(gtask const & t) {
if (check_deps(rdep)) {
m_waiting.erase(rdep);
if (get_state(rdep).load() < task_state::Running) {
lean_assert(get_data(rdep));
lean_always_assert(get_data(rdep));
if (get_data(rdep)->m_flags.m_eager_execution) {
get_state(rdep) = task_state::Running;
execute(rdep);
@ -189,7 +189,7 @@ void mt_task_queue::submit_core(gtask const & t, unsigned prio) {
case task_state::Running: case task_state::Failed: case task_state::Success:
break;
}
lean_assert(get_state(t).load() >= task_state::Waiting);
lean_always_assert(get_state(t).load() >= task_state::Waiting);
}
void mt_task_queue::bump_prio(gtask const & t, unsigned new_prio) {
@ -199,7 +199,7 @@ void mt_task_queue::bump_prio(gtask const & t, unsigned new_prio) {
auto prio = get_prio(t);
auto &q = m_queue[prio];
auto it = std::find(q.begin(), q.end(), t);
lean_assert(it != q.end());
lean_always_assert(it != q.end());
q.erase(it);
if (q.empty()) m_queue.erase(prio);
@ -222,7 +222,7 @@ void mt_task_queue::bump_prio(gtask const & t, unsigned new_prio) {
bool mt_task_queue::check_deps(gtask const & t) {
check_stack("mt_task_queue::check_deps");
lean_assert(get_data(t));
lean_always_assert(get_data(t));
buffer<gtask> deps;
try {
@ -241,7 +241,7 @@ bool mt_task_queue::check_deps(gtask const & t) {
if (!dep) continue;
switch (get_state(dep).load()) {
case task_state::Waiting: case task_state::Queued: case task_state::Running:
lean_assert(get_imp(dep));
lean_always_assert(get_imp(dep));
get_sched_info(dep).m_reverse_deps.push_back(t);
return false;
case task_state::Success:
@ -301,10 +301,10 @@ void mt_task_queue::join() {
}
gtask mt_task_queue::dequeue() {
lean_assert(!m_queue.empty());
lean_always_assert(!m_queue.empty());
auto it = m_queue.begin();
auto & highest_prio = it->second;
lean_assert(!highest_prio.empty());
lean_always_assert(!highest_prio.empty());
auto result = std::move(highest_prio.front());
highest_prio.pop_front();
if (highest_prio.empty()) {
@ -314,8 +314,8 @@ gtask mt_task_queue::dequeue() {
}
void mt_task_queue::enqueue(gtask const & t) {
lean_assert(get_state(t).load() < task_state::Running);
lean_assert(get_imp(t));
lean_always_assert(get_state(t).load() < task_state::Running);
lean_always_assert(get_imp(t));
get_state(t) = task_state::Queued;
m_queue[get_prio(t)].push_back(t);
if (m_required_workers > 0) {

1
src/util/debug.h
View file

@ -84,6 +84,7 @@ Author: Leonardo de Moura
#define lean_assert(COND, ARGS...) DEBUG_CODE({if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }})
#define lean_cond_assert(TAG, COND, ARGS...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && !(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }})
#define lean_always_assert(COND, ARGS...) { if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean_unreachable(); } }
#define lean_assert_eq(A, B) lean_assert(A == B, A, B)
#define lean_assert_ne(A, B) lean_assert(A != B, A, B)

12
src/util/task.cpp
View file

@ -36,10 +36,10 @@ void task_queue::wait_for_success(gtask const & t) {
}
void task_queue::execute(gtask const & t) {
lean_assert(t);
lean_assert(t->m_state.load() == task_state::Running);
lean_assert(t->m_data);
lean_assert(t->m_data->m_imp);
lean_always_assert(t);
lean_always_assert(t->m_state.load() == task_state::Running);
lean_always_assert(t->m_data);
lean_always_assert(t->m_data->m_imp);
try {
{
@ -57,14 +57,14 @@ void task_queue::execute(gtask const & t) {
}
void task_queue::fail(gtask const & t, std::exception_ptr const & ex) {
lean_assert(t->m_state.load() < task_state::Running);
lean_always_assert(t->m_state.load() < task_state::Running);
t->m_exception = ex;
t->m_state = task_state::Failed;
}
void task_queue::fail(gtask const & t, gtask const & failed) {
lean_assert(failed->m_state.load() == task_state::Failed);
lean_always_assert(failed->m_state.load() == task_state::Failed);
fail(t, failed->m_exception);
}