diff --git a/.gitattributes b/.gitattributes index e02a50f0e6e9b6515b6078a68ff9ed39722bb0d6..cb41aab7479fd918fdff59f3cad8d78b09ed7cb1 100644 --- a/.gitattributes +++ b/.gitattributes @@ -215,6 +215,7 @@ README* header_spec=.ignore /doc/MakeLaTeXModern header_spec=.ignore /doc/acsl_tutorial_slides/script header_spec=.ignore /doc/developer/METADOC.txt header_spec=.ignore +/doc/developer/dune-workspace.bench header_spec=.ignore /doc/developer/examples/**/* header_spec=.ignore /doc/developer/tutorial/**/* header_spec=.ignore /doc/qualification/testing header_spec=.ignore diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index bdfec9acc732ea0b1516a19ee06f899857d7360f..a04757d570cae01864941c7121788c435ff696c7 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -4209,9 +4209,9 @@ For quick usage of the library: \item install the instrumented \framac: \texttt{make install DUNE\_WS=bench}. \item enable instrumentation {\em during execution} of \framac, using the \texttt{OCAML\_LANDMARKS} environment variable: - \begin{lstlisting} - OCAML_LANDMARKS=<options> frama-c [files] [options] - \end{lstlisting} +\begin{lstlisting} +OCAML_LANDMARKS=<options> frama-c [files] [options] +\end{lstlisting} The easiest setup is \texttt{OCAML\_LANDMARKS=auto}, which will instrument everything and output timing information to \texttt{stderr} after program termination. @@ -4219,10 +4219,10 @@ For quick usage of the library: output the timing information to file \texttt{landmarks.log}. \item you can also run the instrumented \framac without installing it, via \texttt{dune exec}: - \begin{lstlisting} - OCAML_LANDMARKS=auto dune exec --workspace dev/dune-workspace.bench \ - --context bench -- frama-c [files] [options] - \end{lstlisting} +\begin{shell} +OCAML_LANDMARKS=auto dune exec --workspace dev/dune-workspace.bench \ + --context bench -- frama-c [files] [options] +\end{shell} The \verb+--workspace dev/dune-workspace.bench+ argument tells Dune to use the workspace in which Landmarks is configured. @@ -4243,3 +4243,44 @@ e.g.: \end{lstlisting} Check \url{https://github.com/LexiFi/landmarks} for its documentation. + +\section{Profiling a custom plug-in} + +To profile your own plug-in using Landmarks, do the following: + +\begin{enumerate} +\item Add \verb|(instrumentation (backend landmarks))| to your plug-in's + \verb|dune| file, inside the \verb|library| stanza, as in the example below: +\begin{dunecode} + (library + (name my-plug-in) + (public_name frama-c-my-plug-in.core) + ... + (libraries frama-c.kernel) + (instrumentation (backend landmarks)) ;<<< ADD THIS LINE + ) +\end{dunecode} +\item Create a \verb|dune-workspace.bench| file in your plugin's top-level + directory: + \listingname{dune-workspace.bench} + \duneinput{dune-workspace.bench} +\item Add \verb|--workspace=dune-workspace.bench| to the \verb|dune build| + and \verb|dune install| commands that you run, e.g.: +\begin{lstlisting} +dune build --workspace=dune-workspace.bench @install +dune install --workspace=dune-workspace.bench +\end{lstlisting} +This will compile and install the plug-in with Landmarks instrumentation +enabled. Then you just need to set \verb|OCAML_LANDMARKS| as described in the +previous section, e.g.: +\begin{lstlisting} +OCAML_LANDMARKS=auto frama-c [my-plugin-options] +\end{lstlisting} +\item For \verb|dune exec|, you need to add the \verb|--workspace| option + as well as \verb|--context bench|. Combined with \verb|OCAML_LANDMARKS|, + the command-line will resemble the following: +\begin{lstlisting} +OCAML_LANDMARKS=auto dune exec --workspace dev/dune-workspace.bench \ + --context bench -- frama-c [files] [options] +\end{lstlisting} +\end{enumerate} diff --git a/doc/developer/dune-workspace.bench b/doc/developer/dune-workspace.bench new file mode 100644 index 0000000000000000000000000000000000000000..87e6d04e0ad58aba035cac6a3f7b7c68eda27674 --- /dev/null +++ b/doc/developer/dune-workspace.bench @@ -0,0 +1,9 @@ +(lang dune 3.2) +(context + (default + (name bench) + (profile bench) + (instrument_with landmarks) + (env + (_ (env-vars ("OCAML_LANDMARKS" "auto"))))) +)