Merge pull request #9883 from ethereum/develop

Merge develop into breaking.

.circleci/soltest_all.sh

@@ -30,7 +30,7 @@ REPODIR="$(realpath $(dirname $0)/..)"
 
 EVM_VALUES=(homestead byzantium constantinople petersburg istanbul)
 OPTIMIZE_VALUES=(0 1)
-STEPS=$(( 1 + ${#EVM_VALUES[@]} * ${#OPTIMIZE_VALUES[@]} ))
+STEPS=$(( 2 + ${#EVM_VALUES[@]} * ${#OPTIMIZE_VALUES[@]} ))
 
 if (( $CIRCLE_NODE_TOTAL )) && (( $CIRCLE_NODE_TOTAL > 1 ))
 then
@@ -57,7 +57,12 @@ echo "Running steps $RUN_STEPS..."
 
 STEP=1
 
-[[ " $RUN_STEPS " =~ " $STEP " ]] && EVM=istanbul OPTIMIZE=1 ABI_ENCODER_V2=1 "${REPODIR}/.circleci/soltest.sh"
+# Run SMTChecker tests separately, as the heaviest expected run.
+[[ " $RUN_STEPS " =~ " $STEP " ]] && EVM=istanbul OPTIMIZE=1 ABI_ENCODER_V2=1 BOOST_TEST_ARGS="-t smtCheckerTests/*" "${REPODIR}/.circleci/soltest.sh"
+STEP=$(($STEP + 1))
+
+# Run without SMTChecker tests.
+[[ " $RUN_STEPS " =~ " $STEP " ]] && EVM=istanbul OPTIMIZE=1 ABI_ENCODER_V2=1 BOOST_TEST_ARGS="-t !smtCheckerTests" "${REPODIR}/.circleci/soltest.sh"
 STEP=$(($STEP + 1))
 
 for OPTIMIZE in ${OPTIMIZE_VALUES[@]}

Changelog.md

@@ -14,9 +14,13 @@ Compiler Features:
  * SMTChecker: Support events and low-level logs.
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
+ * SMTChecker: Support compound and, or, and xor operators.
  * SMTChecker: Support structs.
  * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
  * SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``.
+ * Type Checker: Report position of first invalid UTF-8 sequence in ``unicode""`` literals.
+ * Type Checker: More detailed error messages why implicit conversions fail.
+ * Type Checker: Explain why oversized hex string literals can not be explicitly converted to a shorter ``bytesNN`` type.
  * Yul Optimizer: Prune unused parameters in functions.
  * Yul Optimizer: Inline into functions further down in the call graph first.
  * Yul Optimizer: Try to simplify function names.

libsmtutil/Z3CHCInterface.cpp

@@ -142,14 +142,17 @@ instead of a path.
 */
 CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
 {
-	CexGraph graph;
-
 	/// The root fact of the refutation proof is `false`.
 	/// The node itself is not a hyper resolution, so we need to
 	/// extract the `query` hyper resolution node from the
 	/// `false` node (the first child).
-	smtAssert(_proof.is_app(), "");
+	/// The proof has the shape above for z3 >=4.8.8.
-	smtAssert(fact(_proof).decl().decl_kind() == Z3_OP_FALSE, "");
+	/// If an older version is used, this check will fail and no
+	/// counterexample will be generated.
+	if (!_proof.is_app() || fact(_proof).decl().decl_kind() != Z3_OP_FALSE)
+		return {};
+
+	CexGraph graph;
 
 	stack<z3::expr> proofStack;
 	proofStack.push(_proof.arg(0));

libsmtutil/Z3Interface.h

@@ -49,7 +49,7 @@ public:
 
 	// Z3 "basic resources" limit.
 	// This is used to make the runs more deterministic and platform/machine independent.
-	static int const resourceLimit = 12500000;
+	static int const resourceLimit = 1000000;
 
 private:
 	void declareFunction(std::string const& _name, Sort const& _sort);

libsolidity/analysis/SyntaxChecker.cpp

@@ -219,11 +219,12 @@ bool SyntaxChecker::visit(Throw const& _throwStatement)
 
 bool SyntaxChecker::visit(Literal const& _literal)
 {
-	if ((_literal.token() == Token::UnicodeStringLiteral) && !validateUTF8(_literal.value()))
+	size_t invalidSequence;
+	if ((_literal.token() == Token::UnicodeStringLiteral) && !validateUTF8(_literal.value(), invalidSequence))
 		m_errorReporter.syntaxError(
 			8452_error,
 			_literal.location(),
-			"Invalid UTF-8 sequence found"
+			"Contains invalid UTF-8 sequence at position " + toString(invalidSequence) + "."
 		);
 
 	if (_literal.token() != Token::Number)

libsolidity/analysis/TypeChecker.cpp

@@ -1645,7 +1645,8 @@ TypePointer TypeChecker::typeCheckTypeConversionAndRetrieveReturnType(
 			dataLoc = argRefType->location();
 		if (auto type = dynamic_cast<ReferenceType const*>(resultType))
 			resultType = TypeProvider::withLocation(type, dataLoc, type->isPointer());
-		if (argType->isExplicitlyConvertibleTo(*resultType))
+		BoolResult result = argType->isExplicitlyConvertibleTo(*resultType);
+		if (result)
 		{
 			if (auto argArrayType = dynamic_cast<ArrayType const*>(argType))
 			{
@@ -1716,14 +1717,15 @@ TypePointer TypeChecker::typeCheckTypeConversionAndRetrieveReturnType(
 					"you can use the .address member of the function."
 				);
 			else
-				m_errorReporter.typeError(
+				m_errorReporter.typeErrorConcatenateDescriptions(
 					9640_error,
 					_functionCall.location(),
 					"Explicit type conversion not allowed from \"" +
 					argType->toString() +
 					"\" to \"" +
 					resultType->toString() +
-					"\"."
+					"\".",
+					result.message()
 				);
 		}
 		if (auto addressType = dynamic_cast<AddressType const*>(resultType))
@@ -3217,7 +3219,8 @@ Declaration const& TypeChecker::dereference(UserDefinedTypeName const& _typeName
 bool TypeChecker::expectType(Expression const& _expression, Type const& _expectedType)
 {
 	_expression.accept(*this);
-	if (!type(_expression)->isImplicitlyConvertibleTo(_expectedType))
+	BoolResult result = type(_expression)->isImplicitlyConvertibleTo(_expectedType);
+	if (!result)
 	{
 		auto errorMsg = "Type " +
 			type(_expression)->toString() +
@@ -3236,17 +3239,23 @@ bool TypeChecker::expectType(Expression const& _expression, Type const& _expecte
 					errorMsg + ", but it can be explicitly converted."
 				);
 			else
-				m_errorReporter.typeError(
+				m_errorReporter.typeErrorConcatenateDescriptions(
 					2326_error,
 					_expression.location(),
 					errorMsg +
 					". Try converting to type " +
 					type(_expression)->mobileType()->toString() +
-					" or use an explicit conversion."
+					" or use an explicit conversion.",
+					result.message()
 				);
 		}
 		else
-			m_errorReporter.typeError(7407_error, _expression.location(), errorMsg + ".");
+			m_errorReporter.typeErrorConcatenateDescriptions(
+				7407_error,
+				_expression.location(),
+				errorMsg + ".",
+				result.message()
+			);
 		return false;
 	}
 	return true;

libsolidity/ast/Types.cpp

@@ -1352,13 +1352,25 @@ StringLiteralType::StringLiteralType(string _value):
 BoolResult StringLiteralType::isImplicitlyConvertibleTo(Type const& _convertTo) const
 {
 	if (auto fixedBytes = dynamic_cast<FixedBytesType const*>(&_convertTo))
-		return static_cast<size_t>(fixedBytes->numBytes()) >= m_value.size();
+	{
+		if (static_cast<size_t>(fixedBytes->numBytes()) < m_value.size())
+			return BoolResult::err("Literal is larger than the type.");
+		return true;
+	}
 	else if (auto arrayType = dynamic_cast<ArrayType const*>(&_convertTo))
+	{
+		size_t invalidSequence;
+		if (arrayType->isString() && !util::validateUTF8(value(), invalidSequence))
+			return BoolResult::err(
+				"Contains invalid UTF-8 sequence at position " +
+				util::toString(invalidSequence) +
+				"."
+			);
 		return
 			arrayType->location() != DataLocation::CallData &&
 			arrayType->isByteArray() &&
-			!(arrayType->dataStoredIn(DataLocation::Storage) && arrayType->isPointer()) &&
+			!(arrayType->dataStoredIn(DataLocation::Storage) && arrayType->isPointer());
-			!(arrayType->isString() && !util::validateUTF8(value()));
+	}
 	else
 		return false;
 }
@@ -1379,12 +1391,19 @@ bool StringLiteralType::operator==(Type const& _other) const
 
 std::string StringLiteralType::toString(bool) const
 {
-	size_t invalidSequence;
+	auto isPrintableASCII = [](string const& s)
+	{
+		for (auto c: s)
+		{
+			if (static_cast<unsigned>(c) <= 0x1f || static_cast<unsigned>(c) >= 0x7f)
+				return false;
+		}
+		return true;
+	};
 
-	if (!util::validateUTF8(m_value, invalidSequence))
+	return isPrintableASCII(m_value) ?
-		return "literal_string (contains invalid UTF-8 sequence at position " + util::toString(invalidSequence) + ")";
+		("literal_string \"" + m_value + "\"") :
-
+		("literal_string hex\"" + util::toHex(util::asBytes(m_value)) + "\"");
-	return "literal_string \"" + m_value + "\"";
 }
 
 TypePointer StringLiteralType::mobileType() const

libsolidity/codegen/YulUtilFunctions.cpp

@@ -632,6 +632,16 @@ string YulUtilFunctions::overflowCheckedIntExpFunction(
 
 string YulUtilFunctions::overflowCheckedUnsignedExpFunction()
 {
+	// Checks for the "small number specialization" below.
+	using namespace boost::multiprecision;
+	solAssert(pow(bigint(10), 77) < pow(bigint(2), 256), "");
+	solAssert(pow(bigint(11), 77) >= pow(bigint(2), 256), "");
+	solAssert(pow(bigint(10), 78) >= pow(bigint(2), 256), "");
+
+	solAssert(pow(bigint(306), 31) < pow(bigint(2), 256), "");
+	solAssert(pow(bigint(307), 31) >= pow(bigint(2), 256), "");
+	solAssert(pow(bigint(306), 32) >= pow(bigint(2), 256), "");
+
 	string functionName = "checked_exp_unsigned";
 	return m_functionCollector.createFunction(functionName, [&]() {
 		return
@@ -644,25 +654,35 @@ string YulUtilFunctions::overflowCheckedUnsignedExpFunction()
 				if iszero(exponent) { power := 1 leave }
 				if iszero(base) { power := 0 leave }
 
-				power := 1
+				// Specializations for small bases
-
+				switch base
-				for { } gt(exponent, 1) {}
+				// 0 is handled above
+				case 1 { power := 1 leave }
+				case 2
 				{
-					// overflow check for base * base
+					if gt(exponent, 255) { revert(0, 0) }
-					if gt(base, div(max, base)) { revert(0, 0) }
+					power := exp(2, exponent)
-					if and(exponent, 1)
+					if gt(power, max) { revert(0, 0) }
-					{
+					leave
-						// no check needed here because base >= power
-						power := mul(power, base)
-					}
-					base := mul(base, base)
-					exponent := <shr_1>(exponent)
 				}
+				if or(
+					and(lt(base, 11), lt(exponent, 78)),
+					and(lt(base, 307), lt(exponent, 32))
+				)
+				{
+					power := exp(base, exponent)
+					if gt(power, max) { revert(0, 0) }
+					leave
+				}
+
+				power, base := <expLoop>(1, base, exponent, max)
+
 				if gt(power, div(max, base)) { revert(0, 0) }
 				power := mul(power, base)
 			}
 			)")
 			("functionName", functionName)
+			("expLoop", overflowCheckedExpLoopFunction())
 			("shr_1", shiftRightFunction(1))
 			.render();
 	});
@@ -703,6 +723,35 @@ string YulUtilFunctions::overflowCheckedSignedExpFunction()
 
 				// Below this point, base is always positive.
 
+				power, base := <expLoop>(power, base, exponent, max)
+
+				if and(sgt(power, 0), gt(power, div(max, base))) { revert(0, 0) }
+				if and(slt(power, 0), slt(power, sdiv(min, base))) { revert(0, 0) }
+				power := mul(power, base)
+			}
+			)")
+			("functionName", functionName)
+			("expLoop", overflowCheckedExpLoopFunction())
+			("shr_1", shiftRightFunction(1))
+			.render();
+	});
+}
+
+string YulUtilFunctions::overflowCheckedExpLoopFunction()
+{
+	// We use this loop for both signed and unsigned exponentiation
+	// because we pull out the first iteration in the signed case which
+	// results in the base always being positive.
+
+	// This function does not include the final multiplication.
+
+	string functionName = "checked_exp_helper";
+	return m_functionCollector.createFunction(functionName, [&]() {
+		return
+			Whiskers(R"(
+			function <functionName>(_power, _base, exponent, max) -> power, base {
+				power := _power
+				base  := _base
 				for { } gt(exponent, 1) {}
 				{
 					// overflow check for base * base
@@ -712,16 +761,13 @@ string YulUtilFunctions::overflowCheckedSignedExpFunction()
 						// No checks for power := mul(power, base) needed, because the check
 						// for base * base above is sufficient, since:
 						// |power| <= base (proof by induction) and thus:
-						// |power * base| <= base * base <= max <= |min|
+						// |power * base| <= base * base <= max <= |min| (for signed)
+						// (this is equally true for signed and unsigned exp)
 						power := mul(power, base)
 					}
 					base := mul(base, base)
 					exponent := <shr_1>(exponent)
 				}
-
-				if and(sgt(power, 0), gt(power, div(max, base))) { revert(0, 0) }
-				if and(slt(power, 0), slt(power, sdiv(min, base))) { revert(0, 0) }
-				power := mul(power, base)
 			}
 			)")
 			("functionName", functionName)

libsolidity/codegen/YulUtilFunctions.h

@@ -140,6 +140,10 @@ public:
 	/// signature: (base, exponent, min, max) -> power
 	std::string overflowCheckedSignedExpFunction();
 
+	/// Helper function for the two checked exponentiation functions.
+	/// signature: (power, base, exponent, max) -> power
+	std::string overflowCheckedExpLoopFunction();
+
 	/// @returns the name of a function that fetches the length of the given
 	/// array
 	/// signature: (array) -> length

libsolidity/formal/SMTEncoder.cpp

@@ -352,31 +352,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 {
 	createExpr(_assignment);
 
-	static set<Token> const compoundOps{
-		Token::AssignAdd,
-		Token::AssignSub,
-		Token::AssignMul,
-		Token::AssignDiv,
-		Token::AssignMod
-	};
 	Token op = _assignment.assignmentOperator();
-	if (op != Token::Assign && !compoundOps.count(op))
+	solAssert(TokenTraits::isAssignmentOp(op), "");
-	{
-		Expression const* identifier = &_assignment.leftHandSide();
-		if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(identifier))
-			identifier = leftmostBase(*indexAccess);
-		// Give it a new index anyway to keep the SSA scheme sound.
-		solAssert(identifier, "");
-		if (auto varDecl = identifierToVariable(*identifier))
-			m_context.newValue(*varDecl);
 
-		m_errorReporter.warning(
+	if (!smt::isSupportedType(*_assignment.annotation().type))
-			9149_error,
-			_assignment.location(),
-			"Assertion checker does not yet implement this assignment operator."
-		);
-	}
-	else if (!smt::isSupportedType(*_assignment.annotation().type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
 
@@ -394,9 +373,9 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 		else
 		{
 			auto const& type = _assignment.annotation().type;
-			auto rightHandSide = compoundOps.count(op) ?
+			auto rightHandSide = op == Token::Assign ?
-				compoundAssignment(_assignment) :
+				expr(_assignment.rightHandSide(), type) :
-				expr(_assignment.rightHandSide(), type);
+				compoundAssignment(_assignment);
 			defineExpr(_assignment, rightHandSide);
 			assignment(
 				_assignment.leftHandSide(),
@@ -1388,6 +1367,59 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	return {value, valueUnbounded};
 }
 
+smtutil::Expression SMTEncoder::bitwiseOperation(
+	Token _op,
+	smtutil::Expression const& _left,
+	smtutil::Expression const& _right,
+	TypePointer const& _commonType
+)
+{
+	static set<Token> validOperators{
+		Token::BitAnd,
+		Token::BitOr,
+		Token::BitXor,
+		Token::SHL,
+		Token::SHR,
+		Token::SAR
+	};
+	solAssert(validOperators.count(_op), "");
+	solAssert(_commonType, "");
+
+	auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_commonType);
+
+	auto bvLeft = smtutil::Expression::int2bv(_left, bvSize);
+	auto bvRight = smtutil::Expression::int2bv(_right, bvSize);
+
+	optional<smtutil::Expression> result;
+	switch (_op)
+	{
+		case Token::BitAnd:
+			result = bvLeft & bvRight;
+			break;
+		case Token::BitOr:
+			result = bvLeft | bvRight;
+			break;
+		case Token::BitXor:
+			result = bvLeft ^ bvRight;
+			break;
+		case Token::SHL:
+			result = bvLeft << bvRight;
+			break;
+		case Token::SHR:
+			solAssert(false, "");
+		case Token::SAR:
+			result = isSigned ?
+				smtutil::Expression::ashr(bvLeft, bvRight) :
+				bvLeft >> bvRight;
+			break;
+		default:
+			solAssert(false, "");
+	}
+
+	solAssert(result.has_value(), "");
+	return smtutil::Expression::bv2int(*result, isSigned);
+}
+
 void SMTEncoder::compareOperation(BinaryOperation const& _op)
 {
 	auto const& commonType = _op.annotation().commonType;
@@ -1464,39 +1496,12 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
 	auto commonType = _op.annotation().commonType;
 	solAssert(commonType, "");
 
-	auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(commonType);
+	defineExpr(_op, bitwiseOperation(
-
+		_op.getOperator(),
-	auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize);
+		expr(_op.leftExpression(), commonType),
-	auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize);
+		expr(_op.rightExpression(), commonType),
-
+		commonType
-	optional<smtutil::Expression> result;
+	));
-	switch (op)
-	{
-	case Token::BitAnd:
-		result = bvLeft & bvRight;
-		break;
-	case Token::BitOr:
-		result = bvLeft | bvRight;
-		break;
-	case Token::BitXor:
-		result = bvLeft ^ bvRight;
-		break;
-	case Token::SHL:
-		result = bvLeft << bvRight;
-		break;
-	case Token::SHR:
-		solAssert(false, "");
-	case Token::SAR:
-		result = isSigned ?
-			smtutil::Expression::ashr(bvLeft, bvRight) :
-			bvLeft >> bvRight;
-		break;
-	default:
-		solAssert(false, "");
-	}
-
-	solAssert(result, "");
-	defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
 }
 
 void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
@@ -1604,9 +1609,27 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
 		{Token::AssignDiv, Token::Div},
 		{Token::AssignMod, Token::Mod}
 	};
+	static map<Token, Token> const compoundToBitwise{
+		{Token::AssignBitAnd, Token::BitAnd},
+		{Token::AssignBitOr, Token::BitOr},
+		{Token::AssignBitXor, Token::BitXor},
+		{Token::AssignShl, Token::SHL},
+		{Token::AssignShr, Token::SHR},
+		{Token::AssignSar, Token::SAR}
+	};
 	Token op = _assignment.assignmentOperator();
-	solAssert(compoundToArithmetic.count(op), "");
+	solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");
+
 	auto decl = identifierToVariable(_assignment.leftHandSide());
+
+	if (compoundToBitwise.count(op))
+		return bitwiseOperation(
+			compoundToBitwise.at(op),
+			decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
+			expr(_assignment.rightHandSide()),
+			_assignment.annotation().type
+		);
+
 	auto values = arithmeticOperation(
 		compoundToArithmetic.at(op),
 		decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),

libsolidity/formal/SMTEncoder.h

@@ -119,6 +119,14 @@ protected:
 		TypePointer const& _commonType,
 		Expression const& _expression
 	);
+
+	smtutil::Expression bitwiseOperation(
+		Token _op,
+		smtutil::Expression const& _left,
+		smtutil::Expression const& _right,
+		TypePointer const& _commonType
+	);
+
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 	void bitwiseOperation(BinaryOperation const& _op);

test/CMakeLists.txt

@@ -79,9 +79,6 @@ set(libsolidity_sources
     libsolidity/SemanticTest.cpp
     libsolidity/SemanticTest.h
     libsolidity/SemVerMatcher.cpp
-    libsolidity/SMTChecker.cpp
-    libsolidity/SMTCheckerJSONTest.cpp
-    libsolidity/SMTCheckerJSONTest.h
     libsolidity/SMTCheckerTest.cpp
     libsolidity/SMTCheckerTest.h
     libsolidity/SolidityCompiler.cpp

test/InteractiveTests.h

@@ -25,7 +25,6 @@
 #include <test/libsolidity/SyntaxTest.h>
 #include <test/libsolidity/SemanticTest.h>
 #include <test/libsolidity/SMTCheckerTest.h>
-#include <test/libsolidity/SMTCheckerJSONTest.h>
 #include <test/libyul/EwasmTranslationTest.h>
 #include <test/libyul/YulOptimizerTest.h>
 #include <test/libyul/YulInterpreterTest.h>

test/boostTest.cpp

@@ -205,9 +205,6 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
 			removeTestSuite(suite);
 	}
 
-	if (solidity::test::CommonOptions::get().disableSMT)
-		removeTestSuite("SMTChecker");
-
 	return nullptr;
 }
 

test/libsolidity/ASTJSON/non_utf8.json

@@ -86,7 +86,7 @@
                   "typeDescriptions":
                   {
                     "typeIdentifier": "t_stringliteral_8b1a944cf13a9a1c08facb2c9e98623ef3254d2ddb48113885c3e8e97fec8db9",
-                    "typeString": "literal_string (contains invalid UTF-8 sequence at position 0)"
+                    "typeString": "literal_string hex\"ff\""
                   }
                 },
                 "nodeType": "VariableDeclarationStatement",

test/libsolidity/ASTJSON/non_utf8_legacy.json

@@ -131,7 +131,7 @@
                         "isPure": true,
                         "lValueRequested": false,
                         "token": "hexString",
-                        "type": "literal_string (contains invalid UTF-8 sequence at position 0)"
+                        "type": "literal_string hex\"ff\""
                       },
                       "id": 5,
                       "name": "Literal",

test/libsolidity/ASTJSON/unicode.json

@@ -86,7 +86,7 @@
                   "typeDescriptions":
                   {
                     "typeIdentifier": "t_stringliteral_cd7a99177cebb3d14b8cc54e313dbf76867c71cd6fbb9a33ce3870dc80e9992b",
-                    "typeString": "literal_string \"Hello \ud83d\ude03\""
+                    "typeString": "literal_string hex\"48656c6c6f20f09f9883\""
                   },
                   "value": "Hello \ud83d\ude03"
                 },

test/libsolidity/ASTJSON/unicode_legacy.json

@@ -131,7 +131,7 @@
                         "isPure": true,
                         "lValueRequested": false,
                         "token": "unicodeString",
-                        "type": "literal_string \"Hello \ud83d\ude03\"",
+                        "type": "literal_string hex\"48656c6c6f20f09f9883\"",
                         "value": "Hello \ud83d\ude03"
                       },
                       "id": 5,

test/libsolidity/SMTChecker.cpp

@@ -1,143 +0,0 @@
-/*
-    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 SMT checker.
- */
-
-#include <test/libsolidity/AnalysisFramework.h>
-#include <test/Common.h>
-
-#include <boost/test/unit_test.hpp>
-
-#include <string>
-
-using namespace std;
-using namespace solidity::langutil;
-
-namespace solidity::frontend::test
-{
-
-class SMTCheckerFramework: public AnalysisFramework
-{
-protected:
-	std::pair<SourceUnit const*, ErrorList>
-	parseAnalyseAndReturnError(
-		std::string const& _source,
-		bool _reportWarnings = false,
-		bool _insertLicenseAndVersionPragma = true,
-		bool _allowMultipleErrors = false,
-		bool _allowRecoveryErrors = false
-	) override
-	{
-		return AnalysisFramework::parseAnalyseAndReturnError(
-			"pragma experimental SMTChecker;\n" + _source,
-			_reportWarnings,
-			_insertLicenseAndVersionPragma,
-			_allowMultipleErrors,
-			_allowRecoveryErrors
-		);
-	}
-};
-
-BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)
-
-BOOST_AUTO_TEST_CASE(import_base, *boost::unit_test::label("no_options"))
-{
-	CompilerStack c;
-	c.setSources({
-	{"base", R"(
-		pragma solidity >=0.0;
-		contract Base {
-			uint x;
-			address a;
-			function f() internal returns (uint) {
-				a = address(this);
-				++x;
-				return 2;
-			}
-		}
-	)"},
-	{"der", R"(
-		pragma solidity >=0.0;
-		pragma experimental SMTChecker;
-		import "base";
-		contract Der is Base {
-			function g(uint y) public {
-				x += f();
-				assert(y > x);
-			}
-		}
-	)"}
-	});
-	c.setEVMVersion(solidity::test::CommonOptions::get().evmVersion());
-	BOOST_CHECK(c.compile());
-
-	unsigned asserts = 0;
-	for (auto const& e: c.errors())
-	{
-		string const* msg = e->comment();
-		BOOST_REQUIRE(msg);
-		if (msg->find("Assertion violation") != string::npos)
-			++asserts;
-	}
-	BOOST_CHECK_EQUAL(asserts, 1);
-}
-
-BOOST_AUTO_TEST_CASE(import_library, *boost::unit_test::label("no_options"))
-{
-	CompilerStack c;
-	c.setSources({
-	{"lib", R"(
-		pragma solidity >=0.0;
-		library L {
-			uint constant one = 1;
-			function f() internal pure returns (uint) {
-				return one;
-			}
-		}
-	)"},
-	{"c", R"(
-		pragma solidity >=0.0;
-		pragma experimental SMTChecker;
-		import "lib";
-		contract C {
-			function g(uint x) public pure {
-				uint y = L.f();
-				assert(x > y);
-			}
-		}
-	)"}
-	});
-	c.setEVMVersion(solidity::test::CommonOptions::get().evmVersion());
-	BOOST_CHECK(c.compile());
-
-	unsigned asserts = 0;
-	for (auto const& e: c.errors())
-	{
-		string const* msg = e->comment();
-		BOOST_REQUIRE(msg);
-		if (msg->find("Assertion violation") != string::npos)
-			++asserts;
-	}
-	BOOST_CHECK_EQUAL(asserts, 1);
-
-}
-
-
-BOOST_AUTO_TEST_SUITE_END()
-
-}

test/libsolidity/SMTCheckerJSONTest.cpp

@@ -1,176 +0,0 @@
-/*
-	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/>.
-*/
-// SPDX-License-Identifier: GPL-3.0
-
-#include <test/libsolidity/SMTCheckerJSONTest.h>
-#include <test/Common.h>
-
-#include <libsolidity/formal/ModelChecker.h>
-#include <libsolidity/interface/StandardCompiler.h>
-#include <libsolutil/CommonIO.h>
-#include <libsolutil/JSON.h>
-
-#include <boost/algorithm/string.hpp>
-#include <boost/algorithm/string/join.hpp>
-#include <boost/algorithm/string/predicate.hpp>
-#include <boost/test/unit_test.hpp>
-#include <boost/throw_exception.hpp>
-
-#include <fstream>
-#include <memory>
-#include <stdexcept>
-#include <sstream>
-
-using namespace std;
-using namespace solidity;
-using namespace solidity::frontend;
-using namespace solidity::frontend::test;
-using namespace solidity::util;
-using namespace solidity::util::formatting;
-using namespace boost::unit_test;
-
-SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVersion _evmVersion)
-: SyntaxTest(_filename, _evmVersion)
-{
-	if (!boost::algorithm::ends_with(_filename, ".sol"))
-		BOOST_THROW_EXCEPTION(runtime_error("Invalid test contract file name: \"" + _filename + "\"."));
-
-	string jsonFilename = _filename.substr(0, _filename.size() - 4) + ".json";
-	if (
-		!jsonParseStrict(readFileAsString(jsonFilename), m_smtResponses) ||
-		!m_smtResponses.isObject()
-	)
-		BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
-
-	if (ModelChecker::availableSolvers().none())
-		m_shouldRun = false;
-}
-
-TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
-{
-	StandardCompiler compiler;
-
-	// Run the compiler and retrieve the smtlib2queries (1st run)
-	string preamble = "pragma solidity >=0.0;\n// SPDX-License-Identifier: GPL-3.0\n";
-	Json::Value input = buildJson(preamble);
-	Json::Value result = compiler.compile(input);
-
-	// This is the list of query hashes requested by the 1st run
-	vector<string> outHashes = hashesFromJson(result, "auxiliaryInputRequested", "smtlib2queries");
-
-	// This is the list of responses provided in the test
-	string auxInput("auxiliaryInput");
-	if (!m_smtResponses.isMember(auxInput))
-		BOOST_THROW_EXCEPTION(runtime_error("JSON file does not contain field \"auxiliaryInput\"."));
-
-	vector<string> inHashes = hashesFromJson(m_smtResponses, auxInput, "smtlib2responses");
-
-	// Ensure that the provided list matches the requested one
-	if (outHashes != inHashes)
-		BOOST_THROW_EXCEPTION(runtime_error(
-			"SMT query hashes differ: " +
-			boost::algorithm::join(outHashes, ", ") +
-			" x " +
-			boost::algorithm::join(inHashes, ", ")
-		));
-
-	// Rerun the compiler with the provided hashed (2nd run)
-	input[auxInput] = m_smtResponses[auxInput];
-	Json::Value endResult = compiler.compile(input);
-
-	if (endResult.isMember("errors") && endResult["errors"].isArray())
-	{
-		Json::Value const& errors = endResult["errors"];
-		for (auto const& error: errors)
-		{
-			if (
-				!error.isMember("type") ||
-				!error["type"].isString()
-			)
-				BOOST_THROW_EXCEPTION(runtime_error("Error must have a type."));
-			if (
-				!error.isMember("message") ||
-				!error["message"].isString()
-			)
-				BOOST_THROW_EXCEPTION(runtime_error("Error must have a message."));
-			if (!error.isMember("sourceLocation"))
-				continue;
-			Json::Value const& location = error["sourceLocation"];
-			if (
-				!location.isMember("start") ||
-				!location["start"].isInt() ||
-				!location.isMember("end") ||
-				!location["end"].isInt()
-			)
-				BOOST_THROW_EXCEPTION(runtime_error("Error must have a SourceLocation with start and end."));
-			size_t start = location["start"].asUInt();
-			size_t end = location["end"].asUInt();
-			std::string sourceName;
-			if (location.isMember("source") && location["source"].isString())
-				sourceName = location["source"].asString();
-			if (start >= preamble.size())
-				start -= preamble.size();
-			if (end >= preamble.size())
-				end -= preamble.size();
-			m_errorList.emplace_back(SyntaxTestError{
-				error["type"].asString(),
-				error["errorId"].isNull() ?  nullopt : optional<langutil::ErrorId>(langutil::ErrorId{error["errorId"].asUInt()}),
-				error["message"].asString(),
-				sourceName,
-				static_cast<int>(start),
-				static_cast<int>(end)
-			});
-		}
-	}
-
-	return conclude(_stream, _linePrefix, _formatted);
-}
-
-vector<string> SMTCheckerJSONTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib)
-{
-	vector<string> hashes;
-	Json::Value const& auxInputs = _jsonObj[_auxInput];
-	if (!!auxInputs)
-	{
-		Json::Value const& smtlib = auxInputs[_smtlib];
-		if (!!smtlib)
-			for (auto const& hashString: smtlib.getMemberNames())
-				hashes.push_back(hashString);
-	}
-	return hashes;
-}
-
-Json::Value SMTCheckerJSONTest::buildJson(string const& _extra)
-{
-	string language = "\"language\": \"Solidity\"";
-	string sources = " \"sources\": { ";
-	bool first = true;
-	for (auto [sourceName, sourceContent]: m_sources)
-	{
-		string sourceObj = "{ \"content\": \"" + _extra + sourceContent + "\"}";
-		if (!first)
-			sources += ", ";
-		sources += "\"" + sourceName + "\": " + sourceObj;
-		first = false;
-	}
-	sources += "}";
-	string input = "{" + language + ", " + sources + "}";
-	Json::Value source;
-	if (!jsonParseStrict(input, source))
-		BOOST_THROW_EXCEPTION(runtime_error("Could not build JSON from string: " + input));
-	return source;
-}

test/libsolidity/SMTCheckerJSONTest.h

@@ -1,48 +0,0 @@
-/*
-	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/>.
-*/
-// SPDX-License-Identifier: GPL-3.0
-
-#pragma once
-
-#include <test/libsolidity/SyntaxTest.h>
-
-#include <libsolutil/JSON.h>
-
-#include <string>
-
-namespace solidity::frontend::test
-{
-
-class SMTCheckerJSONTest: public SyntaxTest
-{
-public:
-	static std::unique_ptr<TestCase> create(Config const& _config)
-	{
-		return std::make_unique<SMTCheckerJSONTest>(_config.filename, _config.evmVersion);
-	}
-	SMTCheckerJSONTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
-
-	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
-
-private:
-	std::vector<std::string> hashesFromJson(Json::Value const& _jsonObj, std::string const& _auxInput, std::string const& _smtlib);
-	Json::Value buildJson(std::string const& _extra);
-
-	Json::Value m_smtResponses;
-};
-
-}

test/libsolidity/semanticTests/viaYul/exp_neg.sol

@@ -25,4 +25,9 @@ contract C {
 // f(int256,uint256): -2, 2 -> 4
 // f(int256,uint256): -7, 63 -> -174251498233690814305510551794710260107945042018748343
 // f(int256,uint256): -128, 2 -> 0x4000
-// f(int256,uint256): -1, 115792089237316195423570985008687907853269984665640564039457584007913129639935 -> -1
+// f(int256,uint256): -1, 115792089237316195423570985008687907853269984665640564039457584007913129639935 -> -1
+// f(int256,uint256): -2, 255 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968
+// f(int256,uint256): -8, 85 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968
+// f(int256,uint256): -131072, 15 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968
+// f(int256,uint256): -32, 51 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968
+// f(int256,uint256): -57896044618658097711785492504343953926634992332820282019728792003956564819968, 1 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968

test/libsolidity/smtCheckerTests/imports/import_base.sol

@@ -0,0 +1,25 @@
+==== Source: base ====
+contract Base {
+	uint x;
+	address a;
+	function f() internal returns (uint) {
+		a = address(this);
+		++x;
+		return 2;
+	}
+}
+==== Source: der ====
+pragma experimental SMTChecker;
+import "base";
+contract Der is Base {
+	function g(uint y) public {
+		x += f();
+		assert(y > x);
+	}
+}
+// ----
+// Warning 1218: (der:101-109): Error trying to invoke SMT solver.
+// Warning 6328: (der:113-126): Assertion violation happens here.
+// Warning 2661: (base:100-103): Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (der:101-109): Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (base:100-103): Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/imports/import_library.sol

@@ -0,0 +1,19 @@
+==== Source: c ====
+pragma experimental SMTChecker;
+import "lib";
+contract C {
+	function g(uint x) public pure {
+		uint y = L.f();
+		assert(x > y);
+	}
+}
+==== Source: lib ====
+library L {
+	uint constant one = 1;
+	function f() internal pure returns (uint) {
+		return one;
+	}
+}
+// ----
+// Warning 6328: (c:113-126): Assertion violation happens here.
+// Warning 8364: (c:104-105): Assertion checker does not yet implement type type(library L)

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -22,5 +22,7 @@ contract LoopFor2 {
 }
 // ----
 // Warning 1218: (229-234): Error trying to invoke SMT solver.
+// Warning 1218: (296-316): Error trying to invoke SMT solver.
 // Warning 6328: (320-339): Assertion violation happens here.
 // Warning 6328: (343-362): Assertion violation happens here.
+// Warning 4661: (296-316): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-	function f(bool b) public pure {
-		uint v = 1;
-		if (b)
-			v &= 1;
-		assert(v == 1);
-	}
-}
-// ----
-// Warning 6328: (116-130): Assertion violation happens here.
-// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public pure returns (byte) {
+        byte a = 0xff;
+        byte b = 0xf0;
+        a &= b;
+        assert(a == b);
+
+        a &= ~b;
+        assert(a != 0); // fails
+    }
+}
+// ----
+// Warning 6328: (203-217): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		x &= y;
+		assert(x != 0); // fails
+		x = -1; y = 3;
+		y &= x;
+		assert(y == 3);
+		y = -1;
+		y &= x;
+		assert(y == -1);
+		y = 127;
+		x &= y;
+		assert(x == 127);
+	}
+}
+// ----
+// Warning 6328: (114-128): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        uint v = 1;
+        v &= 1;
+        assert(v == 1);
+
+        v = 7;
+        v &= 3;
+        assert(v != 3); // fails, as 7 & 3 = 3
+
+        uint c = 0;
+        c &= v;
+        assert(c == 0);
+
+        uint8 x = 0xff;
+        uint16 y = 0xffff;
+        y &= x;
+        assert(y == 0xff);
+        assert(y == 0xffff); // fails
+
+        y = 0xffff;
+        x = 0xff;
+        y &= y | x;
+        assert(y == 0xffff);
+        assert(y == 0xff); // fails
+    }
+}
+// ----
+// Warning 6328: (177-191): Assertion violation happens here.
+// Warning 6328: (380-399): Assertion violation happens here.
+// Warning 6328: (506-523): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol

@@ -1,10 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	int[1] c;
-	function f(bool b) public {
-		if (b)
-			c[0] |= 1;
-	}
-}
-// ----
-// Warning 9149: (97-106): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol

@@ -1,10 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	int[1][20] c;
-	function f(bool b) public {
-		if (b)
-			c[10][0] |= 1;
-	}
-}
-// ----
-// Warning 9149: (101-114): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	struct S {
-		uint x;
-	}
-	S s;
-	function f(bool b) public {
-		if (b)
-			s.x |= 1;
-	}
-}
-// ----
-// Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-contract C {
-	struct S {
-		uint[] x;
-	}
-	S s;
-	function f(bool b) public {
-		if (b)
-			s.x[2] |= 1;
-	}
-}
-// ----
-// Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public pure returns (byte) {
+        byte a = 0xff;
+        byte b = 0xf0;
+        b |= a;
+        assert(a == b);
+
+        a |= ~b;
+        assert(a == 0); // fails
+    }
+}
+// ----
+// Warning 6328: (203-217): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		x |= y;
+		assert(x == 0); // fails
+		x = -1; y = 3;
+		x |= y;
+		assert(x == -1);
+		x = 4;
+		y |= x;
+		assert(y == 7);
+		y = 127;
+		x |= y;
+		assert(x == 127);
+	}
+}
+// ----
+// Warning 6328: (114-128): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+    int[1][20] c;
+    function f(bool b) public {
+	    require(c[10][0] == 0);
+        if (b)
+            c[10][0] |= 1;
+        assert(c[10][0] == 0 || c[10][0] == 1);
+    }
+}
+// ----
+// Warning 1218: (174-212): Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        uint v = 7;
+        v |= 3;
+        assert(v != 7); // fails, as 7 | 3 = 7
+
+        uint c = 0;
+        c |= v;
+        assert(c == 7);
+
+        uint16 x = 0xff;
+        uint16 y = 0xffff;
+        y |= x;
+        assert(y == 0xff); // fails
+        assert(y == 0xffff);
+
+        y = 0xf1ff;
+        x = 0xff00;
+        x |= y & x;
+        assert(y == 0xffff); // fails
+        assert(x == 0xff00);
+    }
+}
+// ----
+// Warning 6328: (121-135): Assertion violation happens here.
+// Warning 6328: (298-315): Assertion violation happens here.
+// Warning 6328: (424-443): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+    uint[1] c;
+    function f(bool b) public {
+        require(c[0] == 0);
+        if (b)
+            c[0] |= 1;
+        assert(c[0] <= 1);
+    }
+}
+// ----
+// Warning 1218: (166-183): Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+    struct S {
+        uint[] x;
+    }
+    S s;
+    function f(bool b) public {
+        if (b)
+            s.x[2] |= 1;
+        assert(s.x[2] != 1);
+    }
+}
+// ----
+// Warning 1218: (173-192): Error trying to invoke SMT solver.
+// Warning 7812: (173-192): Assertion violation might happen here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}
+// ----
+// Warning 1218: (157-172): Error trying to invoke SMT solver.
+// Warning 7812: (157-172): Assertion violation might happen here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol

@@ -1,13 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-	function f(bool b) public pure {
-		uint v = 0;
-		if (b)
-			v ^= 1;
-		assert(v == 1);
-	}
-}
-// ----
-// Warning 6328: (116-130): Assertion violation happens here.
-// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public pure returns (byte) {
+        byte a = 0xff;
+        byte b = 0xf0;
+        a ^= ~b;
+        assert(a == b);
+
+        a ^= ~b;
+        assert(a != 0xff); // fails
+    }
+}
+// ----
+// Warning 6328: (204-221): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		x ^= y;
+		assert(x != 1); // fails
+		x = -1; y = 1;
+		x ^= y;
+		assert(x == -2);
+		x = 4;
+		y ^= x;
+		assert(y == 5);
+	}
+}
+// ----
+// Warning 6328: (114-128): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        uint v = 7;
+        v ^= 3;
+        assert(v != 4); // fails, as 7 ^ 3 = 4
+
+        uint c = 0;
+        c ^= v;
+        assert(c == 4);
+
+        uint16 x = 0xff;
+        uint16 y = 0xffff;
+        y ^= x;
+        assert(y == 0xff); // fails
+        assert(y == 0xff00);
+
+        y = 0xf1;
+        x = 0xff00;
+        y ^= x | y;
+        assert(y == 0xffff); // fails
+        assert(x == 0xff00);
+    }
+}
+// ----
+// Warning 6328: (121-135): Assertion violation happens here.
+// Warning 6328: (298-315): Assertion violation happens here.
+// Warning 6328: (422-441): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol

@@ -9,5 +9,3 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (123-136): Assertion violation happens here.
-// Warning 9149: (112-119): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol

@@ -10,4 +10,3 @@ contract C {
 }
 // ----
 // Warning 6328: (117-130): Assertion violation happens here.
-// Warning 9149: (106-113): Assertion checker does not yet implement this assignment operator.

test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint256 a, uint256 b) internal pure returns (uint256) {
+        a <<= b;
+        return a;
+    }
+    function t() public pure {
+        assert(f(0x4266, 0x0) == 0x4266);
+        assert(f(0x4266, 0x8) == 0x426600);
+        assert(f(0x4266, 0xf0) == 0x4266000000000000000000000000000000000000000000000000000000000000);
+        assert(f(0x4266, 0x4266) == 0);
+    }
+}
+// ----

test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint256 a, uint256 b) internal pure returns (uint256) {
+        a >>= b;
+        return a;
+    }
+    function t() public pure {
+        assert(f(0x4266, 0) == 0x4266);
+        assert(f(0x4266, 0x8) == 0x42);
+        assert(f(0x4266, 0x11) == 0);
+        assert(f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 5) == 1809251394333065553493296640760748560207343510400633813116524750123642650624);
+    }
+}
+// ----

test/libsolidity/syntaxTests/indexing/array_multidim_rational.sol

@@ -5,7 +5,7 @@ contract C {
   }
 }
 // ----
-// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.
-// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.
 // TypeError 7407: (81-90): Type rational_const 9485...(73 digits omitted)...5712 / 5 is not implicitly convertible to expected type uint256.
 // TypeError 6318: (65-91): Index expression cannot be represented as an unsigned integer.

test/libsolidity/syntaxTests/indexing/array_multim_overflow_index.sol

@@ -5,7 +5,7 @@ contract C {
   }
 }
 // ----
-// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.
-// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.
-// TypeError 7407: (81-90): Type int_const -189...(75 digits omitted)...1423 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (81-90): Type int_const -189...(75 digits omitted)...1423 is not implicitly convertible to expected type uint256. Cannot implicitly convert signed literal to unsigned type.
 // TypeError 6318: (65-91): Index expression cannot be represented as an unsigned integer.

test/libsolidity/syntaxTests/indexing/array_negative_index.sol

@@ -5,4 +5,4 @@ contract C {
   }
 }
 // ----
-// TypeError 7407: (67-69): Type int_const -1 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (67-69): Type int_const -1 is not implicitly convertible to expected type uint256. Cannot implicitly convert signed literal to unsigned type.

test/libsolidity/syntaxTests/indexing/array_noninteger_index.sol

@@ -5,4 +5,4 @@ contract C {
   }
 }
 // ----
-// TypeError 7407: (67-178): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (67-178): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.

test/libsolidity/syntaxTests/indexing/fixedbytes_negative_index.sol

@@ -5,5 +5,5 @@ contract C {
   }
 }
 // ----
-// TypeError 7407: (58-60): Type int_const -1 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (58-60): Type int_const -1 is not implicitly convertible to expected type uint256. Cannot implicitly convert signed literal to unsigned type.
 // TypeError 6318: (56-61): Index expression cannot be represented as an unsigned integer.

test/libsolidity/syntaxTests/indexing/fixedbytes_noninteger_index.sol

@@ -5,5 +5,5 @@ contract C {
   }
 }
 // ----
-// TypeError 7407: (58-169): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (58-169): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.
 // TypeError 6318: (56-170): Index expression cannot be represented as an unsigned integer.

test/libsolidity/syntaxTests/indexing/struct_array_noninteger_index.sol

@@ -7,4 +7,4 @@ contract test {
 }
 
 // ----
-// TypeError 7407: (101-241): Type int_const 7555...(132 digits omitted)...5555 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (101-241): Type int_const 7555...(132 digits omitted)...5555 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.

test/libsolidity/syntaxTests/nameAndTypeResolution/111_overflow_caused_by_ether_units.sol

@@ -5,4 +5,4 @@ contract c {
     uint256 a;
 }
 // ----
-// TypeError 7407: (45-111): Type int_const 1157...(70 digits omitted)...0000 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (45-111): Type int_const 1157...(70 digits omitted)...0000 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.

test/libsolidity/syntaxTests/nameAndTypeResolution/158_storage_variable_initialization_with_incorrect_type_int.sol

@@ -2,4 +2,4 @@ contract c {
     uint8 a = 1000;
 }
 // ----
-// TypeError 7407: (27-31): Type int_const 1000 is not implicitly convertible to expected type uint8.
+// TypeError 7407: (27-31): Type int_const 1000 is not implicitly convertible to expected type uint8. Literal is too large to fit in uint8.

test/libsolidity/syntaxTests/nameAndTypeResolution/190_negative_integers_to_signed_out_of_bound.sol

@@ -2,4 +2,4 @@ contract test {
     int8 public i = -129;
 }
 // ----
-// TypeError 7407: (36-40): Type int_const -129 is not implicitly convertible to expected type int8.
+// TypeError 7407: (36-40): Type int_const -129 is not implicitly convertible to expected type int8. Literal is too large to fit in int8.

test/libsolidity/syntaxTests/nameAndTypeResolution/192_positive_integers_to_signed_out_of_bound.sol

@@ -2,4 +2,4 @@ contract test {
     int8 public j = 128;
 }
 // ----
-// TypeError 7407: (36-39): Type int_const 128 is not implicitly convertible to expected type int8.
+// TypeError 7407: (36-39): Type int_const 128 is not implicitly convertible to expected type int8. Literal is too large to fit in int8.

test/libsolidity/syntaxTests/nameAndTypeResolution/194_negative_integers_to_unsigned.sol

@@ -2,4 +2,4 @@ contract test {
     uint8 public x = -1;
 }
 // ----
-// TypeError 7407: (37-39): Type int_const -1 is not implicitly convertible to expected type uint8.
+// TypeError 7407: (37-39): Type int_const -1 is not implicitly convertible to expected type uint8. Cannot implicitly convert signed literal to unsigned type.

test/libsolidity/syntaxTests/nameAndTypeResolution/195_positive_integers_to_unsigned_out_of_bound.sol

@@ -2,4 +2,4 @@ contract test {
     uint8 public x = 700;
 }
 // ----
-// TypeError 7407: (37-40): Type int_const 700 is not implicitly convertible to expected type uint8.
+// TypeError 7407: (37-40): Type int_const 700 is not implicitly convertible to expected type uint8. Literal is too large to fit in uint8.

test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol

@@ -2,4 +2,4 @@ contract C {
     string s = string("\xa0\x00");
 }
 // ----
-// TypeError 9640: (28-46): Explicit type conversion not allowed from "literal_string (contains invalid UTF-8 sequence at position 0)" to "string memory".
+// TypeError 9640: (28-46): Explicit type conversion not allowed from "literal_string hex"a000"" to "string memory". Contains invalid UTF-8 sequence at position 0.

test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol

@@ -2,4 +2,4 @@ contract C {
     string s = hex"a000";
 }
 // ----
-// TypeError 7407: (28-37): Type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref.
+// TypeError 7407: (28-37): Type literal_string hex"a000" is not implicitly convertible to expected type string storage ref. Contains invalid UTF-8 sequence at position 0.

test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol

@@ -2,4 +2,4 @@ contract C {
     string s = "\xa0\x00";
 }
 // ----
-// TypeError 7407: (28-38): Type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref.
+// TypeError 7407: (28-38): Type literal_string hex"a000" is not implicitly convertible to expected type string storage ref. Contains invalid UTF-8 sequence at position 0.

test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol

@@ -2,5 +2,5 @@ contract C {
     string s = unicode"À";
 }
 // ----
-// SyntaxError 8452: (28-38): Invalid UTF-8 sequence found
+// SyntaxError 8452: (28-38): Contains invalid UTF-8 sequence at position 0.
-// TypeError 7407: (28-38): Type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref.
+// TypeError 7407: (28-38): Type literal_string hex"c0" is not implicitly convertible to expected type string storage ref. Contains invalid UTF-8 sequence at position 0.

test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol

@@ -4,4 +4,4 @@ contract test {
     }
 }
 // ----
-// TypeError 6359: (86-92): Return argument type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type (type of first return variable) string memory.
+// TypeError 6359: (86-92): Return argument type literal_string hex"c1" is not implicitly convertible to expected type (type of first return variable) string memory. Contains invalid UTF-8 sequence at position 0.

test/libsolidity/syntaxTests/types/array_index_too_large.sol

@@ -5,4 +5,4 @@ contract C {
     }
 }
 // ----
-// TypeError 7407: (140-218): Type int_const 1234...(70 digits omitted)...5678 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (140-218): Type int_const 1234...(70 digits omitted)...5678 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.

test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol

@@ -0,0 +1,7 @@
+contract C {
+    function f() public pure returns (bytes2) {
+        return bytes2(hex"123456");
+    }
+}
+// ----
+// TypeError 9640: (76-95): Explicit type conversion not allowed from "literal_string hex"123456"" to "bytes2". Literal is larger than the type.

test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol

@@ -0,0 +1,20 @@
+contract C {
+   function f() public pure {
+     bytes1 b1 = bytes1(hex"");
+     bytes1 b2 = bytes1(hex"1234");
+     bytes2 b3 = bytes2(hex"12");
+     bytes2 b4 = bytes2(hex"1234");
+     bytes2 b5 = bytes2(hex"123456");
+     bytes3 b6 = bytes3(hex"1234");
+     bytes3 b7 = bytes3(hex"123456");
+     bytes3 b8 = bytes3(hex"12345678");
+     bytes4 b9 = bytes4(hex"123456");
+     bytes4 b10 = bytes4(hex"12345678");
+     bytes4 b11 = bytes4(hex"1234567890");
+   }
+}
+// ----
+// TypeError 9640: (92-109): Explicit type conversion not allowed from "literal_string hex"1234"" to "bytes1". Literal is larger than the type.
+// TypeError 9640: (198-217): Explicit type conversion not allowed from "literal_string hex"123456"" to "bytes2". Literal is larger than the type.
+// TypeError 9640: (310-331): Explicit type conversion not allowed from "literal_string hex"12345678"" to "bytes3". Literal is larger than the type.
+// TypeError 9640: (430-453): Explicit type conversion not allowed from "literal_string hex"1234567890"" to "bytes4". Literal is larger than the type.

test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_explicit.sol

@@ -0,0 +1,13 @@
+contract C {
+   function f() public pure {
+     bytes1 b1 = bytes1(hex"01");
+     bytes1 b2 = bytes1(hex"FF");
+     bytes2 b3 = bytes2(hex"0100");
+     bytes2 b4 = bytes2(hex"FFFF");
+     bytes3 b5 = bytes3(hex"010000");
+     bytes3 b6 = bytes3(hex"FFFFFF");
+     bytes4 b7 = bytes4(hex"01000000");
+     bytes4 b8 = bytes4(hex"FFFFFFFF");
+     b1; b2; b3; b4; b5; b6; b7; b8;
+   }
+}

test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_implicit.sol

@@ -0,0 +1,13 @@
+contract C {
+   function f() public pure {
+     bytes1 b1 = hex"01";
+     bytes1 b2 = hex"FF";
+     bytes2 b3 = hex"0100";
+     bytes2 b4 = hex"FFFF";
+     bytes3 b5 = hex"010000";
+     bytes3 b6 = hex"FFFFFF";
+     bytes4 b7 = hex"01000000";
+     bytes4 b8 = hex"FFFFFFFF";
+     b1; b2; b3; b4; b5; b6; b7; b8;
+   }
+}

test/libsolidity/syntaxTests/types/rational_number_bitshift_limit.sol

@@ -7,7 +7,7 @@ contract c {
     }
 }
 // ----
-// TypeError 7407: (71-80): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256.
+// TypeError 7407: (71-80): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (133-142): Operator << not compatible with types int_const 1 and int_const 4096
 // TypeError 2271: (169-182): Operator << not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const 2
-// TypeError 7407: (169-182): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (169-182): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.

test/libsolidity/syntaxTests/types/rational_number_exp_limit_fail.sol

@@ -20,28 +20,28 @@ contract c {
 }
 // ----
 // TypeError 2271: (71-102): Operator ** not compatible with types int_const 1797...(301 digits omitted)...7216 and int_const 4. Precision of rational constants is limited to 4096 bits.
-// TypeError 7407: (71-102): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256.
+// TypeError 7407: (71-102): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (116-148): Operator ** not compatible with types int_const 1797...(301 digits omitted)...7216 and int_const 4. Precision of rational constants is limited to 4096 bits.
 // TypeError 2271: (116-153): Operator ** not compatible with types int_const 1797...(301 digits omitted)...7216 and int_const 4. Precision of rational constants is limited to 4096 bits.
-// TypeError 7407: (116-153): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256.
+// TypeError 7407: (116-153): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (167-203): Operator ** not compatible with types int_const 4 and int_const -179...(302 digits omitted)...7216
 // TypeError 2271: (217-228): Operator ** not compatible with types int_const 2 and int_const 1000...(1226 digits omitted)...0000
 // TypeError 2271: (242-254): Operator ** not compatible with types int_const -2 and int_const 1000...(1226 digits omitted)...0000
 // TypeError 2271: (268-280): Operator ** not compatible with types int_const 2 and int_const -100...(1227 digits omitted)...0000
 // TypeError 2271: (294-307): Operator ** not compatible with types int_const -2 and int_const -100...(1227 digits omitted)...0000
 // TypeError 2271: (321-332): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const 2. Precision of rational constants is limited to 4096 bits.
-// TypeError 7407: (321-332): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (321-332): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (346-358): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const 2. Precision of rational constants is limited to 4096 bits.
-// TypeError 7407: (346-358): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (346-358): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (372-384): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const -2. Precision of rational constants is limited to 4096 bits.
-// TypeError 7407: (372-384): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (372-384): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (398-411): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const -2. Precision of rational constants is limited to 4096 bits.
-// TypeError 7407: (398-411): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (398-411): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (425-441): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const 1000...(1226 digits omitted)...0000
-// TypeError 7407: (425-441): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (425-441): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (455-472): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const -100...(1227 digits omitted)...0000
-// TypeError 7407: (455-472): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (455-472): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (486-503): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const 1000...(1226 digits omitted)...0000
-// TypeError 7407: (486-503): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (486-503): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.
 // TypeError 2271: (517-535): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const -100...(1227 digits omitted)...0000
-// TypeError 7407: (517-535): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256.
+// TypeError 7407: (517-535): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.

test/libsolidity/syntaxTests/types/rational_number_huge_fail.sol

@@ -5,4 +5,4 @@ contract C {
     }
 }
 // ----
-// TypeError 7407: (142-209): Type int_const 1852...(71 digits omitted)...7281 is not implicitly convertible to expected type uint256.
+// TypeError 7407: (142-209): Type int_const 1852...(71 digits omitted)...7281 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256.

test/libsolidity/syntaxTests/types/rational_number_mul_limit.sol

@@ -6,4 +6,4 @@ contract c {
 }
 // ----
 // TypeError 2271: (71-90): Operator * not compatible with types int_const 5221...(1225 digits omitted)...5168 and int_const 5221...(1225 digits omitted)...5168. Precision of rational constants is limited to 4096 bits.
-// TypeError 7407: (71-90): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256.
+// TypeError 7407: (71-90): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256. Literal is too large to fit in int256.

test/libsolidity/util/ContractABIUtils.cpp

@@ -319,8 +319,11 @@ solidity::frontend::test::ParameterList ContractABIUtils::failureParameters(byte
 	ParameterList parameters;
 
 	parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::HexString, ABIType::AlignNone, 4}, FormatInfo{}});
-	parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::Hex}, FormatInfo{}});
+	if (_bytes.size() > 4)
-	parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::UnsignedDec}, FormatInfo{}});
+	{
+		parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::Hex}, FormatInfo{}});
+		parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::UnsignedDec}, FormatInfo{}});
+	}
 
 	/// If _bytes contains at least a 1 byte message (function selector + tail pointer + message length + message)
 	/// append an additional string parameter to represent that message.

test/tools/CMakeLists.txt

@@ -31,7 +31,6 @@ add_executable(isoltest
 	../libsolidity/ABIJsonTest.cpp
 	../libsolidity/ASTJSONTest.cpp
 	../libsolidity/SMTCheckerTest.cpp
-	../libsolidity/SMTCheckerJSONTest.cpp
 	../libyul/Common.cpp
 	../libyul/EwasmTranslationTest.cpp
 	../libyul/FunctionSideEffects.cpp