[SMTChecker] Support structs

libsolidity/formal/SMTEncoder.cpp

@@ -492,7 +492,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			auto innerValue = expr(*subExpr);
 			auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
 			defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
-			arrayIndexAssignment(*subExpr, newValue);
+			indexOrMemberAssignment(_op.subExpression(), newValue);
 		}
 		else
 			m_errorReporter.warning(
@@ -521,8 +521,11 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			auto const& symbVar = m_context.expression(*subExpr);
 			symbVar->increaseIndex();
 			m_context.setZeroValue(*symbVar);
-			if (dynamic_cast<IndexAccess const*>(subExpr))
+			if (
-				arrayIndexAssignment(*subExpr, symbVar->currentValue());
+				dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
+				dynamic_cast<MemberAccess const*>(&_op.subExpression())
+			)
+				indexOrMemberAssignment(_op.subExpression(), symbVar->currentValue());
 			else
 				m_errorReporter.warning(
 					2683_error,
@@ -893,6 +896,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
 		return false;
 	}
+	else if (exprType->category() == Type::Category::Struct)
+	{
+		_memberAccess.expression().accept(*this);
+		auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(_memberAccess.expression()));
+		defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName()));
+		return false;
+	}
 	else if (exprType->category() == Type::Category::TypeType)
 	{
 		if (identifier && dynamic_cast<EnumDefinition const*>(identifier->annotation().referencedDeclaration))
@@ -964,19 +974,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		solAssert(varDecl, "");
 		array = m_context.variable(*varDecl);
 	}
-	else if (auto const* innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
-	{
-		solAssert(m_context.knownExpression(*innerAccess), "");
-		array = m_context.expression(*innerAccess);
-	}
 	else
 	{
-		m_errorReporter.warning(
+		solAssert(m_context.knownExpression(_indexAccess.baseExpression()), "");
-			9118_error,
+		array = m_context.expression(_indexAccess.baseExpression());
-			_indexAccess.location(),
-			"Assertion checker does not yet implement this expression."
-		);
-		return;
 	}
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
@@ -1008,14 +1009,44 @@ void SMTEncoder::arrayAssignment()
 	m_arrayAssignmentHappened = true;
 }
 
-void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
+void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
 {
 	auto toStore = _rightHandSide;
-	auto indexAccess = dynamic_cast<IndexAccess const*>(&_expr);
+	auto const* lastExpr = &_expr;
-	solAssert(indexAccess, "");
 	while (true)
 	{
-		if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess->baseExpression()))
+		if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(lastExpr))
+		{
+			auto const& base = indexAccess->baseExpression();
+			if (dynamic_cast<Identifier const*>(&base))
+				base.accept(*this);
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
+			solAssert(symbArray, "");
+			auto baseType = symbArray->type();
+			toStore = smtutil::Expression::tuple_constructor(
+				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
+				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+			);
+			m_context.expression(*indexAccess)->increaseIndex();
+			defineExpr(*indexAccess, smtutil::Expression::select(
+				symbArray->elements(),
+				expr(*indexAccess->indexExpression())
+			));
+			lastExpr = &indexAccess->baseExpression();
+		}
+		else if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(lastExpr))
+		{
+			auto const& base = memberAccess->expression();
+			if (dynamic_cast<Identifier const*>(&base))
+				base.accept(*this);
+			auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
+			solAssert(symbStruct, "");
+			symbStruct->assignMember(memberAccess->memberName(), toStore);
+			toStore = symbStruct->currentValue();
+			defineExpr(*memberAccess, symbStruct->member(memberAccess->memberName()));
+			lastExpr = &memberAccess->expression();
+		}
+		else if (auto const& id = dynamic_cast<Identifier const*>(lastExpr))
 		{
 			auto varDecl = identifierToVariable(*id);
 			solAssert(varDecl, "");
@@ -1023,36 +1054,11 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi
 			if (varDecl->hasReferenceOrMappingType())
 				resetReferences(*varDecl);
 
-			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
+			m_context.addAssertion(m_context.newValue(*varDecl) == toStore);
-			smtutil::Expression store = smtutil::Expression::store(
+			m_context.expression(*id)->increaseIndex();
-				symbArray->elements(),
+			defineExpr(*id,currentValue(*varDecl));
-				expr(*indexAccess->indexExpression()),
-				toStore
-			);
-			auto oldLength = symbArray->length();
-			symbArray->increaseIndex();
-			m_context.addAssertion(symbArray->elements() == store);
-			m_context.addAssertion(symbArray->length() == oldLength);
-			// Update the SMT select value after the assignment,
-			// necessary for sound models.
-			defineExpr(*indexAccess, smtutil::Expression::select(
-				symbArray->elements(),
-				expr(*indexAccess->indexExpression())
-			));
-
 			break;
 		}
-		else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
-		{
-			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
-			solAssert(symbArray, "");
-			auto baseType = base->annotation().type;
-			toStore = smtutil::Expression::tuple_constructor(
-				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
-				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
-			);
-			indexAccess = base;
-		}
 		else
 		{
 			m_errorReporter.warning(
@@ -1131,9 +1137,14 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 		if (varDecl->hasReferenceOrMappingType())
 			resetReferences(*varDecl);
 		m_context.addAssertion(m_context.newValue(*varDecl) == _array);
+		m_context.expression(*id)->increaseIndex();
+		defineExpr(*id,currentValue(*varDecl));
 	}
-	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(expr))
+	else if (
-		arrayIndexAssignment(*indexAccess, _array);
+		dynamic_cast<IndexAccess const*>(expr) ||
+		dynamic_cast<MemberAccess const*>(expr)
+	)
+		indexOrMemberAssignment(_expr, _array);
 	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
 	{
 		FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
@@ -1475,8 +1486,11 @@ void SMTEncoder::assignment(
 	}
 	else if (auto varDecl = identifierToVariable(*left))
 		assignment(*varDecl, _right);
-	else if (dynamic_cast<IndexAccess const*>(left))
+	else if (
-		arrayIndexAssignment(*left, _right);
+		dynamic_cast<IndexAccess const*>(left) ||
+		dynamic_cast<MemberAccess const*>(left)
+	)
+		indexOrMemberAssignment(*left, _right);
 	else
 		m_errorReporter.warning(
 			8182_error,

libsolidity/formal/SMTEncoder.h

@@ -146,8 +146,8 @@ protected:
 	/// to variable of some SMT array type
 	/// while aliasing is not supported.
 	void arrayAssignment();
-	/// Handles assignment to SMT array index.
+	/// Handles assignments to index or member access.
-	void arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
+	void indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
 
 	void arrayPush(FunctionCall const& _funCall);
 	void arrayPop(FunctionCall const& _funCall);

libsolidity/formal/SymbolicTypes.cpp

@@ -25,6 +25,7 @@
 #include <vector>
 
 using namespace std;
+using namespace solidity::util;
 using namespace solidity::smtutil;
 
 namespace solidity::frontend::smt
@@ -130,18 +131,31 @@ SortPointer smtSort(frontend::Type const& _type)
 	}
 	case Kind::Tuple:
 	{
-		auto tupleType = dynamic_cast<frontend::TupleType const*>(&_type);
-		solAssert(tupleType, "");
 		vector<string> members;
-		auto const& tupleName = _type.identifier();
+		auto const& tupleName = _type.toString(true);
+		vector<SortPointer> sorts;
+
+		if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))
+		{
 			auto const& components = tupleType->components();
 			for (unsigned i = 0; i < components.size(); ++i)
 				members.emplace_back(tupleName + "_accessor_" + to_string(i));
-		return make_shared<TupleSort>(
+			sorts = smtSortAbstractFunction(tupleType->components());
-			tupleName,
+		}
-			members,
+		else if (auto const* structType = dynamic_cast<frontend::StructType const*>(&_type))
-			smtSortAbstractFunction(tupleType->components())
+		{
-		);
+			auto const& structMembers = structType->structDefinition().members();
+			for (auto member: structMembers)
+				members.emplace_back(tupleName + "_accessor_" + member->name());
+			sorts = smtSortAbstractFunction(applyMap(
+				structMembers,
+				[](auto var) { return var->type(); }
+			));
+		}
+		else
+			solAssert(false, "");
+
+		return make_shared<TupleSort>(tupleName, members, sorts);
 	}
 	default:
 		// Abstract case.
@@ -185,7 +199,7 @@ Kind smtKind(frontend::Type::Category _category)
 		return Kind::Function;
 	else if (isMapping(_category) || isArray(_category))
 		return Kind::Array;
-	else if (isTuple(_category))
+	else if (isTuple(_category) || isStruct(_category))
 		return Kind::Tuple;
 	// Abstract case.
 	return Kind::Int;
@@ -197,7 +211,8 @@ bool isSupportedType(frontend::Type::Category _category)
 		isBool(_category) ||
 		isMapping(_category) ||
 		isArray(_category) ||
-		isTuple(_category);
+		isTuple(_category) ||
+		isStruct(_category);
 }
 
 bool isSupportedTypeDeclaration(frontend::Type::Category _category)
@@ -277,6 +292,8 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		auto stringType = TypeProvider::stringMemory();
 		var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
 	}
+	else if (isStruct(_type.category()))
+		var = make_shared<SymbolicStructVariable>(type, _uniqueName, _context);
 	else
 		solAssert(false, "");
 	return make_pair(abstract, var);
@@ -370,6 +387,11 @@ bool isStringLiteral(frontend::Type::Category _category)
 	return _category == frontend::Type::Category::StringLiteral;
 }
 
+bool isStruct(frontend::Type::Category _category)
+{
+	return _category == frontend::Type::Category::Struct;
+}
+
 smtutil::Expression minValue(frontend::IntegerType const& _type)
 {
 	return smtutil::Expression(_type.minValue());
@@ -421,11 +443,24 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 
 			solAssert(zeroArray, "");
 			return smtutil::Expression::tuple_constructor(
-				smtutil::Expression(std::make_shared<SortSort>(smtSort(*_type)), _type->toString(true)),
+				smtutil::Expression(std::make_shared<SortSort>(tupleSort), tupleSort->name),
 				vector<smtutil::Expression>{*zeroArray, length}
 			);
 
 		}
+		if (isStruct(_type->category()))
+		{
+			auto const* structType = dynamic_cast<StructType const*>(_type);
+			solAssert(structType, "");
+			auto structSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
+			return smtutil::Expression::tuple_constructor(
+				smtutil::Expression(make_shared<SortSort>(structSort), structSort->name),
+				applyMap(
+					structType->structDefinition().members(),
+					[](auto var) { return zeroValue(var->type()); }
+				)
+			);
+		}
 		solAssert(false, "");
 	}
 	// Unsupported types are abstracted as Int.

libsolidity/formal/SymbolicTypes.h

@@ -57,6 +57,7 @@ bool isMapping(frontend::Type::Category _category);
 bool isArray(frontend::Type::Category _category);
 bool isTuple(frontend::Type::Category _category);
 bool isStringLiteral(frontend::Type::Category _category);
+bool isStruct(frontend::Type::Category _category);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,

libsolidity/formal/SymbolicVariables.cpp

@@ -21,8 +21,11 @@
 #include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/ast/AST.h>
 
+#include <libsolutil/Algorithms.h>
+
 using namespace std;
 using namespace solidity;
+using namespace solidity::util;
 using namespace solidity::smtutil;
 using namespace solidity::frontend;
 using namespace solidity::frontend::smt;
@@ -319,3 +322,47 @@ smtutil::Expression SymbolicArrayVariable::length()
 {
 	return m_pair.component(1);
 }
+
+SymbolicStructVariable::SymbolicStructVariable(
+	frontend::TypePointer _type,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(_type, _type, move(_uniqueName), _context)
+{
+	solAssert(isStruct(m_type->category()), "");
+	auto const* structType = dynamic_cast<StructType const*>(_type);
+	solAssert(structType, "");
+	auto const& members = structType->structDefinition().members();
+	for (unsigned i = 0; i < members.size(); ++i)
+	{
+		solAssert(members.at(i), "");
+		m_memberIndices.emplace(members.at(i)->name(), i);
+	}
+}
+
+smtutil::Expression SymbolicStructVariable::member(string const& _member)
+{
+	return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member));
+}
+
+smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, smtutil::Expression const& _memberValue)
+{
+	auto const* structType = dynamic_cast<StructType const*>(m_type);
+	solAssert(structType, "");
+	auto const& structDef = structType->structDefinition();
+	auto const& structMembers = structDef.members();
+	auto oldMembers = applyMap(
+		structMembers,
+		[&](auto _member) { return member(_member->name()); }
+	);
+	increaseIndex();
+	for (unsigned i = 0; i < structMembers.size(); ++i)
+	{
+		auto const& memberName = structMembers.at(i)->name();
+		auto newMember = memberName == _member ? _memberValue : oldMembers.at(i);
+		m_context.addAssertion(member(memberName) == newMember);
+	}
+
+	return currentValue();
+}

libsolidity/formal/SymbolicVariables.h

@@ -23,6 +23,8 @@
 #include <libsolidity/ast/TypeProvider.h>
 
 #include <libsmtutil/SolverInterface.h>
+
+#include <map>
 #include <memory>
 
 namespace solidity::frontend::smt
@@ -265,4 +267,29 @@ private:
 	SymbolicTupleVariable m_pair;
 };
 
+/**
+ * Specialization of SymbolicVariable for Struct.
+ */
+class SymbolicStructVariable: public SymbolicVariable
+{
+public:
+	SymbolicStructVariable(
+		frontend::TypePointer _type,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+
+	/// @returns the symbolic expression representing _member.
+	smtutil::Expression member(std::string const& _member);
+
+	/// @returns the symbolic expression representing this struct
+	/// with field _member updated.
+	smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _memberValue);
+
+private:
+	std::map<std::string, unsigned> m_memberIndices;
+};
+
+
+
 }