cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Move global variables and functions to encoding context

Browse Source
This commit is contained in:
Leonardo Alt 2019-05-14 18:57:34 +02:00
parent 54ce3df321
commit 5493a41842
4 changed files with 51 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
libsolidity/formal/EncodingContext.cpp
View File

@ -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<SymbolicVariable> 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()

17
libsolidity/formal/EncodingContext.h
View File

@ -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<SymbolicVariable> globalSymbol(std::string const& _name);
/// @returns all symbolic variables.
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> 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<solidity::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
/// Symbolic representation of global symbols including
/// variables and functions.
std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
/// Symbolic `this` address.
std::unique_ptr<SymbolicAddressVariable> m_thisAddress;

40
libsolidity/formal/SMTChecker.cpp
View File

@ -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<FunctionType const&>(*_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);

8
libsolidity/formal/SMTChecker.h
View File

@ -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<std::string, std::shared_ptr<smt::SymbolicVariable>> 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.