add a 'readable' format for large hex values

11 files changed, 264 insertions, 17 deletions

diff --git a/libdevcore/CommonData.h b/libdevcore/CommonData.h
index fedd3af2..4118907c 100644
--- a/libdevcore/CommonData.h
+++ b/libdevcore/CommonData.h
@@ -50,16 +50,35 @@ enum class HexPrefix
 	DontAdd = 0,
 	Add = 1,
 };
+
+enum class HexCase
+{
+	Lower = 0,
+	Upper = 1,
+	Mixed = 2,
+};
+
 /// Convert a series of bytes to the corresponding string of hex duplets.
 /// @param _w specifies the width of the first of the elements. Defaults to two - enough to represent a byte.
 /// @example toHex("A\x69") == "4169"
 template <class T>
-std::string toHex(T const& _data, int _w = 2, HexPrefix _prefix = HexPrefix::DontAdd)
+std::string toHex(T const& _data, int _w = 2, HexPrefix _prefix = HexPrefix::DontAdd, HexCase _case = HexCase::Lower)
 {
 	std::ostringstream ret;
-	unsigned ii = 0;
-	for (auto i: _data)
-		ret << std::hex << std::setfill('0') << std::setw(ii++ ? 2 : _w) << (int)(typename std::make_unsigned<decltype(i)>::type)i;
+	int rix = _data.size() - 1;
+	for (auto datum: _data)
+	{
+		// switch hex case every four hexchars
+		auto hexcase = std::nouppercase;
+		if (_case == HexCase::Upper)
+			hexcase = std::uppercase;
+		else if (_case == HexCase::Mixed)
+			hexcase = (rix-- & 2) == 0 ? std::nouppercase : std::uppercase;
+
+		ret << std::hex << hexcase << std::setfill('0') << std::setw(_w)
+			<< +static_cast<typename std::make_unsigned<decltype(datum)>::type>(datum);
+	}
+
 	return (_prefix == HexPrefix::Add) ? "0x" + ret.str() : ret.str();
 }
 
diff --git a/libdevcore/StringUtils.h b/libdevcore/StringUtils.h
index b02b9d12..43aa4bd1 100644
--- a/libdevcore/StringUtils.h
+++ b/libdevcore/StringUtils.h
@@ -26,6 +26,8 @@
 #include <string>
 #include <vector>
 
+#include <libdevcore/CommonData.h>
+
 namespace dev
 {
 
@@ -72,4 +74,84 @@ std::string joinHumanReadable
 	return result;
 }
 
+/// 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 will typically by unsigned, u160, u256 or bigint.
+/// @param _value to be formatted
+/// @param _useTruncation if true, internal truncation is also applied,
+/// like  0x5555...{+56 more}...5555
+/// @example formatNumber((u256)0x7ffffff)
+template <class T>
+inline std::string formatNumberReadable(
+	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), 2, 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)), 2, prefix, hexcase) +
+			" * 2**" + std::to_string(i * 8) +
+			" - 1";
+	}
+
+	std::string str = toHex(toCompactBigEndian(_value), 2, prefix, hexcase);
+	if (_useTruncation)
+	{
+		// return as interior-truncated hex.
+		int len = str.size();
+
+		if (len < 24)
+			return str;
+
+		const int initialChars = (prefix == HexPrefix::Add) ? 6 : 4;
+		const int finalChars = 4;
+		int 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;
+}
+
 }
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 0c2af44b..17dc11ac 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -24,6 +24,8 @@
 
 #include <liblangutil/ErrorReporter.h>
 
+#include <libdevcore/StringUtils.h>
+
 #include <boost/range/adaptor/map.hpp>
 #include <boost/algorithm/string/replace.hpp>
 
@@ -300,14 +302,14 @@ void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _
 	checkCondition(
 		_value < minValue(_type),
 		_location,
-		"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
+		"Underflow (resulting value less than " + formatNumberReadable(_type.minValue()) + ")",
 		"<result>",
 		&_value
 	);
 	checkCondition(
 		_value > maxValue(_type),
 		_location,
-		"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
+		"Overflow (resulting value larger than " + formatNumberReadable(_type.maxValue()) + ")",
 		"<result>",
 		&_value
 	);
@@ -963,7 +965,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _exp
 		try
 		{
 			// Parse and re-format nicely
-			value = formatNumber(bigint(value));
+			value = formatNumberReadable(bigint(value));
 		}
 		catch (...) { }
 	}
diff --git a/test/libdevcore/CommonData.cpp b/test/libdevcore/CommonData.cpp
new file mode 100644
index 00000000..2020ddb0
--- /dev/null
+++ b/test/libdevcore/CommonData.cpp
@@ -0,0 +1,87 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+/**
+ * Unit tests for the StringUtils routines.
+ */
+
+
+#include <libdevcore/CommonData.h>
+#include <libdevcore/FixedHash.h>
+#include <libsolidity/ast/Types.h> // for IntegerType
+
+#include <test/Options.h>
+
+using namespace std;
+using namespace dev::solidity;
+
+namespace dev
+{
+namespace test
+{
+
+BOOST_AUTO_TEST_SUITE(CommonData)
+
+BOOST_AUTO_TEST_CASE(test_to_hex)
+{
+	BOOST_CHECK_EQUAL(toHex(fromHex("FF"), 2, HexPrefix::DontAdd,  HexCase::Lower), "ff");
+}
+
+BOOST_AUTO_TEST_CASE(test_format_number)
+{
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x8000000)), "0x08000000");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x80000000)), "0x80000000");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x800000000)), "0x0800000000");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x8000000000)), "0x8000000000");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x80000000000)), "0x080000000000");
+
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x7ffffff)), "0x07ffffff");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x7fffffff)), "0x7fffffff");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x7ffffffff)), "0x07ffffffff");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x7fffffffff)), "0x7fffffffff");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x7ffffffffff)), "0x07ffffffffff");
+
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x88000000)), "0x88000000");
+	BOOST_CHECK_EQUAL(formatNumber(u256(0x8888888888000000)), "0x8888888888000000");
+
+	u256 b = 0;
+	for (int i = 0; i < 32; i++)
+	{
+		b <<= 8;
+		b |= 0x55;
+	}
+	u256 c = u256(FixedHash<32>(
+		fromHex("0xabcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789")
+	));
+	u256 d = u256(0xAAAAaaaaAAAAaaaa) << 192 |
+		u256(0xFFFFffffFFFFffff) << 128 |
+		u256(0xFFFFffffFFFFffff) << 64 |
+		u256(0xFFFFffffFFFFffff);
+	BOOST_CHECK_EQUAL(formatNumber(b), "0x5555555555555555555555555555555555555555555555555555555555555555");
+	BOOST_CHECK_EQUAL(formatNumber(c), "0xabcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789");
+	BOOST_CHECK_EQUAL(formatNumber(d), "0xaaaaaaaaaaaaaaaaffffffffffffffffffffffffffffffffffffffffffffffff");
+
+	BOOST_CHECK_EQUAL(formatNumber(IntegerType(256).minValue()), "0");
+	BOOST_CHECK_EQUAL(
+		formatNumber(IntegerType(256).maxValue()),
+		"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff"
+	);
+}
+
+BOOST_AUTO_TEST_SUITE_END()
+
+}
+}
diff --git a/test/libdevcore/StringUtils.cpp b/test/libdevcore/StringUtils.cpp
index 76c11b82..0baeb964 100644
--- a/test/libdevcore/StringUtils.cpp
+++ b/test/libdevcore/StringUtils.cpp
@@ -18,8 +18,12 @@
  * Unit tests for the StringUtils routines.
  */
 
+#include <libdevcore/CommonData.h>
+#include <libdevcore/FixedHash.h>
 #include <libdevcore/StringUtils.h>
 
+#include <libsolidity/ast/Types.h>  // for IntegerType
+
 #include <test/Options.h>
 
 using namespace std;
@@ -100,6 +104,59 @@ BOOST_AUTO_TEST_CASE(test_human_readable_join)
 	BOOST_CHECK_EQUAL(joinHumanReadable(vector<string>({"a", "b", "c"}), "; ", " or "), "a; b or c");
 }
 
+BOOST_AUTO_TEST_CASE(test_format_number_readable)
+{
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x8000000)), "0x08 * 2**24");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x80000000)), "0x80 * 2**24");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x800000000)), "0x08 * 2**32");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x8000000000)), "0x80 * 2**32");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x80000000000)), "0x08 * 2**40");
+
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x7ffffff)), "0x08 * 2**24 - 1");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x7fffffff)), "0x80 * 2**24 - 1");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x7ffffffff)), "0x08 * 2**32 - 1");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x7fffffffff)), "0x80 * 2**32 - 1");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x7ffffffffff)), "0x08 * 2**40 - 1");
+
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x88000000)), "0x88 * 2**24");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x8888888888000000)), "0x8888888888 * 2**24");
+
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0x100000000)), "2**32");
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(0xFFFFffff)), "2**32 - 1");
+
+	u160 a = 0;
+	for (int i = 0; i < 20; i++)
+	{
+		a <<= 8;
+		a |= 0x55;
+	}
+	u256 b = 0;
+	for (int i = 0; i < 32; i++)
+	{
+		b <<= 8;
+		b |= 0x55;
+	}
+	u256 c = (u256)FixedHash<32>(
+		fromHex("0xabcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789")
+	);
+	u256 d = u256(0xAAAAaaaaAAAAaaaa) << 192 |
+		u256(0xFFFFffffFFFFffff) << 128 |
+		u256(0xFFFFffffFFFFffff) << 64 |
+		u256(0xFFFFffffFFFFffff);
+	BOOST_CHECK_EQUAL(formatNumberReadable(a, true), "0x5555...{+32 more}...5555");
+	BOOST_CHECK_EQUAL(formatNumberReadable(b, true), "0x5555...{+56 more}...5555");
+	BOOST_CHECK_EQUAL(formatNumberReadable(c, true), "0xABCD...{+56 more}...6789");
+	BOOST_CHECK_EQUAL(formatNumberReadable(d, true), "0xAAAAaaaaAAAAaaab * 2**192 - 1");
+
+	//for codegen/ExpressionCompiler
+	BOOST_CHECK_EQUAL(formatNumberReadable(u256(-1)), "2**256 - 1");
+
+	// for formal/SMTChecker
+	BOOST_CHECK_EQUAL(
+			formatNumberReadable(solidity::IntegerType(256).minValue()), "0");
+	BOOST_CHECK_EQUAL(
+			formatNumberReadable(solidity::IntegerType(256).maxValue()), "2**256 - 1");
+}
 
 BOOST_AUTO_TEST_SUITE_END()
 
diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
index ea5bf044..df6eaaa7 100644
--- a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
@@ -12,6 +12,6 @@ contract C
 	}
 }
 // ----
-// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
-// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (146-155): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (179-193): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
index 33e598b6..49a1e0a5 100644
--- a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
+++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
@@ -14,6 +14,6 @@ contract C
 	}
 }
 // ----
-// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
-// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (146-155): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (269-282): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
index 3858403a..2be01c2d 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
@@ -12,6 +12,6 @@ contract C
 	}
 }
 // ----
-// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
-// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (172-181): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (189-203): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
index 7d7b7015..c8232ab6 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
@@ -13,6 +13,6 @@ contract C
 	}
 }
 // ----
-// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
-// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (172-181): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (244-257): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
index 894ff1a4..ec819b80 100644
--- a/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
@@ -3,4 +3,4 @@ contract C {
     function f(uint a, uint b) public pure returns (uint) { return a + b; }
 }
 // ----
-// Warning: (112-117): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (112-117): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol
index 40e5d987..ae60b1e5 100644
--- a/test/libsolidity/smtCheckerTests/special/many.sol
+++ b/test/libsolidity/smtCheckerTests/special/many.sol
@@ -20,6 +20,6 @@ contract C
 // Warning: (165-204): Assertion violation happens here
 // Warning: (208-240): Assertion violation happens here
 // Warning: (244-275): Assertion violation happens here
-// Warning: (311-316): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (311-316): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (336-352): Assertion violation happens here
 // Warning: (356-379): Assertion violation happens here