Merge pull request #5425 from thomasspriggs/tas/bit_vector_binary

 Add binary representation to all bitvector values in the xml trace

Author: hannes-steffenhagen-diffblue

doc/assets/xml_spec.md

@@ -169,8 +169,10 @@ always present
 -   `full_lhs`: original lhs expression (after dereferencing)
 
 -   `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.
+     - If the type of data can be represented as a fixed width sequence of bits
+       then, there will be an attribute `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.
 
 **Example**:
 
@@ -181,7 +183,7 @@ always present
   <location .. />
   <type>signed int</type>
   <full_lhs>b</full_lhs>
-  <full_lhs_value>-1879048192</full_lhs_value>
+  <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 file="main.i" function="main" line="3" working-directory="/home/tkiley/workspace/cbmc/regression/cbmc/Float24"/>

doc/assets/xml_spec.tex

@@ -149,8 +149,10 @@ \subsection{Trace Steps in XML}
 \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 is a floating point number type, there will be an attribute
-    \texttt{binary} showing its value.
+    \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}
@@ -164,7 +166,7 @@ \subsection{Trace Steps in XML}
   <location .. />
   <type>signed int</type>
   <full_lhs>b</full_lhs>
-  <full_lhs_value>-1879048192</full_lhs_value>
+  <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 ../>

regression/cbmc/integral-trace/test.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+#include <inttypes.h>
+#include <math.h>
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdlib.h>
+
+int main()
+{
+  int8_t i1 = 2;
+  int16_t i2 = 3;
+  int32_t i3 = 4;
+  int64_t i4 = 5;
+
+  int8_t in1 = -2;
+  int16_t in2 = -3;
+  int32_t in3 = -4;
+  int64_t in4 = -5;
+
+  uint8_t u8 = 'a';
+  uint16_t u16 = 8;
+  uint32_t u32 = 16;
+  uint64_t u64 = 32;
+
+  void *ptr = malloc(1);
+
+  assert(false);
+
+  return 0;
+}

regression/cbmc/integral-trace/test.desc

@@ -0,0 +1,22 @@
+CORE
+test.c
+--trace --xml-ui
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+<full_lhs>u8</full_lhs>\s*<full_lhs_value binary="01100001">97</full_lhs_value>
+<full_lhs>u16</full_lhs>\s*<full_lhs_value binary="0{12}1000">8</full_lhs_value>
+<full_lhs>u32</full_lhs>\s*<full_lhs_value binary="0{27}10000">16ul?</full_lhs_value>
+<full_lhs>u64</full_lhs>\s*<full_lhs_value binary="0{58}100000">32ull?</full_lhs_value>
+<full_lhs>i1</full_lhs>\s*<full_lhs_value binary="0{6}10">2</full_lhs_value>
+<full_lhs>i2</full_lhs>\s*<full_lhs_value binary="0{14}11">3</full_lhs_value>
+<full_lhs>i3</full_lhs>\s*<full_lhs_value binary="0{29}100">4</full_lhs_value>
+<full_lhs>i4</full_lhs>\s*<full_lhs_value binary="0{61}101">5ll?</full_lhs_value>
+<full_lhs>in1</full_lhs>\s*<full_lhs_value binary="1{6}10">-2</full_lhs_value>
+<full_lhs>in2</full_lhs>\s*<full_lhs_value binary="1{14}01">-3</full_lhs_value>
+<full_lhs>in3</full_lhs>\s*<full_lhs_value binary="1{29}100">-4</full_lhs_value>
+<full_lhs>in4</full_lhs>\s*<full_lhs_value binary="1{61}011">-5ll?</full_lhs_value>
+--
+--
+Checks that the binary value is printed for integral types.

regression/cbmc/xml-trace/test.desc

@@ -8,7 +8,7 @@ VERIFICATION FAILED
 <location file=".*" function="test" line="\d+" working-directory=".*"/>
 <type>union myunion</type>
 <full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>
-<full_lhs_value>\d+ll?</full_lhs_value>
+<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>
 <value>\{ \.i=\d+ll? \}</value>
 <value_expression>
 <union>

src/goto-programs/xml_goto_trace.cpp

@@ -25,31 +25,34 @@ Author: Daniel Kroening
 #include "structured_trace_util.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"};
+  xmlt value_xml{"full_lhs_value"};
+
+  const exprt &value = step.full_lhs_value;
+  if(value.is_nil())
+    return value_xml;
 
   const auto &lhs_object = step.get_lhs_object();
   const irep_idt identifier =
     lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
+  value_xml.data = from_expr(ns, identifier, value);
 
-  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 &bv_type = type_try_dynamic_cast<bitvector_typet>(value.type());
+  const auto &constant = expr_try_dynamic_cast<constant_exprt>(value);
+  if(bv_type && constant)
   {
-    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);
+    const auto width = bv_type->get_width();
+    // It is fine to pass `false` into the `is_signed` parameter, even for
+    // signed values, because the subsequent conversion to binary will result
+    // in the same value either way. E.g. if the value is `-1` for a signed 8
+    // bit value, this will convert to `255` which is `11111111` in binary,
+    // which is the desired result.
+    const auto binary_representation =
+      integer2binary(bvrep2integer(constant->get_value(), width, false), width);
+    value_xml.set_attribute("binary", binary_representation);
   }
-  return full_lhs_value;
+  return value_xml;
 }
 
 void convert(