Merge pull request #10033 from ethereum/develop

Merge develop into breaking

libsolidity/ast/Types.cpp

@@ -3006,8 +3006,11 @@ TypePointers FunctionType::returnParameterTypesWithoutDynamicTypes() const
 		m_kind == Kind::BareStaticCall
 	)
 		for (auto& param: returnParameterTypes)
-			if (param->isDynamicallyEncoded() && !param->dataStoredIn(DataLocation::Storage))
+		{
+			solAssert(param->decodingType(), "");
+			if (param->decodingType()->isDynamicallyEncoded())
 				param = TypeProvider::inaccessibleDynamic();
+		}
 
 	return returnParameterTypes;
 }

libsolidity/codegen/ExpressionCompiler.cpp

@@ -170,7 +170,16 @@ void ExpressionCompiler::appendStateVariableAccessor(VariableDeclaration const&
 			// pop offset
 			m_context << Instruction::POP;
 			utils().copyToStackTop(paramTypes.size() - i + 1, 1);
-			ArrayUtils(m_context).accessIndex(*arrayType);
+
+			ArrayUtils(m_context).retrieveLength(*arrayType, 1);
+			// Stack: ref [length] index length
+			// check out-of-bounds access
+			m_context << Instruction::DUP2 << Instruction::LT;
+			auto tag = m_context.appendConditionalJump();
+			m_context << u256(0) << Instruction::DUP1 << Instruction::REVERT;
+			m_context << tag;
+
+			ArrayUtils(m_context).accessIndex(*arrayType, false);
 			returnType = arrayType->baseType();
 		}
 		else

libsolidity/codegen/ReturnInfo.cpp

@@ -41,16 +41,17 @@ ReturnInfo::ReturnInfo(EVMVersion const& _evmVersion, FunctionType const& _funct
 			returnTypes = _functionType.returnParameterTypesWithoutDynamicTypes();
 
 		for (auto const& retType: returnTypes)
-			if (retType->isDynamicallyEncoded())
+		{
+			solAssert(retType->decodingType(), "");
+			if (retType->decodingType()->isDynamicallyEncoded())
 			{
 				solAssert(haveReturndatacopy, "");
 				dynamicReturnSize = true;
 				estimatedReturnSize = 0;
 				break;
 			}
-			else if (retType->decodingType())
-				estimatedReturnSize += retType->decodingType()->calldataEncodedSize();
 			else
-				estimatedReturnSize += retType->calldataEncodedSize();
+				estimatedReturnSize += retType->decodingType()->calldataEncodedSize();
+		}
 	}
 }

libsolidity/codegen/YulUtilFunctions.cpp

@@ -918,7 +918,7 @@ string YulUtilFunctions::arrayLengthFunction(ArrayType const& _type)
 	string functionName = "array_length_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
 		Whiskers w(R"(
-			function <functionName>(value) -> length {
+			function <functionName>(value<?dynamic><?calldata>, len</calldata></dynamic>) -> length {
 				<?dynamic>
 					<?memory>
 						length := mload(value)
@@ -929,6 +929,9 @@ string YulUtilFunctions::arrayLengthFunction(ArrayType const& _type)
 							length := <extractByteArrayLength>(length)
 						</byteArray>
 					</storage>
+					<?calldata>
+						length := len
+					</calldata>
 				<!dynamic>
 					length := <length>
 				</dynamic>
@@ -940,17 +943,14 @@ string YulUtilFunctions::arrayLengthFunction(ArrayType const& _type)
 			w("length", toCompactHexWithPrefix(_type.length()));
 		w("memory", _type.location() == DataLocation::Memory);
 		w("storage", _type.location() == DataLocation::Storage);
+		w("calldata", _type.location() == DataLocation::CallData);
 		if (_type.location() == DataLocation::Storage)
 		{
 			w("byteArray", _type.isByteArray());
 			if (_type.isByteArray())
 				w("extractByteArrayLength", extractByteArrayLengthFunction());
 		}
-		if (_type.isDynamicallySized())
-			solAssert(
-				_type.location() != DataLocation::CallData,
-				"called regular array length function on calldata array"
-			);
+
 		return w.render();
 	});
 }
@@ -1295,6 +1295,105 @@ string YulUtilFunctions::clearStorageStructFunction(StructType const& _type)
 	});
 }
 
+string YulUtilFunctions::copyArrayToStorage(ArrayType const& _fromType, ArrayType const& _toType)
+{
+	solAssert(
+		*_fromType.copyForLocation(_toType.location(), _toType.isPointer()) == dynamic_cast<ReferenceType const&>(_toType),
+		""
+	);
+	solUnimplementedAssert(!_fromType.isByteArray(), "");
+	solUnimplementedAssert(!_fromType.dataStoredIn(DataLocation::Storage), "");
+
+	string functionName = "copy_array_to_storage_from_" + _fromType.identifier() + "_to_" + _toType.identifier();
+	return m_functionCollector.createFunction(functionName, [&](){
+		Whiskers templ(R"(
+			function <functionName>(slot, value<?isFromDynamicCalldata>, len</isFromDynamicCalldata>) {
+				let length := <arrayLength>(value<?isFromDynamicCalldata>, len</isFromDynamicCalldata>)
+				<?isToDynamic>
+					<resizeArray>(slot, length)
+				</isToDynamic>
+
+				let srcPtr :=
+				<?isFromMemoryDynamic>
+					add(value, 0x20)
+				<!isFromMemoryDynamic>
+					value
+				</isFromMemoryDynamic>
+
+				let elementSlot := <dstDataLocation>(slot)
+				let elementOffset := 0
+
+				for { let i := 0 } lt(i, length) {i := add(i, 1)} {
+					<?fromCalldata>
+						let <elementValues> :=
+						<?dynamicallyEncodedBase>
+							<accessCalldataTail>(value, srcPtr)
+						<!dynamicallyEncodedBase>
+							srcPtr
+						</dynamicallyEncodedBase>
+
+						<?isValueType>
+							<elementValues> := <readFromCalldataOrMemory>(<elementValues>)
+						</isValueType>
+					</fromCalldata>
+
+					<?fromMemory>
+						let <elementValues> := <readFromCalldataOrMemory>(srcPtr)
+					</fromMemory>
+
+					<updateStorageValue>(elementSlot<?isValueType>, elementOffset</isValueType>, <elementValues>)
+
+					srcPtr := add(srcPtr, <stride>)
+
+					<?multipleItemsPerSlot>
+						elementOffset := add(elementOffset, <storageStride>)
+						if gt(elementOffset, sub(32, <storageStride>)) {
+							elementOffset := 0
+							elementSlot := add(elementSlot, 1)
+						}
+					<!multipleItemsPerSlot>
+						elementSlot := add(elementSlot, <storageSize>)
+						elementOffset := 0
+					</multipleItemsPerSlot>
+				}
+			}
+		)");
+		templ("functionName", functionName);
+		bool fromCalldata = _fromType.dataStoredIn(DataLocation::CallData);
+		templ("isFromDynamicCalldata", _fromType.isDynamicallySized() && fromCalldata);
+		templ("fromMemory", _fromType.dataStoredIn(DataLocation::Memory));
+		templ("fromCalldata", fromCalldata);
+		templ("isToDynamic", _toType.isDynamicallySized());
+		templ("isFromMemoryDynamic", _fromType.isDynamicallySized() && _fromType.dataStoredIn(DataLocation::Memory));
+		if (fromCalldata)
+		{
+			templ("dynamicallySizedBase", _fromType.baseType()->isDynamicallySized());
+			templ("dynamicallyEncodedBase", _fromType.baseType()->isDynamicallyEncoded());
+			if (_fromType.baseType()->isDynamicallyEncoded())
+				templ("accessCalldataTail", accessCalldataTailFunction(*_fromType.baseType()));
+		}
+		if (_toType.isDynamicallySized())
+			templ("resizeArray", resizeDynamicArrayFunction(_toType));
+		templ("arrayLength",arrayLengthFunction(_fromType));
+		templ("isValueType", _fromType.baseType()->isValueType());
+		templ("dstDataLocation", arrayDataAreaFunction(_toType));
+		if (!fromCalldata || _fromType.baseType()->isValueType())
+			templ("readFromCalldataOrMemory", readFromMemoryOrCalldata(*_fromType.baseType(), fromCalldata));
+		templ("elementValues", suffixedVariableNameList(
+			"elementValue_",
+			0,
+			_fromType.baseType()->stackItems().size()
+		));
+		templ("updateStorageValue", updateStorageValueFunction(*_fromType.baseType(), *_toType.baseType()));
+		templ("stride", to_string(fromCalldata ? _fromType.calldataStride() : _fromType.memoryStride()));
+		templ("multipleItemsPerSlot", _toType.storageStride() <= 16);
+		templ("storageStride", to_string(_toType.storageStride()));
+		templ("storageSize", _toType.baseType()->storageSize().str());
+
+		return templ.render();
+	});
+}
+
 string YulUtilFunctions::arrayConvertLengthToSize(ArrayType const& _type)
 {
 	string functionName = "array_convert_length_to_size_" + _type.identifier();
@@ -1865,23 +1964,39 @@ string YulUtilFunctions::updateStorageValueFunction(
 		else
 		{
 			auto const* toReferenceType = dynamic_cast<ReferenceType const*>(&_toType);
-			auto const* fromReferenceType = dynamic_cast<ReferenceType const*>(&_toType);
+			auto const* fromReferenceType = dynamic_cast<ReferenceType const*>(&_fromType);
 			solAssert(fromReferenceType && toReferenceType, "");
 			solAssert(*toReferenceType->copyForLocation(
 				fromReferenceType->location(),
 				fromReferenceType->isPointer()
 			).get() == *fromReferenceType, "");
+			solUnimplementedAssert(fromReferenceType->location() != DataLocation::Storage, "");
+			solAssert(toReferenceType->category() == fromReferenceType->category(), "");
 
 			if (_toType.category() == Type::Category::Array)
-				solUnimplementedAssert(false, "");
+			{
+				solAssert(_offset.value_or(0) == 0, "");
+
+				Whiskers templ(R"(
+					function <functionName>(slot, <value>) {
+						<copyArrayToStorage>(slot, <value>)
+					}
+				)");
+				templ("functionName", functionName);
+				templ("value", suffixedVariableNameList("value_", 0, _fromType.sizeOnStack()));
+				templ("copyArrayToStorage", copyArrayToStorage(
+					dynamic_cast<ArrayType const&>(_fromType),
+					dynamic_cast<ArrayType const&>(_toType)
+				));
+
+				return templ.render();
+			}
 			else if (_toType.category() == Type::Category::Struct)
 			{
-				solAssert(_fromType.category() == Type::Category::Struct, "");
 				auto const& fromStructType = dynamic_cast<StructType const&>(_fromType);
 				auto const& toStructType = dynamic_cast<StructType const&>(_toType);
 				solAssert(fromStructType.structDefinition() == toStructType.structDefinition(), "");
-				solAssert(fromStructType.location() != DataLocation::Storage, "");
-				solUnimplementedAssert(_offset.has_value() && _offset.value() == 0, "");
+				solAssert(_offset.value_or(0) == 0, "");
 
 				Whiskers templ(R"(
 					function <functionName>(slot, value) {
@@ -1895,6 +2010,7 @@ string YulUtilFunctions::updateStorageValueFunction(
 				templ("functionName", functionName);
 
 				MemberList::MemberMap structMembers = fromStructType.nativeMembers(nullptr);
+				MemberList::MemberMap toStructMembers = toStructType.nativeMembers(nullptr);
 
 				vector<map<string, string>> memberParams(structMembers.size());
 				for (size_t i = 0; i < structMembers.size(); ++i)
@@ -1902,31 +2018,65 @@ string YulUtilFunctions::updateStorageValueFunction(
 					solAssert(structMembers[i].type->memoryHeadSize() == 32, "");
 					bool fromCalldata = fromStructType.location() == DataLocation::CallData;
 					auto const& [slotDiff, offset] = toStructType.storageOffsetsOfMember(structMembers[i].name);
-					memberParams[i]["updateMemberCall"] = Whiskers(R"(
-						let <memberValues> := <loadFromMemoryOrCalldata>(add(value, <memberOffset>))
-						<updateMember>(add(slot, <memberStorageSlotDiff>), <?hasOffset><memberStorageOffset>,</hasOffset> <memberValues>)
-					)")
-					("memberValues", suffixedVariableNameList(
+
+					Whiskers t(R"(
+						let memberSlot := add(slot, <memberStorageSlotDiff>)
+
+						<?fromCalldata>
+							<?dynamicallyEncodedMember>
+								let <memberCalldataOffset> := <accessCalldataTail>(value, add(value, <memberOffset>))
+							<!dynamicallyEncodedMember>
+								let <memberCalldataOffset> := add(value, <memberOffset>)
+							</dynamicallyEncodedMember>
+
+							<?isValueType>
+								let <memberValues> := <loadFromMemoryOrCalldata>(<memberCalldataOffset>)
+								<updateMember>(memberSlot, <memberStorageOffset>, <memberValues>)
+							<!isValueType>
+								<updateMember>(memberSlot,  <memberCalldataOffset>)
+							</isValueType>
+						<!fromCalldata>
+							let memberMemoryOffset := add(value, <memberOffset>)
+							let <memberValues> := <loadFromMemoryOrCalldata>(memberMemoryOffset)
+							<updateMember>(memberSlot, <?hasOffset><memberStorageOffset>,</hasOffset> <memberValues>)
+						</fromCalldata>
+					)");
+					t("fromCalldata", fromCalldata);
+					if (fromCalldata)
+					{
+						t("memberCalldataOffset", suffixedVariableNameList(
+							"memberCalldataOffset_",
+							0,
+							structMembers[i].type->stackItems().size()
+						));
+						t("dynamicallyEncodedMember", structMembers[i].type->isDynamicallyEncoded());
+						if (structMembers[i].type->isDynamicallySized())
+							t("accessCalldataTail", accessCalldataTailFunction(*structMembers[i].type));
+					}
+					t("isValueType", structMembers[i].type->isValueType());
+					t("memberValues", suffixedVariableNameList(
 						"memberValue_",
 						0,
 						structMembers[i].type->stackItems().size()
-					))
-					("hasOffset", structMembers[i].type->isValueType())
-					(
+					));
+					t("hasOffset", structMembers[i].type->isValueType());
+					t(
 						"updateMember",
 						structMembers[i].type->isValueType() ?
-							updateStorageValueFunction(*structMembers[i].type, *structMembers[i].type) :
-							updateStorageValueFunction(*structMembers[i].type, *structMembers[i].type, offset)
-					)
-					("memberStorageSlotDiff", slotDiff.str())
-					("memberStorageOffset", to_string(offset))
-					("memberOffset",
+							updateStorageValueFunction(*structMembers[i].type, *toStructMembers[i].type) :
+							updateStorageValueFunction(*structMembers[i].type, *toStructMembers[i].type, offset)
+					);
+					t("memberStorageSlotDiff", slotDiff.str());
+					t("memberStorageOffset", to_string(offset));
+					t(
+						"memberOffset",
 						fromCalldata ?
 							to_string(fromStructType.calldataOffsetOfMember(structMembers[i].name)) :
 							fromStructType.memoryOffsetOfMember(structMembers[i].name).str()
-					)
-					("loadFromMemoryOrCalldata", readFromMemoryOrCalldata(*structMembers[i].type, fromCalldata))
-					.render();
+					);
+					if (!fromCalldata || structMembers[i].type->isValueType())
+						t("loadFromMemoryOrCalldata", readFromMemoryOrCalldata(*structMembers[i].type, fromCalldata));
+					memberParams[i]["updateMemberCall"] = t.render();
 				}
 				templ("member", memberParams);
 

libsolidity/codegen/YulUtilFunctions.h

@@ -181,6 +181,10 @@ public:
 	/// signature: (slot) ->
 	std::string clearStorageArrayFunction(ArrayType const& _type);
 
+	/// @returns the name of a function that will copy array from calldata or memory to storage
+	/// signature (to_slot, from_ptr) ->
+	std::string copyArrayToStorage(ArrayType const& _fromType, ArrayType const& _toType);
+
 	/// Returns the name of a function that will convert a given length to the
 	/// size in memory (number of storage slots or calldata/memory bytes) it
 	/// will require.

libsolidity/codegen/ir/IRGenerator.cpp

@@ -348,18 +348,25 @@ string IRGenerator::generateGetter(VariableDeclaration const& _varDecl)
 				mappingType ? *mappingType->keyType() : *TypeProvider::uint256()
 			).stackSlots();
 			parameters += keys;
-			code += Whiskers(R"(
+
+			Whiskers templ(R"(
+				<?array>
+					if iszero(lt(<keys>, <length>(slot))) { revert(0, 0) }
+				</array>
 				slot<?array>, offset</array> := <indexAccess>(slot<?+keys>, <keys></+keys>)
-			)")
-			(
+			)");
+			templ(
 				"indexAccess",
 				mappingType ?
 				m_utils.mappingIndexAccessFunction(*mappingType, *mappingType->keyType()) :
 				m_utils.storageArrayIndexAccessFunction(*arrayType)
 			)
 			("array", arrayType != nullptr)
-			("keys", joinHumanReadable(keys))
-			.render();
+			("keys", joinHumanReadable(keys));
+			if (arrayType)
+				templ("length", m_utils.arrayLengthFunction(*arrayType));
+
+			code += templ.render();
 
 			currentType = mappingType ? mappingType->valueType() : arrayType->baseType();
 		}

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -387,7 +387,11 @@ bool IRGeneratorForStatements::visit(Assignment const& _assignment)
 
 	writeToLValue(*m_currentLValue, value);
 
-	if (m_currentLValue->type.category() != Type::Category::Struct && *_assignment.annotation().type != *TypeProvider::emptyTuple())
+	if (
+		m_currentLValue->type.category() != Type::Category::Struct &&
+		m_currentLValue->type.category() != Type::Category::Array &&
+		*_assignment.annotation().type != *TypeProvider::emptyTuple()
+	)
 		define(_assignment, value);
 	m_currentLValue.reset();
 
@@ -1763,32 +1767,11 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 		auto const& type = dynamic_cast<ArrayType const&>(*_memberAccess.expression().annotation().type);
 
 		if (member == "length")
-		{
-			if (!type.isDynamicallySized())
-				define(_memberAccess) << type.length() << "\n";
-			else
-				switch (type.location())
-				{
-					case DataLocation::CallData:
-						define(_memberAccess, IRVariable(_memberAccess.expression()).part("length"));
-						break;
-					case DataLocation::Storage:
-					{
-						define(_memberAccess) <<
-							m_utils.arrayLengthFunction(type) <<
-							"(" <<
-							IRVariable(_memberAccess.expression()).commaSeparatedList() <<
-							")\n";
-						break;
-					}
-					case DataLocation::Memory:
-						define(_memberAccess) <<
-							"mload(" <<
-							IRVariable(_memberAccess.expression()).commaSeparatedList() <<
-							")\n";
-						break;
-				}
-		}
+			define(_memberAccess) <<
+				m_utils.arrayLengthFunction(type) <<
+				"(" <<
+				IRVariable(_memberAccess.expression()).commaSeparatedList() <<
+				")\n";
 		else if (member == "pop" || member == "push")
 		{
 			solAssert(type.location() == DataLocation::Storage, "");

libsolidity/formal/BMC.cpp

@@ -389,7 +389,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
-	case FunctionType::Kind::BlockHash:
 		SMTEncoder::endVisit(_funCall);
 		abstractFunctionCall(_funCall);
 		break;
@@ -409,6 +408,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		break;
 	}
+	case FunctionType::Kind::BlockHash:
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
 		[[fallthrough]];

libsolidity/formal/CHC.cpp

@@ -120,7 +120,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 		&_contract
 	);
 	addRule(
-		(*implicitConstructorPredicate)({0, state().thisAddress(), state().state()}),
+		(*implicitConstructorPredicate)({0, state().thisAddress(), state().tx(), state().state()}),
 		implicitConstructorPredicate->functor().name
 	);
 	setCurrentBlock(*implicitConstructorPredicate);
@@ -239,8 +239,9 @@ void CHC::endVisit(FunctionDefinition const& _function)
 			auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
 			if (_function.isPublic())
 			{
-				addAssertVerificationTarget(&_function, ifacePre, sum, assertionError);
-				connectBlocks(ifacePre, iface, sum && (assertionError == 0));
+				auto txConstraints = m_context.state().txConstraints(_function);
+				addAssertVerificationTarget(&_function, ifacePre, txConstraints && sum, assertionError);
+				connectBlocks(ifacePre, iface, txConstraints && sum && (assertionError == 0));
 			}
 		}
 		m_currentFunction = nullptr;
@@ -873,7 +874,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
 						auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
 
-						vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state(1)};
+						vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state(1)};
 						args += state1 +
 							applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
 							vector<smtutil::Expression>{state().state(2)} +
@@ -1052,7 +1053,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		return smtutil::Expression(true);
 
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state()};
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	solAssert(funType.kind() == FunctionType::Kind::Internal, "");

libsolidity/formal/Predicate.cpp

@@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 	auto const* fun = programFunction();
 	solAssert(fun, "");
 
-	/// The signature of a function summary predicate is: summary(error, this, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in preInputVars.
-	vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size());
+	vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size());
 	vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
@@ -188,8 +188,8 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 
 vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
-	/// The signature of an implicit constructor summary predicate is: summary(error, this, postBlockchainState, postStateVars).
+	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of an implicit constructor summary predicate is: summary(error, this, txData, preBlockSchainState, postBlockchainState, postStateVars).
 	/// Here we are interested in postStateVars.
 
 	auto stateVars = stateVariables();
@@ -199,12 +199,12 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 	vector<string>::const_iterator stateLast;
 	if (auto const* function = programFunction())
 	{
-		stateFirst = _args.begin() + 3 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
+		stateFirst = _args.begin() + 4 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else if (programContract())
 	{
-		stateFirst = _args.begin() + 3;
+		stateFirst = _args.begin() + 5;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else
@@ -220,7 +220,7 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 
 vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in postInputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -230,7 +230,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
+	vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
 	vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -243,7 +243,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
 
 vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in outputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -253,7 +253,7 @@ vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) c
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
+	vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 

libsolidity/formal/PredicateInstance.cpp

@@ -54,7 +54,7 @@ smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition c
 smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context)
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0)};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
 	return _pred(stateExprs);
 }
 
@@ -64,7 +64,7 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
 		return _pred(currentFunctionVariables(*constructor, &_contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0), state.state()};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
@@ -118,7 +118,7 @@ vector<smtutil::Expression> currentFunctionVariables(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.state(0)};
+	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
 	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
 	exprs += vector<smtutil::Expression>{state.state()};

libsolidity/formal/PredicateSort.cpp

@@ -49,7 +49,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
 SortPointer implicitConstructorSort(SymbolicState& _state)
 {
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()},
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()},
 		SortProvider::boolSort
 	);
 }
@@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
 		return functionSort(*constructor, &_contract, _state);
 
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
@@ -72,7 +72,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} +
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()} +
 			varSorts +
 			inputSorts +
 			vector<SortPointer>{_state.stateSort()} +

libsolidity/formal/PredicateSort.h

@@ -41,19 +41,19 @@ namespace solidity::frontend::smt
  *
  * 3. Implicit constructor
  * The implicit constructor of a contract, that is, without input parameters. Signature:
- * implicit_constructor(error, this, blockchainState).
+ * implicit_constructor(error, this, txData, blockchainState).
  *
  * 4. Constructor entry/summary
  * The summary of an implicit constructor. Signature:
- * constructor_summary(error, this, blockchainState, blockchainState', stateVariables').
+ * constructor_summary(error, this, txData, blockchainState, blockchainState', stateVariables').
  *
  * 5. Function entry/summary
  * The entry point of a function definition. Signature:
- * function_entry(error, this, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
+ * function_entry(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
  *
  * 6. Function body
  * Use for any predicate within a function. Signature:
- * function_body(error, this, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables).
+ * function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables).
  */
 
 /// @returns the interface predicate sort for _contract.

libsolidity/formal/SMTEncoder.cpp

@@ -633,7 +633,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
+		break;
 	case FunctionType::Kind::BlockHash:
+		defineExpr(_funCall, m_context.state().blockhash(expr(*_funCall.arguments().at(0))));
 		break;
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
@@ -1032,7 +1034,11 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 	if (exprType->category() == Type::Category::Magic)
 	{
 		if (identifier)
-			defineGlobalVariable(identifier->name() + "." + _memberAccess.memberName(), _memberAccess);
+		{
+			auto const& name = identifier->name();
+			solAssert(name == "block" || name == "msg" || name == "tx", "");
+			defineExpr(_memberAccess, m_context.state().txMember(name + "." + _memberAccess.memberName()));
+		}
 		else if (auto magicType = dynamic_cast<MagicType const*>(exprType); magicType->kind() == MagicType::Kind::MetaType)
 		{
 			auto const& memberName = _memberAccess.memberName();

libsolidity/formal/SymbolicState.cpp

@@ -26,110 +26,126 @@ using namespace solidity;
 using namespace solidity::smtutil;
 using namespace solidity::frontend::smt;
 
-SymbolicState::SymbolicState(EncodingContext& _context):
+BlockchainVariable::BlockchainVariable(
+	string _name,
+	map<string, smtutil::SortPointer> _members,
+	EncodingContext& _context
+):
+	m_name(move(_name)),
+	m_members(move(_members)),
 	m_context(_context)
 {
-	m_stateMembers.emplace("balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort));
-
 	vector<string> members;
 	vector<SortPointer> sorts;
-	for (auto const& [component, sort]: m_stateMembers)
+	for (auto const& [component, sort]: m_members)
 	{
 		members.emplace_back(component);
 		sorts.emplace_back(sort);
 		m_componentIndices[component] = members.size() - 1;
 	}
-	m_stateTuple = make_unique<SymbolicTupleVariable>(
-		make_shared<smtutil::TupleSort>("state_type", members, sorts),
-		"state",
+	m_tuple = make_unique<SymbolicTupleVariable>(
+		make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts),
+		m_name,
 		m_context
 	);
 }
 
+smtutil::Expression BlockchainVariable::member(string const& _member) const
+{
+	return m_tuple->component(m_componentIndices.at(_member));
+}
+
+smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value)
+{
+	vector<smtutil::Expression> args;
+	for (auto const& m: m_members)
+		if (m.first == _member)
+			args.emplace_back(_value);
+		else
+			args.emplace_back(member(m.first));
+	m_tuple->increaseIndex();
+	auto tuple = m_tuple->currentValue();
+	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
+	m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
+	return m_tuple->currentValue();
+}
+
 void SymbolicState::reset()
 {
 	m_error.resetIndex();
 	m_thisAddress.resetIndex();
-	m_stateTuple->resetIndex();
+	m_state.reset();
+	m_tx.reset();
 }
 
-// Blockchain
-
-SymbolicIntVariable& SymbolicState::errorFlag()
+smtutil::Expression SymbolicState::balances() const
 {
-	return m_error;
+	return m_state.member("balances");
 }
 
-SortPointer SymbolicState::errorFlagSort()
-{
-	return m_error.sort();
-}
-
-smtutil::Expression SymbolicState::thisAddress()
-{
-	return m_thisAddress.currentValue();
-}
-
-smtutil::Expression SymbolicState::thisAddress(unsigned _idx)
-{
-	return m_thisAddress.valueAtIndex(_idx);
-}
-
-SortPointer SymbolicState::thisAddressSort()
-{
-	return m_thisAddress.sort();
-}
-
-smtutil::Expression SymbolicState::state()
-{
-	return m_stateTuple->currentValue();
-}
-
-smtutil::Expression SymbolicState::state(unsigned _idx)
-{
-	return m_stateTuple->valueAtIndex(_idx);
-}
-
-SortPointer SymbolicState::stateSort()
-{
-	return m_stateTuple->sort();
-}
-
-void SymbolicState::newState()
-{
-	m_stateTuple->increaseIndex();
-}
-
-smtutil::Expression SymbolicState::balances()
-{
-	return m_stateTuple->component(m_componentIndices.at("balances"));
-}
-
-smtutil::Expression SymbolicState::balance()
+smtutil::Expression SymbolicState::balance() const
 {
 	return balance(thisAddress());
 }
 
-smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
+smtutil::Expression SymbolicState::balance(smtutil::Expression _address) const
 {
 	return smtutil::Expression::select(balances(), move(_address));
 }
 
+smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) const
+{
+	return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber));
+}
+
 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
-	unsigned indexBefore = m_stateTuple->index();
+	unsigned indexBefore = m_state.index();
 	addBalance(_from, 0 - _value);
 	addBalance(_to, move(_value));
-	unsigned indexAfter = m_stateTuple->index();
+	unsigned indexAfter = m_state.index();
 	solAssert(indexAfter > indexBefore, "");
-	m_stateTuple->increaseIndex();
+	m_state.newVar();
 	/// Do not apply the transfer operation if _from == _to.
 	auto newState = smtutil::Expression::ite(
 		move(_from) == move(_to),
-		m_stateTuple->valueAtIndex(indexBefore),
-		m_stateTuple->valueAtIndex(indexAfter)
+		m_state.value(indexBefore),
+		m_state.value(indexAfter)
 	);
-	m_context.addAssertion(m_stateTuple->currentValue() == newState);
+	m_context.addAssertion(m_state.value() == newState);
+}
+
+smtutil::Expression SymbolicState::txMember(string const& _member) const
+{
+	return m_tx.member(_member);
+}
+
+smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _function) const
+{
+	smtutil::Expression conj = smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::uint(160)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::uint(160)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::uint(160));
+
+	if (_function.isPartOfExternalInterface())
+	{
+		auto sig = TypeProvider::function(_function)->externalIdentifier();
+		conj = conj && m_tx.member("msg.sig") == sig;
+
+		auto b0 = sig >> (3 * 8);
+		auto b1 = (sig & 0x00ff0000) >> (2 * 8);
+		auto b2 = (sig & 0x0000ff00) >> (1 * 8);
+		auto b3 = (sig & 0x000000ff);
+		auto data = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 0);
+		conj = conj && smtutil::Expression::select(data, 0) == b0;
+		conj = conj && smtutil::Expression::select(data, 1) == b1;
+		conj = conj && smtutil::Expression::select(data, 2) == b2;
+		conj = conj && smtutil::Expression::select(data, 3) == b3;
+		auto length = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 1);
+		// TODO add ABI size of function input parameters here \/
+		conj = conj && length >= 4;
+	}
+
+	return conj;
 }
 
 /// Private helpers.
@@ -141,20 +157,5 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
 		_address,
 		balance(_address) + move(_value)
 	);
-	assignStateMember("balances", newBalances);
-}
-
-smtutil::Expression SymbolicState::assignStateMember(string const& _member, smtutil::Expression const& _value)
-{
-	vector<smtutil::Expression> args;
-	for (auto const& member: m_stateMembers)
-		if (member.first == _member)
-			args.emplace_back(_value);
-		else
-			args.emplace_back(m_stateTuple->component(m_componentIndices.at(member.first)));
-	m_stateTuple->increaseIndex();
-	auto tuple = m_stateTuple->currentValue();
-	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
-	m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
-	return m_stateTuple->currentValue();
+	m_state.assignMember("balances", newBalances);
 }

libsolidity/formal/SymbolicState.h

@@ -18,6 +18,7 @@
 
 #pragma once
 
+#include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
 #include <libsmtutil/Sorts.h>
@@ -30,6 +31,31 @@ class EncodingContext;
 class SymbolicAddressVariable;
 class SymbolicArrayVariable;
 
+class BlockchainVariable
+{
+public:
+	BlockchainVariable(std::string _name, std::map<std::string, smtutil::SortPointer> _members, EncodingContext& _context);
+	/// @returns the variable data as a tuple.
+	smtutil::Expression value() const { return m_tuple->currentValue(); }
+	smtutil::Expression value(unsigned _idx) const { return m_tuple->valueAtIndex(_idx); }
+	smtutil::SortPointer const& sort() const { return m_tuple->sort(); }
+	unsigned index() const { return m_tuple->index(); }
+	void newVar() { m_tuple->increaseIndex(); }
+	void reset() { m_tuple->resetIndex(); }
+
+	/// @returns the symbolic _member.
+	smtutil::Expression member(std::string const& _member) const;
+	/// Generates a new tuple where _member is assigned _value.
+	smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _value);
+
+private:
+	std::string const m_name;
+	std::map<std::string, smtutil::SortPointer> const m_members;
+	EncodingContext& m_context;
+	std::map<std::string, unsigned> m_componentIndices;
+	std::unique_ptr<SymbolicTupleVariable> m_tuple;
+};
+
 /**
  * Symbolic representation of the blockchain context:
  * - error flag
@@ -37,49 +63,75 @@ class SymbolicArrayVariable;
  * - state, represented as a tuple of:
  *   - balances
  *   - TODO: potentially storage of contracts
- * - TODO transaction variables
+ * - block and transaction properties, represented as a tuple of:
+ *   - blockhash
+ *   - block coinbase
+ *   - block difficulty
+ *   - block gaslimit
+ *   - block number
+ *   - block timestamp
+ *   - TODO gasleft
+ *   - msg data
+ *   - msg sender
+ *   - msg sig
+ *   - msg value
+ *   - tx gasprice
+ *   - tx origin
  */
 class SymbolicState
 {
 public:
-	SymbolicState(EncodingContext& _context);
+	SymbolicState(EncodingContext& _context): m_context(_context) {}
 
 	void reset();
 
-	/// Blockchain.
+	/// Error flag.
 	//@{
-	SymbolicIntVariable& errorFlag();
-	smtutil::SortPointer errorFlagSort();
+	SymbolicIntVariable& errorFlag() { return m_error; }
+	smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
+	//@}
 
+	/// This.
+	//@{
 	/// @returns the symbolic value of the currently executing contract's address.
-	smtutil::Expression thisAddress();
-	smtutil::Expression thisAddress(unsigned _idx);
-	smtutil::SortPointer thisAddressSort();
-
-	/// @returns the state as a tuple.
-	smtutil::Expression state();
-	smtutil::Expression state(unsigned _idx);
-	smtutil::SortPointer stateSort();
-	void newState();
+	smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); }
+	smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); }
+	smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); }
+	//@}
 
+	/// Blockchain state.
+	//@{
+	smtutil::Expression state() const { return m_state.value(); }
+	smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); }
+	smtutil::SortPointer const& stateSort() const { return m_state.sort(); }
+	void newState() { m_state.newVar(); }
 	/// @returns the symbolic balances.
-	smtutil::Expression balances();
+	smtutil::Expression balances() const;
 	/// @returns the symbolic balance of address `this`.
-	smtutil::Expression balance();
+	smtutil::Expression balance() const;
 	/// @returns the symbolic balance of an address.
-	smtutil::Expression balance(smtutil::Expression _address);
+	smtutil::Expression balance(smtutil::Expression _address) const;
 
 	/// Transfer _value from _from to _to.
 	void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
 	//@}
 
+	/// Transaction data.
+	//@{
+	/// @returns the tx data as a tuple.
+	smtutil::Expression tx() const { return m_tx.value(); }
+	smtutil::Expression tx(unsigned _idx) const { return m_tx.value(_idx); }
+	smtutil::SortPointer const& txSort() const { return m_tx.sort(); }
+	void newTx() { m_tx.newVar(); }
+	smtutil::Expression txMember(std::string const& _member) const;
+	smtutil::Expression txConstraints(FunctionDefinition const& _function) const;
+	smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
+	//@}
+
 private:
 	/// Adds _value to _account's balance.
 	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
 
-	/// Generates a new tuple where _member is assigned _value.
-	smtutil::Expression assignStateMember(std::string const& _member, smtutil::Expression const& _value);
-
 	EncodingContext& m_context;
 
 	SymbolicIntVariable m_error{
@@ -94,10 +146,31 @@ private:
 		m_context
 	};
 
-	std::map<std::string, unsigned> m_componentIndices;
-	/// balances, TODO storage of other contracts
-	std::map<std::string, smtutil::SortPointer> m_stateMembers;
-	std::unique_ptr<SymbolicTupleVariable> m_stateTuple;
+	BlockchainVariable m_state{
+		"state",
+		{{"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}},
+		m_context
+	};
+
+	BlockchainVariable m_tx{
+		"tx",
+		{
+			{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
+			{"block.coinbase", smt::smtSort(*TypeProvider::address())},
+			{"block.difficulty", smtutil::SortProvider::uintSort},
+			{"block.gaslimit", smtutil::SortProvider::uintSort},
+			{"block.number", smtutil::SortProvider::uintSort},
+			{"block.timestamp", smtutil::SortProvider::uintSort},
+			// TODO gasleft
+			{"msg.data", smt::smtSort(*TypeProvider::bytesMemory())},
+			{"msg.sender", smt::smtSort(*TypeProvider::address())},
+			{"msg.sig", smtutil::SortProvider::uintSort},
+			{"msg.value", smtutil::SortProvider::uintSort},
+			{"tx.gasprice", smtutil::SortProvider::uintSort},
+			{"tx.origin", smt::smtSort(*TypeProvider::address())}
+		},
+		m_context
+	};
 };
 
 }

libsolidity/formal/SymbolicTypes.cpp

@@ -18,6 +18,8 @@
 
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsolidity/formal/EncodingContext.h>
+
 #include <libsolidity/ast/TypeProvider.h>
 #include <libsolidity/ast/Types.h>
 #include <libsolutil/CommonData.h>
@@ -535,22 +537,26 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
 }
 
 void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
+{
+	_context.addAssertion(symbolicUnknownConstraints(_expr, _type));
+}
+
+smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type)
 {
 	solAssert(_type, "");
 	if (isEnum(*_type))
 	{
 		auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
 		solAssert(enumType, "");
-		_context.addAssertion(_expr >= 0);
-		_context.addAssertion(_expr < enumType->numberOfMembers());
+		return _expr >= 0 && _expr < enumType->numberOfMembers();
 	}
 	else if (isInteger(*_type))
 	{
 		auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
 		solAssert(intType, "");
-		_context.addAssertion(_expr >= minValue(*intType));
-		_context.addAssertion(_expr <= maxValue(*intType));
+		return _expr >= minValue(*intType) && _expr <= maxValue(*intType);
 	}
+	return smtutil::Expression(true);
 }
 
 optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)

libsolidity/formal/SymbolicTypes.h

@@ -18,7 +18,6 @@
 
 #pragma once
 
-#include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/Types.h>
@@ -26,6 +25,8 @@
 namespace solidity::frontend::smt
 {
 
+class EncodingContext;
+
 /// Returns the SMT sort that models the Solidity type _type.
 smtutil::SortPointer smtSort(frontend::Type const& _type);
 std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
@@ -77,6 +78,7 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
 void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
 void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
+smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type);
 
 std::optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
 }

libsolidity/formal/SymbolicVariables.cpp

@@ -18,6 +18,7 @@
 
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/ast/AST.h>