From c92d3b537db7fdb3b66db800879cc07a23252c73 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Oct 2018 18:00:42 +0200 Subject: [SMTChecker] Refactor expressions such that they also use SymbolicVariable --- libsolidity/formal/SMTChecker.cpp | 63 +++++++++++------------------------- libsolidity/formal/SMTChecker.h | 3 +- libsolidity/formal/SymbolicTypes.cpp | 54 ++++++++++++++++++------------- libsolidity/formal/SymbolicTypes.h | 14 ++++---- 4 files changed, 57 insertions(+), 77 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 671c2049..ef2dc52f 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -458,6 +458,12 @@ void SMTChecker::endVisit(Identifier const& _identifier) { // Will be translated as part of the node that requested the lvalue. } + else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) + { + if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) + return; + createExpr(_identifier); + } else if (isSupportedType(_identifier.annotation().type->category())) { if (VariableDeclaration const* decl = dynamic_cast(_identifier.annotation().referencedDeclaration)) @@ -469,25 +475,15 @@ void SMTChecker::endVisit(Identifier const& _identifier) "Assertion checker does not yet support the type of this variable." ); } - else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) - { - if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) - return; - createExpr(_identifier); - } } void SMTChecker::endVisit(Literal const& _literal) { Type const& type = *_literal.annotation().type; - if (type.category() == Type::Category::Integer || type.category() == Type::Category::Address || type.category() == Type::Category::RationalNumber) - { - if (RationalNumberType const* rational = dynamic_cast(&type)) - solAssert(!rational->isFractional(), ""); + if (isNumber(type.category())) defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); - } - else if (type.category() == Type::Category::Bool) + else if (isBool(type.category())) defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else m_errorReporter.warning( @@ -917,13 +913,10 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) if (hasVariable(_varDecl)) return true; auto const& type = _varDecl.type(); - if (isSupportedType(type->category())) - { - solAssert(m_variables.count(&_varDecl) == 0, ""); - m_variables.emplace(&_varDecl, newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface)); - return true; - } - else + solAssert(m_variables.count(&_varDecl) == 0, ""); + auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface); + m_variables.emplace(&_varDecl, result.second); + if (result.first) { m_errorReporter.warning( _varDecl.location(), @@ -931,6 +924,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) ); return false; } + return true; } string SMTChecker::uniqueSymbol(Expression const& _expr) @@ -980,7 +974,7 @@ smt::Expression SMTChecker::expr(Expression const& _e) m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); } - return prev(m_expressions.upper_bound(&_e))->second; + return m_expressions.at(&_e)->currentValue(); } bool SMTChecker::hasExpr(Expression const& _e) const @@ -996,34 +990,15 @@ bool SMTChecker::hasVariable(VariableDeclaration const& _var) const void SMTChecker::createExpr(Expression const& _e) { solAssert(_e.annotation().type, ""); - string exprSymbol = uniqueSymbol(_e) + "_" + to_string(m_expressions.count(&_e)); - switch (_e.annotation().type->category()) - { - case Type::Category::RationalNumber: - { - if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) - solAssert(!rational->isFractional(), ""); - m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); - break; - } - case Type::Category::Address: - case Type::Category::Integer: - m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); - break; - case Type::Category::Bool: - m_expressions.emplace(&_e, m_interface->newBool(exprSymbol)); - break; - case Type::Category::Function: - // This should be replaced by a `non-deterministic` type in the future. - m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); - break; - default: - m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); + if (hasExpr(_e)) + m_expressions.at(&_e)->increaseIndex(); + auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); + m_expressions.emplace(&_e, result.second); + if (result.first) m_errorReporter.warning( _e.location(), "Assertion checker does not yet implement this type." ); - } } void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 0b078556..f66693d2 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -25,7 +25,6 @@ #include -#include #include #include #include @@ -186,7 +185,7 @@ private: bool m_loopExecutionHappened = false; /// An Expression may have multiple smt::Expression due to /// repeated calls to the same function. - std::multimap m_expressions; + std::unordered_map> m_expressions; std::unordered_map> m_variables; std::vector m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 2d993865..d47869db 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -30,27 +30,44 @@ using namespace dev::solidity; bool dev::solidity::isSupportedType(Type::Category _category) { - return isInteger(_category) || - isAddress(_category) || - isBool(_category); + return isNumber(_category) || + isBool(_category) || + isFunction(_category); } -shared_ptr dev::solidity::newSymbolicVariable( +pair> dev::solidity::newSymbolicVariable( Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver ) { + bool abstract = false; + shared_ptr var; if (!isSupportedType(_type)) - return nullptr; - if (isBool(_type.category())) - return make_shared(_type, _uniqueName, _solver); + { + abstract = true; + var = make_shared(IntegerType{256}, _uniqueName, _solver); + } + else if (isBool(_type.category())) + var = make_shared(_type, _uniqueName, _solver); + else if (isFunction(_type.category())) + var = make_shared(IntegerType{256}, _uniqueName, _solver); else if (isInteger(_type.category())) - return make_shared(_type, _uniqueName, _solver); + var = make_shared(_type, _uniqueName, _solver); else if (isAddress(_type.category())) - return make_shared(_type, _uniqueName, _solver); + var = make_shared(_type, _uniqueName, _solver); + else if (isRational(_type.category())) + { + auto rational = dynamic_cast(&_type); + solAssert(rational, ""); + if (rational->isFractional()) + var = make_shared(IntegerType{256}, _uniqueName, _solver); + else + var = make_shared(_type, _uniqueName, _solver); + } else solAssert(false, ""); + return make_pair(abstract, var); } bool dev::solidity::isSupportedType(Type const& _type) @@ -63,9 +80,9 @@ bool dev::solidity::isInteger(Type::Category _category) return _category == Type::Category::Integer; } -bool dev::solidity::isInteger(Type const& _type) +bool dev::solidity::isRational(Type::Category _category) { - return isInteger(_type.category()); + return _category == Type::Category::RationalNumber; } bool dev::solidity::isAddress(Type::Category _category) @@ -73,30 +90,21 @@ bool dev::solidity::isAddress(Type::Category _category) return _category == Type::Category::Address; } -bool dev::solidity::isAddress(Type const& _type) -{ - return isAddress(_type.category()); -} - bool dev::solidity::isNumber(Type::Category _category) { return isInteger(_category) || + isRational(_category) || isAddress(_category); } -bool dev::solidity::isNumber(Type const& _type) -{ - return isNumber(_type.category()); -} - bool dev::solidity::isBool(Type::Category _category) { return _category == Type::Category::Bool; } -bool dev::solidity::isBool(Type const& _type) +bool dev::solidity::isFunction(Type::Category _category) { - return isBool(_type.category()); + return _category == Type::Category::Function; } smt::Expression dev::solidity::minValue(IntegerType const& _type) diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 77822fed..0887fa41 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -34,18 +34,16 @@ bool isSupportedType(Type::Category _category); bool isSupportedType(Type const& _type); bool isInteger(Type::Category _category); -bool isInteger(Type const& _type); - +bool isRational(Type::Category _category); bool isAddress(Type::Category _category); -bool isAddress(Type const& _type); - bool isNumber(Type::Category _category); -bool isNumber(Type const& _type); - bool isBool(Type::Category _category); -bool isBool(Type const& _type); +bool isFunction(Type::Category _category); -std::shared_ptr newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver); +/// Returns a new symbolic variable, according to _type. +/// Also returns whether the type is abstract or not, +/// which is true for unsupported types. +std::pair> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver); smt::Expression minValue(IntegerType const& _type); smt::Expression maxValue(IntegerType const& _type); -- cgit v1.2.3 From 070471d8d4921d0204b37aa3315b6737f58e7ad0 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Oct 2018 19:00:38 +0200 Subject: Fix possibly effectless map emplace --- libsolidity/formal/SMTChecker.cpp | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index ef2dc52f..e5648eb3 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -992,13 +992,16 @@ void SMTChecker::createExpr(Expression const& _e) solAssert(_e.annotation().type, ""); if (hasExpr(_e)) m_expressions.at(&_e)->increaseIndex(); - auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); - m_expressions.emplace(&_e, result.second); - if (result.first) - m_errorReporter.warning( - _e.location(), - "Assertion checker does not yet implement this type." - ); + else + { + auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); + m_expressions.emplace(&_e, result.second); + if (result.first) + m_errorReporter.warning( + _e.location(), + "Assertion checker does not yet implement this type." + ); + } } void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) -- cgit v1.2.3