fix: ignored time_task blocks

Kha · Mar 23, 2023 · c1ae91f · c1ae91f
1 parent 1360751
commit c1ae91f
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 5 deletions.
diff --git a/src/library/time_task.cpp b/src/library/time_task.cpp
@@ -44,7 +44,7 @@ void finalize_time_task() {
 time_task::time_task(std::string const & category, options const & opts, name decl) :
         m_category(category) {
     if (!m_category.size()) {
-        // exclude given block from surrounding task, if any
+        // ignore given block in timings of surrounding task, if any
         if (g_current_time_task) {
             m_timeit = optional<xtimeit>([](second_duration _) {});
             m_parent_task = g_current_time_task;
@@ -68,11 +68,16 @@ time_task::time_task(std::string const & category, options const & opts, name de
 time_task::~time_task() {
     if (m_timeit) {
         g_current_time_task = m_parent_task;
-        if (m_category.size())
+        if (m_category.size()) {
             report_profiling_time(m_category, m_timeit->get_elapsed());
-        if (m_parent_task && m_parent_task->m_timeit)
-            // report exclusive times
-            m_parent_task->m_timeit->exclude_duration(m_timeit->get_elapsed_inclusive());
+            if (m_parent_task)
+                // report exclusive times
+                m_parent_task->m_timeit->exclude_duration(m_timeit->get_elapsed_inclusive());
+        } else {
+            if (m_parent_task) {
+                m_parent_task->m_timeit->ignore(*m_timeit);
+            }
+        }
     }
 }
 

diff --git a/src/util/timeit.h b/src/util/timeit.h
@@ -75,6 +75,18 @@ class xtimeit {
     void exclude_duration(second_duration d) {
         m_excluded += d;
     }
+
+    void ignore(xtimeit const & ignored) {
+        // propagate nested times as usual,
+        exclude_duration(ignored.m_excluded);
+        // but exclude this block's time from the directly surrounding task only by adjusting its start time
+        m_start += std::chrono::duration_cast<std::chrono::steady_clock::duration>(ignored.get_elapsed());
+        // For example, if elaboration calls an interpreted tactic (without its own category) that calls `simp`,
+        // we subtract the `simp` time from both surrounding categories as usual.
+        // However, if the tactic also spends some time in uncategorized native code,
+        // we subtract it from the interpretation category only by adjusting `m_start`,
+        // which effectively adds the time to the surrounding `elaboration` category instead.
+    }
 };
 
 }