%% file using-bm.tex, which is \input from bismon-doc.tex
\section{Using \emph{Bismon}}
\label{sec:using}

This section \S \ref{sec:using} should become somehow a user manual, and
will be written for the final D1.3\textsuperscript{v2}. It is both for
the ordinary IoT developer just using \emph{bismon} for static
analysis of IoT source code, and for the static analysis expert
configuring and programming it.

Most of that should be generated from data persisted inside \emph{bismon}. Perhaps
should be exchanged with the ``static analysis'' chapter
(\S\ref{sec:staticanalys}).

%\bigskip

%Notice that most of \emph{GCC MELT} documentation was generated. See its
%{\small\bmurl{http://starynkevitch.net/Basile/gcc-melt/meltpluginapi.html/meltpluginapi.html}}. Likewise,
%most of this chapter will be machine generated from the persistent
%state of \emph{Bismon}


\subsection{How JSON is used by Bismon}
\label{subsec:json-usage}

The JSON\footnote{See \bmurl{http://json.org/} for more} \index{JSON}
textual format is a convenient, common and compact structured textual
format. It is used in \emph{Bismon}, in particular because of its web
interface, and supported as a payload \index{payload} (but not
directly\footnote{Adding immutable JSON values as a new kind of Bismon
  value could be considered in the future.} as an immutable value) for
objects of class \texttt{json\_object}.  \index{json
  object@\texttt{json\_object}}

Conceptually, the JSON model is close, but not identical to, the
Bismon persistent model: it provides structured and compositional
\index{object}%
\index{attribute}%
\index{component}%
\index{payload}%
constructs, but JSON objects have \emph{strings} as attributes, while
Bismon objects have arbitrary object references as attributes, and
also components and some optional payload.

\subsubsection{The canonical \emph{JSON} encoding of \emph{Bismon} values}
\label{subsubsec:canonical-json-encoding}

Therefore, there is some way to encode any \emph{Bismon} value into a
JSON value; this is the \emph{canonical JSON encoding of
  values}\index{canonical JSON encoding}, given in table
\ref{tbl:canon-json} below.

\begin{table}[!htbp]
  \begin{relsize}{-1}
  \begin{center}
    \begin{tabular}{lclp{5cm}}
      %%%
      $\llbracket \textrm{nil} \rrbracket_{json}$ \index{nil} &
      $\rightarrow$ &
      \texttt{\textbf{null}}  &
      {\relsize{-1}{The Bismon nil is encoded as the JSON null}} \\
      %%%
      $\llbracket \textrm{unspecified} \rrbracket_{json}$ &
      $\rightarrow$ &
      \texttt{\textbf{false}}  &
      {\relsize{-1}{The Bismon \emph{unspecified} \index{unspecified} is encoded as the JSON false}} \\
      %%%
      $\llbracket \textrm{integer}~ i \rrbracket_{json}$ &
      $\rightarrow$ &
      $i$ {\relsize{-1}{(JSON integer)}} &
      {\relsize{-1}{tagged integers \index{integer} encoded as is}} \\
      %%%
      $\llbracket \textrm{boxed float}~ f \rrbracket_{json}$ &
      $\rightarrow$ &
      $f$ {\relsize{-1}{(JSON float)}} &
      {\relsize{-1}{boxed doubles \index{double} encoded as is, with decimal point}} \\
      %%%
      $\llbracket \textrm{string}~ s \rrbracket_{json}$ &
      $\rightarrow$ &
      $s$  {\relsize{-1}{(JSON string)}}  &
      {\relsize{-1}{Bismon strings \index{string} encoded as is}} \\
      \rule{0pt}{3ex} 
      %%%
      $\llbracket \textrm{object}~ \omega$ {\relsize{-1.5}{\textrm{of objid}~ \textit{oid}}}$ \rrbracket_{json}$ \index{object} \index{objid} &
      $\rightarrow$ &
      \texttt{\textbf{\{ "!oid" :}} $\mathit{oid}$ \texttt{\textbf{\}}} &
             {{\relsize{-1}{Bismon objects encoded with \texttt{"!oid"} JSON attribute giving the \index{objid}objid as a JSON string}}} \\
              \rule{0pt}{3ex}
      %%%
      $\llbracket \textrm{tuple}~ [ \omega_1 \ldots \omega_n ] ~ \rrbracket_{json}$ \index{tuple} &
      $\rightarrow$ & %
      \begin{minipage}[c]{4cm}
         \texttt{\textbf{\{ "!tup" :}} \\
         \hspace*{1.2em}  $\mathtt{\texttt{[}} ~ \mathit{oid}_1 \ldots \mathit{oid}_n ~ \mathtt{\texttt{]}}$ \texttt{\textbf{\}}}
      \end{minipage}
      & {\relsize{-1}{Bismon tuples encoded  with \texttt{"!tup"} JSON attribute giving the JSON array of corresponding objid JSON strings : ~  \mbox{$\mathit{oid}_i = \mathrm{objid} (\omega_i)$}
            }}
      \\
       \rule{0pt}{3ex}
      %%%
      $\llbracket \textrm{set}~ \{ \omega_1 \ldots \omega_n \} ~ \rrbracket_{json}$ \index{set} &
      $\rightarrow$ & %
      \begin{minipage}[c]{4cm}
         \texttt{\textbf{\{ "!set" :}} \\
         \hspace*{1.2em}  $\mathtt{\texttt{[}} ~ \mathit{oid}_1 \ldots \mathit{oid}_n ~ \mathtt{\texttt{]}}$ \texttt{\textbf{\}}}
      \end{minipage}
      & {\relsize{-1}{Bismon sets encoded  with \texttt{"!set"} JSON attribute giving the JSON array of corresponding objid JSON strings : ~  \mbox{$\mathit{oid}_i = \mathrm{objid} (\omega_i)$}
            }}
      \\
       \rule{0pt}{3ex}
      %%%
      $\llbracket \textrm{node}~ \mathtt{\textbf{*}} ~ \omega_{conn} \mathtt{(} \sigma_1 \ldots \sigma_n \mathtt{)} ~ \rrbracket_{json}$ \index{node} &
      $\rightarrow$ & %
      \begin{minipage}[c]{4.5cm}
        \texttt{\textbf{\{ "!node" :}} $\mathit{oid}_{conn}$ \texttt{\textbf{,}} \\
         \hspace*{0.8em}  \texttt{\textbf{"!sons" :}} \\
         \hspace*{1.2em} %
         $\mathtt{\texttt{[}} ~ \llbracket \sigma_1 \rrbracket_{json} ~ \ldots ~  \llbracket \sigma_n \rrbracket_{json} ~ \mathtt{\texttt{]}}$
         \texttt{\textbf{\}}}
      \end{minipage}
      & {\relsize{-1}{Bismon nodes encoded  with \texttt{"!node"} JSON attribute giving the objid $\mathit{oid}_{conn} = \mathrm{objid} (\omega_{conn})$ of the connective $\mathit{oid}_{conn}$, and with  \texttt{"!sons"} JSON attribute associated to the array of encodings of that node's sons $\sigma_i$}
            }
      \\
       \rule{0pt}{3ex}
      %%%
      $\llbracket \textrm{closure}~ \mathtt{\textbf{\%}} ~ \omega_{rout} \mathtt{(} \kappa_1 \ldots \kappa_n \mathtt{)} ~ \rrbracket_{json}$ \index{closure} &
      $\rightarrow$ & %
      \begin{minipage}[c]{4.5cm}
        \texttt{\textbf{\{ "!clos" :}} $\mathit{oid}_{rout}$ \texttt{\textbf{,}} \\
         \hspace*{0.8em}  \texttt{\textbf{"!cval" :}} \\
         \hspace*{1.2em} %
         $\mathtt{\texttt{[}} ~ \llbracket \kappa_1 \rrbracket_{json} ~ \ldots ~  \llbracket \kappa_n \rrbracket_{json} ~ \mathtt{\texttt{]}}$
         \texttt{\textbf{\}}}
      \end{minipage}
      & {\relsize{-1}{Bismon closures encoded  with \texttt{"!clos"} JSON attribute giving the objid  $\mathit{oid}_{rout} = \mathrm{objid} (\omega_{conn})$ of the closure's routine, and with  \texttt{"!cval"} JSON attribute associated to the array of encodings of that closure's closed values $\kappa_i$}
            } \\
%-    \hline \\
%-    \rule{0pt}{6ex} \\
%-    \begin{minipage}[c]{3.5cm}
%-      $ \nu = $ \\ $\mathrm{apply}  ~ \mathtt{\textbf{\%}} ~ \omega_{rout} \mathtt{(} \kappa_1 \ldots \kappa_n \mathtt{)} $ \\
%-      to $\mathit{ctxt}, \mathit{depth}$ 
%-    \end{minipage} &
%-    $\leftarrow$ & %
%-    \begin{minipage}[c]{4.5cm}
%-      \texttt{\textbf{\{ "!apply" :}} $\mathit{oid}_{rout}$ \texttt{\textbf{,}} \\
%-       \hspace*{0.8em}  \texttt{\textbf{"!cval" :}} \\
%-       \hspace*{1.2em} %
%-       $\mathtt{\texttt{[}} ~ \mathit{json}_1 \ldots \mathit{json}_n ~ \mathtt{\texttt{]}}$
%-       \texttt{\textbf{\}}}
%-    \end{minipage}
%-    & {\relsize{-1}{application of object routine $\omega_{rout}$
%-          whose objid is $\mathit{oid}_{rout}$ with closed values
%-          $\kappa_1 = \mathit{encode}_{json} ( \mathit{json}_1 )$
%-          \ldots $\kappa_n = \mathit{encode}_{json} (
%-          \mathit{json}_n )$ to the context, the depth (during
%-          decoding) \textcolor{red}{@@NOT SURE}}} \\ \rule{0pt}{3ex}
%-    %%%
    \end{tabular}
    \smallskip
  \end{center}
  \end{relsize}
  \caption{canonical JSON encoding $\llbracket v \rrbracket_{json}$ of a Bismon value $v$.}
  \label{tbl:canon-json}
\end{table}

The canonical JSON encoding is implemented\footnote{Coded in C, in file
\href{https://github.com/bstarynk/bismon/blob/master/jsonjansson\_BM.c}{\texttt{jsonjansson\_BM.c}}}
as the \texttt{canonjsonifyvalue\_BM} \index{canonjsonifyvalue!\texttt{canonjsonifyvalue\_BM}} function.

\medskip

\subsubsection{The nodal \emph{JSON} decoding into \emph{Bismon} values}
\label{subsubsec:nodal-json-decoding}

Since JSON is a structured and compositional, \index{tree!JSON}
tree-like, representation, and because \index{node} nodes are the only
kind of structured immutable \emph{Bismon} values,
\index{decoding!JSON nodal} \index{nodal!JSON decoding} any JSON value
can obviously be decoded into a \emph{Bismon} values, using mostly
nodes for structuring data, following the rules listed in
table \ref{tbl:nodal-json} below. Actually, there are several variants of
nodal decodings, depending on how JSON strings looking like
\index{objid} full objids (e.g. JSON
\texttt{"\_756o00yB7Zs\_1USbaS25hxl"}), or abbreviated objids
(e.g. JSON \texttt{"€\_9Z2BgJbf4"}), or named objects (e.g.  JSON
\texttt{"arguments"}, related to Bismon object \texttt{arguments},
i.e. \texttt{€\_0jFqaPPHg}) are really decoded.

\begin{table}[!htbp]
  \begin{relsize}{-1}
  \begin{center}
    \begin{tabular}{lclp{5.3cm}}
      %%%
      $\langle \mathtt{\textit{\texttt{null}}} \rangle^{nod}$ \index{null} &
      $\rightarrow$ &
      \texttt{\textbf{json\_null}}  &
             {\relsize{-1}{The JSON \texttt{null}\index{null!JSON} is nodal-decoded as the \texttt{json\_null} Bismon object \texttt{€\_6WOSg1mpN}}}
      \\
      %%%
      $\langle \mathtt{\textit{\texttt{false}}} \rangle^{nod}$ \index{null} &
      $\rightarrow$ &
      \texttt{\textbf{json\_false}}  &
             {\relsize{-1}{The JSON \texttt{false} is nodal-decoded as the \texttt{json\_false} Bismon object \texttt{€\_1h1MMlmQi}}}
      \\
      %%%
      $\langle \mathtt{\textit{\texttt{true}}} \rangle^{nod}$ \index{null} &
      $\rightarrow$ &
      \texttt{\textbf{json\_true}}  &
             {\relsize{-1}{The JSON \texttt{true} is nodal-decoded as the \texttt{json\_true} Bismon object \texttt{€\_0ekuRPtKaI}}}
      \\
      %%%
      $\langle \mathrm{integer} ~ \iota \rangle^{nod}$  &
      $\rightarrow$ &
      tagged integer $\iota$  &
             {\relsize{-1}{The JSON integers are nodal-decoded as the corresponding \emph{Bismon} integer}}
      \\
      %%%
      $\langle \mathrm{real} ~ \delta \rangle^{nod}$  &
      $\rightarrow$ &
      boxed double $\delta$  &
             {\relsize{-1}{The JSON reals are nodal-decoded as the corresponding \emph{Bismon} boxed double}}
      \\
      \rule{0pt}{2ex} \\
      %%%
      $\langle \mathrm{\textrm{objid-looking} ~ string ~} \sigma \rangle^{nod}$ \index{objid} &
      $\rightarrow$ &
      \begin{minipage}{4.7cm}
        object $\omega$, when  $\omega \notin \{ \mathtt{json\_null},$ \\
        \hspace*{0.4em} $ \mathtt{json\_false},$ $  \mathtt{json\_true},$ \\
        \hspace*{0.4em} $\mathtt{json\_array}, \mathtt{json\_object} \}$
      \end{minipage}
      &
      {\relsize{-1}{an objid-looking string $\sigma$, starting with an underscore \texttt{\_} and matching the objid of an existing object, \emph{may} be nodal-decoded as
          \emph{the existing anonymous} object $\omega$ such as
          $\mathrm{objid}(\omega) = \sigma$}  when that $\omega$ is not a special object mentioned here.}
      \\
      %%%
      $\langle \mathrm{\textrm{name-looking} ~ string ~} \sigma \rangle^{nod}$ \index{objid} &
      $\rightarrow$ &
      \begin{minipage}{4.7cm}
        object $\omega$,  with $\omega \notin \{ \mathtt{json\_null},$ \\
        \hspace*{0.4em} $ \mathtt{json\_false},$ $  \mathtt{json\_true},$ \\
        \hspace*{0.4em} $\mathtt{json\_array}, \mathtt{json\_object} \}$
      \end{minipage} &
      {\relsize{-1}{a name-looking string $\sigma$, starting with a letter and naming an existing object, may be nodal-decoded as the \emph{existing named} object $\omega$ such as $\mathrm{name}(\omega) = \sigma$ when that object is not special.}}
      \\
      \rule{0pt}{2ex} \\
      %%%
      $\langle \mathrm{\textrm{any} ~ string} ~ \sigma \rangle^{nod}$ \index{objid} &
      $\rightarrow$ &
      \emph{Bismon} string $\sigma$  &
      {\relsize{-1}{a string $\sigma$ \emph{would} otherwise be nodal-decoded as
          is into the same \emph{Bismon string} $\sigma$}}
      \\
      %%%
      $\langle \mathtt{\textbf{[}} \mathit{\,js}_1 \mathtt{\textbf{,}} \ldots \mathit{\,js}_n \mathtt{\textbf{]}}  \rangle^{nod}$ &
      $\rightarrow$ &
      \begin{minipage}{4.7cm}
      $\mathtt{\texttt{\textbf{*}}} \mathtt{\texttt{\textbf{json\_array}}}$ \\
       \hspace*{1.5em} $ ( \langle \mathit{\,js}_1 \rangle^{nod} \ldots  \langle \mathit{\,js}_n \rangle^{nod} ) $
      \end{minipage}
      &
       {\relsize{-1}{A JSON array is compositionally nodal-decoded into a node of connective \texttt{json\_array} and sons given by nodal-decoding the components of that array}} \\
      \rule{0pt}{6ex} \\
      %%%
      $\langle \mathtt{\textbf{\{}} \alpha_1 \mathtt{\textbf{:}} \mathit{\,js}_1 \mathtt{\textbf{,}} \ldots \alpha_n \mathtt{\textbf{:}} \mathit{\,js}_n \mathtt{\textbf{\}}}  \rangle^{nod}$ &
      $\rightarrow$ &
      \begin{minipage}{4.7cm}
      $\mathtt{\texttt{\textbf{*}}} \mathtt{\texttt{\textbf{json\_object}}} ($ \\
        \hspace*{0.5em} $ \mathtt{\texttt{\textbf{*}}} \mathtt{\texttt{\textbf{json\_entry}}} (  \langle \alpha_1 \rangle^{nod} \mathtt{\texttt{\textbf{,}}} $ \\
         \hspace*{4.5em} $ \langle \mathit{\,js}_1 \rangle^{nod} )$ \\
       \hspace*{2em} $\vdots$ \\
        \hspace*{0.5em} $ \mathtt{\texttt{\textbf{*}}} \mathtt{\texttt{\textbf{json\_entry}}} (  \langle \alpha_n \rangle^{nod} \mathtt{\texttt{\textbf{,}}} $ \\
         \hspace*{4.5em} $ \langle \mathit{\,js}_n \rangle^{nod} )$ \\
        \hspace*{1em} $)$
      \end{minipage}
      &
       {\relsize{-1}{A JSON object is compositionally nodal-decoded into a node of connective \texttt{json\_objects} and sons given by \texttt{json\_entries} subnodes whose first son is a string $\alpha_i$ or object $\omega_i$ or node $\mathtt{\textbf{\texttt{* id}}} (\omega_i)$ where $\alpha_i = \mathrm{objid}(\omega_i)$ or node  $\mathtt{\textbf{\texttt{* name}}} (\omega_i)$ where $\alpha_i = \mathrm{objname}(\omega_i)$ }} \\
      \rule{0pt}{6ex} \\
    \end{tabular}
  \end{center}
  \end{relsize}
  \caption{nodal JSON decoding $\langle \mathit{js} \rangle^{nod}$ of a JSON value $\mathit{js}$.}
  \label{tbl:nodal-json}
\end{table}


\subsubsection{\emph{JSON} extraction with \texttt{extract\_json}}
\label{subsubsec:json-extraction}

A \emph{Bismon} statement of class \texttt{basiclo\_extractjsonstmt},
\index{basiclo extractjsonstmt@\texttt{basiclo\_extractjsonstmt}}
obtained with the \texttt{{\^{}}{extract\_json} (} \textit{objson}
\textit {extractornode} \textit{sub-statements}... \texttt{)}
readmacro, so having the attributes \texttt{json\_object :}
\textit{objson} and \texttt{extract\_json :} \textit{extractornode},
\index{extract json@\texttt{extract\_json}} \index{JSON!extractor}
\index{extractor!from JSON} can extract data from the JSON in a
payload (of some object \textit{objson}, usually of class
\texttt{json\_object}). That extraction\footnote{Our JSON extraction
  is inspired by some pattern matching constructs on linear patterns
  with semi-unification.} \index{extraction!from JSON} is driven by
the given \textit{extractornode} in the statement, which should be a
node, as explained in tables \ref{tbl:extract-json-simple} (for simple
extractions) and \ref{tbl:extract-json-complex} (for more complex
extractions) below.

%%%%%%%%%%%%%%%%
\begin{table}%[!htbp]
  \begin{relsize}{-1.3}
  \begin{center}
    \begin{tabular}{lcp{6.3cm}}
      \textbf{extractor node} & \hspace*{1cm} \textbf{success condition} \hspace*{1cm}  & \textbf{side effects and explanation} \\
      %%%
      \texttt{\textbf{* json\_null ()}} &
      $\mathit{js} \equiv \mathtt{null}$ &
      succeeds when $\mathit{js}$ is the null JSON \\
      %%%
      \texttt{\textbf{* json\_false ()}} &
      $\mathit{js} \equiv \mathtt{false}$ &
      succeeds when $\mathit{js}$ is the false JSON \\
      %%%
      \texttt{\textbf{* json\_true ()}} &
      $\mathit{js} \equiv \mathtt{true}$ &
      succeeds when $\mathit{js}$ is the true JSON \\
      %%%
      \texttt{\textbf{* int ($v^{\mathrm{\textcolor{blue}{int}}}$)}} &
      $\mathit{js} \equiv \mathrm{some ~ JSON ~ integer}~ i$ &
      succeeds when $\mathit{js}$ is a JSON integer $i$, and assign to integer
      variable $v$ its integral value $v \leftarrow i$\\
      %%%
      \texttt{\textbf{* double\_float ($v^{\mathrm{\textcolor{blue}{val}}}$)}} &
      $\mathit{js} \equiv \mathrm{some ~ JSON ~ real}~ \delta$ &
      succeeds when $\mathit{js}$ is a JSON real $\delta$, and assign to double
      variable $v$ its \emph{boxed} double value $v \leftarrow
      \mathrm{\textrm{boxed-double}} (\delta)$\\
      %%%
      \texttt{\textbf{* string ($v^{\mathrm{\textcolor{blue}{val}}}$)}} &
      $\mathit{js} \equiv \mathrm{some ~ JSON ~ string}~ \sigma$ &
      succeeds when $\mathit{js}$ is a JSON string $\sigma$, and assign to
      value variable $v$ its \emph{boxed} string value $v \leftarrow
      \mathrm{\textrm{boxed-string}} (\sigma)$ \\
            \rule{0pt}{1ex} \\
      %%%
      \texttt{\textbf{* id ($v^{\mathrm{\textcolor{blue}{obj}}}$)}} &
      \begin{minipage}[t]{4cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ string}~ \sigma$\\
        \hspace*{0.5em} $ \wedge ~ \exists ~ \mathrm{object} ~ \omega, \mathrm{objid}(\omega) = \sigma$ 
      \end{minipage}
      &
      succeeds when $\mathit{js}$ is some JSON string $\sigma$ looking like an objid, and that string $\sigma$ is the \emph{objid} of some \emph{existing} object $\omega$, then assign to
      object variable $v$ that object $\omega$, so  $v \leftarrow \omega$ \\
            \rule{0pt}{1ex} \\
      %%%
      \texttt{\textbf{* name ($v^{\mathrm{\textcolor{blue}{obj}}}$)}} &
      \begin{minipage}[t]{4.5cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ string}~ \sigma$\\
        \hspace*{0.5em} $ \wedge ~ \exists ~ \mathrm{object} ~ \omega, \mathrm{objname}(\omega) = \sigma$ 
      \end{minipage}
      &
      succeeds when $\mathit{js}$ is some JSON string $\sigma$ looking like a name, and that string $\sigma$ is the \emph{objname} of some \emph{existing} object $\omega$, then assign to
      object variable $v$ that named object $\omega$, so  $v \leftarrow \omega$ \\
      \rule{0pt}{3ex} \\
      %%%
      \begin{minipage}[t]{3.5cm}
        \texttt{\textbf{* member ($x^{\mathrm{\textcolor{blue}{val}}} ~ v^{\mathrm{\textcolor{blue}{obj}}}$)}} \\
        with $x$ being \\
        some Bismon set
      \end{minipage}
        &
      \begin{minipage}[t]{4.5cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ string}~ \sigma$\\
        \hspace*{0.5em} $ \wedge ~ \exists ~ \mathrm{object} ~ \omega \in x, $  \\
        \hspace*{1.8em} $ ( \mathrm{objname}(\omega) = \sigma $ \\
        \hspace*{2em} $  \vee  \mathrm{objid}(\omega) = \sigma )$ 
      \end{minipage}
      &
      succeeds when $\mathit{js}$ is some JSON string $\sigma$ looking like a name or an id, and that string $\sigma$ is the \emph{objname} or \emph{objid} of some \emph{existing} object $\omega$ member of  set $x$, then assign to
      object variable $v$ that object $\omega$, so  $v \leftarrow \omega$ \\
      \rule{0pt}{3ex} \\
      %%%
      \texttt{\textbf{* put ($\omega$)}} &
        \emph{always succeeds} &
        then put in that given Bismon object $\omega$ a JSON payload with $\mathit{js}$ inside \\
      %%%%%%%
    \end{tabular}
  \end{center}
  \bigskip
  \textbf{Notation:} \hspace{0.6em} \begin{minipage}{0.9\textwidth}
    %
    The $\chi, \chi', \chi_i$... are extractors; the $\mathit{js},
    \mathit{js}', \mathit{js}_i$... are JSON values; $\chi
    \triangleright \mathit{js}$ means that the extraction using
    extractor $\chi$ on JSON $ \mathit{js}$ was successful; the $v,
    v', v'', v_i, w, $... are \emph{Bismon} local variables whose type
    is explained with blue annotations like ${}^{\mathrm{\textcolor{blue}{val}}}$; the $x, y$... are Bismon values, the
    $\omega,$... are Bismon objects.
  \end{minipage}
  \end{relsize}
  \caption{simple extraction from some JSON thing $\mathit{js}$;
    {\relsize{-1}{(see also table \ref{tbl:extract-json-complex} below.)}}
  }
  \label{tbl:extract-json-simple}
  \end{table}

Such a JSON extraction is compositional, has side-effects (e.g. could
set local variables), and could fail. When the extraction has
succeeded, the given \textit{sub-statements}... are executed (they are
the components of that JSON extraction statement). No backtracking
occurs during extraction.

For example, a JSON thing\footnote{We may call JSON things what the
  JSON standard call JSON values; and that example could be inside
  some AJAX or REST POST HTTP request.} like {\relsize{-1}{\texttt{\{
      "do": "foo" , "obj" : "\_3d9rq9TD6PH\_6qUv4Hao767", "targets" :
      [ "\_3dmcFZldtxI\_1bEIFl4jqe3", "\_6vMEdC0qxdp\_7shHwvOZEQx" ]
      \}}}} could be extracted with the composite extractor
{\relsize{-1.2}{\texttt{*json\_object(*json\_entry("do"
      *string(v\_str)) *json\_entry("obj" *id(o\_comp))
      *json\_entry("targets" *set(v\_set)))}}} successfully extracting
the value variable \texttt{v\_str} assigned (as a side effect) to the
boxed string \texttt{"foo"}, the object variable \texttt{o\_comp}
assigned to object \texttt{€\_3d9rq9TD} (that is, the object named
\texttt{a\_to\_c}) and the value variable \texttt{v\_set} assigned to
set \texttt{\{ €\_3dmcFZldt €\_6vMEdC0qxd \}} that is to
\texttt{\{also and\}}.


%%%%%%%%%%%%%%%%
\begin{table}%[!htbp]
  \begin{relsize}{-1.3}
  \begin{center}
    \begin{tabular}{lcp{6.4cm}}
      \textbf{extractor node} & \hspace*{1cm} \textbf{success condition} \hspace*{1cm}  & \textbf{side effects and explanation} \\

      %%%
      \texttt{\textbf{* set ($v^{\mathrm{\textcolor{blue}{val}}}$)}} &
      \begin{minipage}[t]{4.5cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ array}$ \\
        \hspace*{2em}  $ \mathtt{\textbf{[}} \; \mathit{js}_1  \mathtt{\textbf{,}} \ldots  \mathit{js}_n \; \mathtt{\textbf{]}} $ of strings, so \\
        \hspace*{1em} $\mathit{js}_1 = \mathrm{string} ~ \sigma_1 ~ \wedge$ \\
        \hspace*{2em} $ \ldots ~ \wedge ~ \mathit{js}_n = \mathrm{string} ~ \sigma_n$ \\
        \hspace*{0.5em} $ \wedge ~ \forall i, ~ \; ~ \exists ~ \mathrm{object} ~ \omega_i,$ \\
        \hspace*{1em} $( ~ \mathrm{objname}(\omega_i) = \sigma_i $ \\
        \hspace*{1.8em} $ \vee ~ \mathrm{objid} (\omega_i) = \sigma_i ~ )$ 
      \end{minipage}
      &
      succeeds when $\mathit{js}$ is some JSON array of JSON strings
      $\mathit{js}_i = \mathrm{string} ~ \sigma_i$,
      then builds a Bismon set of \emph{existing} objects $ v_{set} = \{ \ldots \omega_i \ldots \} $ from these, with
      $\sigma_i \rightarrow \omega_i$ such that $\mathrm{objname}(\omega_i) = \sigma_i$ or  $\mathrm{objid}(\omega_i) = \sigma_i$  \\
            \rule{0pt}{1ex} \\
      %%%
      \texttt{\textbf{* json\_array ($\chi_1 \ldots \chi_n$)}} &
      \begin{minipage}[t]{4.5cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ array}$ \\
        \hspace*{3em}  $ \mathtt{\textbf{[}} \; \mathit{js}_1  \mathtt{\textbf{,}} \ldots  \mathit{js}_n \; \mathtt{\textbf{]}}$ \\
        \hspace*{1em} $\wedge ~ \chi_1 \triangleright \mathit{js}_1 ~ \wedge ~ \ldots ~ \chi_n \triangleright \mathit{js}_n$\\
      \end{minipage}
      &
      succeeds when $\mathit{js}$ is a JSON array of \emph{\textbf{exactly}
      $n$ elements} : $\mathit{js}_1, \ldots \mathit{js}_n$, and extracts them in sequence,
      using $\chi_1$ on $\mathit{js}_1$, then $\chi_2$ on $\mathit{js}_2$, etc... and at
      last $\chi_n$ on $\mathit{js}_n$
            \rule{0pt}{1ex} \\
      \\
      %%%
      \texttt{\textbf{* json\_entry ($\alpha ~ \chi$)}} &
      \begin{minipage}[t]{4.5cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ object}$ having \\
        \hspace*{1.5em}  $ \exists i, \mathtt{\textbf{\{}} ~ \ldots \alpha ~ \mathtt{\textbf{:}} ~ \mathit{js}_i ~ \ldots  \mathtt{\textbf{\}}} ~ \wedge \chi \triangleright \mathit{js}_i $
      \end{minipage} &
      succeeds when $\mathit{js}$ is a JSON object having an attribute string $\alpha$ associated to some JSON value $\mathit{js}_i$ which can be extracted using $\chi$.
            %\rule{0pt}{1ex} \\
      \\
      %%%
      \texttt{\textbf{* json\_entry\_object ($\omega ~ \chi$)}} &
      \begin{minipage}[t]{4.8cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ object}$ having \\
        \hspace*{0.4em} $\exists ~ \mathrm{some ~ Bismon ~ object} ~ \omega$ \\
        \hspace*{0.6em}  $ \exists ~ \mathrm{some ~ JSON ~ string} ~ \alpha, $\\
        \hspace*{0.8em} {\relsize{-0.6}{$ (\mathrm{objid}(\omega) = \alpha  ~ \vee ~ \mathrm{objname}(\omega) = \alpha )$}}  \\
        \hspace*{1.5em}  $ \exists i, \mathtt{\textbf{\{}} ~ \ldots \alpha ~ \mathtt{\textbf{:}} ~ \mathit{js}_i ~ \ldots  \mathtt{\textbf{\}}} ~ \wedge \chi \triangleright \mathit{js}_i $
      \end{minipage} &
      succeeds when $\mathit{js}$ is a JSON object having an attribute string $\alpha$ which is the name or objid of the given Bismon object $\omega$, associated to some JSON value $\mathit{js}_i$ which can be extracted using $\chi$.
            \rule{0pt}{1ex} \\
      \\
      %%%
      \texttt{\textbf{* json\_object ($\chi_1 \ldots \chi_n$)}} &
      \begin{minipage}[t]{4.5cm}
        $\mathit{js} \equiv \mathrm{some ~ JSON ~ object}$ of length exactly $n$ such that \\
        \hspace*{3em}  $ \chi_1 \triangleright \mathit{js} ~ \wedge \ldots ~ \wedge ~ \chi_n \triangleright \mathit{js}$ \\
      \end{minipage}
      &
      succeeds when $\mathit{js}$ is a JSON object of
      \emph{\textbf{exactly} $n$ members} : $\mathtt{\textbf{\{}} \;
      \alpha_1 \; \mathtt{\textbf{:}} \; \mathit{js}_1, \ldots ~
      \alpha_n \; \mathtt{\textbf{:}} \;\mathit{js}_n \;
      \mathtt{\textbf{\}}}$, and that same object $\mathit{js}$ can be
      extracted by each of the $\chi_1 \ldots \chi_n$ in sequence; the
      sub-extractors $\chi_i$ are often but not always of form
      \texttt{\textbf{* json\_entry ($\alpha_i ~ \chi'_i$)}}, \ldots. \\
      \rule{0pt}{1ex} \\ 
      %%%
      \texttt{\textbf{* json\_value ($v^{\mathrm{\textcolor{blue}{val}}}$)}} &
      always succeeds &
      assign  $v ~ \leftarrow ~ \langle \mathit{js} \rangle^{nod}$ to value variable $v$ the \emph{nodal-encoding} of $js$ \\
      \rule{0pt}{1ex} \\    
      %%%
      \texttt{\textbf{* value ($v^{\mathrm{\textcolor{blue}{val}}}$)}} &
      $\exists x ~ \mathrm{Bismon ~ value}, js \equiv  \llbracket x \rrbracket_{json}$  &
      succeeds when $js$ is the minimal canonical encoding of some value $x$;
      then assign $v \leftarrow x$ to value variable $v$ that Bismon value $x$ \\
      \rule{0pt}{1ex} \\      
      %%%
      %
      \texttt{\textbf{* when ($\epsilon ~ \mathit{stmt}_1 ~ \ldots ~ \mathit{stmt}_n$)}} &
      \begin{minipage}[t]{4.5cm}
      The testing expression $\epsilon$
      evaluates as true (non-nil value, or non-zero integer)
      \end{minipage} &
      succeeds when expression $\epsilon$ is true (it usually involves
      some variables computed by previous extractors), then executes
      in sequence the statements $\mathit{stmt}_1 \ldots
      \mathit{stmt}_n$ for their side effects
      \\
      \rule{0pt}{1ex} \\     
      %%%
      %
      \texttt{\textbf{* and\_then ($\chi_1 ~ \ldots ~ \chi_n)$}} &
      \begin{minipage}[t]{4.5cm} sequentially and lazily \\
        $ ( ~ \chi_1 \triangleright \mathit{js} ~ \wedge $ \\
        \hspace*{2em} $ \vdots$ \\
        \hspace*{1em} $ \wedge ~ \chi_n \triangleright \mathit{js} ~ ) $
      \end{minipage} &      
      succeeds when the same $\mathit{js}$ can be successfully
      extracted by \emph{each} of the $\chi_1$ \ldots $\chi_n$ in sequence from left to right
      (failing lazily as soon as some $\chi_j$ fails), and combine
      their side effects (visible from $\chi_j$ to the next
      $\chi_{j+1}$).  \\
      \rule{0pt}{1ex} \\
      %%%%
      \texttt{\textbf{* or\_else ($\chi_1 ~ \ldots ~ \chi_n)$}} &
      \begin{minipage}[t]{4.5cm} sequentially and lazily \\
        $ ( ~ \chi_1 \triangleright \mathit{js} ~ \vee $ \\
        \hspace*{2em} $ \vdots$ \\
        \hspace*{1em} $ \vee ~ \chi_n \triangleright \mathit{js} ~ ) $
      \end{minipage} &      
      succeeds as soon as the same $\mathit{js}$ can be successfully
      extracted -from left to right- by \emph{some} of the $\chi_i$ 
      (continuing lazily to the next $\chi_{i+1}$ when it fails), and combine
      their side effects (visible from $\chi_j$ to the next
      $\chi_{j+1}$).  \\
      % \rule{0pt}{1ex} \\  
      %%%
      %%% {\textcolor{red}{@@ INCOMPLETE @@}} & {\textcolor{red}{...}} & {\textcolor{red}{...}} \\
      %%%
    \end{tabular}
  \end{center}
  \bigskip
  \textbf{Notation:} \hspace{0.6em} \begin{minipage}{0.9\textwidth}
    %
    Share notation with table \ref{tbl:extract-json-simple} above. In
    addition, the $\epsilon$ are Bismon expressions. The $\alpha$ are
    JSON strings in attribute position. The $\sigma$ are strings
    (usually JSON strings). The $\mathit{stmt}$ are Bismon statements.
  \end{minipage}
  \end{relsize}
  \caption{complex extraction from some JSON thing $\mathit{js}$;
    {\relsize{-1}{(see also table \ref{tbl:extract-json-simple} above.)}}
    }
  \label{tbl:extract-json-complex}
  \end{table}



\subsection{Web interface internal design}
\label{subsec:webinterf}

The Web interface \index{web interface} of \emph{bismon} is supposed
to be used without malice (see
\S\ref{subsubsec:leveraging-static-analysis} and
\S\ref{subsubsec:about-bismon}), with a \emph{recent} graphical web
browser~\footnote{Such as Firefox 60.7 or later, or Google Chrome 75.0
  or later, both exist in 2019Q2.}  using HTTP/1.1. In particular,
\emph{bismon} does not take any measure against
\index{denial-of-service} denial-of-service attacks, since it is
supposed to be used on a trusted and friendly corporate intranet or
local area network, not directly on the wild Internet. The network
administrator running \emph{bismon} could deploy usual relevant
techniques (firewalls, \texttt{iptables}, HTTP proxying, DMZ, etc ...)
to avoid such attacks. In practice, there are few web browsers - so
few HTTP clients - interacting with \emph{bismon} simultaneously :
only a dozen of people in some IoT development team, and each uses
his/her graphical browser \index{browser} - a \emph{recent} Firefox or
Chrome~\footnote{So no particular effort is even taken to support a
  variety of old browsers: we don't have any code to e.g. support
  Internet Explorer pecularities or deficiencies. Likewise,
  scalability to thousands of simultaneous HTTP connections is out of
  scope in \emph{bismon}, but it is essential in most web
  applications.}. Compatibility with other browsers\footnote{See
  \bmurl{https://caniuse.com/} and
  \bmurl{https://developer.mozilla.org/} and elsewhere for the many
  subtle but present compatibility issues of current Web technologies,
  and notably \bmurl{https://stackoverflow.com/q/33540051/841108} or
  \bmurl{https://softwareengineering.stackexchange.com/q/393837/40065}
  for some tricky questions directly relevant to our \emph{Bismon}
  development.} is not yet a concern, given the low TRL\index{TRL}
ambitioned. Each \emph{Bismon} user is expected to have one, or only a
few, browser tab[s] interacting with the \texttt{bismon} server, and
these tabs, if there are more than one, are handled as different web
browsers so have different web sessions.  They are physically and
geographically located on the same local area network as the machine
running the \emph{bismon} monitor. So, from web technologies
perspective, \emph{bismon} is making different
trade-offs~\footnote{For example, we could accept making some HTTP
  exchange - e.g. with AJAX - on \emph{every} keystroke on the
  keyboard, but such practice won't be acceptable in usual web
  services. Also, we don't care much about minimizing the HTTP
  exchanges - no ``minification'' needed in practice!} than
``traditional'' web servers or web applications : the web browser
$\leftrightarrow$ \emph{bismon} web server round-trip transmission
time is supposed to be very small so frequent AJAX requests are
possible, the bandwidth is expected to be quite large so voluminous
HTTP responses are acceptable, the number of simultaneous web
connections or of web sessions is tiny. Therefore most web
optimizations are practically unneeded.

With its initial (and current, in mid-2019) naive stop-the-world
garbage collector, the interactive performance and user experience
(i.e. user look-and-feel) of \emph{Bismon} is expected to be
unsatisfactory (since that GC could ``block'' the \texttt{bismon}
monitor and web service for more than half a second - during which the
web interface stays unresponsive, if running the GC on a large enough
heap; but see footnote \ref{fn:initial-gc} suggesting an
improvement). With significant work, that could be improved.

Each HTTP request \index{request} \index{web request} either
corresponds to a ``static'' file path under \texttt{webroot/} (for a
\texttt{GET} or \texttt{HEAD} HTTP request) or else it is handled
dynamically. For a static file path, that file is served directly by
the routine \texttt{onion\_handler\_export\_local\_new} with a
\texttt{Content-Type} corresponding to its suffix; for example an HTTP
\texttt{GET} request of \texttt{favicon.ico} is answered with the
content of \texttt{webroot/favicon.ico} file, and an HTTP \texttt{GET}
request of \texttt{jscript/jquery.js} is served by the content of
\texttt{webroot/jscript/jscript.js}. Care is taken~\footnote{In
  particular, any HTTP request containing \texttt{..} is rejected.} to
avoid serving any static file outside of \texttt{webroot/}. So the
\texttt{webroot/} directory contains static content such as images,
external JavaScript libraries, CSS stylesheets, etc... Static content
requests are always handled the same, so they work even without any
cookies. \index{request!static} \index{static request}

Any HTTP request which cannot be handled as a static resource like
above, because it has no corresponding file under \texttt{webroot/},
is considered as a request for dynamic content and is called a
\index{request!dynamic} \index{dynamic request} \emph{dynamic
  request}. Dynamic content requires a web session \index{web session}
\index{session!web session} cookie \index{web cookie} \index{cookie}
named \texttt{BISMONCOOKIE} which contains~\footnote{A practical
  example of \texttt{BISMONCOOKIE} value might be
  \texttt{n000041R970099188t330716425o\_6IHYL1fOROi\_58xJPnBLCTe}: 41
  is the serial number counting web sessions in the running
  \emph{bismon} process, 970099188 and 330716425 are two random
  numbers, \texttt{\_6IHYL1fOROi\_58xJPnBLCTe} is the
  randomly-generated objid of the web session object.} a cryptographic
quality hash (in practice unforgeable) and mentions the objid
\index{objid} (cf \S\ref{subsubsec:objects}) of some web session
object. If there is no cookie, or if the \index{cookie} cookie is
invalid or wrong (e.g. forged), a login \index{login} form is
returned. So any HTTP request for a dynamic content (that is which is
not handled as a static resource like above) is rejected (with HTTP
status \texttt{403 Forbidden}) if the user (a \index{contributor}
contributor in \emph{bismon} parlance,
cf. \S\ref{subsubsec:bismon-evolving}) is not logged in.

Dynamic requests are reified as very temporary \emph{bismon} objects
of class \texttt{webexchange\_object}. Their \emph{web exchange}
payload~\footnote{There is no programmatic way to create such a web
  exchange payload. It can only be created by processing such dynamic
  HTTP requests.} contains not only a string buffer~\footnote{Since a
  string buffer should contain valid UTF-8 string content without nul
  bytes, this restriction forbids binary contents in HTTP replies to
  dynamic requests. Hence, dynamically computed image contents are not
  possible, unless they use a textual format like SVG.}, to be filled
with the HTTP response content, but also mentions the web request (as
processed by \texttt{libonion}) and the web session object computed
from the \texttt{BISMONCOOKIE} and may contain some arbitrary data
value. The web exchange object is supposed to be filled -like string
buffers are- and at last given some integer HTTP status and
immediately sent back to the browser.  Their web session object is
created at web login time and is of class
\texttt{websession\_object}~\footnote{So the only way to create a web
  session payload is thru the login form. There is no programmatic way
  to create it.}. It knows the contributor who is logged in, the
expiration time of the session, some session data (an arbitrary
\emph{bismon} value; of course more data can sit in attributes or in
components of that web session object), and the web socket \index{web
  socket} connection (if any) to the browser using that session. The
session storage~\footnote{See
  \url{https://developer.mozilla.org/en-US/docs/Web/API/Window/sessionStorage}
  for more.} associated to key \texttt{"bismontab"} identifies and
gives the tab number in the browser. An inactive web session expires
in about an hour~\footnote{See the
  \texttt{USER\_WEBSESSION\_EXPIRATION\_DELAY} constant in
  \texttt{web\_ONIONBM.c}}.

Of course, web request objects or web session objects are
\index{transient} transient and are not and should not be persisted at
dump \index{dump} time (cf. \S\ref{subsec:persistence}). So after each
restart of the \emph{bismon} monitor, its web users
(i.e. contributors) should login \index{login} again.

A dynamic request is handled by some closure \index{closure} and
should be answered in a couple~\footnote{See the
  \texttt{WEBEXCHANGE\_DELAY\_BM} constant in file
  \texttt{web\_ONIONBM.c} ...} of seconds; otherwise a \index{web
  timeout} web timeout \index{timeout!web} occurs. That web handler
\index{web handler} closure is applied to the remaining URL path
string and to the web exchange object created in the
\texttt{libonion}-specific thread dealing with the HTTP request, so
outside of the agenda machinery (cf \S\ref{subsec:multithreadist}), and
usually would add some \index{tasklet} tasklet into the \index{agenda}
agenda. Most of the time, a fraction of a second later, some other
tasklet would complete the filling the web request object and give
some HTTP status code such as \texttt{200 OK}, then an HTTP reply is
sent back to the browser. If a timeout occurs because the web request
object has not been taken care of quickly enough, an HTTP \texttt{500
  Internal Server Error} is given back to the browser and that web
request object is cleared.

The mapping between URL paths (or prefixes) and web handler closures
handling dynamic requests for them is given by the \index{webdict
  root@\texttt{webdict\_root}} \texttt{webdict\_root}\footnote{For
  example: an URL like \texttt{http://localhost:8086/show/status} is
  handled by some \emph{bismon} monitor listening HTTP requests on
  port 8086 and with \texttt{webdict\_root} associating the string
  \texttt{"show"} to some closure $\kappa$, that web handler closure
  $\kappa$ would be applied to the suffix string \texttt{"status"} and
  to the web exchange object $\omega$ created for that HTTP
  request. The result of that application is ignored, only side
  effects -often adding some tasklets into the agenda, and/or filling
  the web exchange object with some XHTML5, etc...- are useful. If the
  string in such a web handling dictionnary $w_{dict}$ is associated
  to some other object $\omega_{wh}$ of class
  \texttt{webhandler\_dict\_object}, that dictionnary object
  $\omega_{wh}$ is recursively explored with the rest of that URL path
  (e.g. \texttt{"status"} in our example). If $w_{dict}$ has some
  \texttt{and\_then} attribute associated to an object
  $\omega_{andthen}$ which is a web dictionnary object, that
  $\omega_{andthen}$ is explored with an incremented depth.}
\index{and then@\texttt{and\_then}} dictionnary predefined object of
class \index{webhandler dict object@\texttt{webhandler\_dict\_object}}
\texttt{webhandler\_dict\_object}; for an empty path in the URL (such
as {\relsize{-1}{\texttt{http://localhost:8086/}}} for example), its
\texttt{web\_empty\_handler} attribute is~\footnote{Since dictionnary
  objects map \emph{non-empty} strings to non-nil values
  (cf. \S\ref{subsubsec:objects}).} used.  If finally no web handler
closure is found, an \texttt{404 Not found} status is returned. The
\texttt{the\_web\_sessions} predefined object stores the dictionnary
of transient web session objects and associates a cookie string to its
web session object. That dictionnary is forcibly cleared at start of
the web server inside \emph{bismon}, but it should be loaded empty,
since web session objects are created and should remain transient.  A
class \texttt{temporary\_webhandler\_dict\_object}, \index{temporary
  webhandler dict object@\texttt{temporary\_webhandler\_dict\_object}}
sub-class of the \texttt{webhandler\_dict\_object} class, also exists
and have \index{transient} \emph{transient dictionnary entries} which
are not dumped.

In practice, dynamic requests are usually generating the HTML5
\index{HTML5} content very dynamically. For generated HTML, it is much
easier to produce \index{XHTML5} XHTML5, the XML variant \index{XML}
of HTML5, because its textual syntax is~\footnote{For instance, within
  a \texttt{<script} HTML5 element containing JavaScript, it is not
  even allowed in HTML5 to have \texttt{if (x \&lt; 5)} even if
  ordinary HTML rules suggest to use \texttt{\&lt;} instead of
  \texttt{<} in textual content... That makes compositional generation
  of mixture of HTML and JavaScript emitting HTML much harder.} much
more regular and easier to generate than with plain HTML5.

The \texttt{webxhtml\_module} \index{module!\texttt{webxhtml\_module}}
in \emph{bismon} has code to ease the emission of XHTML5. And XHTML5
fragments are emitted by the \texttt{emit\_xhtml} routine
\index{emit xhtml@\texttt{emit\_xhtml}}
object~\footnote{So that \texttt{emit\_xhtml} is, like PHP, a
  machinery to emit arbitrary XHTML. However, we want to avoid
  thinking -like PHP was originally designed- in terms of emitting a
  stream of characters, and \texttt{emit\_xhtml} is supposed to emit
  structured XHTML from some structured, tree-like, internal
  representation. That internal representation is a DAG (directed
  acyclic graph).}. That \texttt{emit\_xhtml}, which get as arguments:
the value \texttt{v\_html} to emit; an arbitrary web context object
\texttt{o\_emitctx} which might be in simple cases just some web
session object; a string buffer object \texttt{o\_strbuf} which is
often the web exchange object; the tagged integer recursion depth
\texttt{v\_depth}, which is in general \emph{not}~\footnote{In very
  simple cases, without closures or sequences in the DAG of emitted
  values, the depth could be the depth of XHTML elements, so could be
  the indentation. In general, it is not.} the emitted
  indentation. When the string buffer is too full or the recursion
  depth is too deep, that \texttt{emit\_xhtml} fails. When the emitted
  HTML-reifying value \texttt{v\_html} is nil, nothing happens. When
  it is a scalar, it is emitted trivially: a string is emitted
  HTML-encoded (so \texttt{\&lt;} for \texttt{<}, etc...); a tagged
  integer is emitted in decimal notation; When \texttt{v\_html} is an
  object $\omega_{html}$, it is emitted per the following rules:

  \begin{itemize}
    
\item the \texttt{newline} object emits an indented newline.
  \index{newline@\texttt{newline}}
  
\item the \texttt{nlsp} object emits a newline when the current line
  is long enough, or else a space.
  \index{nlsp@\texttt{nlsp}}
  
\item the \texttt{space} object emits a space character.
  \index{space@\texttt{space}}
  
\item instances of \texttt{html\_void\_element\_object} emit some void
\index{html void element object@\texttt{html\_void\_element\_object}}
  element like e.g. \texttt{<hr class='foo'/>} using the
  \texttt{€\_0FRLxSGQlZ} routine. The \texttt{emit\_xhtml\_open}
\index{emit xhtml open@\texttt{emit\_xhtml\_open}}
  selector should emit -as a side effect- the opening tag \texttt{<hr
    class='foo'} without the ending \texttt{/>}, and returns the string naming the tag, e.g. \texttt{"hr"}.
  
\item instances of \texttt{html\_element\_object} emit recursively
\index{html element object@\texttt{html\_element\_object}}
  using \texttt{€\_5NH940lCHYJ} some nested XHTML element starting
  with a start tag like \texttt{<div} but ending with an end tag like
  \texttt{</div>}; the components of that objects are emitted
  recursively (with an incremented recursion depth). The spacing style
\index{html spacing@\texttt{html\_spacing}}
  is first determined by sending \texttt{html\_spacing} with the
  \texttt{o\_emitctx} and the depth. It can be \texttt{newline} for
  indented, newline separated, content; or \texttt{nlsp} for space or
  newline separated, unindented content; or \texttt{space} for space
  separated content; any other spacing style -notably nil- don't emit
  any separators in the content. The start tag is emitted with
  \texttt{emit\_xhtml\_open} returning the tag string like before
  (e.g. \texttt{"span"} for a \texttt{<span class='somecl'} emission,
  then \texttt{>} is output to end the opening tag, then the
  components, then the end tag is emitted, using the returned tag
  string from \texttt{emit\_xhtml\_open}.
  
\item instances of \texttt{html\_sequence\_object} emit
      recursively their components but without surrounding tags.
      \index{html sequence object@\texttt{html\_sequence\_object}}
      
\item instances of \texttt{html\_active\_object} emit recursively HTML
      \index{html active object@\texttt{html\_active\_object}}
      stuff thru a message of selector \texttt{emit\_xhtml} sent to them.
      
\item any other object is emitted by its name, if it has some, or by
  its objid. This is mostly intended to represent common repeated names or
  words by a single and shared object.
\end{itemize}

When  \texttt{v\_html} is a node of connective $\omega_{conn}$, it is emitted per the following rules:

\begin{itemize}

  \index{int@\texttt{int}}
\item if $\omega_{conn}$ is one of \texttt{int}, \texttt{hexa},
  \index{int@\texttt{int}}
  \index{hexa@\texttt{hexa}}
  \index{octa@\texttt{octa}}
  \texttt{octa} and \texttt{v\_html} is an unary node with a integer
  son $n$, that integer $n$ is emitted in decimal, hexadecimal, octal respectively.

\item if $\omega_{conn}$ is \texttt{id}~\footnote{So nodes of
  connective \texttt{id}, \texttt{object} or \texttt{name} can be used
  to emit objects of class \texttt{html\_void\_element\_object},
  \texttt{html\_element\_object}, \texttt{html\_sequence\_object},
  \texttt{html\_active\_object} which would be handled specially
  otherwise.}  and \texttt{v\_html} is an unary node with an object
  \index{id@\texttt{id}}
  \index{object@\texttt{object}}
  \index{name@\texttt{name}}
  son $\omega_{son}$ its objid is emitted.
  
\item if $\omega_{conn}$ is \texttt{buffer} and \texttt{v\_html} is an
  \index{buffer@\texttt{buffer}}
  unary node with an object son $\omega_{son}$ which has a string
  buffer payload, that string is emitted HTML-encoded.
  
\item if $\omega_{conn}$ is \texttt{object} and \texttt{v\_html} is an unary node with an object son $\omega_{son}$ its name or objid is emitted.
  \index{object@\texttt{object}}
  
\item if $\omega_{conn}$ is \texttt{name} and \texttt{v\_html} is an
  unary node with an object son $\omega_{son}$ its name is emitted,
  \index{name@\texttt{name}}
  and when $\omega_{son}$ is not a named object, we have a failure. If $\omega_{conn}$ is \texttt{name} and \texttt{v\_html} is an
  binary node with an object first son $\omega_{son}$, and some arbirary non-nil second son $\epsilon$ its name is emitted,
  and when $\omega_{son}$ is not a named object, the $\epsilon$ is recursively emitted
  
\item if $\omega_{conn}$ is \texttt{sequence}, every son of
  \texttt{v\_html} is emitted in sequence, with an incremented
  $depth$. Nothing is additionally emitted between
  them. \index{sequence@\texttt{sequence}}

\item if $\omega_{conn}$ is \texttt{space}, or \texttt{newline}, or
  \texttt{nlsp}, every son of \texttt{v\_html} is emitted in sequence,
  with an incremented $depth$. Between each son, a space
  (respectively, a newline, or a smart space of newline) is emitted.
  \index{space@\texttt{space}} \index{newline@\texttt{newline}}
  \index{nlsp@\texttt{nlsp}}


\item for any other object $\omega_{conn}$ as connective, we extract
  its \texttt{emit\_xhtml\_node} attribute $v_{emit~node}$ and its
  \texttt{emit\_xhtml\_connective\_open} attribute
  $v_{emit~open}$. Only one of them should be present (non-nil value)
  and it should be a closure. If $v_{emit~node}$ is given, it is
  applied to $\omega_{conn}$ \texttt{o\_emitctx o\_strbuf $depth + 1$
    v\_html}, else if $v_{emit~open}$ is present, we apply it (like
  the \texttt{emit\_xhtml\_open} selector above) to $\omega_{conn}$
  \texttt{o\_emitctx o\_strbuf $depth + 1$ v\_html} to obtain an XHTML
  element tag. We also extract and use its \texttt{html\_spacing}
  attribute. Then proceed like for \texttt{html\_element\_object}
  using the sons as components....
  
\item {\color{red}{@@ to be completed a lot.}}
  
\end{itemize}


When \texttt{v\_html} is a closure, it is applied {\color{red}{@@ to
    be completed}} and the result of that application is recursively
emitted. When \texttt{v\_html} is a sequence (set or tuple), its
components are emitted recursively.

If no rule is applicable, \texttt{emit\_xhtml} fails.

\medskip

The web session objects are also used for \index{WebSocket}
\emph{WebSockets} with the following additional conventions. The
\texttt{bismon} server uses WebSockets only for asynchronous
communication from that \texttt{bismon} server to Web
browsers~\footnote{So web browsers don't communicate
  \emph{asynchronously} with the \texttt{bismon} server. For such
  communications from browser to \texttt{bismon}, Web browser always
  use synchronous HTTP requests, e.g. using AJAX techniques.}. The
WebSocket messages from \texttt{bismon} to web browsers are arbitrary
\emph{JSON} values.

\bigskip

The \emph{syntax-oriented editor} \index{syntax-oriented!editor}
\index{mentor@\textsc{Mentor} system}
\index{editor!syntactical} (inspired by \textsc{Mentor}:
\cite{donzeaugouge:inria-mentor}) needed\footnote{See also end of
  \ref{subsubsec:about-bismon} above, and also
  \bmurl{https://stackoverflow.com/a/47116008/841108} for more.} in
\emph{Bismon} by its homoiconicity \index{homoiconicity}, and used by
the \index{expert!static analysis} static analysis expert, won't
handle lines of tokens in an editor widget\footnote{Of course, using
  \bmurl{https://codemirror.net/} will be useful to show analysed C or
  C++ source code, but not for our \emph{Bismon}'s \index{DSL} DSL.},
but should enable that expert user to enter and \emph{conveniently}
manipulate the \emph{abstract syntax tree} (or \index{AST} AST) of our
\emph{Bismon} \index{DSL} DSL. That AST should appear in the web
browser as some ``graphical'' tree (e.g. displayed as
\href{https://en.wikipedia.org/wiki/Scalable\_Vector\_Graphics}{SVG}
\index{SVG} elements or in some
\href{https://en.wikipedia.org/wiki/Canvas\_element}{Canvas element})
and/or more probably as nested, but with visible borders,
\href{https://en.wikipedia.org/wiki/HTML5}{HTML5} \index{HTML5} markup
\index{markup!element} elements updated thru the \index{DOM}
\href{https://en.wikipedia.org/wiki/Document\_Object\_Model}{DOM}. AST
manipulation should be easy, e.g. using contextual menus and/or
keyboard \index{keyboard} function keys \index{function!key} like
\fbox{\texttt{F1}}, \fbox{\texttt{F2}} and/or control keyboard
sequences\index{control!keyboard sequence} -with e.g. the
\fbox{\texttt{Ctrl}} or \fbox{\texttt{Esc}} keys- inspired by those of
\texttt{emacs} or \texttt{vim}, etc... The set of elementary AST
user-doable manipulations\index{manipulation!of AST} -including copy
and pasting \index{copy/paste} of AST sub-trees- should be carefully
designed, but small. The design insight could represent these ASTs
both in user's browser as DOM elements and inside \emph{Bismon} as AST
transient \index{transient}\index{object} objects and/or \index{node}
nodes.

\medskip

\subsection{Using \texttt{bismon} for \textsc{Chariot}}
\label{subsec:bismon-for-chariot}

To run the \texttt{bismon} monitor for \textsc{Chariot} related
activities, that monitor should initialize its state for these
activities. So you need to pass \texttt{-i init\_chariotdemo} as a
program argument when running \texttt{bismon} in that case.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Local Variables: ;;
%% compile-command: "cd ..; ./build-bismon-doc.sh" ;;
%% End: ;;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
