diff options
author | Leonardo Alt <leo@ethereum.org> | 2018-10-18 00:00:42 +0800 |
---|---|---|
committer | Leonardo Alt <leo@ethereum.org> | 2018-10-18 00:36:24 +0800 |
commit | c92d3b537db7fdb3b66db800879cc07a23252c73 (patch) | |
tree | 0f052d294651ae56fa976d94aa119fe277aead2a | |
parent | 3db1ce0e144b9d35aa894b5e485c0761ab5aa033 (diff) | |
download | dexon-solidity-c92d3b537db7fdb3b66db800879cc07a23252c73.tar dexon-solidity-c92d3b537db7fdb3b66db800879cc07a23252c73.tar.gz dexon-solidity-c92d3b537db7fdb3b66db800879cc07a23252c73.tar.bz2 dexon-solidity-c92d3b537db7fdb3b66db800879cc07a23252c73.tar.lz dexon-solidity-c92d3b537db7fdb3b66db800879cc07a23252c73.tar.xz dexon-solidity-c92d3b537db7fdb3b66db800879cc07a23252c73.tar.zst dexon-solidity-c92d3b537db7fdb3b66db800879cc07a23252c73.zip |
[SMTChecker] Refactor expressions such that they also use SymbolicVariable
-rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 63 | ||||
-rw-r--r-- | libsolidity/formal/SMTChecker.h | 3 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicTypes.cpp | 54 | ||||
-rw-r--r-- | 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<FunctionType const*>(_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<VariableDeclaration const*>(_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<FunctionType const*>(_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<RationalNumberType const*>(&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<RationalNumberType const*>(_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 <libsolidity/interface/ReadFile.h> -#include <map> #include <unordered_map> #include <string> #include <vector> @@ -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<Expression const*, smt::Expression> m_expressions; + std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions; std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; std::vector<smt::Expression> 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<SymbolicVariable> dev::solidity::newSymbolicVariable( +pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable( Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver ) { + bool abstract = false; + shared_ptr<SymbolicVariable> var; if (!isSupportedType(_type)) - return nullptr; - if (isBool(_type.category())) - return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver); + { + abstract = true; + var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver); + } + else if (isBool(_type.category())) + var = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver); + else if (isFunction(_type.category())) + var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver); else if (isInteger(_type.category())) - return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver); + var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver); else if (isAddress(_type.category())) - return make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver); + var = make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver); + else if (isRational(_type.category())) + { + auto rational = dynamic_cast<RationalNumberType const*>(&_type); + solAssert(rational, ""); + if (rational->isFractional()) + var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver); + else + var = make_shared<SymbolicIntVariable>(_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<SymbolicVariable> 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<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver); smt::Expression minValue(IntegerType const& _type); smt::Expression maxValue(IntegerType const& _type); |