Fix simplify_extractbit and simplify_extractbits

With hexadecimal coding of constants we need to use expr2bits/bits2expr to
evaluate extractbits, and just the underlying get_bvrep_bit for extractbit. Also
document these expressions to clarify their semantics with regard to endianness.

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include "arith_tools.h"
 #include "base_type.h"
 #include "bv_arithmetic.h"
+#include "byte_operators.h"
 #include "config.h"
 #include "expr_util.h"
 #include "fixedbv.h"
@@ -845,28 +846,20 @@ bool simplify_exprt::simplify_extractbit(exprt &expr)
 
   const auto index_converted_to_int =
     numeric_cast<mp_integer>(extractbit_expr.index());
-  if(!index_converted_to_int.has_value())
+  if(!index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
+     *index_converted_to_int >= src_bit_width)
   {
     return true;
   }
-  const mp_integer index_as_int = index_converted_to_int.value();
-  if(!extractbit_expr.src().is_constant())
-    return true;
-
-  if(index_as_int < 0 || index_as_int >= src_bit_width)
-    return true;
-
-  const irep_idt &src_value =
-    to_constant_expr(extractbit_expr.src()).get_value();
 
-  std::string src_value_as_string = id2string(src_value);
-
-  if(src_value_as_string.size() != src_bit_width)
+  if(!extractbit_expr.src().is_constant())
     return true;
 
   const bool bit =
-    (src_value_as_string[src_bit_width -
-                         numeric_cast_v<std::size_t>(index_as_int) - 1] == '1');
+    get_bvrep_bit(
+      to_constant_expr(extractbit_expr.src()).get_value(),
+      src_bit_width,
+      numeric_cast_v<std::size_t>(*index_converted_to_int));
 
   expr.make_bool(bit);
 
@@ -1136,18 +1129,19 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr)
 
   if(expr.src().is_constant())
   {
-    const irep_idt &value = to_constant_expr(expr.src()).get_value();
+    const auto svalue = expr2bits(expr.src(), true);
 
-    if(value.size() != *width)
+    if(!svalue.has_value() || svalue->size() != *width)
       return true;
 
-    std::string svalue=id2string(value);
-
-    std::string extracted_value = svalue.substr(
-      numeric_cast_v<std::size_t>(*width - start - 1),
+    std::string extracted_value = svalue->substr(
+      numeric_cast_v<std::size_t>(end),
       numeric_cast_v<std::size_t>(start - end + 1));
 
-    constant_exprt result(extracted_value, expr.type());
+    exprt result = bits2expr(extracted_value, expr.type(), true);
+    if(result.is_nil())
+      return true;
+
     expr.swap(result);
 
     return false;

src/util/std_expr.h

@@ -3085,12 +3085,14 @@ class extractbit_exprt:public binary_predicate_exprt
   {
   }
 
+  /// Extract the \p _index-th least significant bit from \p _src.
   extractbit_exprt(
     const exprt &_src,
     const exprt &_index):binary_predicate_exprt(_src, ID_extractbit, _index)
   {
   }
 
+  /// \copydoc extractbit_exprt(const exprt &, const exprt &)
   extractbit_exprt(
     const exprt &_src,
     const std::size_t _index);
@@ -3161,7 +3163,11 @@ class extractbits_exprt:public exprt
     operands().resize(3);
   }
 
-  // the ordering upper-lower matches the SMT-LIB
+  /// Extract the bits [\p _lower .. \p _upper] from \p _src to produce a result
+  /// of type \p _type. Note that this specifies a closed interval, i.e., both
+  /// bits \p _lower and \p _upper are included. Indices count from the
+  /// least-significant bit, and are not affected by endianness.
+  /// The ordering upper-lower matches what SMT-LIB uses.
   extractbits_exprt(
     const exprt &_src,
     const exprt &_upper,
@@ -3171,6 +3177,8 @@ class extractbits_exprt:public exprt
     add_to_operands(_src, _upper, _lower);
   }
 
+  /// \copydoc extractbits_exprt(const exprt &, const exprt &, const exprt &,
+  /// const typet &)
   extractbits_exprt(
     const exprt &_src,
     const std::size_t _upper,

unit/util/simplify_expr.cpp

@@ -106,3 +106,52 @@ TEST_CASE("expr2bits and bits2expr respect bit order")
     simp.bits2expr(*be, unsignedbv_typet(32), false);
   REQUIRE(deadbeef == should_be_deadbeef2);
 }
+
+TEST_CASE("Simplify extractbit")
+{
+  // this test does require a proper architecture to be set so that byte extract
+  // uses adequate endianness
+  const cmdlinet cmdline;
+  config.set(cmdline);
+
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  // binary: 1101 1110 1010 1101 1011 1110 1110 1111
+  //         ^MSB                               LSB^
+  //              bit23^                  bit4^
+  // extractbit and extractbits use offsets with respect to the
+  // least-significant bit, endianess does not impact them
+  const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32));
+
+  exprt eb1 = extractbit_exprt(deadbeef, 4);
+  bool unmodified = simplify(eb1, ns);
+
+  REQUIRE(!unmodified);
+  REQUIRE(eb1 == false_exprt());
+
+  exprt eb2 = extractbit_exprt(deadbeef, 23);
+  unmodified = simplify(eb2, ns);
+
+  REQUIRE(!unmodified);
+  REQUIRE(eb2 == true_exprt());
+}
+
+TEST_CASE("Simplify extractbits")
+{
+  // this test does require a proper architecture to be set so that byte extract
+  // uses adequate endianness
+  const cmdlinet cmdline;
+  config.set(cmdline);
+
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32));
+
+  exprt eb = extractbits_exprt(deadbeef, 15, 8, unsignedbv_typet(8));
+  bool unmodified = simplify(eb, ns);
+
+  REQUIRE(!unmodified);
+  REQUIRE(eb == from_integer(0xbe, unsignedbv_typet(8)));
+}