Merge pull request #5322 from thk123/print-binary-values-of-floats

Print binary values of floats

Author: Thomas Kiley

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)

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
   <full_lhs>b</full_lhs>
   <full_lhs_value>-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 file="main.i" function="main" line="3" working-directory="/home/tkiley/workspace/cbmc/regression/cbmc/Float24"/>
+  <type>double</type>
+  <full_lhs>d</full_lhs>
+  <full_lhs_value binary="0100000000010100011001100110011001100110011001100110011001100110">5.1</full_lhs_value>
+</assignment>
 ```
 
 **XSD**:
@@ -192,7 +200,15 @@ always present
       <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" type="xs:int"></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>

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}
 <assignment assignment_type="state" base_name="b" display_name="main::1::b"
@@ -160,6 +166,13 @@ \subsection{Trace Steps in XML}
   <full_lhs>b</full_lhs>
   <full_lhs_value>-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}:
@@ -170,7 +183,15 @@ \subsection{Trace Steps in XML}
       <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" type="xs:int"></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>

doc/assets/xml_spec.xsd

@@ -40,7 +40,15 @@
       <xs:element ref="location" minOccurs="0"/>
       <xs:element name="type" type="xs:string" minOccurs="0"/>
       <xs:element name="full_lhs" type="xs:string"/>
-      <xs:element name="full_lhs_value" type="xs:string"/>
+      <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"/>

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/).
-

regression/cbmc/Float24/test.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-<full_lhs_value>5\.1</full_lhs_value>
+<full_lhs_value binary="[01]+">5\.1</full_lhs_value>
 --
 ^warning: ignoring
-<full_lhs_value>5\.1l</full_lhs_value>
+<full_lhs_value binary="[01]+">5\.1l</full_lhs_value>

regression/cbmc/float-trace/test.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+#include <math.h>
+#include <stdbool.h>
+
+int main()
+{
+  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;
+  double dinf = INFINITY;
+  double dnan = NAN;
+  double dcomplex = -5.56268e-309;
+
+  assert(false);
+
+  return 0;
+}
+
+void test(float value)
+{
+  assert(value == 1.0f);
+  assert(value == 0.0f);
+}

regression/cbmc/float-trace/test.desc

@@ -0,0 +1,32 @@
+CORE
+test.c
+--trace --xml-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+<full_lhs>fzero</full_lhs>
+<full_lhs_value binary="0{32}">0.0f</full_lhs_value>
+<full_lhs>fone</full_lhs>
+<full_lhs_value binary="00111111100000000000000000000000">1.0f</full_lhs_value>
+<full_lhs>fcomplex</full_lhs>
+<full_lhs_value binary="01010010000000000000000000000000">1\.374390e\+11f</full_lhs_value>
+<full_lhs>finf</full_lhs>
+<full_lhs_value binary="01{8}0{23}">\+INFINITY</full_lhs_value>
+<full_lhs>fnan</full_lhs>
+<full_lhs_value binary="01{8}[01]*1[01]*">\+NAN</full_lhs_value>
+<full_lhs_value binary="[01]{32}">\+NAN</full_lhs_value>
+<full_lhs>dzero</full_lhs>
+<full_lhs_value binary="0{64}">0.0</full_lhs_value>
+<full_lhs>done</full_lhs>
+<full_lhs_value binary="001{10}0{52}">1.0</full_lhs_value>
+<full_lhs>dcomplex</full_lhs>
+<full_lhs_value binary="1000000000000011111111111111111111000111111100100110011101110111">-5\.562680e-309</full_lhs_value>
+<full_lhs>finf</full_lhs>
+<full_lhs_value binary="01{11}0{52}">\+INFINITY</full_lhs_value>
+<full_lhs>fnan</full_lhs>
+<full_lhs_value binary="01{11}[01]*1[01]*">\+NAN</full_lhs_value>
+<full_lhs_value binary="[01]{64}">\+NAN</full_lhs_value>
+--
+--
+Checks that the binary value is printed for floating point types
+point types

src/goto-programs/xml_goto_trace.cpp

@@ -19,10 +19,38 @@ Author: Daniel Kroening
 #include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
+#include <util/arith_tools.h>
 
 #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<floatbv_typet>(step.full_lhs_value.type());
+}
+
+xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
+{
+  xmlt full_lhs_value{"full_lhs_value"};
+
+  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())
+    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;
+}
+
 void convert(
   const namespacet &ns,
   const goto_tracet &goto_trace,
@@ -88,16 +116,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));