fix: harden SMT, JSON input, and TVM gas estimation

libevmasm/ConstantOptimiser.cpp

@@ -383,7 +383,7 @@ bigint ComputeMethod::gasNeeded(AssemblyItems const& _routine) const
 {
 	auto numExps = static_cast<size_t>(count(_routine.begin(), _routine.end(), Instruction::EXP));
 	return combineGas(
-		simpleRunGas(_routine, m_params.evmVersion) + numExps * (GasCosts::expGas + GasCosts::expByteGas(m_params.evmVersion)),
+		simpleRunGas(_routine, m_params.evmVersion) + numExps * GasCosts::expByteGasInTVM,
 		// Data gas for routine: Some bytes are zero, but we ignore them.
 		bytesRequired(_routine, m_params.evmVersion) * (m_params.isCreation ? GasCosts::txDataNonZeroGas(m_params.evmVersion) : GasCosts::createDataGas),
 		0

libevmasm/GasMeter.cpp

@@ -20,6 +20,8 @@
 
 #include <libevmasm/KnownState.h>
 
+#include <algorithm>
+
 using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::evmasm;
@@ -87,17 +89,11 @@ GasMeter::GasConsumption GasMeter::estimateMax(AssemblyItem const& _item, bool _
 		case Instruction::MLOAD:
 		case Instruction::MSTORE:
 			gas = runGas(_item.instruction(), m_evmVersion);
-			gas += memoryGas(classes.find(Instruction::ADD, {
-				m_state->relativeStackElement(0),
-				classes.find(AssemblyItem(32))
-			}));
+			gas += memoryGas(m_state->relativeStackElement(0), u256(32));
 			break;
 		case Instruction::MSTORE8:
 			gas = runGas(_item.instruction(), m_evmVersion);
-			gas += memoryGas(classes.find(Instruction::ADD, {
-				m_state->relativeStackElement(0),
-				classes.find(AssemblyItem(1))
-			}));
+			gas += memoryGas(m_state->relativeStackElement(0), u256(1));
 			break;
 		case Instruction::KECCAK256:
 			gas = GasCosts::keccak256Gas;
@@ -113,11 +109,18 @@ GasMeter::GasConsumption GasMeter::estimateMax(AssemblyItem const& _item, bool _
 			break;
 		case Instruction::MCOPY:
 		{
-			GasConsumption memoryGasFromRead = memoryGas(-1, -2);
-			GasConsumption memoryGasFromWrite = memoryGas(0, -2);
-
 			gas = runGas(_item.instruction(), m_evmVersion);
-			gas += (memoryGasFromRead < memoryGasFromWrite ? memoryGasFromWrite : memoryGasFromRead);
+			ExpressionClasses::Id sizeExpression = m_state->relativeStackElement(-2);
+			if (!classes.knownZero(sizeExpression))
+			{
+				u256 const* source = classes.knownConstant(m_state->relativeStackElement(-1));
+				u256 const* destination = classes.knownConstant(m_state->relativeStackElement(0));
+				u256 const* size = classes.knownConstant(sizeExpression);
+				if (!source || !destination || !size)
+					gas = GasConsumption::infinite();
+				else
+					gas += memoryGas(bigint(std::max(*source, *destination)) + *size);
+			}
 			gas += wordGas(GasCosts::copyGas, m_state->relativeStackElement(-2));
 			break;
 		}
@@ -192,6 +195,8 @@ GasMeter::GasConsumption GasMeter::estimateMax(AssemblyItem const& _item, bool _
 			{
 				gas = GasCosts::createGas;
 				gas += memoryGas(-1, -2);
+				if (_item.instruction() == Instruction::CREATE2)
+					gas += wordGas(GasCosts::create2WordGasInTVM, m_state->relativeStackElement(-2));
 			}
 			break;
 		case Instruction::EXP:
@@ -202,11 +207,11 @@ GasMeter::GasConsumption GasMeter::estimateMax(AssemblyItem const& _item, bool _
 				{
 					// Note: msb() counts from 0 and throws on 0 as input.
 					unsigned const significantByteCount  = (static_cast<unsigned>(boost::multiprecision::msb(*value)) + 1u + 7u) / 8u;
-					gas += GasCosts::expByteGas(m_evmVersion) * significantByteCount;
+					gas += GasCosts::expByteGasInTVM * significantByteCount;
 				}
 			}
 			else
-				gas += GasCosts::expByteGas(m_evmVersion) * 32;
+				gas += GasCosts::expByteGasInTVM * 32;
 			break;
 		case Instruction::BALANCE:
 		case Instruction::TOKENBALANCE:
@@ -267,55 +272,66 @@ GasMeter::GasConsumption GasMeter::wordGas(u256 const& _multiplier, ExpressionCl
 	u256 const* value = m_state->expressionClasses().knownConstant(_value);
 	if (!value)
 		return GasConsumption::infinite();
-	return GasConsumption(_multiplier * ((*value + 31) / 32));
+	bigint gas = bigint(_multiplier) * ((bigint(*value) + 31) / 32);
+	if (gas > std::numeric_limits<u256>::max())
+		return GasConsumption::infinite();
+	return GasConsumption(u256(gas));
 }
 
-GasMeter::GasConsumption GasMeter::memoryGas(ExpressionClasses::Id _position)
+GasMeter::GasConsumption GasMeter::memoryGas(bigint const& _position)
 {
-	u256 const* value = m_state->expressionClasses().knownConstant(_position);
-	if (!value)
+	if (
+		_position < 0 ||
+		_position > GasCosts::memorySizeLimitInTVM ||
+		bigint(m_largestMemoryAccess) > GasCosts::memorySizeLimitInTVM
+	)
 		return GasConsumption::infinite();
-	if (*value < m_largestMemoryAccess)
+	u256 const value = u256(_position);
+	if (value < m_largestMemoryAccess)
 		return GasConsumption(0);
 	u256 previous = m_largestMemoryAccess;
-	m_largestMemoryAccess = *value;
+	m_largestMemoryAccess = value;
 	auto memGas = [=](u256 const& pos) -> u256
 	{
 		u256 size = (pos + 31) / 32;
 		return GasCosts::memoryGas * size + size * size / GasCosts::quadCoeffDiv;
 	};
-	return memGas(*value) - memGas(previous);
+	return memGas(value) - memGas(previous);
+}
+
+GasMeter::GasConsumption GasMeter::memoryGas(ExpressionClasses::Id _offset, u256 const& _size)
+{
+	u256 const* offset = m_state->expressionClasses().knownConstant(_offset);
+	if (!offset)
+		return GasConsumption::infinite();
+	return memoryGas(bigint(*offset) + _size);
 }
 
 GasMeter::GasConsumption GasMeter::memoryGas(int _stackPosOffset, int _stackPosSize)
 {
 	ExpressionClasses& classes = m_state->expressionClasses();
-	if (classes.knownZero(m_state->relativeStackElement(_stackPosSize)))
+	ExpressionClasses::Id offsetExpression = m_state->relativeStackElement(_stackPosOffset);
+	ExpressionClasses::Id sizeExpression = m_state->relativeStackElement(_stackPosSize);
+	if (classes.knownZero(sizeExpression))
 		return GasConsumption(0);
-	else
-		return memoryGas(classes.find(Instruction::ADD, {
-			m_state->relativeStackElement(_stackPosOffset),
-			m_state->relativeStackElement(_stackPosSize)
-		}));
+	u256 const* offset = classes.knownConstant(offsetExpression);
+	u256 const* size = classes.knownConstant(sizeExpression);
+	if (!offset || !size)
+		return GasConsumption::infinite();
+	return memoryGas(bigint(*offset) + *size);
 }
 
 GasMeter::GasConsumption GasMeter::memoryGasForWordArray(int _stackPosOffset, int _stackPosElementCount)
 {
 	ExpressionClasses& classes = m_state->expressionClasses();
 	// The TVM reads and charges the 32-byte length slot even for empty arrays,
 	// so unlike memoryGas(int, int) there is no zero-size shortcut here.
-	ExpressionClasses::Id byteSize = classes.find(Instruction::MUL, {
-		m_state->relativeStackElement(_stackPosElementCount),
-		classes.find(u256(32))
-	});
-	ExpressionClasses::Id byteSizeWithLengthSlot = classes.find(Instruction::ADD, {
-		byteSize,
-		classes.find(u256(32))
-	});
-	return memoryGas(classes.find(Instruction::ADD, {
-		m_state->relativeStackElement(_stackPosOffset),
-		byteSizeWithLengthSlot
-	}));
+	u256 const* offset = classes.knownConstant(m_state->relativeStackElement(_stackPosOffset));
+	u256 const* elementCount = classes.knownConstant(m_state->relativeStackElement(_stackPosElementCount));
+	if (!offset || !elementCount)
+		return GasConsumption::infinite();
+	bigint const byteSizeWithLengthSlot = bigint(*elementCount) * 32 + 32;
+	return memoryGas(bigint(*offset) + byteSizeWithLengthSlot);
 }
 
 namespace

libevmasm/GasMeter.h

@@ -190,6 +190,9 @@ namespace GasCosts
 	static unsigned const extCodeHashGasInTVM = 400;
 	static unsigned const callGasInTVM = 40;
 	static unsigned const selfdestructGasInTVM = 5000;
+	static unsigned const expByteGasInTVM = 10;
+	static unsigned const create2WordGasInTVM = 6;
+	static unsigned const memorySizeLimitInTVM = 3 * 1024 * 1024;
 
 	static unsigned const freezeV1GasInTVM = 20000;
 	static unsigned const freezeExpireTimeGasInTVM = 50;
@@ -267,11 +270,13 @@ class GasMeter
 	static u256 dataGas(uint64_t _length, bool _inCreation, langutil::EVMVersion _evmVersion);
 
 private:
-	/// @returns _multiplier * (_value + 31) / 32, if _value is a known constant and infinite otherwise.
+	/// @returns _multiplier * ceil(_value / 32), if _value is a known constant and infinite otherwise.
 	GasConsumption wordGas(u256 const& _multiplier, ExpressionClasses::Id _value);
-	/// @returns the gas needed to access the given memory position.
+	/// @returns the gas needed to access the given memory end position.
 	/// @todo this assumes that memory was never accessed before and thus over-estimates gas usage.
-	GasConsumption memoryGas(ExpressionClasses::Id _position);
+	GasConsumption memoryGas(bigint const& _position);
+	/// @returns the memory gas for a known-size access starting at an offset on the stack.
+	GasConsumption memoryGas(ExpressionClasses::Id _offset, u256 const& _size);
 	/// @returns the memory gas for accessing the memory at a specific offset for a number of bytes
 	/// given as values on the stack at the given relative positions.
 	GasConsumption memoryGas(int _stackPosOffset, int _stackPosSize);

libsolidity/formal/Predicate.cpp

@@ -253,7 +253,12 @@ std::string Predicate::formatSummaryCall(
 					if (magicKind == MagicType::Kind::Block && memberName == "difficulty")
 						memberName = "prevrandao";
 
-					if (magicKind == MagicType::Kind::Block || magicKind == MagicType::Kind::Message || magicKind == MagicType::Kind::Transaction)
+					if (
+						magicKind == MagicType::Kind::Block ||
+						magicKind == MagicType::Kind::Chain ||
+						magicKind == MagicType::Kind::Message ||
+						magicKind == MagicType::Kind::Transaction
+					)
 						txVars.insert(magicType->toString(true) + "." + memberName);
 				}
 				return true;

libsolidity/formal/SMTEncoder.cpp

@@ -741,6 +741,8 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		// not modeled explicitly, conservatively invalidate the symbolic blockchain
 		// state so balances and other observable state cannot remain falsely stable.
 		state().newState();
+		if (!funType.returnParameterTypes().empty())
+			setSymbolicUnknownValue(*m_context.expression(_funCall), m_context);
 		m_unsupportedErrors.warning(
 			4588_error,
 			_funCall.location(),
@@ -1470,7 +1472,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		if (auto const* identifier = dynamic_cast<Identifier const*>(&memberExpr))
 		{
 			auto const& name = identifier->name();
-			solAssert(name == "block" || name == "msg" || name == "tx", "");
+			solAssert(name == "block" || name == "chain" || name == "msg" || name == "tx", "");
 			auto memberName = _memberAccess.memberName();
 
 			// TODO remove this for 0.9.0

libsolidity/formal/SymbolicState.cpp

@@ -234,20 +234,34 @@ smtutil::Expression SymbolicState::txTypeConstraints() const
 		smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.number"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.timestamp"), TypeProvider::uint256()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("chain.totalEnergyCurrentLimit"), TypeProvider::uint(64)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("chain.totalEnergyWeight"), TypeProvider::uint(64)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("chain.totalNetLimit"), TypeProvider::uint(64)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("chain.totalNetWeight"), TypeProvider::uint(64)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("chain.unfreezeDelayDays"), TypeProvider::uint(64)) &&
 		smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::address()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("msg.tokenid"), TypeProvider::trcToken()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("msg.tokenvalue"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("msg.value"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::address()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("tx.gasprice"), TypeProvider::uint256());
 }
 
 smtutil::Expression SymbolicState::txNonPayableConstraint() const
 {
-	return m_tx.member("msg.value") == 0;
+	return
+		m_tx.member("msg.value") == 0 &&
+		m_tx.member("msg.tokenid") == 0 &&
+		m_tx.member("msg.tokenvalue") == 0;
 }
 
 smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition const& _function) const
 {
-	smtutil::Expression conj = _function.isPayable() ? smtutil::Expression(true) : txNonPayableConstraint();
+	// Library functions inherit the caller's transaction values through DELEGATECALL.
+	smtutil::Expression conj =
+		(_function.isPayable() || _function.libraryFunction()) ?
+		smtutil::Expression(true) :
+		txNonPayableConstraint();
 	if (_function.isPartOfExternalInterface())
 	{
 		auto sig = TypeProvider::function(_function)->externalIdentifier();

libsolidity/formal/SymbolicTypes.cpp

@@ -682,9 +682,16 @@ std::map<std::string, frontend::Type const*> transactionMemberTypes()
 		{"block.timestamp", TypeProvider::uint256()},
 		{"blobhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
 		{"blockhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
+		{"chain.totalEnergyCurrentLimit", TypeProvider::uint(64)},
+		{"chain.totalEnergyWeight", TypeProvider::uint(64)},
+		{"chain.totalNetLimit", TypeProvider::uint(64)},
+		{"chain.totalNetWeight", TypeProvider::uint(64)},
+		{"chain.unfreezeDelayDays", TypeProvider::uint(64)},
 		{"msg.data", TypeProvider::bytesCalldata()},
 		{"msg.sender", TypeProvider::address()},
 		{"msg.sig", TypeProvider::fixedBytes(4)},
+		{"msg.tokenid", TypeProvider::trcToken()},
+		{"msg.tokenvalue", TypeProvider::uint256()},
 		{"msg.value", TypeProvider::uint256()},
 		{"tx.gasprice", TypeProvider::uint256()},
 		{"tx.origin", TypeProvider::address()}

libsolidity/interface/StandardCompiler.cpp

@@ -400,7 +400,7 @@ Json formatImmutableReferences(std::map<u256, evmasm::LinkerObject::ImmutableRef
 
 std::optional<Json> checkKeys(Json const& _input, std::set<std::string> const& _keys, std::string const& _name)
 {
-	if (!_input.empty() && !_input.is_object())
+	if (!_input.is_object())
 		return formatFatalError(Error::Type::JSONError, "\"" + _name + "\" must be an object");
 
 	for (auto const& [member, _]: _input.items())
@@ -526,7 +526,7 @@ std::optional<Json> checkMetadataKeys(Json const& _input)
 
 std::optional<Json> checkOutputSelection(Json const& _outputSelection)
 {
-	if (!_outputSelection.empty() && !_outputSelection.is_object())
+	if (!_outputSelection.is_object())
 		return formatFatalError(Error::Type::JSONError, "\"settings.outputSelection\" must be an object");
 
 	for (auto const& [sourceName, sourceVal]: _outputSelection.items())
@@ -649,6 +649,8 @@ std::variant<StandardCompiler::InputsAndSettings, Json> StandardCompiler::parseI
 	if (auto result = checkRootKeys(_input))
 		return *result;
 
+	if (_input.contains("language") && !_input["language"].is_string())
+		return formatFatalError(Error::Type::JSONError, "\"language\" must be a string.");
 	ret.language = _input.value<std::string>("language", "");
 
 	Json const& sources = _input.value<Json>("sources", Json());
@@ -772,31 +774,28 @@ std::variant<StandardCompiler::InputsAndSettings, Json> StandardCompiler::parseI
 	if (!auxInputs.empty())
 	{
 		Json const& smtlib2Responses = auxInputs.value("smtlib2responses", Json::object());
-		if (!smtlib2Responses.empty())
-		{
-			if (!smtlib2Responses.is_object())
-				return formatFatalError(Error::Type::JSONError, "\"auxiliaryInput.smtlib2responses\" must be an object.");
+		if (!smtlib2Responses.is_object())
+			return formatFatalError(Error::Type::JSONError, "\"auxiliaryInput.smtlib2responses\" must be an object.");
 
-			for (auto const& [hashString, response]: smtlib2Responses.items())
+		for (auto const& [hashString, response]: smtlib2Responses.items())
+		{
+			util::h256 hash;
+			try
 			{
-				util::h256 hash;
-				try
-				{
-					hash = util::h256(hashString);
-				}
-				catch (util::BadHexCharacter const&)
-				{
-					return formatFatalError(Error::Type::JSONError, "Invalid hex encoding of SMTLib2 auxiliary input.");
-				}
+				hash = util::h256(hashString);
+			}
+			catch (util::BadHexCharacter const&)
+			{
+				return formatFatalError(Error::Type::JSONError, "Invalid hex encoding of SMTLib2 auxiliary input.");
+			}
 
-				if (!response.is_string())
-					return formatFatalError(
-						Error::Type::JSONError,
-						"\"smtlib2Responses." + hashString + "\" must be a string."
-					);
+			if (!response.is_string())
+				return formatFatalError(
+					Error::Type::JSONError,
+					"\"smtlib2Responses." + hashString + "\" must be a string."
+				);
 
-				ret.smtLib2Responses[hash] = response.get<std::string>();
-			}
+			ret.smtLib2Responses[hash] = response.get<std::string>();
 		}
 	}
 
@@ -872,7 +871,11 @@ std::variant<StandardCompiler::InputsAndSettings, Json> StandardCompiler::parseI
 
 			std::vector<std::string> components;
 			for (Json const& arrayValue: settings["debug"]["debugInfo"])
+			{
+				if (!arrayValue.is_string())
+					return formatFatalError(Error::Type::JSONError, "Every value in settings.debug.debugInfo must be a string.");
 				components.push_back(arrayValue.get<std::string>());
+			}
 
 			std::optional<DebugInfoSelection> debugInfoSelection = DebugInfoSelection::fromComponents(
 				components,

libyul/backends/evm/EVMMetrics.cpp

@@ -115,7 +115,7 @@ bigint GasMeterVisitor::singleByteDataGas() const
 void GasMeterVisitor::instructionCostsInternal(evmasm::Instruction _instruction)
 {
 	if (_instruction == evmasm::Instruction::EXP)
-		m_runGas += evmasm::GasCosts::expGas + evmasm::GasCosts::expByteGas(m_dialect.evmVersion());
+		m_runGas += evmasm::GasCosts::expGas + evmasm::GasCosts::expByteGasInTVM;
 	else if (_instruction == evmasm::Instruction::KECCAK256)
 		// Assumes that Keccak-256 is computed on a single word (rounded up).
 		m_runGas += evmasm::GasCosts::keccak256Gas + evmasm::GasCosts::keccak256WordGas;