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

Merge pull request #5272 from ethereum/smt_special_vars

Browse Source 
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
This commit is contained in:
chriseth 2018-10-24 14:34:17 +02:00 committed by GitHub
commit 01566c2e1a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
23 changed files with 272 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

115
libsolidity/formal/SMTChecker.cpp
View File

@ -363,6 +363,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
visitAssert(_funCall);
else if (funType.kind() == FunctionType::Kind::Require)
visitRequire(_funCall);
else if (funType.kind() == FunctionType::Kind::GasLeft)
visitGasLeft(_funCall);
else if (funType.kind() == FunctionType::Kind::BlockHash)
visitBlockHash(_funCall);
else if (funType.kind() == FunctionType::Kind::Internal)
inlineFunctionCall(_funCall);
else
@ -393,6 +397,27 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall)
addPathImpliedExpression(expr(*args[0]));
}
void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
{
string gasLeft = "gasleft()";
// We increase the variable index since gasleft changes
// inside a tx.
defineSpecialVariable(gasLeft, _funCall, true);
auto const& symbolicVar = m_specialVariables.at(gasLeft);
unsigned index = symbolicVar->index();
// We set the current value to unknown anyway to add type constraints.
symbolicVar->setUnknownValue();
if (index > 0)
m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
}
void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
{
string blockHash = "blockhash()";
// TODO Define blockhash as an uninterpreted function
defineSpecialVariable(blockHash, _funCall);
}
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* _funDef = nullptr;
@ -460,7 +485,12 @@ void SMTChecker::endVisit(Identifier const& _identifier)
}
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
if (
fun->kind() == FunctionType::Kind::Assert ||
fun->kind() == FunctionType::Kind::Require ||
fun->kind() == FunctionType::Kind::GasLeft ||
fun->kind() == FunctionType::Kind::BlockHash
)
return;
createExpr(_identifier);
}
@ -468,6 +498,8 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
defineExpr(_identifier, currentValue(*decl));
else if (_identifier.name() == "now")
defineSpecialVariable(_identifier.name(), _identifier);
else
// TODO: handle MagicVariableDeclaration here
m_errorReporter.warning(
@ -496,7 +528,7 @@ void SMTChecker::endVisit(Literal const& _literal)
void SMTChecker::endVisit(Return const& _return)
{
if (hasExpr(*_return.expression()))
if (knownExpr(*_return.expression()))
{
auto returnParams = m_functionPath.back()->returnParameters();
if (returnParams.size() > 1)
@ -509,6 +541,54 @@ void SMTChecker::endVisit(Return const& _return)
}
}
bool SMTChecker::visit(MemberAccess const& _memberAccess)
{
auto const& exprType = _memberAccess.expression().annotation().type;
solAssert(exprType, "");
if (exprType->category() == Type::Category::Magic)
{
auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
string accessedName;
if (identifier)
accessedName = identifier->name();
else
m_errorReporter.warning(
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
return false;
}
else
m_errorReporter.warning(
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
return true;
}
void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
{
if (!knownSpecialVariable(_name))
{
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
m_specialVariables.emplace(_name, result.second);
result.second->setUnknownValue();
if (result.first)
m_errorReporter.warning(
_expr.location(),
"Assertion checker does not yet support this special variable."
);
}
else if (_increaseIndex)
m_specialVariables.at(_name)->increaseIndex();
// The default behavior is not to increase the index since
// most of the special values stay the same throughout a tx.
defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
}
void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
{
switch (_op.getOperator())
@ -681,11 +761,15 @@ void SMTChecker::checkCondition(
expressionNames.push_back(_additionalValueName);
}
for (auto const& var: m_variables)
if (knownVariable(*var.first))
{
expressionsToEvaluate.emplace_back(currentValue(*var.first));
expressionNames.push_back(var.first->name());
}
{
expressionsToEvaluate.emplace_back(currentValue(*var.first));
expressionNames.push_back(var.first->name());
}
for (auto const& var: m_specialVariables)
{
expressionsToEvaluate.emplace_back(var.second->currentValue());
expressionNames.push_back(var.first);
}
}
smt::CheckResult result;
vector<string> values;
@ -910,7 +994,7 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{
// This might be the case for multiple calls to the same function.
if (hasVariable(_varDecl))
if (knownVariable(_varDecl))
return true;
auto const& type = _varDecl.type();
solAssert(m_variables.count(&_varDecl) == 0, "");
@ -927,11 +1011,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
return true;
}
string SMTChecker::uniqueSymbol(Expression const& _expr)
{
return "expr_" + to_string(_expr.id());
}
bool SMTChecker::knownVariable(VariableDeclaration const& _decl)
{
return m_variables.count(&_decl);
@ -969,7 +1048,7 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
smt::Expression SMTChecker::expr(Expression const& _e)
{
if (!hasExpr(_e))
if (!knownExpr(_e))
{
m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
createExpr(_e);
@ -977,20 +1056,20 @@ smt::Expression SMTChecker::expr(Expression const& _e)
return m_expressions.at(&_e)->currentValue();
}
bool SMTChecker::hasExpr(Expression const& _e) const
bool SMTChecker::knownExpr(Expression const& _e) const
{
return m_expressions.count(&_e);
}
bool SMTChecker::hasVariable(VariableDeclaration const& _var) const
bool SMTChecker::knownSpecialVariable(string const& _var) const
{
return m_variables.count(&_var);
return m_specialVariables.count(_var);
}
void SMTChecker::createExpr(Expression const& _e)
{
solAssert(_e.annotation().type, "");
if (hasExpr(_e))
if (knownExpr(_e))
m_expressions.at(&_e)->increaseIndex();
else
{

16
libsolidity/formal/SMTChecker.h
View File

@ -66,6 +66,7 @@ private:
virtual void endVisit(Identifier const& _node) override;
virtual void endVisit(Literal const& _node) override;
virtual void endVisit(Return const& _node) override;
virtual bool visit(MemberAccess const& _node) override;
void arithmeticOperation(BinaryOperation const& _op);
void compareOperation(BinaryOperation const& _op);
@ -73,10 +74,14 @@ private:
void visitAssert(FunctionCall const&);
void visitRequire(FunctionCall const&);
void visitGasLeft(FunctionCall const&);
void visitBlockHash(FunctionCall const&);
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const&);
void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
@ -129,8 +134,6 @@ private:
/// This fails if the type is not supported.
bool createVariable(VariableDeclaration const& _varDecl);
static std::string uniqueSymbol(Expression const& _expr);
/// @returns true if _delc is a variable that is known at the current point, i.e.
/// has a valid index
bool knownVariable(VariableDeclaration const& _decl);
@ -154,10 +157,13 @@ private:
/// Creates the expression (value can be arbitrary)
void createExpr(Expression const& _e);
/// Checks if expression was created
bool hasExpr(Expression const& _e) const;
bool knownExpr(Expression const& _e) const;
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smt::Expression _value);
/// Checks if special variable was seen.
bool knownSpecialVariable(std::string const& _var) const;
/// Adds a new path condition
void pushPathCondition(smt::Expression const& _e);
/// Remove the last path condition
@ -172,9 +178,6 @@ private:
/// Removes local variables from the context.
void removeLocalVariables();
/// Checks if VariableDeclaration was seen.
bool hasVariable(VariableDeclaration const& _e) const;
/// Copy the SSA indices of m_variables.
VariableIndices copyVariableIndices();
/// Resets the variable indices.
@ -187,6 +190,7 @@ private:
/// repeated calls to the same function.
std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;

2
libsolidity/formal/SSAVariable.cpp
View File

@ -28,6 +28,6 @@ SSAVariable::SSAVariable()
void SSAVariable::resetIndex()
{
m_currentIndex = 0;
m_nextFreeIndex.reset (new int);
m_nextFreeIndex.reset (new unsigned);
*m_nextFreeIndex = 1;
}

10
libsolidity/formal/SSAVariable.h
View File

@ -34,19 +34,19 @@ public:
void resetIndex();
/// This function returns the current index of this SSA variable.
int index() const { return m_currentIndex; }
int& index() { return m_currentIndex; }
unsigned index() const { return m_currentIndex; }
unsigned& index() { return m_currentIndex; }
int operator++()
unsigned operator++()
{
return m_currentIndex = (*m_nextFreeIndex)++;
}
private:
int m_currentIndex;
unsigned m_currentIndex;
/// The next free index is a shared pointer because we want
/// the copy and the copied to share it.
std::shared_ptr<int> m_nextFreeIndex;
std::shared_ptr<unsigned> m_nextFreeIndex;
};
}

11
libsolidity/formal/SymbolicAddressVariable.cpp
View File

@ -24,18 +24,17 @@ using namespace dev;
using namespace dev::solidity;
SymbolicAddressVariable::SymbolicAddressVariable(
Type const& _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
SymbolicIntVariable(_type, _uniqueName, _interface)
SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
{
solAssert(isAddress(_type.category()), "");
}
void SymbolicAddressVariable::setUnknownValue()
{
IntegerType intType{160};
m_interface.addAssertion(currentValue() >= minValue(intType));
m_interface.addAssertion(currentValue() <= maxValue(intType));
auto intType = dynamic_cast<IntegerType const*>(m_type.get());
solAssert(intType, "");
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));
}

1
libsolidity/formal/SymbolicAddressVariable.h
View File

@ -31,7 +31,6 @@ class SymbolicAddressVariable: public SymbolicIntVariable
{
public:
SymbolicAddressVariable(
Type const& _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);

6
libsolidity/formal/SymbolicBoolVariable.cpp
View File

@ -22,13 +22,13 @@ using namespace dev;
using namespace dev::solidity;
SymbolicBoolVariable::SymbolicBoolVariable(
Type const& _type,
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface&_interface
):
SymbolicVariable(_type, _uniqueName, _interface)
SymbolicVariable(move(_type), _uniqueName, _interface)
{
solAssert(_type.category() == Type::Category::Bool, "");
solAssert(m_type->category() == Type::Category::Bool, "");
}
smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const

2
libsolidity/formal/SymbolicBoolVariable.h
View File

@ -31,7 +31,7 @@ class SymbolicBoolVariable: public SymbolicVariable
{
public:
SymbolicBoolVariable(
Type const& _type,
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);

8
libsolidity/formal/SymbolicIntVariable.cpp
View File

@ -24,13 +24,13 @@ using namespace dev;
using namespace dev::solidity;
SymbolicIntVariable::SymbolicIntVariable(
Type const& _type,
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
SymbolicVariable(_type, _uniqueName, _interface)
SymbolicVariable(move(_type), _uniqueName, _interface)
{
solAssert(isNumber(_type.category()), "");
solAssert(isNumber(m_type->category()), "");
}
smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
@ -45,7 +45,7 @@ void SymbolicIntVariable::setZeroValue()
void SymbolicIntVariable::setUnknownValue()
{
auto intType = dynamic_cast<IntegerType const*>(&m_type);
auto intType = dynamic_cast<IntegerType const*>(m_type.get());
solAssert(intType, "");
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));

2
libsolidity/formal/SymbolicIntVariable.h
View File

@ -31,7 +31,7 @@ class SymbolicIntVariable: public SymbolicVariable
{
public:
SymbolicIntVariable(
Type const& _type,
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);

15
libsolidity/formal/SymbolicTypes.cpp
View File

@ -43,27 +43,28 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
{
bool abstract = false;
shared_ptr<SymbolicVariable> var;
TypePointer type = _type.shared_from_this();
if (!isSupportedType(_type))
{
abstract = true;
var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
}
else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
else if (isFunction(_type.category()))
var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
else if (isAddress(_type.category()))
var = make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
var = make_shared<SymbolicAddressVariable>(_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);
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
else
var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
}
else
solAssert(false, "");

6
libsolidity/formal/SymbolicVariable.cpp
View File

@ -24,18 +24,18 @@ using namespace dev;
using namespace dev::solidity;
SymbolicVariable::SymbolicVariable(
Type const& _type,
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
m_type(_type),
m_type(move(_type)),
m_uniqueName(_uniqueName),
m_interface(_interface),
m_ssa(make_shared<SSAVariable>())
{
}
string SymbolicVariable::uniqueSymbol(int _index) const
string SymbolicVariable::uniqueSymbol(unsigned _index) const
{
return m_uniqueName + "_" + to_string(_index);
}

11
libsolidity/formal/SymbolicVariable.h
View File

@ -39,10 +39,11 @@ class SymbolicVariable
{
public:
SymbolicVariable(
Type const& _type,
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
virtual ~SymbolicVariable() = default;
smt::Expression currentValue() const
@ -58,8 +59,8 @@ public:
return currentValue();
}
int index() const { return m_ssa->index(); }
int& index() { return m_ssa->index(); }
unsigned index() const { return m_ssa->index(); }
unsigned& index() { return m_ssa->index(); }
/// Sets the var to the default value of its type.
/// Inherited types must implement.
@ -69,9 +70,9 @@ public:
virtual void setUnknownValue() {}
protected:
std::string uniqueSymbol(int _index) const;
std::string uniqueSymbol(unsigned _index) const;
Type const& m_type;
TypePointer m_type = nullptr;
std::string m_uniqueName;
smt::SolverInterface& m_interface;
std::shared_ptr<SSAVariable> m_ssa = nullptr;

17
test/libsolidity/SMTChecker.cpp
View File

@ -133,23 +133,6 @@ BOOST_AUTO_TEST_CASE(assignment_in_declaration)
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
{
string text = R"(
contract C {
function g() public pure {}
function f() public view {
uint a = 3;
this.g();
assert(a == 3);
g();
assert(a == 3);
}
}
)";
CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
}
BOOST_AUTO_TEST_CASE(branches_merge_variables)
{
// Branch does not touch variable a

14
test/libsolidity/smtCheckerTests/special/blockhash.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
function f() public payable {
assert(blockhash(2) > 0);
}
}
// ----
// Warning: (86-98): Assertion checker does not yet support this special variable.
// Warning: (86-98): Assertion checker does not yet implement this type.
// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons
// Warning: (86-102): Internal error: Expression undefined for SMT solver.
// Warning: (79-103): Assertion violation happens here

10
test/libsolidity/smtCheckerTests/special/difficulty.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C
{
function f(uint difficulty) public view {
assert(block.difficulty == difficulty);
}
}
// ----
// Warning: (91-129): Assertion violation happens here

14
test/libsolidity/smtCheckerTests/special/gasleft.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
function f() public view {
assert(gasleft() > 0);
uint g = gasleft();
assert(g < gasleft());
assert(g >= gasleft());
}
}
// ----
// Warning: (76-97): Assertion violation happens here
// Warning: (123-144): Assertion violation happens here

25
test/libsolidity/smtCheckerTests/special/many.sol Normal file
View File

@ -0,0 +1,25 @@
pragma experimental SMTChecker;
contract C
{
function f() public payable {
assert(msg.sender == block.coinbase);
assert(block.difficulty == block.gaslimit);
assert(block.number == block.timestamp);
assert(tx.gasprice == msg.value);
assert(tx.origin == msg.sender);
uint x = block.number;
assert(x + 2 > block.number);
assert(now > 10);
assert(gasleft() > 100);
}
}
// ----
// Warning: (79-115): Assertion violation happens here
// Warning: (119-161): Assertion violation happens here
// Warning: (165-204): Assertion violation happens here
// Warning: (208-240): Assertion violation happens here
// Warning: (244-275): Assertion violation happens here
// Warning: (311-316): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
// Warning: (336-352): Assertion violation happens here
// Warning: (356-379): Assertion violation happens here

14
test/libsolidity/smtCheckerTests/special/msg_data.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
function f() public payable {
assert(msg.data.length > 0);
}
}
// ----
// Warning: (86-101): Assertion checker does not yet support this expression.
// Warning: (86-94): Assertion checker does not yet support this special variable.
// Warning: (86-94): Assertion checker does not yet implement this type.
// Warning: (86-101): Internal error: Expression undefined for SMT solver.
// Warning: (79-106): Assertion violation happens here

10
test/libsolidity/smtCheckerTests/special/msg_sender_1.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C
{
function f() public view {
address a = msg.sender;
address b = msg.sender;
assert(a == b);
}
}

14
test/libsolidity/smtCheckerTests/special/msg_sender_2.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
function f() public view {
require(msg.sender != address(0));
address a = msg.sender;
address b = msg.sender;
assert(a == b);
}
}
// ----
// Warning: (98-108): Assertion checker does not yet implement this expression.
// Warning: (98-108): Internal error: Expression undefined for SMT solver.

13
test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
function f(address c) public view {
address a = msg.sender;
address b = msg.sender;
assert(a == b);
assert(c == msg.sender);
}
}
// ----
// Warning: (155-178): Assertion violation happens here

14
test/libsolidity/smtCheckerTests/special/msg_sig.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
function f() public payable {
assert(msg.sig == 0x00000000);
}
}
// ----
// Warning: (86-93): Assertion checker does not yet support this special variable.
// Warning: (86-93): Assertion checker does not yet implement this type.
// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons
// Warning: (86-107): Internal error: Expression undefined for SMT solver.
// Warning: (79-108): Assertion violation happens here