diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 5d2c08f53..8a0df57b3 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -332,7 +332,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) { if (auto init = _varDecl.initialValue()) { - auto symbTuple = dynamic_pointer_cast(m_expressions[init]); + auto symbTuple = dynamic_pointer_cast(m_expressions[init]); /// symbTuple == nullptr if it is the return of a non-inlined function call. if (symbTuple) { @@ -375,7 +375,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) _assignment.location(), "Assertion checker does not yet implement this assignment operator." ); - else if (!isSupportedType(_assignment.annotation().type->category())) + else if (!smt::isSupportedType(_assignment.annotation().type->category())) { m_errorReporter.warning( _assignment.location(), @@ -390,7 +390,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) vector rightArguments; if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple) { - auto symbTuple = dynamic_pointer_cast(m_expressions[&_assignment.rightHandSide()]); + auto symbTuple = dynamic_pointer_cast(m_expressions[&_assignment.rightHandSide()]); solAssert(symbTuple, ""); for (auto const& component: symbTuple->components()) { @@ -426,7 +426,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) else if (_tuple.annotation().type->category() == Type::Category::Tuple) { createExpr(_tuple); - vector> components; + vector> components; for (auto const& component: _tuple.components()) if (component) { @@ -441,7 +441,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) else components.push_back(nullptr); solAssert(components.size() == _tuple.components().size(), ""); - auto const& symbTuple = dynamic_pointer_cast(m_expressions[&_tuple]); + auto const& symbTuple = dynamic_pointer_cast(m_expressions[&_tuple]); solAssert(symbTuple, ""); symbTuple->setComponents(move(components)); } @@ -450,7 +450,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) /// Parenthesized expressions are also TupleExpression regardless their type. auto const& components = _tuple.components(); solAssert(components.size() == 1, ""); - if (isSupportedType(components.front()->annotation().type->category())) + if (smt::isSupportedType(components.front()->annotation().type->category())) defineExpr(_tuple, expr(*components.front())); } } @@ -490,7 +490,7 @@ void SMTChecker::checkUnderflow(OverflowTarget& _target) solAssert(_target.type != OverflowTarget::Type::Overflow, ""); auto intType = dynamic_cast(_target.intType); checkCondition( - _target.path && _target.value < minValue(*intType), + _target.path && _target.value < smt::minValue(*intType), _target.location, "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")", "", @@ -503,7 +503,7 @@ void SMTChecker::checkOverflow(OverflowTarget& _target) solAssert(_target.type != OverflowTarget::Type::Underflow, ""); auto intType = dynamic_cast(_target.intType); checkCondition( - _target.path && _target.value > maxValue(*intType), + _target.path && _target.value > smt::maxValue(*intType), _target.location, "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")", "", @@ -520,7 +520,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) { case Token::Not: // ! { - solAssert(isBool(_op.annotation().type->category()), ""); + solAssert(smt::isBool(_op.annotation().type->category()), ""); defineExpr(_op, !expr(_op.subExpression())); break; } @@ -528,7 +528,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) case Token::Dec: // -- (pre- or postfix) { - solAssert(isInteger(_op.annotation().type->category()), ""); + solAssert(smt::isInteger(_op.annotation().type->category()), ""); solAssert(_op.subExpression().annotation().lValueRequested, ""); if (auto identifier = dynamic_cast(&_op.subExpression())) { @@ -785,13 +785,13 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) auto const& returnParams = funDef->returnParameters(); if (returnParams.size() > 1) { - vector> components; + vector> components; for (auto param: returnParams) { solAssert(m_variables[param.get()], ""); components.push_back(m_variables[param.get()]); } - auto const& symbTuple = dynamic_pointer_cast(m_expressions[&_funCall]); + auto const& symbTuple = dynamic_pointer_cast(m_expressions[&_funCall]); solAssert(symbTuple, ""); symbTuple->setComponents(move(components)); } @@ -837,7 +837,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) } else if (_identifier.annotation().type->category() == Type::Category::Function) visitFunctionIdentifier(_identifier); - else if (isSupportedType(_identifier.annotation().type->category())) + else if (smt::isSupportedType(_identifier.annotation().type->category())) { if (auto decl = identifierToVariable(_identifier)) defineExpr(_identifier, currentValue(*decl)); @@ -880,7 +880,7 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall) { auto const& intType = dynamic_cast(*m_expressions.at(&_funCall)->type()); defineExpr(_funCall, smt::Expression::ite( - expr(*argument) >= minValue(intType) && expr(*argument) <= maxValue(intType), + expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType), expr(*argument), expr(_funCall) )); @@ -908,9 +908,9 @@ void SMTChecker::endVisit(Literal const& _literal) { solAssert(_literal.annotation().type, "Expected type for AST node"); Type const& type = *_literal.annotation().type; - if (isNumber(type.category())) + if (smt::isNumber(type.category())) defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); - else if (isBool(type.category())) + else if (smt::isBool(type.category())) defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else { @@ -919,7 +919,7 @@ void SMTChecker::endVisit(Literal const& _literal) auto stringType = TypeProvider::stringMemory(); auto stringLit = dynamic_cast(_literal.annotation().type); solAssert(stringLit, ""); - auto result = newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); + auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); m_expressions.emplace(&_literal, result.second); } m_errorReporter.warning( @@ -1006,7 +1006,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess) void SMTChecker::endVisit(IndexAccess const& _indexAccess) { - shared_ptr array; + shared_ptr array; if (auto const& id = dynamic_cast(&_indexAccess.baseExpression())) { auto varDecl = identifierToVariable(*id); @@ -1111,7 +1111,7 @@ void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _ex { if (!knownGlobalSymbol(_name)) { - auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); + auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); m_globalContext.emplace(_name, result.second); setUnknownValue(*result.second); if (result.first) @@ -1124,7 +1124,7 @@ void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _ex m_globalContext.at(_name)->increaseIndex(); // The default behavior is not to increase the index since // most of the global values stay the same throughout a tx. - if (isSupportedType(_expr.annotation().type->category())) + if (smt::isSupportedType(_expr.annotation().type->category())) defineExpr(_expr, m_globalContext.at(_name)->currentValue()); } @@ -1132,7 +1132,7 @@ void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _ex { if (!knownGlobalSymbol(_name)) { - auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); + auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); m_globalContext.emplace(_name, result.second); if (result.first) m_errorReporter.warning( @@ -1235,16 +1235,16 @@ smt::Expression SMTChecker::arithmeticOperation( _location ); - smt::Expression intValueRange = (0 - minValue(intType)) + maxValue(intType) + 1; + smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1; value = smt::Expression::ite( - value > maxValue(intType) || value < minValue(intType), + value > smt::maxValue(intType) || value < smt::minValue(intType), value % intValueRange, value ); if (intType.isSigned()) { value = smt::Expression::ite( - value > maxValue(intType), + value > smt::maxValue(intType), value - intValueRange, value ); @@ -1256,13 +1256,13 @@ smt::Expression SMTChecker::arithmeticOperation( void SMTChecker::compareOperation(BinaryOperation const& _op) { solAssert(_op.annotation().commonType, ""); - if (isSupportedType(_op.annotation().commonType->category())) + if (smt::isSupportedType(_op.annotation().commonType->category())) { smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); Token op = _op.getOperator(); shared_ptr value; - if (isNumber(_op.annotation().commonType->category())) + if (smt::isNumber(_op.annotation().commonType->category())) { value = make_shared( op == Token::Equal ? (left == right) : @@ -1275,7 +1275,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op) } else // Bool { - solUnimplementedAssert(isBool(_op.annotation().commonType->category()), "Operation not yet supported"); + solUnimplementedAssert(smt::isBool(_op.annotation().commonType->category()), "Operation not yet supported"); value = make_shared( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) @@ -1339,7 +1339,7 @@ void SMTChecker::assignment( langutil::SourceLocation const& _location ) { - if (!isSupportedType(_type->category())) + if (!smt::isSupportedType(_type->category())) m_errorReporter.warning( _location, "Assertion checker does not yet implement type " + _type->toString() @@ -1459,7 +1459,7 @@ void SMTChecker::checkCondition( auto const& type = var.second->type(); if ( type->isValueType() && - smtKind(type->category()) != smt::Kind::Function + smt::smtKind(type->category()) != smt::Kind::Function ) { expressionsToEvaluate.emplace_back(var.second->currentValue()); @@ -1756,7 +1756,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) return true; auto const& type = _varDecl.type(); solAssert(m_variables.count(&_varDecl) == 0, ""); - auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface); + auto result = smt::newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface); m_variables.emplace(&_varDecl, result.second); if (result.first) { @@ -1798,7 +1798,7 @@ void SMTChecker::setZeroValue(VariableDeclaration const& _decl) setZeroValue(*m_variables.at(&_decl)); } -void SMTChecker::setZeroValue(SymbolicVariable& _variable) +void SMTChecker::setZeroValue(smt::SymbolicVariable& _variable) { smt::setSymbolicZeroValue(_variable, *m_interface); } @@ -1809,7 +1809,7 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) setUnknownValue(*m_variables.at(&_decl)); } -void SMTChecker::setUnknownValue(SymbolicVariable& _variable) +void SMTChecker::setUnknownValue(smt::SymbolicVariable& _variable) { smt::setSymbolicUnknownValue(_variable, *m_interface); } @@ -1841,7 +1841,7 @@ void SMTChecker::createExpr(Expression const& _e) m_expressions.at(&_e)->increaseIndex(); else { - auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); + auto result = smt::newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); m_expressions.emplace(&_e, result.second); if (result.first) m_errorReporter.warning( @@ -1854,7 +1854,7 @@ void SMTChecker::createExpr(Expression const& _e) void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) { createExpr(_e); - solAssert(smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); + solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); m_interface->addAssertion(expr(_e) == _value); } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 81710c890..6c5c1177b 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -245,10 +245,10 @@ private: /// Sets the value of the declaration to zero. void setZeroValue(VariableDeclaration const& _decl); - void setZeroValue(SymbolicVariable& _variable); + void setZeroValue(smt::SymbolicVariable& _variable); /// Resets the variable to an unknown value (in its range). void setUnknownValue(VariableDeclaration const& decl); - void setUnknownValue(SymbolicVariable& _variable); + void setUnknownValue(smt::SymbolicVariable& _variable); /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. smt::Expression expr(Expression const& _e); @@ -294,7 +294,7 @@ private: VariableDeclaration const* identifierToVariable(Expression const& _expr); std::unique_ptr m_interface; - VariableUsage m_variableUsage; + smt::VariableUsage m_variableUsage; bool m_loopExecutionHappened = false; bool m_arrayAssignmentHappened = false; bool m_externalFunctionCallHappened = false; @@ -302,9 +302,9 @@ private: bool m_noSolverWarning = false; /// An Expression may have multiple smt::Expression due to /// repeated calls to the same function. - std::unordered_map> m_expressions; - std::unordered_map> m_variables; - std::unordered_map> m_globalContext; + std::unordered_map> m_expressions; + std::unordered_map> m_variables; + std::unordered_map> m_globalContext; /// Stores the instances of an Uninterpreted Function applied to arguments. /// These may be direct application of UFs or Array index access. diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index fe6136fb9..7c8ecc2b4 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -18,7 +18,7 @@ #include using namespace std; -using namespace dev::solidity; +using namespace dev::solidity::smt; SSAVariable::SSAVariable() { diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index f1682b320..b4cd59133 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -23,6 +23,8 @@ namespace dev { namespace solidity { +namespace smt +{ /** * This class represents the SSA representation of a program variable. @@ -49,3 +51,4 @@ private: } } +} diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 9c0763f69..7f0cb21ea 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -22,79 +22,85 @@ #include using namespace std; -using namespace dev::solidity; -smt::SortPointer dev::solidity::smtSort(Type const& _type) +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +SortPointer smtSort(solidity::Type const& _type) { switch (smtKind(_type.category())) { - case smt::Kind::Int: - return make_shared(smt::Kind::Int); - case smt::Kind::Bool: - return make_shared(smt::Kind::Bool); - case smt::Kind::Function: + case Kind::Int: + return make_shared(Kind::Int); + case Kind::Bool: + return make_shared(Kind::Bool); + case Kind::Function: { - auto fType = dynamic_cast(&_type); + auto fType = dynamic_cast(&_type); solAssert(fType, ""); - vector parameterSorts = smtSort(fType->parameterTypes()); + vector parameterSorts = smtSort(fType->parameterTypes()); auto returnTypes = fType->returnParameterTypes(); - smt::SortPointer returnSort; + SortPointer returnSort; // TODO change this when we support tuples. if (returnTypes.size() == 0) // We cannot declare functions without a return sort, so we use the smallest. - returnSort = make_shared(smt::Kind::Bool); + returnSort = make_shared(Kind::Bool); else if (returnTypes.size() > 1) // Abstract sort. - returnSort = make_shared(smt::Kind::Int); + returnSort = make_shared(Kind::Int); else returnSort = smtSort(*returnTypes.front()); - return make_shared(parameterSorts, returnSort); + return make_shared(parameterSorts, returnSort); } - case smt::Kind::Array: + case Kind::Array: { if (isMapping(_type.category())) { - auto mapType = dynamic_cast(&_type); + auto mapType = dynamic_cast(&_type); solAssert(mapType, ""); - return make_shared(smtSort(*mapType->keyType()), smtSort(*mapType->valueType())); + return make_shared(smtSort(*mapType->keyType()), smtSort(*mapType->valueType())); } else { solAssert(isArray(_type.category()), ""); - auto arrayType = dynamic_cast(&_type); + auto arrayType = dynamic_cast(&_type); solAssert(arrayType, ""); - return make_shared(make_shared(smt::Kind::Int), smtSort(*arrayType->baseType())); + return make_shared(make_shared(Kind::Int), smtSort(*arrayType->baseType())); } } default: // Abstract case. - return make_shared(smt::Kind::Int); + return make_shared(Kind::Int); } } -vector dev::solidity::smtSort(vector const& _types) +vector smtSort(vector const& _types) { - vector sorts; + vector sorts; for (auto const& type: _types) sorts.push_back(smtSort(*type)); return sorts; } -smt::Kind dev::solidity::smtKind(Type::Category _category) +Kind smtKind(solidity::Type::Category _category) { if (isNumber(_category)) - return smt::Kind::Int; + return Kind::Int; else if (isBool(_category)) - return smt::Kind::Bool; + return Kind::Bool; else if (isFunction(_category)) - return smt::Kind::Function; + return Kind::Function; else if (isMapping(_category) || isArray(_category)) - return smt::Kind::Array; + return Kind::Array; // Abstract case. - return smt::Kind::Int; + return Kind::Int; } -bool dev::solidity::isSupportedType(Type::Category _category) +bool isSupportedType(solidity::Type::Category _category) { return isNumber(_category) || isBool(_category) || @@ -103,25 +109,25 @@ bool dev::solidity::isSupportedType(Type::Category _category) isTuple(_category); } -bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category) +bool isSupportedTypeDeclaration(solidity::Type::Category _category) { return isSupportedType(_category) || isFunction(_category); } -pair> dev::solidity::newSymbolicVariable( - Type const& _type, +pair> newSymbolicVariable( + solidity::Type const& _type, std::string const& _uniqueName, - smt::SolverInterface& _solver + SolverInterface& _solver ) { bool abstract = false; shared_ptr var; - TypePointer type = &_type; + solidity::TypePointer type = &_type; if (!isSupportedTypeDeclaration(_type)) { abstract = true; - var = make_shared(TypeProvider::uint256(), _uniqueName, _solver); + var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _solver); } else if (isBool(_type.category())) var = make_shared(type, _uniqueName, _solver); @@ -131,7 +137,7 @@ pair> dev::solidity::newSymbolicVariable( var = make_shared(type, _uniqueName, _solver); else if (isFixedBytes(_type.category())) { - auto fixedBytesType = dynamic_cast(type); + auto fixedBytesType = dynamic_cast(type); solAssert(fixedBytesType, ""); var = make_shared(fixedBytesType->numBytes(), _uniqueName, _solver); } @@ -141,10 +147,10 @@ pair> dev::solidity::newSymbolicVariable( var = make_shared(type, _uniqueName, _solver); else if (isRational(_type.category())) { - auto rational = dynamic_cast(&_type); + auto rational = dynamic_cast(&_type); solAssert(rational, ""); if (rational->isFractional()) - var = make_shared(TypeProvider::uint256(), _uniqueName, _solver); + var = make_shared(solidity::TypeProvider::uint256(), _uniqueName, _solver); else var = make_shared(type, _uniqueName, _solver); } @@ -159,47 +165,47 @@ pair> dev::solidity::newSymbolicVariable( return make_pair(abstract, var); } -bool dev::solidity::isSupportedType(Type const& _type) +bool isSupportedType(solidity::Type const& _type) { return isSupportedType(_type.category()); } -bool dev::solidity::isSupportedTypeDeclaration(Type const& _type) +bool isSupportedTypeDeclaration(solidity::Type const& _type) { return isSupportedTypeDeclaration(_type.category()); } -bool dev::solidity::isInteger(Type::Category _category) +bool isInteger(solidity::Type::Category _category) { - return _category == Type::Category::Integer; + return _category == solidity::Type::Category::Integer; } -bool dev::solidity::isRational(Type::Category _category) +bool isRational(solidity::Type::Category _category) { - return _category == Type::Category::RationalNumber; + return _category == solidity::Type::Category::RationalNumber; } -bool dev::solidity::isFixedBytes(Type::Category _category) +bool isFixedBytes(solidity::Type::Category _category) { - return _category == Type::Category::FixedBytes; + return _category == solidity::Type::Category::FixedBytes; } -bool dev::solidity::isAddress(Type::Category _category) +bool isAddress(solidity::Type::Category _category) { - return _category == Type::Category::Address; + return _category == solidity::Type::Category::Address; } -bool dev::solidity::isContract(Type::Category _category) +bool isContract(solidity::Type::Category _category) { - return _category == Type::Category::Contract; + return _category == solidity::Type::Category::Contract; } -bool dev::solidity::isEnum(Type::Category _category) +bool isEnum(solidity::Type::Category _category) { - return _category == Type::Category::Enum; + return _category == solidity::Type::Category::Enum; } -bool dev::solidity::isNumber(Type::Category _category) +bool isNumber(solidity::Type::Category _category) { return isInteger(_category) || isRational(_category) || @@ -209,75 +215,79 @@ bool dev::solidity::isNumber(Type::Category _category) isEnum(_category); } -bool dev::solidity::isBool(Type::Category _category) +bool isBool(solidity::Type::Category _category) { - return _category == Type::Category::Bool; + return _category == solidity::Type::Category::Bool; } -bool dev::solidity::isFunction(Type::Category _category) +bool isFunction(solidity::Type::Category _category) { - return _category == Type::Category::Function; + return _category == solidity::Type::Category::Function; } -bool dev::solidity::isMapping(Type::Category _category) +bool isMapping(solidity::Type::Category _category) { - return _category == Type::Category::Mapping; + return _category == solidity::Type::Category::Mapping; } -bool dev::solidity::isArray(Type::Category _category) +bool isArray(solidity::Type::Category _category) { - return _category == Type::Category::Array; + return _category == solidity::Type::Category::Array; } -bool dev::solidity::isTuple(Type::Category _category) +bool isTuple(solidity::Type::Category _category) { - return _category == Type::Category::Tuple; + return _category == solidity::Type::Category::Tuple; } -smt::Expression dev::solidity::minValue(IntegerType const& _type) +Expression minValue(solidity::IntegerType const& _type) { - return smt::Expression(_type.minValue()); + return Expression(_type.minValue()); } -smt::Expression dev::solidity::maxValue(IntegerType const& _type) +Expression maxValue(solidity::IntegerType const& _type) { - return smt::Expression(_type.maxValue()); + return Expression(_type.maxValue()); } -void dev::solidity::smt::setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface) +void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface) { setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _interface); } -void dev::solidity::smt::setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) +void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface) { solAssert(_type, ""); if (isInteger(_type->category())) _interface.addAssertion(_expr == 0); else if (isBool(_type->category())) - _interface.addAssertion(_expr == smt::Expression(false)); + _interface.addAssertion(_expr == Expression(false)); } -void dev::solidity::smt::setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface) +void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface) { setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _interface); } -void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) +void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface) { solAssert(_type, ""); if (isEnum(_type->category())) { - auto enumType = dynamic_cast(_type); + auto enumType = dynamic_cast(_type); solAssert(enumType, ""); _interface.addAssertion(_expr >= 0); _interface.addAssertion(_expr < enumType->numberOfMembers()); } else if (isInteger(_type->category())) { - auto intType = dynamic_cast(_type); + auto intType = dynamic_cast(_type); solAssert(intType, ""); _interface.addAssertion(_expr >= minValue(*intType)); _interface.addAssertion(_expr <= maxValue(*intType)); } } + +} +} +} diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index e9132a819..8993575e3 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -26,50 +26,48 @@ namespace dev { namespace solidity { +namespace smt +{ /// Returns the SMT sort that models the Solidity type _type. -smt::SortPointer smtSort(Type const& _type); -std::vector smtSort(std::vector const& _types); +SortPointer smtSort(solidity::Type const& _type); +std::vector smtSort(std::vector const& _types); /// Returns the SMT kind that models the Solidity type type category _category. -smt::Kind smtKind(Type::Category _category); +Kind smtKind(solidity::Type::Category _category); /// Returns true if type is fully supported (declaration and operations). -bool isSupportedType(Type::Category _category); -bool isSupportedType(Type const& _type); +bool isSupportedType(solidity::Type::Category _category); +bool isSupportedType(solidity::Type const& _type); /// Returns true if type is partially supported (declaration). -bool isSupportedTypeDeclaration(Type::Category _category); -bool isSupportedTypeDeclaration(Type const& _type); +bool isSupportedTypeDeclaration(solidity::Type::Category _category); +bool isSupportedTypeDeclaration(solidity::Type const& _type); -bool isInteger(Type::Category _category); -bool isRational(Type::Category _category); -bool isFixedBytes(Type::Category _category); -bool isAddress(Type::Category _category); -bool isContract(Type::Category _category); -bool isEnum(Type::Category _category); -bool isNumber(Type::Category _category); -bool isBool(Type::Category _category); -bool isFunction(Type::Category _category); -bool isMapping(Type::Category _category); -bool isArray(Type::Category _category); -bool isTuple(Type::Category _category); +bool isInteger(solidity::Type::Category _category); +bool isRational(solidity::Type::Category _category); +bool isFixedBytes(solidity::Type::Category _category); +bool isAddress(solidity::Type::Category _category); +bool isContract(solidity::Type::Category _category); +bool isEnum(solidity::Type::Category _category); +bool isNumber(solidity::Type::Category _category); +bool isBool(solidity::Type::Category _category); +bool isFunction(solidity::Type::Category _category); +bool isMapping(solidity::Type::Category _category); +bool isArray(solidity::Type::Category _category); +bool isTuple(solidity::Type::Category _category); /// 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); +std::pair> newSymbolicVariable(solidity::Type const& _type, std::string const& _uniqueName, SolverInterface& _solver); -smt::Expression minValue(IntegerType const& _type); -smt::Expression maxValue(IntegerType const& _type); +Expression minValue(solidity::IntegerType const& _type); +Expression maxValue(solidity::IntegerType const& _type); -namespace smt -{ - -void setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface); -void setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface); -void setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface); -void setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface); - -} +void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface); +void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface); +void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface); +void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface); } } +} diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index db2e68b55..398924b5d 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -23,12 +23,12 @@ using namespace std; using namespace dev; -using namespace dev::solidity; +using namespace dev::solidity::smt; SymbolicVariable::SymbolicVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): m_type(move(_type)), m_uniqueName(move(_uniqueName)), @@ -41,9 +41,9 @@ SymbolicVariable::SymbolicVariable( } SymbolicVariable::SymbolicVariable( - smt::SortPointer _sort, + SortPointer _sort, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): m_sort(move(_sort)), m_uniqueName(move(_uniqueName)), @@ -53,7 +53,7 @@ SymbolicVariable::SymbolicVariable( solAssert(m_sort, ""); } -smt::Expression SymbolicVariable::currentValue() const +Expression SymbolicVariable::currentValue() const { return valueAtIndex(m_ssa->index()); } @@ -63,7 +63,7 @@ string SymbolicVariable::currentName() const return uniqueSymbol(m_ssa->index()); } -smt::Expression SymbolicVariable::valueAtIndex(int _index) const +Expression SymbolicVariable::valueAtIndex(int _index) const { return m_interface.newVariable(uniqueSymbol(_index), m_sort); } @@ -73,26 +73,26 @@ string SymbolicVariable::uniqueSymbol(unsigned _index) const return m_uniqueName + "_" + to_string(_index); } -smt::Expression SymbolicVariable::increaseIndex() +Expression SymbolicVariable::increaseIndex() { ++(*m_ssa); return currentValue(); } SymbolicBoolVariable::SymbolicBoolVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicVariable(move(_type), move(_uniqueName), _interface) { - solAssert(m_type->category() == Type::Category::Bool, ""); + solAssert(m_type->category() == solidity::Type::Category::Bool, ""); } SymbolicIntVariable::SymbolicIntVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicVariable(move(_type), move(_uniqueName), _interface) { @@ -101,7 +101,7 @@ SymbolicIntVariable::SymbolicIntVariable( SymbolicAddressVariable::SymbolicAddressVariable( string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _interface) { @@ -110,21 +110,21 @@ SymbolicAddressVariable::SymbolicAddressVariable( SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( unsigned _numBytes, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _interface) { } SymbolicFunctionVariable::SymbolicFunctionVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicVariable(move(_type), move(_uniqueName), _interface), m_declaration(m_interface.newVariable(currentName(), m_sort)) { - solAssert(m_type->category() == Type::Category::Function, ""); + solAssert(m_type->category() == solidity::Type::Category::Function, ""); } void SymbolicFunctionVariable::resetDeclaration() @@ -132,22 +132,22 @@ void SymbolicFunctionVariable::resetDeclaration() m_declaration = m_interface.newVariable(currentName(), m_sort); } -smt::Expression SymbolicFunctionVariable::increaseIndex() +Expression SymbolicFunctionVariable::increaseIndex() { ++(*m_ssa); resetDeclaration(); return currentValue(); } -smt::Expression SymbolicFunctionVariable::operator()(vector _arguments) const +Expression SymbolicFunctionVariable::operator()(vector _arguments) const { return m_declaration(_arguments); } SymbolicMappingVariable::SymbolicMappingVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicVariable(move(_type), move(_uniqueName), _interface) { @@ -155,9 +155,9 @@ SymbolicMappingVariable::SymbolicMappingVariable( } SymbolicArrayVariable::SymbolicArrayVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicVariable(move(_type), move(_uniqueName), _interface) { @@ -165,9 +165,9 @@ SymbolicArrayVariable::SymbolicArrayVariable( } SymbolicEnumVariable::SymbolicEnumVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicVariable(move(_type), move(_uniqueName), _interface) { @@ -175,9 +175,9 @@ SymbolicEnumVariable::SymbolicEnumVariable( } SymbolicTupleVariable::SymbolicTupleVariable( - TypePointer _type, + solidity::TypePointer _type, string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ): SymbolicVariable(move(_type), move(_uniqueName), _interface) { @@ -187,7 +187,7 @@ SymbolicTupleVariable::SymbolicTupleVariable( void SymbolicTupleVariable::setComponents(vector> _components) { solAssert(m_components.empty(), ""); - auto const& tupleType = dynamic_cast(m_type); + auto const& tupleType = dynamic_cast(m_type); solAssert(_components.size() == tupleType->components().size(), ""); m_components = move(_components); } diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 0b616a235..42e3beb1e 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -26,6 +26,8 @@ namespace dev { namespace solidity { +namespace smt +{ class Type; @@ -36,23 +38,23 @@ class SymbolicVariable { public: SymbolicVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); SymbolicVariable( - smt::SortPointer _sort, + SortPointer _sort, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); virtual ~SymbolicVariable() = default; - smt::Expression currentValue() const; + Expression currentValue() const; std::string currentName() const; - virtual smt::Expression valueAtIndex(int _index) const; - virtual smt::Expression increaseIndex(); - virtual smt::Expression operator()(std::vector /*_arguments*/) const + virtual Expression valueAtIndex(int _index) const; + virtual Expression increaseIndex(); + virtual Expression operator()(std::vector /*_arguments*/) const { solAssert(false, "Function application to non-function."); } @@ -60,17 +62,17 @@ public: unsigned index() const { return m_ssa->index(); } unsigned& index() { return m_ssa->index(); } - TypePointer const& type() const { return m_type; } + solidity::TypePointer const& type() const { return m_type; } protected: std::string uniqueSymbol(unsigned _index) const; /// SMT sort. - smt::SortPointer m_sort; + SortPointer m_sort; /// Solidity type, used for size and range in number types. - TypePointer m_type; + solidity::TypePointer m_type; std::string m_uniqueName; - smt::SolverInterface& m_interface; + SolverInterface& m_interface; std::unique_ptr m_ssa; }; @@ -81,9 +83,9 @@ class SymbolicBoolVariable: public SymbolicVariable { public: SymbolicBoolVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); }; @@ -94,9 +96,9 @@ class SymbolicIntVariable: public SymbolicVariable { public: SymbolicIntVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); }; @@ -108,7 +110,7 @@ class SymbolicAddressVariable: public SymbolicIntVariable public: SymbolicAddressVariable( std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); }; @@ -121,7 +123,7 @@ public: SymbolicFixedBytesVariable( unsigned _numBytes, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); }; @@ -132,20 +134,20 @@ class SymbolicFunctionVariable: public SymbolicVariable { public: SymbolicFunctionVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); - smt::Expression increaseIndex(); - smt::Expression operator()(std::vector _arguments) const; + Expression increaseIndex(); + Expression operator()(std::vector _arguments) const; private: /// Creates a new function declaration. void resetDeclaration(); /// Stores the current function declaration. - smt::Expression m_declaration; + Expression m_declaration; }; /** @@ -155,9 +157,9 @@ class SymbolicMappingVariable: public SymbolicVariable { public: SymbolicMappingVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); }; @@ -168,9 +170,9 @@ class SymbolicArrayVariable: public SymbolicVariable { public: SymbolicArrayVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); }; @@ -181,9 +183,9 @@ class SymbolicEnumVariable: public SymbolicVariable { public: SymbolicEnumVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); }; @@ -194,9 +196,9 @@ class SymbolicTupleVariable: public SymbolicVariable { public: SymbolicTupleVariable( - TypePointer _type, + solidity::TypePointer _type, std::string _uniqueName, - smt::SolverInterface& _interface + SolverInterface& _interface ); std::vector> const& components() @@ -212,3 +214,4 @@ private: } } +} diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 6d63e2980..b2fb38a46 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -24,6 +24,7 @@ using namespace std; using namespace dev; using namespace dev::solidity; +using namespace dev::solidity::smt; void VariableUsage::endVisit(Identifier const& _identifier) { diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h index b5e067c79..b7f994b69 100644 --- a/libsolidity/formal/VariableUsage.h +++ b/libsolidity/formal/VariableUsage.h @@ -26,6 +26,8 @@ namespace dev { namespace solidity { +namespace smt +{ /** * This class computes information about which variables are modified in a certain subtree. @@ -51,3 +53,4 @@ private: } } +}