From 226b71bb40fdf8bc09e65a45b7c42382ebb44650 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 24 Apr 2020 17:25:30 +0100 Subject: [PATCH 01/10] Add test for printing different float values in the trace --- regression/cbmc/float-trace/test.c | 20 ++++++++++++++++++++ regression/cbmc/float-trace/test.desc | 14 ++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 regression/cbmc/float-trace/test.c create mode 100644 regression/cbmc/float-trace/test.desc diff --git a/regression/cbmc/float-trace/test.c b/regression/cbmc/float-trace/test.c new file mode 100644 index 00000000000..a79ea673e06 --- /dev/null +++ b/regression/cbmc/float-trace/test.c @@ -0,0 +1,20 @@ +#include +#include + +int main() +{ + float zero = 0.0f; + float one = 1.0f; + double dzero = 0.0; + float complex = 0x1p+37f; + + assert(false); + + return 0; +} + +void test(float value) +{ + assert(value == 1.0f); + assert(value == 0.0f); +} diff --git a/regression/cbmc/float-trace/test.desc b/regression/cbmc/float-trace/test.desc new file mode 100644 index 00000000000..51945a3d5ea --- /dev/null +++ b/regression/cbmc/float-trace/test.desc @@ -0,0 +1,14 @@ +CORE +test.c +--trace --xml-ui +^EXIT=10$ +^SIGNAL=0$ +VERIFICATION FAILED +0.0f +1.0f +0.0 +1\.374390e\+11f +-- +-- +Checks that the binary value is printed for floating point types +point types From 7e5b37e22a25ef8df9eb2af053bac0e4e5b611a4 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 24 Apr 2020 17:30:32 +0100 Subject: [PATCH 02/10] Adapt test to check for binary in trace --- regression/cbmc/Float24/test.desc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/Float24/test.desc b/regression/cbmc/Float24/test.desc index fbb546488c7..1306f3ad6f5 100644 --- a/regression/cbmc/Float24/test.desc +++ b/regression/cbmc/Float24/test.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -5\.1 +5\.1 -- ^warning: ignoring -5\.1l +5\.1l From 9384b911adab0977f5687df63cb6c50aaed37797 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 24 Apr 2020 18:06:27 +0100 Subject: [PATCH 03/10] Add additional tests for more types --- regression/cbmc/float-trace/test.c | 10 +++++++++- regression/cbmc/float-trace/test.desc | 22 ++++++++++++++++++++-- 2 files changed, 29 insertions(+), 3 deletions(-) diff --git a/regression/cbmc/float-trace/test.c b/regression/cbmc/float-trace/test.c index a79ea673e06..794fba0a494 100644 --- a/regression/cbmc/float-trace/test.c +++ b/regression/cbmc/float-trace/test.c @@ -1,12 +1,20 @@ #include +#include #include int main() { float zero = 0.0f; float one = 1.0f; - double dzero = 0.0; float complex = 0x1p+37f; + float inf = INFINITY; + float nan = NAN; + + double dzero = 0.0; + double done = 1.0; + double dinf = INFINITY; + double dnan = NAN; + double dcomplex = -5.56268e-309; assert(false); diff --git a/regression/cbmc/float-trace/test.desc b/regression/cbmc/float-trace/test.desc index 51945a3d5ea..ae6a9c465b8 100644 --- a/regression/cbmc/float-trace/test.desc +++ b/regression/cbmc/float-trace/test.desc @@ -4,10 +4,28 @@ test.c ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -0.0f +zero +0.0f +one 1.0f -0.0 +complex 1\.374390e\+11f +inf +\+INFINITY +nan +\+NAN +\+NAN +dzero +0.0 +done +1.0 +dcomplex +-5\.562680e-309 +inf +\+INFINITY +nan +\+NAN +\+NAN -- -- Checks that the binary value is printed for floating point types From b64757e4409ce59f0493ff4fa10511d1856c018b Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 24 Apr 2020 18:12:56 +0100 Subject: [PATCH 04/10] Pull out function for producing the full_lhs_value --- src/goto-programs/xml_goto_trace.cpp | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 9051ee5230c..033fbe7d9af 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -23,6 +23,19 @@ Author: Daniel Kroening #include "printf_formatter.h" #include "xml_expr.h" +xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) +{ + xmlt full_lhs_value{"full_lhs_value"}; + + auto lhs_object = step.get_lhs_object(); + irep_idt identifier = + lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt(); + + if(step.full_lhs_value.is_not_nil()) + full_lhs_value.data = from_expr(ns, identifier, step.full_lhs_value); + return full_lhs_value; +} + void convert( const namespacet &ns, const goto_tracet &goto_trace, @@ -88,16 +101,13 @@ void convert( } } - std::string full_lhs_string, full_lhs_value_string; + std::string full_lhs_string; if(step.full_lhs.is_not_nil()) full_lhs_string = from_expr(ns, identifier, step.full_lhs); - if(step.full_lhs_value.is_not_nil()) - full_lhs_value_string = from_expr(ns, identifier, step.full_lhs_value); - xml_assignment.new_element("full_lhs").data = full_lhs_string; - xml_assignment.new_element("full_lhs_value").data = full_lhs_value_string; + xml_assignment.new_element(full_lhs_value(step, ns)); xml_assignment.set_attribute_bool("hidden", step.hidden); xml_assignment.set_attribute("thread", std::to_string(step.thread_nr)); From e57e194b7e5007ebb7e237bebbad1801cfabb3c9 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 6 May 2020 10:17:57 +0100 Subject: [PATCH 05/10] Tidy up full_lhs_value Applied modern coding standards to pulled out code Co-authored-by: Peter Schrammel --- src/goto-programs/xml_goto_trace.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 033fbe7d9af..1b2d236fdb7 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -27,8 +27,8 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) { xmlt full_lhs_value{"full_lhs_value"}; - auto lhs_object = step.get_lhs_object(); - irep_idt identifier = + const auto &lhs_object = step.get_lhs_object(); + const irep_idt identifier = lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt(); if(step.full_lhs_value.is_not_nil()) From 304c92c3cf0bbe185d14f2919378ecd236b397d8 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 30 Apr 2020 11:22:14 +0100 Subject: [PATCH 06/10] Adapt full_lhs_value to output binary for floating values This is a precise representation of the floats, which can be useful --- src/goto-programs/xml_goto_trace.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 1b2d236fdb7..caf41b1c83d 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -19,10 +19,18 @@ Author: Daniel Kroening #include #include +#include #include "printf_formatter.h" #include "xml_expr.h" +bool full_lhs_value_includes_binary( + const goto_trace_stept &step, + const namespacet &ns) +{ + return can_cast_type(step.full_lhs_value.type()); +} + xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) { xmlt full_lhs_value{"full_lhs_value"}; @@ -33,6 +41,13 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) if(step.full_lhs_value.is_not_nil()) full_lhs_value.data = from_expr(ns, identifier, step.full_lhs_value); + if(full_lhs_value_includes_binary(step, ns)) + { + const auto width = to_floatbv_type(step.full_lhs_value.type()).get_width(); + const auto binary_representation = integer2binary( + bvrep2integer(step.full_lhs_value.get(ID_value), width, false), width); + full_lhs_value.set_attribute("binary", binary_representation); + } return full_lhs_value; } From 4049f155e1c08048f329680da2ee5e11522ebce4 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 30 Apr 2020 12:05:54 +0100 Subject: [PATCH 07/10] Adapt the XSD to include the binary output Also updat the LaTeX and markdown documentation to include the new attribute --- doc/assets/xml_spec.md | 20 ++++++++++++++++++-- doc/assets/xml_spec.tex | 25 +++++++++++++++++++++++-- doc/assets/xml_spec.xsd | 10 +++++++++- 3 files changed, 50 insertions(+), 5 deletions(-) diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md index 05df421b0c9..fe3ca41020e 100644 --- a/doc/assets/xml_spec.md +++ b/doc/assets/xml_spec.md @@ -168,7 +168,9 @@ always present - `full_lhs`: original lhs expression (after dereferencing) -- `full_lhs_value`: a constant with the new value +- `full_lhs_value`: a constant with the new value. + - if the type is a floating point number type, there will be an attribute`binary` + showing its value. **Example**: @@ -181,6 +183,12 @@ always present b -1879048192 + ``` **XSD**: @@ -192,7 +200,15 @@ always present - + + + + + + + + + diff --git a/doc/assets/xml_spec.tex b/doc/assets/xml_spec.tex index 8789c58e962..ea78a67e99c 100644 --- a/doc/assets/xml_spec.tex +++ b/doc/assets/xml_spec.tex @@ -147,9 +147,15 @@ \subsection{Trace Steps in XML} always present \begin{itemize} \item \texttt{full\_lhs}: original lhs expression (after dereferencing) -\item \texttt{full\_lhs\_value}: a constant with the new value +\item \texttt{full\_lhs\_value}: a constant with the new value. + \begin{itemize} + \item if the type is a floating point number type, there will be an attribute + \texttt{binary} showing its value. + \end{itemize} + \end{itemize} + \noindent\textbf{Example}: \begin{minted}{xml} b -1879048192 + \end{minted} \noindent\textbf{XSD}: @@ -170,7 +183,15 @@ \subsection{Trace Steps in XML} - + + + + + + + + + diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd index 1255c524022..dd3c4b7f11b 100644 --- a/doc/assets/xml_spec.xsd +++ b/doc/assets/xml_spec.xsd @@ -40,7 +40,15 @@ - + + + + + + + + + From 4fcbd37fe6dd1e10942ea18dce3f53d4fa5e599b Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 30 Apr 2020 12:16:57 +0100 Subject: [PATCH 08/10] Add folder readme for doc/assets Includes dependencies for builing the xml_spec LaTeX, as well as running the trace through the specification. --- doc/assets/README.md | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 doc/assets/README.md diff --git a/doc/assets/README.md b/doc/assets/README.md new file mode 100644 index 00000000000..7addd9399dd --- /dev/null +++ b/doc/assets/README.md @@ -0,0 +1,27 @@ +This folder contains resources for the documentation. + +# XML Spec + +The folllowing files relate to the specification of the XML trace output when using the `--xml-ui` flag. + +## xml_spec.xsd +The`xml_spec.xsd` file is an XSD specification of the trace. You can validate an +output xml file from CBMC using the following invocation: + +```bash +$ cbmc --xml-ui main.c | \ + xmllint --schema xml_spec.xsd --xpath "cprover/result/goto_trace" - +``` + +## xml_spec.tex + +This is a LaTeX document describing the specification of the trace. It can be compiled to pdf using: + +```bash +$ pdflatex -shell-escape xml_spec.tex +``` + +This requires: + + - texlive-latex-base + - texlive-latex-extra (for minted package) From cdb0b7898d068b23009a28a4b25f68d36fea5bfd Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 30 Apr 2020 12:17:53 +0100 Subject: [PATCH 09/10] Referenced readme in cprover docs The links were not relative, so updated to be relative. Mentioned that you can find more in the readme. --- doc/cprover-manual/cbmc-tutorial.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md index 10a6660523d..2c1ab33510d 100644 --- a/doc/cprover-manual/cbmc-tutorial.md +++ b/doc/cprover-manual/cbmc-tutorial.md @@ -138,9 +138,11 @@ possible output format. ``` 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). +Specification](../assets/xml_spec.tex) +and can be built by `pdflatex -shell-escape xml_spec.tex`. See the [README +](../assets/README.md#xml_spec.tex) for details. + +Alternatively, you can view it in [Markdown](../assets/xml_spec.md). ### Verifying Modules @@ -348,4 +350,3 @@ comes with a small set of definitions, which includes functions such as We also have a [list of interesting applications of CBMC](http://www.cprover.org/cbmc/applications/). - From be6f20fe93bdf7499a988599943809abaf9f6cc4 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 6 May 2020 12:29:27 +0100 Subject: [PATCH 10/10] Rename variables in test to avoid clash on windows complex is renamed in the trace to _complex on Windows. Therefore adapt the test to use a non-reserved name since not important to the test. --- regression/cbmc/float-trace/test.c | 10 +++++----- regression/cbmc/float-trace/test.desc | 14 +++++++------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/regression/cbmc/float-trace/test.c b/regression/cbmc/float-trace/test.c index 794fba0a494..1f09d8b3ab4 100644 --- a/regression/cbmc/float-trace/test.c +++ b/regression/cbmc/float-trace/test.c @@ -4,11 +4,11 @@ int main() { - float zero = 0.0f; - float one = 1.0f; - float complex = 0x1p+37f; - float inf = INFINITY; - float nan = NAN; + float fzero = 0.0f; + float fone = 1.0f; + float fcomplex = 0x1p+37f; + float finf = INFINITY; + float fnan = NAN; double dzero = 0.0; double done = 1.0; diff --git a/regression/cbmc/float-trace/test.desc b/regression/cbmc/float-trace/test.desc index ae6a9c465b8..acfd2834cca 100644 --- a/regression/cbmc/float-trace/test.desc +++ b/regression/cbmc/float-trace/test.desc @@ -4,15 +4,15 @@ test.c ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -zero +fzero 0.0f -one +fone 1.0f -complex +fcomplex 1\.374390e\+11f -inf +finf \+INFINITY -nan +fnan \+NAN \+NAN dzero @@ -21,9 +21,9 @@ VERIFICATION FAILED 1.0 dcomplex -5\.562680e-309 -inf +finf \+INFINITY -nan +fnan \+NAN \+NAN --