Merge pull request #6703 from tautschnig/bugfixes/6702-ctz

Fix count-trailing-zeros lowering for value zero

Author: tautschnig

regression/cbmc/__builtin_ctz-01/main.c

@@ -43,7 +43,9 @@ int main()
       [((unsigned)((u & -u) * 0x077CB531U)) >> 27] == __builtin_ctz(u));
 
   // a failing assertion should be generated as __builtin_ctz is undefined for 0
-  __builtin_ctz(0U);
+  int r = __builtin_ctz(0U);
+  __CPROVER_assert(
+    r == sizeof(unsigned) * 8, "count trailing zeros of 0 is bit width");
 
   return 0;
 }

regression/cbmc/__builtin_ctz-01/test.desc

@@ -2,6 +2,7 @@ CORE
 main.c
 --bounds-check
 ^\[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$

src/util/bitvector_expr.cpp

@@ -129,18 +129,14 @@ exprt count_leading_zeros_exprt::lower() const
 exprt count_trailing_zeros_exprt::lower() const
 {
   exprt x = op();
-  const auto int_width = to_bitvector_type(x.type()).get_width();
-  CHECK_RETURN(int_width >= 1);
-
-  // popcount(x ^ ((unsigned)x - 1)) - 1
-  const unsignedbv_typet ut{int_width};
-  minus_exprt minus_one{typecast_exprt::conditional_cast(x, ut),
-                        from_integer(1, ut)};
-  popcount_exprt popcount{
-    bitxor_exprt{x, typecast_exprt::conditional_cast(minus_one, x.type())}};
-  minus_exprt result{popcount.lower(), from_integer(1, x.type())};
-
-  return typecast_exprt::conditional_cast(result, type());
+
+  // popcount(~(x | (~x + 1)))
+  // compute -x using two's complement
+  plus_exprt minus_x{bitnot_exprt{x}, from_integer(1, x.type())};
+  bitor_exprt x_or_minus_x{x, std::move(minus_x)};
+  popcount_exprt popcount{bitnot_exprt{std::move(x_or_minus_x)}};
+
+  return typecast_exprt::conditional_cast(popcount.lower(), type());
 }
 
 exprt bitreverse_exprt::lower() const