/* Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich */ #include #include #include "library/time_task.h" namespace lean { static std::map * g_cum_times; static mutex * g_cum_times_mutex; LEAN_THREAD_PTR(time_task, g_current_time_task); void report_profiling_time(std::string const & category, second_duration time) { lock_guard _(*g_cum_times_mutex); (*g_cum_times)[category] += time; } void display_cumulative_profiling_times(std::ostream & out) { if (g_cum_times->empty()) return; out << "cumulative profiling times:\n"; for (auto const & p : *g_cum_times) out << "\t" << p.first << " " << display_profiling_time{p.second} << "\n"; } void initialize_time_task() { g_cum_times_mutex = new mutex; g_cum_times = new std::map; } void finalize_time_task() { delete g_cum_times; delete g_cum_times_mutex; } time_task::time_task(std::string const & category, message_builder builder, name decl) : m_category(category) { auto const & opts = builder.get_text_stream().get_options(); if (get_profiler(opts)) { m_timeit = optional(get_profiling_threshold(opts), [=](second_duration duration) mutable { builder.get_text_stream().get_stream() << m_category; if (decl) builder.get_text_stream().get_stream() << " of " << decl; builder.get_text_stream().get_stream() << " took " << display_profiling_time{duration} << "\n"; builder.report(); }); m_parent_task = g_current_time_task; g_current_time_task = this; } } time_task::~time_task() { if (m_timeit) { g_current_time_task = m_parent_task; auto time = m_timeit->get_elapsed(); report_profiling_time(m_category, time); if (m_parent_task) // do not report inclusive times report_profiling_time(m_parent_task->m_category, -time); } } }