Add binary representation to all bitvector values in the xml trace

The purpose of this is to provide a consistent interface for getting the
values of bitvector-ed types out of the trace.

An existing test is updated in this commit in order for the existing
to test to match new functionality and so that every commit still passes
all tests.

There are instances when running with `--cprover-smt2` where the type of
the expression is `bitvector_typet`, but the expression is not a
`constant_exprt`. By removing the printing in this case we can avoid
breaking the partial functionality available with the `--cprover-smt2`
option.

Author: thomasspriggs

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,13 +25,6 @@ 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"};
@@ -40,13 +33,19 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
   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))
+  if(step.full_lhs_value.is_nil())
+    return full_lhs_value;
+  full_lhs_value.data = from_expr(ns, identifier, step.full_lhs_value);
+
+  const auto &bv_type =
+    type_try_dynamic_cast<bitvector_typet>(step.full_lhs_value.type());
+  const auto &constant =
+    expr_try_dynamic_cast<constant_exprt>(step.full_lhs_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);
+    const auto width = bv_type->get_width();
+    const auto binary_representation =
+      integer2binary(bvrep2integer(constant->get_value(), width, false), width);
     full_lhs_value.set_attribute("binary", binary_representation);
   }
   return full_lhs_value;