From 5d9dd654cf6152a63b19ec08a905a9cd5691a61d Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 3 Apr 2020 15:10:16 +0200 Subject: [PATCH] [SMTChecker] Add and use tuple sort --- libsolidity/formal/CVC4Interface.cpp | 15 ++++++ libsolidity/formal/SMTEncoder.cpp | 64 ++++++++++++------------ libsolidity/formal/SMTLib2Interface.cpp | 26 ++++++++++ libsolidity/formal/SMTLib2Interface.h | 1 + libsolidity/formal/SolverInterface.h | 16 +++++- libsolidity/formal/Sorts.h | 43 +++++++++++++++- libsolidity/formal/SymbolicTypes.cpp | 43 ++++++++++++++++ libsolidity/formal/SymbolicTypes.h | 2 + libsolidity/formal/SymbolicVariables.cpp | 55 ++++++++++++-------- libsolidity/formal/SymbolicVariables.h | 18 ++++--- libsolidity/formal/Z3Interface.cpp | 27 ++++++++++ 11 files changed, 248 insertions(+), 62 deletions(-) diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index 9aecc2586..067786061 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -196,6 +196,16 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) solAssert(sortSort, ""); return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1])); } + else if (n == "tuple_get") + { + shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); + solAssert(tupleSort, ""); + CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); + CVC4::Datatype const& dt = tt.getDatatype(); + size_t index = std::stoi(_expr.arguments[1].name); + CVC4::Expr s = dt[0][index].getSelector(); + return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]); + } solAssert(false, ""); } @@ -229,6 +239,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort) auto const& arraySort = dynamic_cast(_sort); return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range)); } + case Kind::Tuple: + { + auto const& tupleSort = dynamic_cast(_sort); + return m_context.mkTupleType(cvc4Sort(tupleSort.components)); + } default: break; } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index f02d32aae..67a488507 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -296,16 +296,22 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl) { auto symbTuple = dynamic_pointer_cast(m_context.expression(*init)); solAssert(symbTuple, ""); - auto const& components = symbTuple->components(); + auto const& symbComponents = symbTuple->components(); + + auto tupleType = dynamic_cast(init->annotation().type); + solAssert(tupleType, ""); + solAssert(tupleType->components().size() == symbTuple->components().size(), ""); + auto const& components = tupleType->components(); + auto const& declarations = _varDecl.declarations(); - solAssert(components.size() == declarations.size(), ""); + solAssert(symbComponents.size() == declarations.size(), ""); for (unsigned i = 0; i < declarations.size(); ++i) if ( components.at(i) && declarations.at(i) && m_context.knownVariable(*declarations.at(i)) ) - assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type())); + assignment(*declarations.at(i), symbTuple->component(i, components.at(i), declarations.at(i)->type())); } } else if (m_context.knownVariable(*_varDecl.declarations().front())) @@ -354,7 +360,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment) { auto const& type = _assignment.annotation().type; vector rightArguments; - if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple) + if (auto const* tupleTypeRight = dynamic_cast(_assignment.rightHandSide().annotation().type)) { auto symbTupleLeft = dynamic_pointer_cast(m_context.expression(_assignment.leftHandSide())); solAssert(symbTupleLeft, ""); @@ -365,17 +371,16 @@ void SMTEncoder::endVisit(Assignment const& _assignment) auto const& rightComponents = symbTupleRight->components(); solAssert(leftComponents.size() == rightComponents.size(), ""); - for (unsigned i = 0; i < leftComponents.size(); ++i) - { - auto const& left = leftComponents.at(i); - auto const& right = rightComponents.at(i); - /// Right hand side tuple component cannot be empty. - solAssert(right, ""); - if (left) - rightArguments.push_back(right->currentValue(left->originalType())); - else - rightArguments.push_back(right->currentValue()); - } + auto tupleTypeLeft = dynamic_cast(_assignment.leftHandSide().annotation().type); + solAssert(tupleTypeLeft, ""); + solAssert(tupleTypeLeft->components().size() == leftComponents.size(), ""); + auto const& typesLeft = tupleTypeLeft->components(); + + solAssert(tupleTypeRight->components().size() == rightComponents.size(), ""); + auto const& typesRight = tupleTypeRight->components(); + + for (unsigned i = 0; i < rightComponents.size(); ++i) + rightArguments.push_back(symbTupleRight->component(i, typesRight.at(i), typesLeft.at(i))); } else { @@ -418,17 +423,16 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) solAssert(symbComponents.size() == tupleComponents->size(), ""); for (unsigned i = 0; i < symbComponents.size(); ++i) { - auto sComponent = symbComponents.at(i); auto tComponent = tupleComponents->at(i); - if (sComponent && tComponent) + if (tComponent) { if (auto varDecl = identifierToVariable(*tComponent)) - m_context.addAssertion(sComponent->currentValue() == currentValue(*varDecl)); + m_context.addAssertion(symbTuple->component(i) == currentValue(*varDecl)); else { if (!m_context.knownExpression(*tComponent)) createExpr(*tComponent); - m_context.addAssertion(sComponent->currentValue() == expr(*tComponent)); + m_context.addAssertion(symbTuple->component(i) == expr(*tComponent)); } } } @@ -807,13 +811,15 @@ void SMTEncoder::endVisit(Return const& _return) { auto const& symbTuple = dynamic_pointer_cast(m_context.expression(*_return.expression())); solAssert(symbTuple, ""); - auto const& components = symbTuple->components(); - solAssert(components.size() == returnParams.size(), ""); + solAssert(symbTuple->components().size() == returnParams.size(), ""); + + auto const* tupleType = dynamic_cast(_return.expression()->annotation().type); + solAssert(tupleType, ""); + auto const& types = tupleType->components(); + solAssert(types.size() == returnParams.size(), ""); + for (unsigned i = 0; i < returnParams.size(); ++i) - { - solAssert(components.at(i), ""); - m_context.addAssertion(components.at(i)->currentValue(returnParams.at(i)->type()) == m_context.newValue(*returnParams.at(i))); - } + m_context.addAssertion(symbTuple->component(i, types.at(i), returnParams.at(i)->type()) == m_context.newValue(*returnParams.at(i))); } else if (returnParams.size() == 1) m_context.addAssertion(expr(*_return.expression(), returnParams.front()->type()) == m_context.newValue(*returnParams.front())); @@ -1676,14 +1682,10 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) solAssert(symbComponents.size() == returnParams.size(), ""); for (unsigned i = 0; i < symbComponents.size(); ++i) { - auto sComponent = symbComponents.at(i); auto param = returnParams.at(i); solAssert(param, ""); - if (sComponent) - { - solAssert(m_context.knownVariable(*param), ""); - m_context.addAssertion(sComponent->currentValue() == currentValue(*param)); - } + solAssert(m_context.knownVariable(*param), ""); + m_context.addAssertion(symbTuple->component(i) == currentValue(*param)); } } else if (returnParams.size() == 1) diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 74529b4c5..0c6b8715d 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -28,6 +28,7 @@ #include #include #include +#include using namespace std; using namespace solidity; @@ -50,6 +51,7 @@ void SMTLib2Interface::reset() m_accumulatedOutput.clear(); m_accumulatedOutput.emplace_back(); m_variables.clear(); + m_userSorts.clear(); write("(set-option :produce-models true)"); write("(set-logic ALL)"); } @@ -145,6 +147,14 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr) sexpr += "(as const " + toSmtLibSort(*arraySort) + ") "; sexpr += toSExpr(_expr.arguments.at(1)); } + else if (_expr.name == "tuple_get") + { + solAssert(_expr.arguments.size() == 2, ""); + auto tupleSort = dynamic_pointer_cast(_expr.arguments.at(0).sort); + unsigned index = std::stoi(_expr.arguments.at(1).name); + solAssert(index < tupleSort->members.size(), ""); + sexpr += tupleSort->members.at(index) + " " + toSExpr(_expr.arguments.at(0)); + } else { sexpr += _expr.name; @@ -169,6 +179,22 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) solAssert(arraySort.domain && arraySort.range, ""); return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')'; } + case Kind::Tuple: + { + auto const& tupleSort = dynamic_cast(_sort); + if (!m_userSorts.count(tupleSort.name)) + { + m_userSorts.insert(tupleSort.name); + string decl("(declare-datatypes ((" + tupleSort.name + " 0)) (((" + tupleSort.name); + solAssert(tupleSort.members.size() == tupleSort.components.size(), ""); + for (unsigned i = 0; i < tupleSort.members.size(); ++i) + decl += " (" + tupleSort.members.at(i) + " " + toSmtLibSort(*tupleSort.components.at(i)) + ")"; + decl += "))))"; + write(decl); + } + + return tupleSort.name; + } default: solAssert(false, "Invalid SMT sort"); } diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 17d385cb2..e3ebd8b5e 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -74,6 +74,7 @@ private: std::vector m_accumulatedOutput; std::map m_variables; + std::set m_userSorts; std::map const& m_queryResponses; std::vector m_unhandledQueries; diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 106ada820..cac412c4b 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -94,7 +94,8 @@ public: {"mod", 2}, {"select", 2}, {"store", 3}, - {"const_array", 2} + {"const_array", 2}, + {"tuple_get", 2} }; return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size(); } @@ -166,6 +167,19 @@ public: ); } + static Expression tuple_get(Expression _tuple, size_t _index) + { + solAssert(_tuple.sort->kind == Kind::Tuple, ""); + std::shared_ptr tupleSort = std::dynamic_pointer_cast(_tuple.sort); + solAssert(tupleSort, ""); + solAssert(_index < tupleSort->components.size(), ""); + return Expression( + "tuple_get", + std::vector{std::move(_tuple), Expression(_index)}, + tupleSort->components.at(_index) + ); + } + friend Expression operator!(Expression _a) { return Expression("not", std::move(_a), Kind::Bool); diff --git a/libsolidity/formal/Sorts.h b/libsolidity/formal/Sorts.h index d26644462..2acd46975 100644 --- a/libsolidity/formal/Sorts.h +++ b/libsolidity/formal/Sorts.h @@ -33,7 +33,8 @@ enum class Kind Bool, Function, Array, - Sort + Sort, + Tuple }; struct Sort @@ -115,6 +116,46 @@ struct SortSort: public Sort SortPointer inner; }; +struct TupleSort: public Sort +{ + TupleSort( + std::string _name, + std::vector _members, + std::vector _components + ): + Sort(Kind::Tuple), + name(std::move(_name)), + members(std::move(_members)), + components(std::move(_components)) + {} + + bool operator==(Sort const& _other) const override + { + if (!Sort::operator==(_other)) + return false; + auto _otherTuple = dynamic_cast(&_other); + solAssert(_otherTuple, ""); + if (name != _otherTuple->name) + return false; + if (members != _otherTuple->members) + return false; + if (components.size() != _otherTuple->components.size()) + return false; + if (!std::equal( + components.begin(), + components.end(), + _otherTuple->components.begin(), + [&](SortPointer _a, SortPointer _b) { return *_a == *_b; } + )) + return false; + return true; + } + + std::string const name; + std::vector const members; + std::vector const components; +}; + /** Frequently used sorts.*/ struct SortProvider { diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 1d9655a9c..b90500ce4 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -75,6 +75,23 @@ SortPointer smtSort(frontend::Type const& _type) return make_shared(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType())); } } + case Kind::Tuple: + { + auto tupleType = dynamic_cast(&_type); + solAssert(tupleType, ""); + vector members; + static unsigned tupleTypeId = 0; + for (auto const& component: tupleType->components()) + if (component) + members.emplace_back(component->identifier() + "_" + to_string(tupleTypeId++)); + else + members.emplace_back("null_type_" + to_string(tupleTypeId++)); + return make_shared( + _type.identifier() + "_" + to_string(tupleTypeId++), + members, + smtSortAbstractFunction(tupleType->components()) + ); + } default: // Abstract case. return SortProvider::intSort; @@ -96,6 +113,17 @@ SortPointer smtSortAbstractFunction(frontend::Type const& _type) return smtSort(_type); } +vector smtSortAbstractFunction(vector const& _types) +{ + vector sorts; + for (auto const& type: _types) + if (type) + sorts.push_back(smtSortAbstractFunction(*type)); + else + sorts.push_back(SortProvider::intSort); + return sorts; +} + Kind smtKind(frontend::Type::Category _category) { if (isNumber(_category)) @@ -106,6 +134,8 @@ Kind smtKind(frontend::Type::Category _category) return Kind::Function; else if (isMapping(_category) || isArray(_category)) return Kind::Array; + else if (isTuple(_category)) + return Kind::Tuple; // Abstract case. return Kind::Int; } @@ -350,4 +380,17 @@ void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _typ } } +optional symbolicTypeConversion(TypePointer _from, TypePointer _to) +{ + if (_to && _from) + // StringLiterals are encoded as SMT arrays in the generic case, + // but they can also be compared/assigned to fixed bytes, in which + // case they'd need to be encoded as numbers. + if (auto strType = dynamic_cast(_from)) + if (_to->category() == frontend::Type::Category::FixedBytes) + return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add))); + + return std::nullopt; +} + } diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 55c88811d..a05d606fe 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -31,6 +31,7 @@ std::vector smtSort(std::vector const& _type /// If _type has type Function, abstract it to Integer. /// Otherwise return smtSort(_type). SortPointer smtSortAbstractFunction(frontend::Type const& _type); +std::vector smtSortAbstractFunction(std::vector const& _types); /// Returns the SMT kind that models the Solidity type type category _category. Kind smtKind(frontend::Type::Category _category); @@ -69,4 +70,5 @@ void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context); void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); +std::optional symbolicTypeConversion(TypePointer _from, TypePointer _to); } diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 549fc05e9..35cd4f9c2 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -230,16 +230,9 @@ SymbolicArrayVariable::SymbolicArrayVariable( smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const { - if (_targetType) - { - solAssert(m_originalType, ""); - // StringLiterals are encoded as SMT arrays in the generic case, - // but they can also be compared/assigned to fixed bytes, in which - // case they'd need to be encoded as numbers. - if (auto strType = dynamic_cast(m_originalType)) - if (_targetType->category() == frontend::Type::Category::FixedBytes) - return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add))); - } + optional conversion = symbolicTypeConversion(m_originalType, _targetType); + if (conversion) + return *conversion; return SymbolicVariable::currentValue(_targetType); } @@ -262,16 +255,34 @@ SymbolicTupleVariable::SymbolicTupleVariable( SymbolicVariable(_type, _type, move(_uniqueName), _context) { solAssert(isTuple(m_type->category()), ""); - auto const& tupleType = dynamic_cast(*m_type); - auto const& componentsTypes = tupleType.components(); - for (unsigned i = 0; i < componentsTypes.size(); ++i) - if (componentsTypes.at(i)) - { - string componentName = m_uniqueName + "_component_" + to_string(i); - auto result = smt::newSymbolicVariable(*componentsTypes.at(i), componentName, m_context); - solAssert(result.second, ""); - m_components.emplace_back(move(result.second)); - } - else - m_components.emplace_back(nullptr); +} + +SymbolicTupleVariable::SymbolicTupleVariable( + SortPointer _sort, + string _uniqueName, + EncodingContext& _context +): + SymbolicVariable(move(_sort), move(_uniqueName), _context) +{ + solAssert(m_sort->kind == Kind::Tuple, ""); +} + +vector const& SymbolicTupleVariable::components() +{ + auto tupleSort = dynamic_pointer_cast(m_sort); + solAssert(tupleSort, ""); + return tupleSort->components; +} + +smt::Expression SymbolicTupleVariable::component( + size_t _index, + TypePointer _fromType, + TypePointer _toType +) +{ + optional conversion = symbolicTypeConversion(_fromType, _toType); + if (conversion) + return *conversion; + + return smt::Expression::tuple_get(currentValue(), _index); } diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index e1c28a8b5..6f7ad6ec4 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -249,14 +249,18 @@ public: std::string _uniqueName, EncodingContext& _context ); + SymbolicTupleVariable( + SortPointer _sort, + std::string _uniqueName, + EncodingContext& _context + ); - std::vector> const& components() - { - return m_components; - } - -private: - std::vector> m_components; + std::vector const& components(); + Expression component( + size_t _index, + TypePointer _fromType = nullptr, + TypePointer _toType = nullptr + ); }; } diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 20150c337..f175e45d2 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -193,6 +193,11 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) solAssert(arraySort && arraySort->domain, ""); return z3::const_array(z3Sort(*arraySort->domain), arguments[1]); } + else if (n == "tuple_get") + { + size_t index = std::stoi(_expr.arguments[1].name); + return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]); + } solAssert(false, ""); } @@ -217,6 +222,28 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort) auto const& arraySort = dynamic_cast(_sort); return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range)); } + case Kind::Tuple: + { + auto const& tupleSort = dynamic_cast(_sort); + vector cMembers; + for (auto const& member: tupleSort.members) + cMembers.emplace_back(member.c_str()); + /// Using this instead of the function below because with that one + /// we can't use `&sorts[0]` here. + vector sorts; + for (auto const& sort: tupleSort.components) + sorts.push_back(z3Sort(*sort)); + z3::func_decl_vector projs(m_context); + z3::func_decl tupleConstructor = m_context.tuple_sort( + tupleSort.name.c_str(), + tupleSort.members.size(), + &cMembers[0], + &sorts[0], + projs + ); + return tupleConstructor.range(); + } + default: break; }