diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 0ad746349..150b5813d 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -38,6 +38,7 @@ void EncodingContext::reset() { resetAllVariables(); m_expressions.clear(); + m_globalContext.clear(); m_thisAddress->increaseIndex(); m_balances->increaseIndex(); } @@ -153,6 +154,28 @@ bool EncodingContext::knownExpression(solidity::Expression const& _e) const return m_expressions.count(&_e); } +/// Global variables and functions. + +shared_ptr EncodingContext::globalSymbol(string const& _name) +{ + solAssert(knownGlobalSymbol(_name), ""); + return m_globalContext.at(_name); +} + +bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr) +{ + solAssert(!knownGlobalSymbol(_name), ""); + auto result = newSymbolicVariable(*_expr.annotation().type, _name, m_solver); + m_globalContext.emplace(_name, result.second); + setUnknownValue(*result.second); + return result.first; +} + +bool EncodingContext::knownGlobalSymbol(string const& _var) const +{ + return m_globalContext.count(_var); +} + // Blockchain Expression EncodingContext::thisAddress() diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index a7c35527e..4a7d05863 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -88,6 +88,19 @@ public: bool knownExpression(solidity::Expression const& _e) const; //@} + /// Methods related to global variables and functions. + //@{ + /// Global variables and functions. + std::shared_ptr globalSymbol(std::string const& _name); + /// @returns all symbolic variables. + std::unordered_map> const& globalSymbols() const { return m_globalContext; } + /// Defines a new global variable or function + /// and @returns true if type was abstracted. + bool createGlobalSymbol(std::string const& _name, solidity::Expression const& _expr); + /// Checks if special variable or function was seen. + bool knownGlobalSymbol(std::string const& _var) const; + //@} + /// Blockchain related methods. //@{ /// Value of `this` address. @@ -112,6 +125,10 @@ private: /// Symbolic expressions. std::unordered_map> m_expressions; + /// Symbolic representation of global symbols including + /// variables and functions. + std::unordered_map> m_globalContext; + /// Symbolic `this` address. std::unique_ptr m_thisAddress; diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 996c4bbc3..c94d9a655 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -111,7 +111,6 @@ bool SMTChecker::visit(FunctionDefinition const& _function) m_pathConditions.clear(); m_callStack.clear(); pushCallStack({&_function, nullptr}); - m_globalContext.clear(); m_uninterpretedTerms.clear(); m_overflowTargets.clear(); resetStateVariables(); @@ -730,7 +729,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) // We increase the variable index since gasleft changes // inside a tx. defineGlobalVariable(gasLeft, _funCall, true); - auto const& symbolicVar = m_globalContext.at(gasLeft); + auto const& symbolicVar = m_context.globalSymbol(gasLeft); unsigned index = symbolicVar->index(); // We set the current value to unknown anyway to add type constraints. m_context.setUnknownValue(*symbolicVar); @@ -897,8 +896,8 @@ void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier) auto const& fType = dynamic_cast(*_identifier.annotation().type); if (fType.returnParameterTypes().size() == 1) { - defineGlobalFunction(fType.richIdentifier(), _identifier); - m_context.createExpression(_identifier, m_globalContext.at(fType.richIdentifier())); + defineGlobalVariable(fType.richIdentifier(), _identifier); + m_context.createExpression(_identifier, m_context.globalSymbol(fType.richIdentifier())); } } @@ -1117,37 +1116,21 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex) { - if (!knownGlobalSymbol(_name)) + if (!m_context.knownGlobalSymbol(_name)) { - auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); - m_globalContext.emplace(_name, result.second); - m_context.setUnknownValue(*result.second); - if (result.first) + bool abstract = m_context.createGlobalSymbol(_name, _expr); + if (abstract) m_errorReporter.warning( _expr.location(), "Assertion checker does not yet support this global variable." ); } else if (_increaseIndex) - m_globalContext.at(_name)->increaseIndex(); + m_context.globalSymbol(_name)->increaseIndex(); // The default behavior is not to increase the index since // most of the global values stay the same throughout a tx. if (smt::isSupportedType(_expr.annotation().type->category())) - defineExpr(_expr, m_globalContext.at(_name)->currentValue()); -} - -void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _expr) -{ - if (!knownGlobalSymbol(_name)) - { - auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); - m_globalContext.emplace(_name, result.second); - if (result.first) - m_errorReporter.warning( - _expr.location(), - "Assertion checker does not yet support the type of this function." - ); - } + defineExpr(_expr, m_context.globalSymbol(_name)->currentValue()); } bool SMTChecker::shortcutRationalNumber(Expression const& _expr) @@ -1462,7 +1445,7 @@ void SMTChecker::checkCondition( expressionNames.push_back(var.first->name()); } } - for (auto const& var: m_globalContext) + for (auto const& var: m_context.globalSymbols()) { auto const& type = var.second->type(); if ( @@ -1763,11 +1746,6 @@ smt::Expression SMTChecker::expr(Expression const& _e) return m_context.expression(_e)->currentValue(); } -bool SMTChecker::knownGlobalSymbol(string const& _var) const -{ - return m_globalContext.count(_var); -} - void SMTChecker::createExpr(Expression const& _e) { bool abstract = m_context.createExpression(_e); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 5ae63076e..54254c3a6 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -126,8 +126,9 @@ private: /// visit depth. void visitFunctionOrModifier(); + /// Defines a new global variable or function. void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); - void defineGlobalFunction(std::string const& _name, Expression const& _expr); + /// Handles the side effects of assignment /// to variable of some SMT array type /// while aliasing is not supported. @@ -241,9 +242,6 @@ private: /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smt::Expression _value); - /// Checks if special variable or function was seen. - bool knownGlobalSymbol(std::string const& _var) const; - /// Adds a new path condition void pushPathCondition(smt::Expression const& _e); /// Remove the last path condition @@ -280,8 +278,6 @@ private: // True if the "No SMT solver available" warning was already created. bool m_noSolverWarning = false; - 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. /// Used to retrieve models.