changed output of formatNumberReadable so that it shows powers of two and one-less-than powers of two in a more compact format

Author: Ruko97

Changelog.md

@@ -16,6 +16,8 @@ Compiler Features:
 Bugfixes:
  * Yul Optimizer: Hash hex and decimal literals according to their value instead of their representation, improving the detection of equivalent functions.
  * Solidity Upgrade Tool ``solidity-upgrade``: Fix the tool returning success code on uncaught exceptions.
+ * SMTChecker: Fix display error for negative integers that are one more than powers of two.
+ * SMTChecker: Improved readability for large integers that are powers of two or almost powers of two in error messages.
 
 
 ### 0.8.17 (2022-09-08)

libsolutil/CMakeLists.txt

@@ -43,7 +43,7 @@ set(sources
 )
 
 add_library(solutil ${sources})
-target_link_libraries(solutil PUBLIC jsoncpp Boost::boost Boost::filesystem Boost::system range-v3)
+target_link_libraries(solutil PUBLIC jsoncpp Boost::boost Boost::filesystem Boost::system range-v3 fmt::fmt-header-only)
 target_include_directories(solutil PUBLIC "${CMAKE_SOURCE_DIR}")
 add_dependencies(solutil solidity_BuildInfo.h)
 

libsolutil/StringUtils.cpp

@@ -27,6 +27,7 @@
 #include <vector>
 
 using namespace std;
+using namespace solidity;
 using namespace solidity::util;
 
 bool solidity::util::stringWithinDistance(string const& _str1, string const& _str2, size_t _maxDistance, size_t _lenThreshold)
@@ -113,3 +114,80 @@ string solidity::util::suffixedVariableNameList(string const& _baseName, size_t
 	}
 	return result;
 }
+
+namespace
+{
+
+/// Try to format as N * 2**x
+optional<string> tryFormatPowerOfTwo(bigint const& _value)
+{
+	bigint prefix = _value;
+
+	// when multiple trailing zero bytes, format as N * 2**x
+	int i = 0;
+	for (; (prefix & 0xff) == 0; prefix >>= 8)
+		++i;
+	if (i <= 2)
+		return nullopt;
+
+	// 0x100 yields 2**8 (N is 1 and redundant)
+	if (prefix == 1)
+		return {fmt::format("2**{}", i * 8)};
+	else if ((prefix & (prefix - 1)) == 0)
+	{
+		int j = 0;
+		for (; (prefix & 0x1) == 0; prefix >>= 1)
+			j++;
+		return {fmt::format("2**{}", i * 8 + j)};
+	}
+	else
+		return {fmt::format(
+			"{} * 2**{}",
+			toHex(toCompactBigEndian(prefix), HexPrefix::Add, HexCase::Mixed),
+			i * 8
+		)};
+}
+
+}
+
+string solidity::util::formatNumberReadable(bigint const& _value, bool _useTruncation)
+{
+	bool const isNegative = _value < 0;
+	bigint const absValue = isNegative ? (bigint(-1) * _value) : bigint(_value);
+	string const sign = isNegative ? "-" : "";
+
+	// smaller numbers return as decimal
+	if (absValue <= 0x1000000)
+		return sign + absValue.str();
+
+	if (auto result = tryFormatPowerOfTwo(absValue))
+		return {sign + *result};
+	else if (auto result = tryFormatPowerOfTwo(absValue + 1))
+		return {sign + *result + (isNegative ? " + 1" : " - 1")};
+
+	string str = toHex(toCompactBigEndian(absValue), HexPrefix::Add, HexCase::Mixed);
+
+	if (_useTruncation)
+	{
+		// return as interior-truncated hex.
+		size_t len = str.size();
+
+		if (len < 24)
+			return sign + str;
+
+		size_t const initialChars = 6;
+		size_t const finalChars = 4;
+		size_t numSkipped = len - initialChars - finalChars;
+
+		return fmt::format(
+			"{}{}...{{+{} more}}...{}",
+			sign,
+			str.substr(0, initialChars),
+			numSkipped,
+			str.substr(len-finalChars, len)
+		);
+	}
+
+	return sign + str;
+}
+

libsolutil/StringUtils.h

@@ -27,6 +27,8 @@
 #include <libsolutil/CommonData.h>
 #include <libsolutil/Numeric.h>
 
+#include <fmt/format.h>
+
 #include <algorithm>
 #include <limits>
 #include <locale>
@@ -101,110 +103,17 @@ std::string joinHumanReadablePrefixed
 		return _separator + joinHumanReadable(_list, _separator, _lastSeparator);
 }
 
-/// Same as @ref formatNumberReadable but only for unsigned numbers
-template <class T>
-inline std::string formatUnsignedNumberReadable (
-	T const& _value,
-	bool _useTruncation = false
-)
-{
-	static_assert(
-		std::is_same<bigint, T>::value || !std::numeric_limits<T>::is_signed,
-		"only unsigned types or bigint supported"
-	); //bigint does not carry sign bit on shift
-
-	// smaller numbers return as decimal
-	if (_value <= 0x1000000)
-		return _value.str();
-
-	HexCase hexcase = HexCase::Mixed;
-	HexPrefix prefix = HexPrefix::Add;
-
-	// when multiple trailing zero bytes, format as N * 2**x
-	int i = 0;
-	T v = _value;
-	for (; (v & 0xff) == 0; v >>= 8)
-		++i;
-	if (i > 2)
-	{
-		// 0x100 yields 2**8 (N is 1 and redundant)
-		if (v == 1)
-			return "2**" + std::to_string(i * 8);
-		return toHex(toCompactBigEndian(v), prefix, hexcase) +
-			" * 2**" +
-			std::to_string(i * 8);
-	}
-
-	// when multiple trailing FF bytes, format as N * 2**x - 1
-	i = 0;
-	for (v = _value; (v & 0xff) == 0xff; v >>= 8)
-		++i;
-	if (i > 2)
-	{
-		// 0xFF yields 2**8 - 1 (v is 0 in that case)
-		if (v == 0)
-			return "2**" + std::to_string(i * 8) + " - 1";
-		return toHex(toCompactBigEndian(T(v + 1)), prefix, hexcase) +
-			" * 2**" + std::to_string(i * 8) +
-			" - 1";
-	}
-
-	std::string str = toHex(toCompactBigEndian(_value), prefix, hexcase);
-	if (_useTruncation)
-	{
-		// return as interior-truncated hex.
-		size_t len = str.size();
-
-		if (len < 24)
-			return str;
-
-		size_t const initialChars = (prefix == HexPrefix::Add) ? 6 : 4;
-		size_t const finalChars = 4;
-		size_t numSkipped = len - initialChars - finalChars;
-
-		return str.substr(0, initialChars) +
-			"...{+" +
-			std::to_string(numSkipped) +
-			" more}..." +
-			str.substr(len-finalChars, len);
-	}
-
-	// otherwise, show whole value.
-	return str;
-}
-
 /// Formats large numbers to be easily readable by humans.
 /// Returns decimal representation for smaller numbers; hex for large numbers.
 /// "Special" numbers, powers-of-two and powers-of-two minus 1, are returned in
 /// formulaic form like 0x01 * 2**24 - 1.
-/// @a T can be any integer variable, will typically be u160, u256 or bigint.
+/// @a T can be any integer type, will typically be u160, u256 or bigint.
 /// @param _value to be formatted
 /// @param _useTruncation if true, internal truncation is also applied,
 /// like  0x5555...{+56 more}...5555
-/// @example formatNumberReadable((u256)0x7ffffff) = "0x08 * 2**24"
-/// @example formatNumberReadable(-57896044618658097711785492504343953926634992332820282019728792003956564819968) = -0x80 * 2**248
-template <class T>
-inline std::string formatNumberReadable(
-	T const& _value,
-	bool _useTruncation = false
-)
-{
-	static_assert(
-		std::numeric_limits<T>::is_integer,
-		"only integer numbers are supported"
-	);
-
-	if (_value >= 0)
-	{
-		bigint const _v = bigint(_value);
-		return formatUnsignedNumberReadable(_v, _useTruncation);
-	}
-	else
-	{
-		bigint const _abs_value = bigint(-1) * _value;
-		return "-" + formatUnsignedNumberReadable(_abs_value, _useTruncation);
-	}
-}
+/// @example formatNumberReadable((u256)0x7ffffff) = "2**27 - 1"
+/// @example formatNumberReadable(-57896044618658097711785492504343953926634992332820282019728792003956564819968) = -2**255
+std::string formatNumberReadable(bigint const& _value, bool _useTruncation = false);
 
 /// Safely converts an unsigned integer as string into an unsigned int type.
 ///

test/libsolidity/smtCheckerTests/operators/division_3.sol

@@ -7,4 +7,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (95-100): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))
+// Warning 4984: (95-100): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))

test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol

@@ -7,5 +7,5 @@ contract C  {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
+// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
 // Warning 4281: (77-82): CHC: Division by zero happens here.

test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol

@@ -8,4 +8,4 @@ contract C  {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
+// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))

test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol

@@ -8,5 +8,5 @@ contract C  {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 3944: (78-83): CHC: Underflow (resulting value less than -0x80 * 2**248) happens here.
-// Warning 4984: (78-83): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
+// Warning 3944: (78-83): CHC: Underflow (resulting value less than -2**255) happens here.
+// Warning 4984: (78-83): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.

test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol

@@ -7,5 +7,5 @@ contract C  {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 3944: (77-82): CHC: Underflow (resulting value less than -0x80 * 2**248) happens here.
-// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
+// Warning 3944: (77-82): CHC: Underflow (resulting value less than -2**255) happens here.
+// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.

test/libsolidity/smtCheckerTests/overflow/signed_sub_overflow.sol

@@ -7,5 +7,5 @@ contract C  {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 3944: (77-82): CHC: Underflow (resulting value less than -0x80 * 2**248) happens here.
-// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
+// Warning 3944: (77-82): CHC: Underflow (resulting value less than -2**255) happens here.
+// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.