From e24410373f8a54f3efe3ec71fd191949c13e917c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 1 Mar 2022 17:59:05 +0000
Subject: [PATCH] Fix count-trailing-zeros lowering for value zero

The previous implementation would produce an off-by-one error in case of
an argument 0, which count_trailing_zeros is defined for (even when
__builtin_ctz is undefined in that case).

Fixes: #6702
---
 regression/cbmc/__builtin_ctz-01/main.c    |  4 +++-
 regression/cbmc/__builtin_ctz-01/test.desc |  1 +
 src/util/bitvector_expr.cpp                | 20 ++++++++------------
 3 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/regression/cbmc/__builtin_ctz-01/main.c b/regression/cbmc/__builtin_ctz-01/main.c
index 0eb5521f979..c339b27b63c 100644
--- a/regression/cbmc/__builtin_ctz-01/main.c
+++ b/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;
 }
diff --git a/regression/cbmc/__builtin_ctz-01/test.desc b/regression/cbmc/__builtin_ctz-01/test.desc
index e8bed1dae70..fbbd69442a3 100644
--- a/regression/cbmc/__builtin_ctz-01/test.desc
+++ b/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$
diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp
index 354c06bfaea..ddc7296f943 100644
--- a/src/util/bitvector_expr.cpp
+++ b/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