From e21a56acc2d28995aef4586668f756806a53869b Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 17 Dec 2020 12:06:37 +0100
Subject: add profiling entry-points in the htmldoc.

---
 doc/index-kvx.html | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/index-kvx.html b/doc/index-kvx.html
index 39fdf799..dc646a67 100644
--- a/doc/index-kvx.html
+++ b/doc/index-kvx.html
@@ -253,6 +253,23 @@ This IR is generic over the processor, even if currently, only used for KVX.
   <TD><A HREF="html/compcert.backend.Unusedglobproof.html">Unusedglobproof</A></TD>
 </TR>
 
+<TR valign="top" style="color:#000000">
+  <TD colspan="4"><b>Passes introduced for profiling (for later use in trace selection)</b></TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Insert profiling annotations (for recording experiments -- see PROFILE.md).
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Profiling.html">Profiling</A></TD>
+  <TD><A HREF="html/compcert.backend.Profilingproof.html">Profilingproof</A></TD>
+</TR>
+<TR valign="top" style="color:#000000">
+  <TD>Update ICond nodes (from recorded experiments -- see PROFILE.md).
+  </TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.ProfilingExploit.html">ProfilingExploit</A></TD>
+  <TD><A HREF="html/compcert.backend.ProfilingExploitproof.html">ProfilingExploitproof</A></TD>
+</TR>
 <TR valign="top" style="color:#000000">
   <TD colspan="4"><b>Passes introduced for superblock prepass scheduling</b></TD>
 </TR>
@@ -372,12 +389,13 @@ This IR is generic over the processor, even if currently, only used for KVX.
 </TR>
 </TABLE>
 
-<font color=gray>
-<H3>All together</H3>
+<H3>All together (there are many more RTL passes than on vanilla CompCert: their order is specified in Compiler)</H3>
 
 <UL>
+</font>
 <LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together;
 whole-compiler semantic preservation theorems.
+<font color=gray>
 <LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
 </UL>
 
-- 
cgit