xml_spec.tex

\documentclass[12pt]{article}
\usepackage{a4wide}
\usepackage{minted}

\begin{document}

\section{XML Specification for CBMC Traces}

Traces of GOTO programs consist of \emph{steps}, i.e. steps are elements of the
XML object.

\subsection{Trace Step Types}

\begin{itemize}
\item assignment
\item assume
\item assert
\item goto instruction
\item function call
\item function return
\item output
\item input
\item declaration
\item dead statement
\item spawn statement
\item memory barrier
\end{itemize}

unused:
\begin{itemize}
\item constraint
\item location
\item shared read
\item shared write
\item atomic begin
\item atomic end
\end{itemize}

\subsection{Source Location}

\noindent Every trace step optionally contains the source location as an
element.

\noindent\textbf{Attributes} (all are optional):
\begin{itemize}
\item \texttt{working-directory}: string of the full path
\item \texttt{file}: name of the file containing this location
\item \texttt{line}: non-negative integer
\item \texttt{column}: non-negative integer
\item \texttt{function}: name of the function this line belongs to
\end{itemize}

\noindent\textbf{Example}:
\begin{minted}{xml}
<location file="test.c" function="main" line="7"
          working-directory="/tmp/subfolder"/>
\end{minted}

\noindent\textbf{XSD}:
\begin{minted}{xml}
<xs:element name="location">
  <xs:complexType>
    <xs:attribute name="file" type="xs:string" use="optional"/>
    <xs:attribute name="line" type="xs:int" use="optional"/>
    <xs:attribute name="column" type="xs:int" use="optional"/>
    <xs:attribute name="working-directory" type="xs:string"
                  use="optional"/>
    <xs:attribute name="function" type="xs:string" use="optional"/>
  </xs:complexType>
</xs:element>
\end{minted}

\subsection{Trace Steps in XML}

\noindent The attributes \texttt{hidden, thread, step\_nr} are common to all trace steps.

\begin{minted}{xml}
<xs:attributeGroup name="traceStepAttrs">
  <xs:attribute name="hidden" type="xs:string"></xs:attribute>
  <xs:attribute name="step_nr" type="xs:int"></xs:attribute>
  <xs:attribute name="thread" type="xs:int"></xs:attribute>
</xs:attributeGroup>
\end{minted}

\begin{center}
{\Large Assert} (element name: \texttt{failure})
\end{center}

\noindent\textbf{Attributes}:
\begin{itemize}
\item \texttt{hidden}: boolean attribute
\item \texttt{thread}: thread number (positive integer)
\item \texttt{step\_nr}: number in the trace (positive integer)
\item \texttt{reason}: comment (string)
\item \texttt{property}: property ID (irep\_idt)
\end{itemize}

\noindent\textbf{Example}:
\begin{minted}{xml}
<failure hidden="false" step_nr="23" thread="0"
         property="main.assertion.1"
         reason="assertion a + b &lt; 10">
  <location .. />
</failure>
\end{minted}

\noindent\textbf{XSD}:
\begin{minted}{xml}
<xs:element name="failure">
  <xs:complexType>
    <xs:all>
      <xs:element name="location" minOccurs="0"></xs:element>
    </xs:all>
    <xs:attributeGroup ref="traceStepAttrs">
    <xs:attribute name="property" type="xs:string"></xs:attribute>
    <xs:attribute name="reason" type="xs:string"></xs:attribute>
  </xs:complexType>
</xs:element>
\end{minted}


\begin{center}
{\Large Assignment, Declaration} (element name: \texttt{assignment})
\end{center}

\noindent\textbf{Attributes}:\\
if the lhs symbol is known
\begin{itemize}
\item \texttt{mode}: \{C, Java, …\}
\item \texttt{identifier}: string (symbol name)
\item \texttt{base\_name}: string (e.g. ``counter'')
\item \texttt{display\_name}: string (e.g. ``main::1::counter'')
\end{itemize}
always present
\begin{itemize}
\item \texttt{hidden}: boolean attribute
\item \texttt{thread}: thread number (positive integer)
\item \texttt{step\_nr}: number in the trace (positive integer)
\item \texttt{assignment\_type}: \{actual\_parameter, state\}
\end{itemize}

\noindent\textbf{Elements}:\\
if the lhs symbol is known
\begin{itemize}
\item \texttt{type}: C type (e.g. ``signed int'')
\end{itemize}
always present
\begin{itemize}
\item \texttt{full\_lhs}: original lhs expression (after dereferencing)
\item \texttt{full\_lhs\_value}: a constant with the new value.
  \begin{itemize}
    \item If the type of data can be represented as a fixed width sequence of bits
     then, there will be an attribute \texttt{`binary`} containing the binary
     representation. If the data type is signed and the value is negative
     then the binary will be encoded using two's complement.
  \end{itemize}

\end{itemize}


\noindent\textbf{Example}:
\begin{minted}{xml}
<assignment assignment_type="state" base_name="b" display_name="main::1::b"
            hidden="false" identifier="main::1::b" mode="C" step_nr="22"
            thread="0">
  <location .. />
  <type>signed int</type>
  <full_lhs>b</full_lhs>
  <full_lhs_value binary="10010000000000000000000000000000">-1879048192</full_lhs_value>
</assignment>
<assignment assignment_type="state" base_name="d" display_name="main::1::d" hidden="false" identifier="main::1::d" mode="C" step_nr="26" thread="0">
  <location ../>
  <type>double</type>
  <full_lhs>d</full_lhs>
  <full_lhs_value
binary="0100000000010100011001100110011001100110011001100110011001100110">5.1</full_lhs_value>
</assignment>
\end{minted}

\noindent\textbf{XSD}:
\begin{minted}{xml}
<xs:element name="assignment">
  <xs:complexType>
    <xs:all>
      <xs:element name="location" minOccurs="0"></xs:element>
      <xs:element name="type" type="xs:string" minOccurs="0"></xs:element>
      <xs:element name="full_lhs" type="xs:string"></xs:element>
      <xs:element name="full_lhs_value">
        <xs:complexType>
          <xs:simpleContent>
            <xs:extension base="xs:string">
              <xs:attribute name="binary" type="xs:string"/>
            </xs:extension>
          </xs:simpleContent>
        </xs:complexType>
      </xs:element>
    </xs:all>
    <xs:attributeGroup ref="traceStepAttrs">
    <xs:attribute name="assignment_type" type="xs:string"></xs:attribute>
    <xs:attribute name="base_name" type="xs:string"
                  use="optional"></xs:attribute>
    <xs:attribute name="display_name" type="xs:string"
                  use="optional"></xs:attribute>
    <xs:attribute name="identifier" type="xs:string"
                  use="optional"></xs:attribute>
    <xs:attribute name="mode" type="xs:string" use="optional"></xs:attribute>
  </xs:complexType>
</xs:element>
\end{minted}


\begin{center}
{\Large Input} (element name: \texttt{input})
\end{center}

\noindent\textbf{Attributes}:
\begin{itemize}
\item \texttt{hidden}: boolean attribute
\item \texttt{thread}: thread number (positive integer)
\item \texttt{step\_nr}: number in the trace (positive integer)
\end{itemize}

\noindent\textbf{Elements}:
\begin{itemize}
\item \texttt{input\_id}: IO id (the variable name)
\end{itemize}
for each IO argument
\begin{itemize}
\item \texttt{value}: the (correctly typed) value the input is initialised with
\item \texttt{value\_expression}: the internal representation of the value
\end{itemize}

\noindent\textbf{Example}:
\begin{minted}{xml}
<input hidden="false" step_nr="21" thread="0">
  <input_id>i</input_id>
  <value>-2147145201</value>
  <value_expression>
    <integer binary="10000000000001010010101000001111"
             c_type="int" width="32">
      -2147145201
    </integer>
  </value_expression>
  <location .. />
</input>
\end{minted}

\noindent\textbf{XSD}:
\begin{minted}{xml}
<xs:element name="input">
  <xs:complexType>
    <xs:sequence>
      <xs:element name="input_id" type="xs:string"/>
      <xs:sequence minOccurs="0" maxOccurs="unbounded">
        <xs:element name="value" type="xs:string"/>
        <xs:element ref="value_expression"/>
      </xs:sequence>
      <xs:element ref="location" minOccurs="0"/>
    </xs:sequence>
    <xs:attributeGroup ref="traceStepAttrs"/>
  </xs:complexType>
</xs:element>
\end{minted}


\begin{center}
  {\Large Output} (element name: \texttt{output})
\end{center}

\noindent\textbf{Attributes}:
\begin{itemize}
\item \texttt{hidden}: boolean attribute
\item \texttt{thread}: thread number (positive integer)
\item \texttt{step\_nr}: number in the trace (positive integer)
\end{itemize}

\noindent\textbf{Elements}:
\begin{itemize}
\item \texttt{text}: formatted list of IO arguments
\end{itemize}
for each IO argument
\begin{itemize}
\item \texttt{text}: The textual representation of the output
\item \texttt{location}: The original source location of the output
\item \texttt{value}: the (correctly typed) value of the object that is being output
\item \texttt{value\_expression}: the internal representation of the value
\end{itemize}

\begin{minted}{xml}
<xs:element name="output">
  <xs:complexType>
    <xs:sequence>
      <xs:element name="text" type="xs:string"/>
      <xs:element ref="location" minOccurs="0"/>
      <xs:sequence minOccurs="0" maxOccurs="unbounded">
        <xs:element name="value" type="xs:string"/>
        <xs:element ref="value_expression"/>
      </xs:sequence>
    </xs:sequence>
  <xs:attributeGroup ref="traceStepAttrs"/>
  </xs:complexType>
</xs:element>
\end{minted}


\begin{center}
  {\Large Function Call} (element name: \texttt{function\_call})\\
  {\Large Function Return} (element name: \texttt{function\_return})
\end{center}

\noindent\textbf{Attributes}:
\begin{itemize}
\item \texttt{hidden}: boolean attribute
\item \texttt{thread}: thread number (positive integer)
\item \texttt{step\_nr}: number in the trace (positive integer)
\end{itemize}

\noindent\textbf{Elements}:
\begin{itemize}
\item \texttt{function}: compound element containing the following\\
  Attributes:
  \begin{itemize}
  \item \texttt{display\_name}: language specific pretty name
  \item \texttt{identifier}: the internal unique identifier
  \end{itemize}
  Elements:
  \begin{itemize}
  \item \texttt{location}: source location of the called function
  \item \texttt{function}: The function that is being called/returned from.
  \end{itemize}
\end{itemize}

\noindent\textbf{Example}:
\begin{minted}{xml}
<function_call hidden="false" step_nr="20" thread="0">
  <function display_name="main" identifier="main">
    <location .. />
  </function>
  <location .. />
</function_call>
\end{minted}

\noindent\textbf{XSD}:
\begin{minted}{xml}
<xs:element name="function_call">
  <xs:complexType>
    <xs:all>
      <xs:element name="location" minOccurs="0"></xs:element>
      <xs:element ref="function"/>
    </xs:all>
    <xs:attributeGroup ref="traceStepAttrs">
  </xs:complexType>
</xs:element>

<xs:element name="function_return">
  <xs:complexType>
    <xs:sequence>
      <xs:element ref="function"/>
      <xs:element ref="location" minOccurs="0"/>
    </xs:sequence>
    <xs:attributeGroup ref="traceStepAttrs"/>
  </xs:complexType>
</xs:element>

<xs:element name="function">
  <xs:complexType>
    <xs:all>
      <xs:element name="location" minOccurs="0"></xs:element>
    </xs:all>
    <xs:attribute name="display_name" type="xs:string"></xs:attribute>
    <xs:attribute name="identifier" type="xs:string"></xs:attribute>
  </xs:complexType>
</xs:element>
\end{minted}


\begin{center}
  {\Large All Other Steps} (element name: \texttt{location-only} and
\texttt{loop-head})
\end{center}

\noindent A step that indicates where in the source program we are.

A \texttt{location-only} step is emitted if the source location exists and
differs from the previous one.

A  \texttt{loop-head} step is emitted if the location relates to the start of a loop,
even if the previous step is also the same start of the loop (to ensure
that it is printed out for each loop iteration) \\

\noindent\textbf{Attributes}:
\begin{itemize}
\item \texttt{hidden}: boolean attribute
\item \texttt{thread}: thread number (positive integer)
\item \texttt{step\_nr}: number in the trace (positive integer)
\end{itemize}

\noindent\textbf{Elements}:
\begin{itemize}
\item \texttt{location}: location of the called function
\end{itemize}

\noindent\textbf{Example}:
\begin{minted}{xml}
<location-only hidden="false" step_nr="19" thread="0">
  <location .. />
</location-only>
<loop-head hidden="false" step_nr="19" thread="0">
<location .. />
</loop-head>
\end{minted}

\noindent\textbf{XSD}:
\begin{minted}{xml}
<xs:element name="location-only">
  <xs:complexType>
    <xs:all>
      <xs:element name="location" minOccurs="0"></xs:element>
    </xs:all>
    <xs:attributeGroup ref="traceStepAttrs">
  </xs:complexType>
</xs:element>
<xs:element name="loop-head">
  <xs:complexType>
    <xs:all>
      <xs:element name="location" minOccurs="0"></xs:element>
    </xs:all>
    <xs:attributeGroup ref="traceStepAttrs">
  </xs:complexType>
</xs:element>
\end{minted}

\subsection{Full Trace XSD}

\begin{minted}{xml}
<xs:element name="goto_trace">
  <xs:complexType>
    <xs:choice minOccurs="0" maxOccurs="unbounded">
      <xs:element ref="assignment"></xs:element>
      <xs:element ref="failure"></xs:element>
      <xs:element ref="function_call"></xs:element>
      <xs:element ref="function_return"></xs:element>
      <xs:element ref="input"></xs:element>
      <xs:element ref="output"></xs:element>
      <xs:element ref="location-only"></xs:element>
      <xs:element ref="loop-head"></xs:element>
    </xs:choice>
  </xs:complexType>
</xs:element>
\end{minted}

\subsection{Notes}

The path from the input C code to XML trace goes through the following steps:\\

\texttt{C} → \texttt{GOTO} → \texttt{SSA} → \texttt{GOTO Trace} → \texttt{XML Trace}

\paragraph{SSA to GOTO Trace}

SSA steps are sorted by clocks and the following steps are skipped: PHI, GUARD
assignments; shared-read, shared-write, constraint, spawn, atomic-begin,
atomic-end.

\end{document}