From 39b2b1243b2b3c435584958f5b8bd4b420d24994 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Feb 2020 12:41:06 +0000 Subject: [PATCH 1/3] Add XML trace specification and a reference in the documentation. --- doc/assets/xml_spec.md | 416 ++++++++++++++++++++++++++++ doc/assets/xml_spec.tex | 403 +++++++++++++++++++++++++++ doc/cprover-manual/cbmc-tutorial.md | 12 + 3 files changed, 831 insertions(+) create mode 100644 doc/assets/xml_spec.md create mode 100644 doc/assets/xml_spec.tex diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md new file mode 100644 index 00000000000..4578689e326 --- /dev/null +++ b/doc/assets/xml_spec.md @@ -0,0 +1,416 @@ +XML Specification for CBMC Traces +================================= + +Traces of GOTO programs consist of *steps*, i.e. steps are elements of +the XML object. + +Trace Step Types +---------------- + +- assignment + +- assume + +- assert + +- goto instruction + +- function call + +- function return + +- output + +- input + +- declaration + +- dead statement + +- spawn statement + +- memory barrier + +unused: + +- constraint + +- location + +- shared read + +- shared write + +- atomic begin + +- atomic end + +Source Location +--------------- + +Every trace step optionally contains the source location as an element. + +**Attributes** (all are optional): + +- `working-directory`: string of the full path + +- `file`: name of the file containing this location + +- `line`: non-negative integer + +- `column`: non-negative integer + +- `function`: name of the function this line belongs to + +**Example**: + +``` {.xml} + +``` + +**XSD**: + +``` {.xml} + + + + + + + +``` + +Trace Steps in XML +------------------ + +The attributes `hidden, thread, step_nr` are common to all trace steps. + +``` {.xml} + + + + + +``` + +[Assert]{} (element name: `failure`) + +**Attributes**: + +- `hidden`: boolean attribute + +- `thread`: thread number (positive integer) + +- `step_nr`: number in the trace (positive integer) + +- `reason`: comment (string) + +- `property`: property ID (irep\_idt) + +**Example**: + +``` {.xml} + +``` + +**XSD**: + +``` {.xml} + + + + + + + + + + +``` + +[Assignment, Declaration]{} (element name: `assignment`) + +**Attributes**:\ +if the lhs symbol is known + +- `mode`: {C, Java, ...} + +- `identifier`: string (symbol name) + +- `base_name`: string (e.g. “counter”) + +- `display_name`: string (e.g. "main::1::counter") + +always present + +- `hidden`: boolean attribute + +- `thread`: thread number (positive integer) + +- `step_nr`: number in the trace (positive integer) + +- `assignment_type`: {actual\_parameter, state} + +**Elements**:\ +if the lhs symbol is known + +- `type`: C type (e.g. “signed int”) + +always present + +- `full_lhs`: original lhs expression (after dereferencing) + +- `full_lhs_value`: a constant with the new value + +**Example**: + +``` {.xml} + +``` + +**XSD**: + +``` {.xml} + + + + + + + + + + + + + + + + +``` + +[Input]{} (element name: `input`) + +**Attributes**: + +- `hidden`: boolean attribute + +- `thread`: thread number (positive integer) + +- `step_nr`: number in the trace (positive integer) + +**Elements**: + +- `input_id`: IO id (the variable name) + +for each IO argument + +- `value`: the (correctly typed) value the input is initialised with + +- `value_expression`: the internal representation of the value + +**Example**: + +``` {.xml} + + i + -2147145201 + + + -2147145201 + + + + +``` + +**XSD**: + +``` {.xml} + + + + + + + + + + + + + + + + + + + +``` + +[Output]{} (element name: `output`) + +**Attributes**: + +- `hidden`: boolean attribute + +- `thread`: thread number (positive integer) + +- `step_nr`: number in the trace (positive integer) + +**Elements**: + +- `text`: formatted list of IO arguments + +for each IO argument + +- `value`: the (correctly typed) value the input is initialised with + +- `value_expression`: the internal representation of the value + +[Function Call]{} (element name: `function_call`)\ +[Function Return]{} (element name: `function_return`) + +**Attributes**: + +- `hidden`: boolean attribute + +- `thread`: thread number (positive integer) + +- `step_nr`: number in the trace (positive integer) + +**Elements**: + +- `function`: compound element containing the following\ + Attributes: + + - `display_name`: language specific pretty name + + - `identifier`: the internal unique identifier + + Elements: + + - `location`: source location of the called function + +**Example**: + +``` {.xml} + +``` + +**XSD**: + +``` {.xml} + + + + + + + + + + + + + + + + + + + + + +``` + +[All Other Steps]{} (element name: `location-only`) + +Only included if the source location exists and differs from the +previous one.\ +**Attributes**: + +- `hidden`: boolean attribute + +- `thread`: thread number (positive integer) + +- `step_nr`: number in the trace (positive integer) + +**Elements**: + +- `location`: location of the called function + +**Example**: + +``` {.xml} + +``` + +**XSD**: + +``` {.xml} + + + + + + + + +``` + +Full Trace XSD +-------------- + +``` {.xml} + + + + + + + + + + + + + +``` + +Notes +----- + +The path from the input C code to XML trace goes through the following +steps:\ +C -> GOTO -> SSA -> GOTO Trace -> XML Trace + +#### 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. diff --git a/doc/assets/xml_spec.tex b/doc/assets/xml_spec.tex new file mode 100644 index 00000000000..eaed20d66f7 --- /dev/null +++ b/doc/assets/xml_spec.tex @@ -0,0 +1,403 @@ +\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} + +\end{minted} + +\noindent\textbf{XSD}: +\begin{minted}{xml} + + + + + + + +\end{minted} + +\subsection{Trace Steps in XML} +\vspace{1em} +\noindent The attributes \texttt{hidden, thread, step\_nr} are common to all trace steps. + +\begin{minted}{xml} + + + + + +\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} + +\end{minted} + +\noindent\textbf{XSD}: +\begin{minted}{xml} + + + + + + + + + + +\end{minted} + +\hrulefill + +\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, $\ldots$\} +\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 +\end{itemize} + +\noindent\textbf{Example}: +\begin{minted}{xml} + +\end{minted} + +\noindent\textbf{XSD}: +\begin{minted}{xml} + + + + + + + + + + + + + + + + +\end{minted} + +\hrulefill + +\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} + + i + -2147145201 + + + -2147145201 + + + + +\end{minted} + +\noindent\textbf{XSD}: +\begin{minted}{xml} + + + + + + + + + + + + + + + + + + + +\end{minted} + +\hrulefill + +\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{value}: the (correctly typed) value the input is initialised with +\item \texttt{value\_expression}: the internal representation of the value +\end{itemize} + +\hrulefill + +\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 + \end{itemize} +\end{itemize} + +\noindent\textbf{Example}: +\begin{minted}{xml} + +\end{minted} + +\noindent\textbf{XSD}: +\begin{minted}{xml} + + + + + + + + + + + + + + + + + + + + + +\end{minted} + +\hrulefill + +\begin{center} + {\Large All Other Steps} (element name: \texttt{location-only}) +\end{center} + +\noindent Only included if the source location exists and differs from the previous one.\\ + +\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} + +\end{minted} + +\noindent\textbf{XSD}: +\begin{minted}{xml} + + + + + + + + +\end{minted} + +\subsection{Full Trace XSD} + +\begin{minted}{xml} + + + + + + + + + + + + + +\end{minted} + +\subsection{Notes} + +The path from the input C code to XML trace goes through the following steps:\\ + +$\textrm{C} \to \textrm{GOTO} \to \textrm{SSA} \to \textrm{GOTO Trace} \to \textrm{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} diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md index 133f01cebb1..10a6660523d 100644 --- a/doc/cprover-manual/cbmc-tutorial.md +++ b/doc/cprover-manual/cbmc-tutorial.md @@ -130,6 +130,18 @@ access. If you add a branch to the example that requires that `argc>=3`, the bug is fixed and CBMC will report that the proofs of all properties have been successful. +To simplify further processing of counterexample traces, CBMC supports XML as a +possible output format. + +``` + cbmc file1.c --trace --xml-ui +``` + +The specification of the XML trace output can be found here: [XML +Specification](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/assets/xml_spec.tex) +and can be build by `pdflatex -shell-escape xml_spec.tex`. Alternatively, you +view it in Markdown [here](../../../assets/xml_spec). + ### Verifying Modules In the example above, we used a program that starts with a `main` From 7e2ad3829c7e9753a883d934d956ab8b049ed82a Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 24 Feb 2020 16:22:17 +0000 Subject: [PATCH 2/3] Fix some typos/syntax errors in xml_spec.tex MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Also replace some latex instructions that pandoc can’t handle with some it can. --- doc/assets/xml_spec.md | 111 +++++++++++++++++++++++++--------------- doc/assets/xml_spec.tex | 86 +++++++++++++++++++------------ 2 files changed, 121 insertions(+), 76 deletions(-) diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md index 4578689e326..05df421b0c9 100644 --- a/doc/assets/xml_spec.md +++ b/doc/assets/xml_spec.md @@ -74,10 +74,12 @@ Every trace step optionally contains the source location as an element. ``` {.xml} - - + + + + use="optional"/> + ``` @@ -88,14 +90,14 @@ Trace Steps in XML The attributes `hidden, thread, step_nr` are common to all trace steps. ``` {.xml} - + ``` -[Assert]{} (element name: `failure`) +Assert (element name: `failure`) **Attributes**: @@ -127,14 +129,14 @@ The attributes `hidden, thread, step_nr` are common to all trace steps. - + ``` -[Assignment, Declaration]{} (element name: `assignment`) +Assignment, Declaration (element name: `assignment`) **Attributes**:\ if the lhs symbol is known @@ -143,7 +145,7 @@ if the lhs symbol is known - `identifier`: string (symbol name) -- `base_name`: string (e.g. “counter”) +- `base_name`: string (e.g. "counter") - `display_name`: string (e.g. "main::1::counter") @@ -160,7 +162,7 @@ always present **Elements**:\ if the lhs symbol is known -- `type`: C type (e.g. “signed int”) +- `type`: C type (e.g. "signed int") always present @@ -192,7 +194,7 @@ always present - + @@ -205,7 +207,7 @@ always present ``` -[Input]{} (element name: `input`) +Input (element name: `input`) **Attributes**: @@ -244,28 +246,22 @@ for each IO argument **XSD**: ``` {.xml} - - - - - - - - - - - - - - + + + + + + + + ``` -[Output]{} (element name: `output`) +Output (element name: `output`) **Attributes**: @@ -281,12 +277,33 @@ for each IO argument for each IO argument -- `value`: the (correctly typed) value the input is initialised with +- `text`: The textual representation of the output + +- `location`: The original source location of the output + +- `value`: the (correctly typed) value of the object that is being + output - `value_expression`: the internal representation of the value -[Function Call]{} (element name: `function_call`)\ -[Function Return]{} (element name: `function_return`) +``` {.xml} + + + + + + + + + + + + + +``` + +Function Call (element name: `function_call`)\ +Function Return (element name: `function_return`) **Attributes**: @@ -309,6 +326,8 @@ for each IO argument - `location`: source location of the called function + - `function`: The function that is being called/returned from. + **Example**: ``` {.xml} @@ -327,10 +346,18 @@ for each IO argument - - - + + + + + + + + + + + @@ -346,7 +373,7 @@ for each IO argument ``` -[All Other Steps]{} (element name: `location-only`) +All Other Steps (element name: `location-only`) Only included if the source location exists and differs from the previous one.\ @@ -378,7 +405,7 @@ previous one.\ - + ``` @@ -390,13 +417,13 @@ Full Trace XSD - - - - - - - + + + + + + + @@ -407,7 +434,7 @@ Notes The path from the input C code to XML trace goes through the following steps:\ -C -> GOTO -> SSA -> GOTO Trace -> XML Trace +`C` → `GOTO` → `SSA` → `GOTO Trace` → `XML Trace` #### SSA to GOTO Trace diff --git a/doc/assets/xml_spec.tex b/doc/assets/xml_spec.tex index eaed20d66f7..8789c58e962 100644 --- a/doc/assets/xml_spec.tex +++ b/doc/assets/xml_spec.tex @@ -60,16 +60,18 @@ \subsection{Source Location} \begin{minted}{xml} - - + + + + use="optional"/> + -\end{minted} - +\end{minted} + \subsection{Trace Steps in XML} -\vspace{1em} + \noindent The attributes \texttt{hidden, thread, step\_nr} are common to all trace steps. \begin{minted}{xml} @@ -98,7 +100,7 @@ \subsection{Trace Steps in XML} \end{minted} @@ -115,8 +117,7 @@ \subsection{Trace Steps in XML} \end{minted} - -\hrulefill + \begin{center} {\Large Assignment, Declaration} (element name: \texttt{assignment}) @@ -125,7 +126,7 @@ \subsection{Trace Steps in XML} \noindent\textbf{Attributes}:\\ if the lhs symbol is known \begin{itemize} -\item \texttt{mode}: \{C, Java, $\ldots$\} +\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'') @@ -184,7 +185,6 @@ \subsection{Trace Steps in XML} \end{minted} -\hrulefill \begin{center} {\Large Input} (element name: \texttt{input}) @@ -224,28 +224,21 @@ \subsection{Trace Steps in XML} \noindent\textbf{XSD}: \begin{minted}{xml} - - - - - - - - - - - - - - - + + + + + + + + + \end{minted} -\hrulefill \begin{center} {\Large Output} (element name: \texttt{output}) @@ -264,11 +257,28 @@ \subsection{Trace Steps in XML} \end{itemize} for each IO argument \begin{itemize} -\item \texttt{value}: the (correctly typed) value the input is initialised with +\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} -\hrulefill +\begin{minted}{xml} + + + + + + + + + + + + + +\end{minted} + \begin{center} {\Large Function Call} (element name: \texttt{function\_call})\\ @@ -293,6 +303,7 @@ \subsection{Trace Steps in XML} 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} @@ -312,14 +323,22 @@ \subsection{Trace Steps in XML} - - - + + + + + + + + + + + @@ -331,7 +350,6 @@ \subsection{Trace Steps in XML} \end{minted} -\hrulefill \begin{center} {\Large All Other Steps} (element name: \texttt{location-only}) @@ -392,7 +410,7 @@ \subsection{Notes} The path from the input C code to XML trace goes through the following steps:\\ -$\textrm{C} \to \textrm{GOTO} \to \textrm{SSA} \to \textrm{GOTO Trace} \to \textrm{XML Trace}$ +\texttt{C} → \texttt{GOTO} → \texttt{SSA} → \texttt{GOTO Trace} → \texttt{XML Trace} \paragraph{SSA to GOTO Trace} From 44879df4fe5e048bb5a6200cb58264bdedda8e94 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 25 Feb 2020 14:38:22 +0000 Subject: [PATCH 3/3] Add XSD that describes output of cbmc --trace Note that this is based on observed outputs from cbmc, there is currently no mechanism in place that enforces CBMC to conform to this. We have discussed adding a regression test pass for checking that at least our own regression tests conform to the spec. In a future PR. --- doc/assets/xml_spec.xsd | 180 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 doc/assets/xml_spec.xsd diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd new file mode 100644 index 00000000000..1255c524022 --- /dev/null +++ b/doc/assets/xml_spec.xsd @@ -0,0 +1,180 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +