z3 conditions

This commit is contained in:
chriseth 2017-07-06 11:05:05 +02:00
parent 3b07c4d38e
commit 1ece7bf443
10 changed files with 649 additions and 3 deletions

View File

@ -16,6 +16,7 @@ option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms"
# Let's find our dependencies
include(EthDependencies)
include(deps/jsoncpp.cmake)
include(deps/z3.cmake)
find_package(Threads)

View File

@ -25,7 +25,7 @@ function(eth_apply TARGET REQUIRED SUBMODULE)
if (${SUBMODULE} STREQUAL "solidity" OR ${SUBMODULE} STREQUAL "")
eth_use(${TARGET} ${REQUIRED} Dev::soldevcore Solidity::solevmasm)
target_link_libraries(${TARGET} ${Solidity_SOLIDITY_LIBRARIES})
target_link_libraries(${TARGET} ${Solidity_SOLIDITY_LIBRARIES} z3)
endif()
target_compile_definitions(${TARGET} PUBLIC ETH_SOLIDITY)

2
deps

@ -1 +1 @@
Subproject commit e5c8316db8d3daa0abc3b5af8545ce330057608c
Subproject commit cd9c6ff69134e8f53bde70d92cce12ad294752de

View File

@ -3,4 +3,4 @@ file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp")
file(GLOB_RECURSE headers "*.h" "../libjulia/*.h")
add_library(solidity ${sources} ${headers})
target_link_libraries(solidity PUBLIC evmasm devcore)
target_link_libraries(solidity PUBLIC evmasm devcore z3)

View File

@ -22,6 +22,7 @@
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/Exceptions.h>
#include <libsolidity/ast/AST_accept.h>
#include <libdevcore/SHA3.h>

View File

@ -0,0 +1,36 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/SMTChecker.h>
#include <libsolidity/formal/SMTCheckerImpl.h>
#include <libsolidity/interface/ErrorReporter.h>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SMTChecker::SMTChecker(ErrorReporter& _errorReporter):
m_impl(make_shared<SMTCheckerImpl>(_errorReporter))
{
}
void SMTChecker::analyze(SourceUnit const& _source)
{
m_impl->analyze(_source);
}

View File

@ -0,0 +1,45 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#pragma once
#include <map>
#include <string>
#include <memory>
namespace dev
{
namespace solidity
{
class ErrorReporter;
class SourceUnit;
class SMTCheckerImpl;
class SMTChecker
{
public:
SMTChecker(ErrorReporter& _errorReporter);
void analyze(SourceUnit const& _sources);
private:
std::shared_ptr<SMTCheckerImpl> m_impl;
};
}
}

View File

@ -0,0 +1,456 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/SMTCheckerImpl.h>
#include <libsolidity/interface/ErrorReporter.h>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SMTCheckerImpl::SMTCheckerImpl(ErrorReporter& _errorReporter):
m_solver(m_context),
m_errorReporter(_errorReporter)
{
}
void SMTCheckerImpl::analyze(SourceUnit const& _source)
{
bool pragmaFound = false;
for (auto const& node: _source.nodes())
if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get()))
if (pragma->literals()[0] == "checkAssertionsZ3")
pragmaFound = true;
if (pragmaFound)
{
m_solver.reset();
m_currentSequenceCounter.clear();
_source.accept(*this);
}
}
void SMTCheckerImpl::endVisit(VariableDeclaration const& _varDecl)
{
if (_varDecl.value())
{
m_errorReporter.warning(
_varDecl.location(),
"Assertion checker does not yet support this."
);
}
else if (_varDecl.isLocalOrReturn())
createVariable(_varDecl, true);
else if (_varDecl.isCallableParameter())
createVariable(_varDecl, false);
}
bool SMTCheckerImpl::visit(FunctionDefinition const& _function)
{
if (!_function.modifiers().empty() || _function.isConstructor())
m_errorReporter.warning(
_function.location(),
"Assertion checker does not yet support constructors and functions with modifiers."
);
// TODO actually we probably also have to reset all local variables and similar things.
m_currentFunction = &_function;
m_solver.push();
return true;
}
void SMTCheckerImpl::endVisit(FunctionDefinition const&)
{
// TOOD we could check for "reachability", i.e. satisfiability here.
m_solver.pop();
m_currentFunction = nullptr;
}
void SMTCheckerImpl::endVisit(VariableDeclarationStatement const& _varDecl)
{
if (_varDecl.declarations().size() != 1)
m_errorReporter.warning(
_varDecl.location(),
"Assertion checker does not yet support such variable declarations."
);
else if (knownVariable(*_varDecl.declarations()[0]) && _varDecl.initialValue())
// TODO more checks?
// TODO add restrictions about type (might be assignment from smaller type)
m_solver.add(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
else
m_errorReporter.warning(
_varDecl.location(),
"Assertion checker does not yet implement such variable declarations."
);
}
void SMTCheckerImpl::endVisit(ExpressionStatement const&)
{
}
void SMTCheckerImpl::endVisit(Assignment const& _assignment)
{
if (_assignment.assignmentOperator() != Token::Value::Assign)
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement compound assignment."
);
else if (_assignment.annotation().type->category() != Type::Category::Integer)
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
);
else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide()))
{
Declaration const* decl = identifier->annotation().referencedDeclaration;
if (knownVariable(*decl))
// TODO more checks?
// TODO add restrictions about type (might be assignment from smaller type)
m_solver.add(newValue(*decl) == expr(_assignment.rightHandSide()));
else
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement such assignments."
);
}
else
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement such assignments."
);
}
void SMTCheckerImpl::endVisit(TupleExpression const& _tuple)
{
if (_tuple.isInlineArray() || _tuple.components().size() != 1)
m_errorReporter.warning(
_tuple.location(),
"Assertion checker does not yet implement tules and inline arrays."
);
else
m_solver.add(expr(_tuple) == expr(*_tuple.components()[0]));
}
void SMTCheckerImpl::endVisit(BinaryOperation const& _op)
{
if (Token::isArithmeticOp(_op.getOperator()))
arithmeticOperation(_op);
else if (Token::isCompareOp(_op.getOperator()))
compareOperation(_op);
else if (Token::isBooleanOp(_op.getOperator()))
booleanOperation(_op);
else
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement this operator."
);
}
void SMTCheckerImpl::endVisit(FunctionCall const& _funCall)
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
if (funType.kind() == FunctionType::Kind::Assert)
{
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
m_solver.add(expr(*args[0]));
}
else if (funType.kind() == FunctionType::Kind::Require)
{
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
m_solver.add(expr(*args[0]));
checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code");
// TODO is there something meaningful we can check here?
// We can check whether the condition is always fulfilled or never fulfilled.
}
}
void SMTCheckerImpl::endVisit(Identifier const& _identifier)
{
Declaration const* decl = _identifier.annotation().referencedDeclaration;
solAssert(decl, "");
if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
{
m_solver.add(expr(_identifier) == currentValue(*decl));
return;
}
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;
// TODO for others, clear our knowledge about storage and memory
}
m_errorReporter.warning(
_identifier.location(),
"Assertion checker does not yet support the type of this expression (" +
_identifier.annotation().type->toString() +
")."
);
}
void SMTCheckerImpl::endVisit(Literal const& _literal)
{
Type const& type = *_literal.annotation().type;
if (type.category() == Type::Category::Integer || type.category() == Type::Category::RationalNumber)
{
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
solAssert(!rational->isFractional(), "");
m_solver.add(expr(_literal) == m_context.int_val(type.literalValue(&_literal).str().c_str()));
}
else
m_errorReporter.warning(
_literal.location(),
"Assertion checker does not yet support the type of this expression (" +
_literal.annotation().type->toString() +
")."
);
}
void SMTCheckerImpl::arithmeticOperation(BinaryOperation const& _op)
{
switch (_op.getOperator())
{
case Token::Add:
case Token::Sub:
case Token::Mul:
{
solAssert(_op.annotation().commonType, "");
solAssert(_op.annotation().commonType->category() == Type::Category::Integer, "");
z3::expr left(expr(_op.leftExpression()));
z3::expr right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator();
z3::expr value(
op == Token::Add ? left + right :
op == Token::Sub ? left - right :
/*op == Token::Mul*/ left * right
);
// Overflow check
auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
checkCondition(
value < minValue(intType),
_op.location(),
"Underflow (resulting value less than " + intType.minValue().str() + ")",
"value",
&value
);
checkCondition(
value > maxValue(intType),
_op.location(),
"Overflow (resulting value larger than " + intType.maxValue().str() + ")",
"value",
&value
);
m_solver.add(expr(_op) == value);
break;
}
default:
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement this operator."
);
}
}
void SMTCheckerImpl::compareOperation(BinaryOperation const& _op)
{
solAssert(_op.annotation().commonType, "");
if (_op.annotation().commonType->category() == Type::Category::Integer)
{
z3::expr left(expr(_op.leftExpression()));
z3::expr right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator();
z3::expr value = (
op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) :
op == Token::LessThan ? (left < right) :
op == Token::LessThanOrEqual ? (left <= right) :
op == Token::GreaterThan ? (left > right) :
/*op == Token::GreaterThanOrEqual*/ (left >= right)
);
// TODO: check that other values for op are not possible.
m_solver.add(expr(_op) == value);
}
else
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
);
}
void SMTCheckerImpl::booleanOperation(BinaryOperation const& _op)
{
solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, "");
solAssert(_op.annotation().commonType, "");
if (_op.annotation().commonType->category() == Type::Category::Bool)
{
if (_op.getOperator() == Token::And)
m_solver.add(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
else
m_solver.add(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
}
else
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
);
}
void SMTCheckerImpl::checkCondition(
z3::expr _condition,
SourceLocation const& _location,
string const& _description,
string const& _additionalValueName,
z3::expr* _additionalValue
)
{
m_solver.push();
m_solver.add(_condition);
switch (m_solver.check())
{
case z3::check_result::sat:
{
std::ostringstream message;
message << _description << " happens here";
if (m_currentFunction)
{
message << " for:\n";
z3::model m = m_solver.get_model();
if (_additionalValue)
message << " " << _additionalValueName << " = " << m.eval(*_additionalValue) << "\n";
for (auto const& param: m_currentFunction->parameters())
if (knownVariable(*param))
message << " " << param->name() << " = " << m.eval(currentValue(*param)) << "\n";
for (auto const& var: m_currentFunction->localVariables())
if (knownVariable(*var))
message << " " << var->name() << " = " << m.eval(currentValue(*var)) << "\n";
// message << m << endl;
// message << m_solver << endl;
}
else
message << ".";
m_errorReporter.warning(_location, message.str());
break;
}
case z3::check_result::unsat:
break;
case z3::check_result::unknown:
m_errorReporter.warning(_location, _description + " might happen here.");
break;
}
m_solver.pop();
}
void SMTCheckerImpl::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
{
if (auto intType = dynamic_cast<IntegerType const*>(_varDecl.type().get()))
{
solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_z3Variables.count(&_varDecl) == 0, "");
m_currentSequenceCounter[&_varDecl] = 0;
m_z3Variables.emplace(&_varDecl, m_context.function(uniqueSymbol(_varDecl).c_str(), m_context.int_sort(), m_context.int_sort()));
if (_setToZero)
m_solver.add(currentValue(_varDecl) == 0);
else
{
m_solver.add(currentValue(_varDecl) >= minValue(*intType));
m_solver.add(currentValue(_varDecl) <= maxValue(*intType));
}
}
else
m_errorReporter.warning(
_varDecl.location(),
"Assertion checker does not yet support the type of this variable."
);
}
string SMTCheckerImpl::uniqueSymbol(Declaration const& _decl)
{
return _decl.name() + "_" + to_string(_decl.id());
}
string SMTCheckerImpl::uniqueSymbol(Expression const& _expr)
{
return "expr_" + to_string(_expr.id());
}
bool SMTCheckerImpl::knownVariable(Declaration const& _decl)
{
return m_currentSequenceCounter.count(&_decl);
}
z3::expr SMTCheckerImpl::currentValue(Declaration const& _decl)
{
solAssert(m_currentSequenceCounter.count(&_decl), "");
return var(_decl)(m_currentSequenceCounter.at(&_decl));
}
z3::expr SMTCheckerImpl::newValue(const Declaration& _decl)
{
solAssert(m_currentSequenceCounter.count(&_decl), "");
m_currentSequenceCounter[&_decl]++;
return currentValue(_decl);
}
z3::expr SMTCheckerImpl::minValue(IntegerType const& _t)
{
return m_context.int_val(_t.minValue().str().c_str());
}
z3::expr SMTCheckerImpl::maxValue(IntegerType const& _t)
{
return m_context.int_val(_t.maxValue().str().c_str());
}
z3::expr SMTCheckerImpl::expr(Expression const& _e)
{
if (!m_z3Expressions.count(&_e))
{
solAssert(_e.annotation().type, "");
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_z3Expressions.emplace(&_e, m_context.int_const(uniqueSymbol(_e).c_str()));
break;
}
case Type::Category::Integer:
m_z3Expressions.emplace(&_e, m_context.int_const(uniqueSymbol(_e).c_str()));
break;
case Type::Category::Bool:
m_z3Expressions.emplace(&_e, m_context.bool_const(uniqueSymbol(_e).c_str()));
break;
default:
solAssert(false, "Type not implemented.");
}
}
return m_z3Expressions.at(&_e);
}
z3::func_decl SMTCheckerImpl::var(Declaration const& _decl)
{
solAssert(m_z3Variables.count(&_decl), "");
return m_z3Variables.at(&_decl);
}

View File

@ -0,0 +1,99 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#pragma once
#include <libsolidity/ast/ASTVisitor.h>
#include <z3++.h>
#include <map>
#include <string>
namespace dev
{
namespace solidity
{
class ErrorReporter;
class SMTCheckerImpl: private ASTConstVisitor
{
public:
SMTCheckerImpl(ErrorReporter& _errorReporter);
void analyze(SourceUnit const& _sources);
private:
// TODO: Check that we do not have concurrent reads and writes to a variable,
// because the order of expression evaluation is undefined
// TODO: or just force a certain order, but people might have a different idea about that.
virtual void endVisit(VariableDeclaration const& _node) override;
virtual bool visit(FunctionDefinition const& _node) override;
virtual void endVisit(FunctionDefinition const& _node) override;
virtual void endVisit(VariableDeclarationStatement const& _node) override;
virtual void endVisit(ExpressionStatement const& _node) override;
virtual void endVisit(Assignment const& _node) override;
virtual void endVisit(TupleExpression const& _node) override;
virtual void endVisit(BinaryOperation const& _node) override;
virtual void endVisit(FunctionCall const& _node) override;
virtual void endVisit(Identifier const& _node) override;
virtual void endVisit(Literal const& _node) override;
void arithmeticOperation(BinaryOperation const& _op);
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
void checkCondition(
z3::expr _condition,
SourceLocation const& _location,
std::string const& _description,
std::string const& _additionalValueName = "",
z3::expr* _additionalValue = nullptr
);
void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
std::string uniqueSymbol(Declaration const& _decl);
std::string uniqueSymbol(Expression const& _expr);
bool knownVariable(Declaration const& _decl);
z3::expr currentValue(Declaration const& _decl);
z3::expr newValue(Declaration const& _decl);
z3::expr minValue(IntegerType const& _t);
z3::expr maxValue(IntegerType const& _t);
/// Returns the z3 expression corresponding to the AST node. Creates a new expression
/// if it does not exist yet.
z3::expr expr(Expression const& _e);
/// Returns the z3 function declaration corresponding to the given variable.
/// The function takes one argument which is the "sequence number".
z3::func_decl var(Declaration const& _decl);
z3::context m_context;
z3::solver m_solver;
std::map<Declaration const*, int> m_currentSequenceCounter;
std::map<Expression const*, z3::expr> m_z3Expressions;
std::map<Declaration const*, z3::func_decl> m_z3Variables;
ErrorReporter& m_errorReporter;
FunctionDefinition const* m_currentFunction = nullptr;
};
}
}

View File

@ -37,6 +37,7 @@
#include <libsolidity/analysis/PostTypeChecker.h>
#include <libsolidity/analysis/SyntaxChecker.h>
#include <libsolidity/codegen/Compiler.h>
#include <libsolidity/formal/SMTChecker.h>
#include <libsolidity/interface/ABI.h>
#include <libsolidity/interface/Natspec.h>
#include <libsolidity/interface/GasEstimator.h>
@ -236,6 +237,13 @@ bool CompilerStack::analyze()
noErrors = false;
}
if (noErrors)
{
SMTChecker smtChecker(m_errorReporter);
for (Source const* source: m_sourceOrder)
smtChecker.analyze(*source->ast);
}
if (noErrors)
{
m_stackState = AnalysisSuccessful;