Fix simplification of bit counting for big endian architectures

We need to start searching from the least or most significant bit, the
position of which depends on endianness.

Author: tautschnig

regression/cbmc/__builtin_clz-01/big-endian.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --big-endian
+^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/__builtin_ctz-01/big-endian.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--bounds-check --big-endian
+^\[main.bit_count.\d+\] line 46 count trailing zeros is undefined for value zero in __builtin_ctz\(0u\): FAILURE$
+^\[main.assertion.2\] line 47 count trailing zeros of 0 is bit width: SUCCESS$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/__builtin_ffs-01/big-endian.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --big-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/util/simplify_expr.cpp

@@ -150,24 +150,24 @@ simplify_exprt::simplify_popcount(const popcount_exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_clz(const count_leading_zeros_exprt &expr)
 {
-  const auto const_bits_opt = expr2bits(
-    expr.op(),
-    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
-    ns);
+  const bool is_little_endian =
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN;
+
+  const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
 
   if(!const_bits_opt.has_value())
     return unchanged(expr);
 
-  // expr2bits generates a bit string starting with the least-significant bit
-  std::size_t n_leading_zeros = const_bits_opt->rfind('1');
+  std::size_t n_leading_zeros =
+    is_little_endian ? const_bits_opt->rfind('1') : const_bits_opt->find('1');
   if(n_leading_zeros == std::string::npos)
   {
     if(!expr.zero_permitted())
       return unchanged(expr);
 
     n_leading_zeros = const_bits_opt->size();
   }
-  else
+  else if(is_little_endian)
     n_leading_zeros = const_bits_opt->size() - n_leading_zeros - 1;
 
   return from_integer(n_leading_zeros, expr.type());
@@ -176,44 +176,48 @@ simplify_exprt::simplify_clz(const count_leading_zeros_exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_ctz(const count_trailing_zeros_exprt &expr)
 {
-  const auto const_bits_opt = expr2bits(
-    expr.op(),
-    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
-    ns);
+  const bool is_little_endian =
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN;
+
+  const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
 
   if(!const_bits_opt.has_value())
     return unchanged(expr);
 
-  // expr2bits generates a bit string starting with the least-significant bit
-  std::size_t n_trailing_zeros = const_bits_opt->find('1');
+  std::size_t n_trailing_zeros =
+    is_little_endian ? const_bits_opt->find('1') : const_bits_opt->rfind('1');
   if(n_trailing_zeros == std::string::npos)
   {
     if(!expr.zero_permitted())
       return unchanged(expr);
 
     n_trailing_zeros = const_bits_opt->size();
   }
+  else if(!is_little_endian)
+    n_trailing_zeros = const_bits_opt->size() - n_trailing_zeros - 1;
 
   return from_integer(n_trailing_zeros, expr.type());
 }
 
 simplify_exprt::resultt<>
 simplify_exprt::simplify_ffs(const find_first_set_exprt &expr)
 {
-  const auto const_bits_opt = expr2bits(
-    expr.op(),
-    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
-    ns);
+  const bool is_little_endian =
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN;
+
+  const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
 
   if(!const_bits_opt.has_value())
     return unchanged(expr);
 
-  // expr2bits generates a bit string starting with the least-significant bit
-  std::size_t first_one_bit = const_bits_opt->find('1');
+  std::size_t first_one_bit =
+    is_little_endian ? const_bits_opt->find('1') : const_bits_opt->rfind('1');
   if(first_one_bit == std::string::npos)
     first_one_bit = 0;
-  else
+  else if(is_little_endian)
     ++first_one_bit;
+  else
+    first_one_bit = const_bits_opt->size() - first_one_bit;
 
   return from_integer(first_one_bit, expr.type());
 }