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 #2538 from ethereum/z3Conditions

Browse Source 
z3 conditions
This commit is contained in:
Alex Beregszaszi 2017-08-24 00:27:09 +01:00 committed by GitHub
commit 957f23a9f4
21 changed files with 1503 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -2,6 +2,7 @@
Features:
* ABI JSON: Include new field ``statemutability`` with values ``view``, ``nonpayable`` and ``payable``.
* Analyzer: Experimental partial support for Z3 SMT checker.
* Parser: Display previous visibility specifier in error if multiple are found.
* Parser: Introduce ``view`` keyword on functions (``constant`` remains an alias for ``view``).
* Syntax Checker: Support ``pragma experimental <feature>;`` to turn on experimental features.

9
cmake/FindZ3.cmake Normal file
View File

@ -0,0 +1,9 @@
find_path(Z3_INCLUDE_DIR z3++.h)
find_library(Z3_LIBRARY NAMES z3 )
include(${CMAKE_CURRENT_LIST_DIR}/FindPackageHandleStandardArgs.cmake)
FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR)
if(Z3_FOUND)
set(Z3_LIBRARIES ${Z3_LIBRARY})
endif()

11
libdevcore/CommonData.h
View File

@ -145,6 +145,17 @@ inline std::string toHex(u256 val, HexPrefix prefix = HexPrefix::DontAdd)
return (prefix == HexPrefix::Add) ? "0x" + str : str;
}
/// Returns decimal representation for small numbers and hex for large numbers.
inline std::string formatNumber(bigint const& _value)
{
if (_value < 0)
return "-" + formatNumber(-_value);
if (_value > 0x1000000)
return toHex(toCompactBigEndian(_value), 2, HexPrefix::Add);
else
return _value.str();
}
inline std::string toCompactHexWithPrefix(u256 val)
{
std::ostringstream ret;

14
libsolidity/CMakeLists.txt
View File

@ -2,5 +2,19 @@
file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp")
file(GLOB_RECURSE headers "*.h" "../libjulia/*.h")
find_package(Z3 QUIET)
if (${Z3_FOUND})
include_directories(${Z3_INCLUDE_DIR})
add_definitions(-DHAVE_Z3)
message("Z3 SMT solver FOUND.")
else()
message("Z3 SMT solver NOT found.")
list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp")
endif()
add_library(solidity ${sources} ${headers})
target_link_libraries(solidity PUBLIC evmasm devcore)
if (${Z3_FOUND})
target_link_libraries(solidity PUBLIC ${Z3_LIBRARY})
endif()

1
libsolidity/ast/AST.cpp
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>

3
libsolidity/ast/ExperimentalFeatures.h
View File

@ -29,6 +29,7 @@ namespace solidity
enum class ExperimentalFeature
{
SMTChecker,
ABIEncoderV2, // new ABI encoder that makes use of JULIA
Test,
TestOnlyAnalysis
@ -36,11 +37,13 @@ enum class ExperimentalFeature
static const std::map<ExperimentalFeature, bool> ExperimentalFeatureOnlyAnalysis =
{
{ ExperimentalFeature::SMTChecker, true },
{ ExperimentalFeature::TestOnlyAnalysis, true },
};
static const std::map<std::string, ExperimentalFeature> ExperimentalFeatureNames =
{
{ "SMTChecker", ExperimentalFeature::SMTChecker },
{ "ABIEncoderV2", ExperimentalFeature::ABIEncoderV2 },
{ "__test", ExperimentalFeature::Test },
{ "__testOnlyAnalysis", ExperimentalFeature::TestOnlyAnalysis },

588
libsolidity/formal/SMTChecker.cpp Normal file
View File

@ -0,0 +1,588 @@
/*
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>
#ifdef HAVE_Z3
#include <libsolidity/formal/Z3Interface.h>
#else
#include <libsolidity/formal/SMTLib2Interface.h>
#endif
#include <libsolidity/interface/ErrorReporter.h>
#include <boost/range/adaptor/map.hpp>
using namespace std;
using namespace dev;
using namespace dev::solidity;
SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
#ifdef HAVE_Z3
m_interface(make_shared<smt::Z3Interface>()),
#else
m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
#endif
m_errorReporter(_errorReporter)
{
(void)_readFileCallback;
}
void SMTChecker::analyze(SourceUnit const& _source)
{
if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
{
m_interface->reset();
m_currentSequenceCounter.clear();
m_nextFreeSequenceCounter.clear();
_source.accept(*this);
}
}
void SMTChecker::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 SMTChecker::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_interface->push();
return true;
}
void SMTChecker::endVisit(FunctionDefinition const&)
{
// TOOD we could check for "reachability", i.e. satisfiability here.
// We only handle local variables, so we clear everything.
// If we add storage variables, those should be cleared differently.
m_currentSequenceCounter.clear();
m_nextFreeSequenceCounter.clear();
m_interface->pop();
m_currentFunction = nullptr;
}
bool SMTChecker::visit(IfStatement const& _node)
{
_node.condition().accept(*this);
// TODO Check if condition is always true
auto countersAtStart = m_currentSequenceCounter;
m_interface->push();
m_interface->addAssertion(expr(_node.condition()));
_node.trueStatement().accept(*this);
auto countersAtEndOfTrue = m_currentSequenceCounter;
m_interface->pop();
decltype(m_currentSequenceCounter) countersAtEndOfFalse;
if (_node.falseStatement())
{
m_currentSequenceCounter = countersAtStart;
m_interface->push();
m_interface->addAssertion(!expr(_node.condition()));
_node.falseStatement()->accept(*this);
countersAtEndOfFalse = m_currentSequenceCounter;
m_interface->pop();
}
else
countersAtEndOfFalse = countersAtStart;
// Reset all values that have been touched.
// TODO this should use a previously generated side-effect structure
solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), "");
for (auto const& declCounter: countersAtEndOfTrue)
{
solAssert(countersAtEndOfFalse.count(declCounter.first), "");
auto decl = declCounter.first;
int trueCounter = countersAtEndOfTrue.at(decl);
int falseCounter = countersAtEndOfFalse.at(decl);
if (trueCounter == falseCounter)
continue; // Was not modified
newValue(*decl);
setValue(*decl, 0);
}
return false;
}
bool SMTChecker::visit(WhileStatement const& _node)
{
_node.condition().accept(*this);
//m_interface->push();
//m_interface->addAssertion(expr(_node.condition()));
// TDOO clear knowledge (increment sequence numbers and add bounds assertions ) apart from assertions
// TODO combine similar to if
return true;
}
void SMTChecker::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]))
{
if (_varDecl.initialValue())
// TODO more checks?
// TODO add restrictions about type (might be assignment from smaller type)
m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
}
else
m_errorReporter.warning(
_varDecl.location(),
"Assertion checker does not yet implement such variable declarations."
);
}
void SMTChecker::endVisit(ExpressionStatement const&)
{
}
void SMTChecker::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_interface->addAssertion(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 SMTChecker::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_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
}
void SMTChecker::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 SMTChecker::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_interface->addAssertion(expr(*args[0]));
}
else if (funType.kind() == FunctionType::Kind::Require)
{
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
m_interface->addAssertion(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 SMTChecker::endVisit(Identifier const& _identifier)
{
Declaration const* decl = _identifier.annotation().referencedDeclaration;
solAssert(decl, "");
if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
{
m_interface->addAssertion(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 SMTChecker::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_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
}
else
m_errorReporter.warning(
_literal.location(),
"Assertion checker does not yet support the type of this expression (" +
_literal.annotation().type->toString() +
")."
);
}
void SMTChecker::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, "");
smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator();
smt::Expression 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 " + formatNumber(intType.minValue()) + ")",
"value",
&value
);
checkCondition(
value > maxValue(intType),
_op.location(),
"Overflow (resulting value larger than " + formatNumber(intType.maxValue()) + ")",
"value",
&value
);
m_interface->addAssertion(expr(_op) == value);
break;
}
default:
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement this operator."
);
}
}
void SMTChecker::compareOperation(BinaryOperation const& _op)
{
solAssert(_op.annotation().commonType, "");
if (_op.annotation().commonType->category() == Type::Category::Integer)
{
smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator();
smt::Expression 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_interface->addAssertion(expr(_op) == value);
}
else
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
);
}
void SMTChecker::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_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
else
m_interface->addAssertion(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 SMTChecker::checkCondition(
smt::Expression _condition,
SourceLocation const& _location,
string const& _description,
string const& _additionalValueName,
smt::Expression* _additionalValue
)
{
m_interface->push();
m_interface->addAssertion(_condition);
vector<smt::Expression> expressionsToEvaluate;
vector<string> expressionNames;
if (m_currentFunction)
{
if (_additionalValue)
{
expressionsToEvaluate.emplace_back(*_additionalValue);
expressionNames.push_back(_additionalValueName);
}
for (auto const& param: m_currentFunction->parameters())
if (knownVariable(*param))
{
expressionsToEvaluate.emplace_back(currentValue(*param));
expressionNames.push_back(param->name());
}
for (auto const& var: m_currentFunction->localVariables())
if (knownVariable(*var))
{
expressionsToEvaluate.emplace_back(currentValue(*var));
expressionNames.push_back(var->name());
}
}
smt::CheckResult result;
vector<string> values;
try
{
tie(result, values) = m_interface->check(expressionsToEvaluate);
}
catch (smt::SolverError const& _e)
{
string description("Error querying SMT solver");
if (_e.comment())
description += ": " + *_e.comment();
m_errorReporter.warning(_location, description);
return;
}
switch (result)
{
case smt::CheckResult::SATISFIABLE:
{
std::ostringstream message;
message << _description << " happens here";
if (m_currentFunction)
{
message << " for:\n";
solAssert(values.size() == expressionNames.size(), "");
for (size_t i = 0; i < values.size(); ++i)
{
string formattedValue = values.at(i);
try
{
// Parse and re-format nicely
formattedValue = formatNumber(bigint(formattedValue));
}
catch (...) { }
message << " " << expressionNames.at(i) << " = " << formattedValue << "\n";
}
}
else
message << ".";
m_errorReporter.warning(_location, message.str());
break;
}
case smt::CheckResult::UNSATISFIABLE:
break;
case smt::CheckResult::UNKNOWN:
m_errorReporter.warning(_location, _description + " might happen here.");
break;
case smt::CheckResult::ERROR:
m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
break;
default:
solAssert(false, "");
}
m_interface->pop();
}
void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
{
if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
{
solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_Variables.count(&_varDecl) == 0, "");
m_currentSequenceCounter[&_varDecl] = 0;
m_nextFreeSequenceCounter[&_varDecl] = 1;
m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
setValue(_varDecl, _setToZero);
}
else
m_errorReporter.warning(
_varDecl.location(),
"Assertion checker does not yet support the type of this variable."
);
}
string SMTChecker::uniqueSymbol(Declaration const& _decl)
{
return _decl.name() + "_" + to_string(_decl.id());
}
string SMTChecker::uniqueSymbol(Expression const& _expr)
{
return "expr_" + to_string(_expr.id());
}
bool SMTChecker::knownVariable(Declaration const& _decl)
{
return m_currentSequenceCounter.count(&_decl);
}
smt::Expression SMTChecker::currentValue(Declaration const& _decl)
{
solAssert(m_currentSequenceCounter.count(&_decl), "");
return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl));
}
smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence)
{
return var(_decl)(_sequence);
}
smt::Expression SMTChecker::newValue(Declaration const& _decl)
{
solAssert(m_currentSequenceCounter.count(&_decl), "");
solAssert(m_nextFreeSequenceCounter.count(&_decl), "");
m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++;
return currentValue(_decl);
}
void SMTChecker::setValue(Declaration const& _decl, bool _setToZero)
{
auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
if (_setToZero)
m_interface->addAssertion(currentValue(_decl) == 0);
else
{
m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
}
}
smt::Expression SMTChecker::minValue(IntegerType const& _t)
{
return smt::Expression(_t.minValue());
}
smt::Expression SMTChecker::maxValue(IntegerType const& _t)
{
return smt::Expression(_t.maxValue());
}
smt::Expression SMTChecker::expr(Expression const& _e)
{
if (!m_Expressions.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_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break;
}
case Type::Category::Integer:
m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break;
case Type::Category::Bool:
m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
break;
default:
solAssert(false, "Type not implemented.");
}
}
return m_Expressions.at(&_e);
}
smt::Expression SMTChecker::var(Declaration const& _decl)
{
solAssert(m_Variables.count(&_decl), "");
return m_Variables.at(&_decl);
}

114
libsolidity/formal/SMTChecker.h Normal file
View File

@ -0,0 +1,114 @@
/*
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 <libsolidity/formal/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <map>
#include <string>
namespace dev
{
namespace solidity
{
class ErrorReporter;
class SMTChecker: private ASTConstVisitor
{
public:
SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
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 bool visit(IfStatement const& _node) override;
virtual bool visit(WhileStatement 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(
smt::Expression _condition,
SourceLocation const& _location,
std::string const& _description,
std::string const& _additionalValueName = "",
smt::Expression* _additionalValue = nullptr
);
void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
static std::string uniqueSymbol(Declaration const& _decl);
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 sequence number
bool knownVariable(Declaration const& _decl);
/// @returns an expression denoting the value of the variable declared in @a _decl
/// at the current point.
smt::Expression currentValue(Declaration const& _decl);
/// @returns an expression denoting the value of the variable declared in @a _decl
/// at the given sequence point. Does not ensure that this sequence point exists.
smt::Expression valueAtSequence(Declaration const& _decl, int _sequence);
/// Allocates a new sequence number for the declaration, updates the current
/// sequence number to this value and returns the expression.
smt::Expression newValue(Declaration const& _decl);
/// Sets the value of the declaration either to zero or to its intrinsic range.
void setValue(Declaration const& _decl, bool _setToZero);
static smt::Expression minValue(IntegerType const& _t);
static smt::Expression maxValue(IntegerType const& _t);
/// Returns the expression corresponding to the AST node. Creates a new expression
/// if it does not exist yet.
smt::Expression expr(Expression const& _e);
/// Returns the function declaration corresponding to the given variable.
/// The function takes one argument which is the "sequence number".
smt::Expression var(Declaration const& _decl);
std::shared_ptr<smt::SolverInterface> m_interface;
std::map<Declaration const*, int> m_currentSequenceCounter;
std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_Expressions;
std::map<Declaration const*, smt::Expression> m_Variables;
ErrorReporter& m_errorReporter;
FunctionDefinition const* m_currentFunction = nullptr;
};
}
}

187
libsolidity/formal/SMTLib2Interface.cpp Normal file
View File

@ -0,0 +1,187 @@
/*
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/SMTLib2Interface.h>
#include <libsolidity/interface/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
#include <boost/algorithm/string/predicate.hpp>
#include <boost/algorithm/string/join.hpp>
#include <boost/filesystem/operations.hpp>
#include <cstdio>
#include <fstream>
#include <iostream>
#include <memory>
#include <stdexcept>
#include <string>
#include <array>
using namespace std;
using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback):
m_queryCallback(_queryCallback)
{
reset();
}
void SMTLib2Interface::reset()
{
m_accumulatedOutput.clear();
m_accumulatedOutput.emplace_back();
write("(set-option :produce-models true)");
write("(set-logic QF_UFLIA)");
}
void SMTLib2Interface::push()
{
m_accumulatedOutput.emplace_back();
}
void SMTLib2Interface::pop()
{
solAssert(!m_accumulatedOutput.empty(), "");
m_accumulatedOutput.pop_back();
}
Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
{
write(
"(declare-fun |" +
_name +
"| (" +
(_domain == Sort::Int ? "Int" : "Bool") +
") " +
(_codomain == Sort::Int ? "Int" : "Bool") +
")"
);
return SolverInterface::newFunction(move(_name), _domain, _codomain);
}
Expression SMTLib2Interface::newInteger(string _name)
{
write("(declare-const |" + _name + "| Int)");
return SolverInterface::newInteger(move(_name));
}
Expression SMTLib2Interface::newBool(string _name)
{
write("(declare-const |" + _name + "| Bool)");
return SolverInterface::newBool(std::move(_name));
}
void SMTLib2Interface::addAssertion(Expression const& _expr)
{
write("(assert " + toSExpr(_expr) + ")");
}
pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
string response = querySolver(
boost::algorithm::join(m_accumulatedOutput, "\n") +
checkSatAndGetValuesCommand(_expressionsToEvaluate)
);
CheckResult result;
// TODO proper parsing
if (boost::starts_with(response, "sat\n"))
result = CheckResult::SATISFIABLE;
else if (boost::starts_with(response, "unsat\n"))
result = CheckResult::UNSATISFIABLE;
else if (boost::starts_with(response, "unknown\n"))
result = CheckResult::UNKNOWN;
else
result = CheckResult::ERROR;
vector<string> values;
if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR)
values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
return make_pair(result, values);
}
string SMTLib2Interface::toSExpr(Expression const& _expr)
{
if (_expr.arguments.empty())
return _expr.name;
std::string sexpr = "(" + _expr.name;
for (auto const& arg: _expr.arguments)
sexpr += " " + toSExpr(arg);
sexpr += ")";
return sexpr;
}
void SMTLib2Interface::write(string _data)
{
solAssert(!m_accumulatedOutput.empty(), "");
m_accumulatedOutput.back() += move(_data) + "\n";
}
string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
{
string command;
if (_expressionsToEvaluate.empty())
command = "(check-sat)\n";
else
{
// TODO make sure these are unique
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
{
auto const& e = _expressionsToEvaluate.at(i);
// TODO they don't have to be ints...
command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
}
command += "(check-sat)\n";
command += "(get-value (";
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
command += "|EVALEXPR_" + to_string(i) + "| ";
command += "))\n";
}
return command;
}
vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end)
{
vector<string> values;
while (_start < _end)
{
auto valStart = find(_start, _end, ' ');
if (valStart < _end)
++valStart;
auto valEnd = find(valStart, _end, ')');
values.emplace_back(valStart, valEnd);
_start = find(valEnd, _end, '(');
}
return values;
}
string SMTLib2Interface::querySolver(string const& _input)
{
if (!m_queryCallback)
BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
ReadCallback::Result queryResult = m_queryCallback(_input);
if (!queryResult.success)
BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
return queryResult.responseOrErrorMessage;
}

75
libsolidity/formal/SMTLib2Interface.h Normal file
View File

@ -0,0 +1,75 @@
/*
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/formal/SolverInterface.h>
#include <libsolidity/interface/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
#include <libdevcore/Common.h>
#include <boost/noncopyable.hpp>
#include <map>
#include <string>
#include <vector>
#include <cstdio>
namespace dev
{
namespace solidity
{
namespace smt
{
class SMTLib2Interface: public SolverInterface, public boost::noncopyable
{
public:
SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
void reset() override;
void push() override;
void pop() override;
Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
Expression newInteger(std::string _name) override;
Expression newBool(std::string _name) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
std::string toSExpr(Expression const& _expr);
void write(std::string _data);
std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
/// Communicates with the solver via the callback. Throws SMTSolverError on error.
std::string querySolver(std::string const& _input);
ReadCallback::Callback m_queryCallback;
std::vector<std::string> m_accumulatedOutput;
};
}
}
}

178
libsolidity/formal/SolverInterface.h Normal file
View File

@ -0,0 +1,178 @@
/*
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/interface/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
#include <libdevcore/Common.h>
#include <libdevcore/Exceptions.h>
#include <boost/noncopyable.hpp>
#include <map>
#include <string>
#include <vector>
#include <cstdio>
namespace dev
{
namespace solidity
{
namespace smt
{
enum class CheckResult
{
SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
};
enum class Sort
{
Int, Bool
};
/// C++ representation of an SMTLIB2 expression.
class Expression
{
friend class SolverInterface;
public:
Expression(size_t _number): name(std::to_string(_number)) {}
Expression(u256 const& _number): name(_number.str()) {}
Expression(bigint const& _number): name(_number.str()) {}
Expression(Expression const& _other) = default;
Expression(Expression&& _other) = default;
Expression& operator=(Expression const& _other) = default;
Expression& operator=(Expression&& _other) = default;
static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
{
return Expression("ite", std::vector<Expression>{
std::move(_condition), std::move(_trueValue), std::move(_falseValue)
});
}
friend Expression operator!(Expression _a)
{
return Expression("not", std::move(_a));
}
friend Expression operator&&(Expression _a, Expression _b)
{
return Expression("and", std::move(_a), std::move(_b));
}
friend Expression operator||(Expression _a, Expression _b)
{
return Expression("or", std::move(_a), std::move(_b));
}
friend Expression operator==(Expression _a, Expression _b)
{
return Expression("=", std::move(_a), std::move(_b));
}
friend Expression operator!=(Expression _a, Expression _b)
{
return !(std::move(_a) == std::move(_b));
}
friend Expression operator<(Expression _a, Expression _b)
{
return Expression("<", std::move(_a), std::move(_b));
}
friend Expression operator<=(Expression _a, Expression _b)
{
return Expression("<=", std::move(_a), std::move(_b));
}
friend Expression operator>(Expression _a, Expression _b)
{
return Expression(">", std::move(_a), std::move(_b));
}
friend Expression operator>=(Expression _a, Expression _b)
{
return Expression(">=", std::move(_a), std::move(_b));
}
friend Expression operator+(Expression _a, Expression _b)
{
return Expression("+", std::move(_a), std::move(_b));
}
friend Expression operator-(Expression _a, Expression _b)
{
return Expression("-", std::move(_a), std::move(_b));
}
friend Expression operator*(Expression _a, Expression _b)
{
return Expression("*", std::move(_a), std::move(_b));
}
Expression operator()(Expression _a) const
{
solAssert(arguments.empty(), "Attempted function application to non-function.");
return Expression(name, _a);
}
std::string const name;
std::vector<Expression> const arguments;
private:
/// Manual constructor, should only be used by SolverInterface and this class itself.
Expression(std::string _name, std::vector<Expression> _arguments):
name(std::move(_name)), arguments(std::move(_arguments)) {}
explicit Expression(std::string _name):
Expression(std::move(_name), std::vector<Expression>{}) {}
Expression(std::string _name, Expression _arg):
Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
Expression(std::string _name, Expression _arg1, Expression _arg2):
Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
};
DEV_SIMPLE_EXCEPTION(SolverError);
class SolverInterface
{
public:
virtual void reset() = 0;
virtual void push() = 0;
virtual void pop() = 0;
virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/)
{
// Subclasses should do something here
return Expression(std::move(_name), {});
}
virtual Expression newInteger(std::string _name)
{
// Subclasses should do something here
return Expression(std::move(_name), {});
}
virtual Expression newBool(std::string _name)
{
// Subclasses should do something here
return Expression(std::move(_name), {});
}
virtual void addAssertion(Expression const& _expr) = 0;
/// Checks for satisfiability, evaluates the expressions if a model
/// is available. Throws SMTSolverError on error.
virtual std::pair<CheckResult, std::vector<std::string>>
check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
};
}
}
}

189
libsolidity/formal/Z3Interface.cpp Normal file
View File

@ -0,0 +1,189 @@
/*
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/Z3Interface.h>
#include <libsolidity/interface/Exceptions.h>
#include <libdevcore/CommonIO.h>
using namespace std;
using namespace dev;
using namespace dev::solidity::smt;
Z3Interface::Z3Interface():
m_solver(m_context)
{
}
void Z3Interface::reset()
{
m_constants.clear();
m_functions.clear();
m_solver.reset();
}
void Z3Interface::push()
{
m_solver.push();
}
void Z3Interface::pop()
{
m_solver.pop();
}
Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain)
{
m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
return SolverInterface::newFunction(move(_name), _domain, _codomain);
}
Expression Z3Interface::newInteger(string _name)
{
m_constants.insert({_name, m_context.int_const(_name.c_str())});
return SolverInterface::newInteger(move(_name));
}
Expression Z3Interface::newBool(string _name)
{
m_constants.insert({_name, m_context.bool_const(_name.c_str())});
return SolverInterface::newBool(std::move(_name));
}
void Z3Interface::addAssertion(Expression const& _expr)
{
m_solver.add(toZ3Expr(_expr));
}
pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
// cout << "---------------------------------" << endl;
// cout << m_solver << endl;
CheckResult result;
switch (m_solver.check())
{
case z3::check_result::sat:
result = CheckResult::SATISFIABLE;
cout << "sat" << endl;
break;
case z3::check_result::unsat:
result = CheckResult::UNSATISFIABLE;
cout << "unsat" << endl;
break;
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
cout << "unknown" << endl;
break;
default:
solAssert(false, "");
}
// cout << "---------------------------------" << endl;
vector<string> values;
if (result != CheckResult::UNSATISFIABLE)
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)
values.push_back(toString(m.eval(toZ3Expr(e))));
}
return make_pair(result, values);
}
z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
{
if (_expr.arguments.empty() && m_constants.count(_expr.name))
return m_constants.at(_expr.name);
z3::expr_vector arguments(m_context);
for (auto const& arg: _expr.arguments)
arguments.push_back(toZ3Expr(arg));
static map<string, unsigned> arity{
{"ite", 3},
{"not", 1},
{"and", 2},
{"or", 2},
{"=", 2},
{"<", 2},
{"<=", 2},
{">", 2},
{">=", 2},
{"+", 2},
{"-", 2},
{"*", 2},
{">=", 2}
};
string const& n = _expr.name;
if (m_functions.count(n))
return m_functions.at(n)(arguments);
else if (m_constants.count(n))
{
solAssert(arguments.empty(), "");
return m_constants.at(n);
}
else if (arguments.empty())
{
// We assume it is an integer...
return m_context.int_val(n.c_str());
}
assert(arity.count(n) && arity.at(n) == arguments.size());
if (n == "ite")
return z3::ite(arguments[0], arguments[1], arguments[2]);
else if (n == "not")
return !arguments[0];
else if (n == "and")
return arguments[0] && arguments[1];
else if (n == "or")
return arguments[0] || arguments[1];
else if (n == "=")
return arguments[0] == arguments[1];
else if (n == "<")
return arguments[0] < arguments[1];
else if (n == "<=")
return arguments[0] <= arguments[1];
else if (n == ">")
return arguments[0] > arguments[1];
else if (n == ">=")
return arguments[0] >= arguments[1];
else if (n == "+")
return arguments[0] + arguments[1];
else if (n == "-")
return arguments[0] - arguments[1];
else if (n == "*")
return arguments[0] * arguments[1];
// Cannot reach here.
solAssert(false, "");
return arguments[0];
}
z3::sort Z3Interface::z3Sort(Sort _sort)
{
switch (_sort)
{
case Sort::Bool:
return m_context.bool_sort();
case Sort::Int:
return m_context.int_sort();
default:
break;
}
solAssert(false, "");
// Cannot be reached.
return m_context.int_sort();
}

65
libsolidity/formal/Z3Interface.h Normal file
View File

@ -0,0 +1,65 @@
/*
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/formal/SolverInterface.h>
#include <boost/noncopyable.hpp>
#include <z3++.h>
namespace dev
{
namespace solidity
{
namespace smt
{
class Z3Interface: public SolverInterface, public boost::noncopyable
{
public:
Z3Interface();
void reset() override;
void push() override;
void pop() override;
Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
Expression newInteger(std::string _name) override;
Expression newBool(std::string _name) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
z3::expr toZ3Expr(Expression const& _expr);
z3::sort z3Sort(smt::Sort _sort);
std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
z3::context m_context;
z3::solver m_solver;
std::map<std::string, z3::expr> m_constants;
std::map<std::string, z3::func_decl> m_functions;
};
}
}
}

14
libsolidity/interface/CompilerStack.cpp
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, m_smtQuery);
for (Source const* source: m_sourceOrder)
smtChecker.analyze(*source->ast);
}
if (noErrors)
{
m_stackState = AnalysisSuccessful;
@ -527,17 +535,17 @@ StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string
if (m_sources.count(importPath) || newSources.count(importPath))
continue;
ReadFile::Result result{false, string("File not supplied initially.")};
ReadCallback::Result result{false, string("File not supplied initially.")};
if (m_readFile)
result = m_readFile(importPath);
if (result.success)
newSources[importPath] = result.contentsOrErrorMessage;
newSources[importPath] = result.responseOrErrorMessage;
else
{
m_errorReporter.parserError(
import->location(),
string("Source \"" + importPath + "\" not found: " + result.contentsOrErrorMessage)
string("Source \"" + importPath + "\" not found: " + result.responseOrErrorMessage)
);
continue;
}

5
libsolidity/interface/CompilerStack.h
View File

@ -82,7 +82,7 @@ public:
/// Creates a new compiler stack.
/// @param _readFile callback to used to read files for import statements. Must return
/// and must not emit exceptions.
explicit CompilerStack(ReadFile::Callback const& _readFile = ReadFile::Callback()):
explicit CompilerStack(ReadCallback::Callback const& _readFile = ReadCallback::Callback()):
m_readFile(_readFile),
m_errorList(),
m_errorReporter(m_errorList) {}
@ -287,7 +287,8 @@ private:
std::string target;
};
ReadFile::Callback m_readFile;
ReadCallback::Callback m_readFile;
ReadCallback::Callback m_smtQuery;
bool m_optimize = false;
unsigned m_optimizeRuns = 200;
std::map<std::string, h160> m_libraries;

8
libsolidity/interface/ReadFile.h
View File

@ -27,17 +27,17 @@ namespace dev
namespace solidity
{
class ReadFile: boost::noncopyable
class ReadCallback: boost::noncopyable
{
public:
/// File reading result.
/// File reading or generic query result.
struct Result
{
bool success;
std::string contentsOrErrorMessage;
std::string responseOrErrorMessage;
};
/// File reading callback.
/// File reading or generic query callback.
using Callback = std::function<Result(std::string const&)>;
};

8
libsolidity/interface/StandardCompiler.cpp
View File

@ -203,10 +203,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
for (auto const& url: sources[sourceName]["urls"])
{
ReadFile::Result result = m_readFile(url.asString());
ReadCallback::Result result = m_readFile(url.asString());
if (result.success)
{
if (!hash.empty() && !hashMatchesContent(hash, result.contentsOrErrorMessage))
if (!hash.empty() && !hashMatchesContent(hash, result.responseOrErrorMessage))
errors.append(formatError(
false,
"IOError",
@ -215,13 +215,13 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
));
else
{
m_compilerStack.addSource(sourceName, result.contentsOrErrorMessage);
m_compilerStack.addSource(sourceName, result.responseOrErrorMessage);
found = true;
break;
}
}
else
failures.push_back("Cannot import url (\"" + url.asString() + "\"): " + result.contentsOrErrorMessage);
failures.push_back("Cannot import url (\"" + url.asString() + "\"): " + result.responseOrErrorMessage);
}
for (auto const& failure: failures)

4
libsolidity/interface/StandardCompiler.h
View File

@ -40,7 +40,7 @@ public:
/// Creates a new StandardCompiler.
/// @param _readFile callback to used to read files for import statements. Must return
/// and must not emit exceptions.
explicit StandardCompiler(ReadFile::Callback const& _readFile = ReadFile::Callback())
explicit StandardCompiler(ReadCallback::Callback const& _readFile = ReadCallback::Callback())
: m_compilerStack(_readFile), m_readFile(_readFile)
{
}
@ -56,7 +56,7 @@ private:
Json::Value compileInternal(Json::Value const& _input);
CompilerStack m_compilerStack;
ReadFile::Callback m_readFile;
ReadCallback::Callback m_readFile;
};
}

55
scripts/install_deps.sh
View File

@ -115,7 +115,7 @@ case $(uname -s) in
echo "Installing solidity dependencies on FreeBSD."
echo "ERROR - 'install_deps.sh' doesn't have FreeBSD support yet."
echo "Please let us know if you see this error message, and we can work out what is missing."
echo "Drop us a message at https://gitter.im/ethereum/solidity."
echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
exit 1
;;
@ -167,6 +167,7 @@ case $(uname -s) in
Debian)
#Debian
install_z3=""
case $(lsb_release -cs) in
wheezy)
#wheezy
@ -174,7 +175,7 @@ case $(uname -s) in
echo "ERROR - 'install_deps.sh' doesn't have Debian Wheezy support yet."
echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
echo "If you would like to get 'install_deps.sh' working for Debian Wheezy, that would be fantastic."
echo "Drop us a message at https://gitter.im/ethereum/solidity."
echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
echo "See also https://github.com/ethereum/webthree-umbrella/issues/495 where we are working through Alpine support."
exit 1
;;
@ -185,20 +186,19 @@ case $(uname -s) in
stretch)
#stretch
echo "Installing solidity dependencies on Debian Stretch (9.x)."
echo "ERROR - 'install_deps.sh' doesn't have Debian Stretch support yet."
echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
echo "If you would like to get 'install_deps.sh' working for Debian Stretch, that would be fantastic."
echo "Drop us a message at https://gitter.im/ethereum/solidity."
exit 1
install_z3="libz3-dev"
;;
buster)
#buster
echo "Installing solidity dependencies on Debian Buster (10.x)."
install_z3="libz3-dev"
;;
*)
#other Debian
echo "Installing solidity dependencies on unknown Debian version."
echo "ERROR - Debian Jessie is the only Debian version which solidity has been tested on."
echo "If you are using a different release and would like to get 'install_deps.sh'"
echo "working for that release that would be fantastic."
echo "Drop us a message at https://gitter.im/ethereum/solidity."
exit 1
echo "ERROR - This might not work, but we are trying anyway."
echo "Drop us a message at https://gitter.im/ethereum/solidity-dev"
install_z3="libz3-dev"
;;
esac
@ -211,7 +211,9 @@ case $(uname -s) in
gcc \
git \
libboost-all-dev \
unzip
unzip \
"$install_z3"
;;
@ -267,6 +269,7 @@ case $(uname -s) in
Ubuntu)
#Ubuntu
install_z3=""
case $(lsb_release -cs) in
trusty)
#trusty
@ -287,22 +290,25 @@ case $(uname -s) in
xenial)
#xenial
echo "Installing solidity dependencies on Ubuntu Xenial Xerus (16.04)."
install_z3="libz3-dev"
;;
yakkety)
#yakkety
echo "Installing solidity dependencies on Ubuntu Yakkety Yak (16.10)."
echo ""
echo "NOTE - You are in unknown territory with this preview OS."
echo "We will need to update the Ethereum PPAs, work through build and runtime breaks, etc."
echo "See https://github.com/ethereum/webthree-umbrella/issues/624."
echo "If you would like to partner with us to work through these, that"
echo "would be fantastic. Please just comment on that issue. Thanks!"
install_z3="libz3-dev"
;;
zesty)
#zesty
echo "Installing solidity dependencies on Ubuntu Zesty (17.04)."
install_z3="libz3-dev"
;;
*)
#other Ubuntu
echo "ERROR - Unknown or unsupported Ubuntu version (" $(lsb_release -cs) ")"
echo "We only support Trusty, Utopic, Vivid, Wily and Xenial, with work-in-progress on Yakkety."
exit 1
echo "ERROR - This might not work, but we are trying anyway."
echo "Please drop us a message at https://gitter.im/ethereum/solidity-dev."
echo "We only support Trusty, Utopic, Vivid, Wily, Xenial and Yakkety."
install_z3="libz3-dev"
;;
esac
@ -311,7 +317,8 @@ case $(uname -s) in
build-essential \
cmake \
git \
libboost-all-dev
libboost-all-dev \
"$install_z3"
if [ "$CI" = true ]; then
# Install 'eth', for use in the Solidity Tests-over-IPC.
# We will not use this 'eth', but its dependencies
@ -375,7 +382,7 @@ case $(uname -s) in
echo "ERROR - Unsupported or unidentified Linux distro."
echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
echo "If you would like to get your distro working, that would be fantastic."
echo "Drop us a message at https://gitter.im/ethereum/solidity."
echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
exit 1
;;
esac
@ -392,6 +399,6 @@ case $(uname -s) in
echo "ERROR - Unsupported or unidentified operating system."
echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
echo "If you would like to get your operating system working, that would be fantastic."
echo "Drop us a message at https://gitter.im/ethereum/solidity."
echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
;;
esac

14
solc/CommandLineInterface.cpp
View File

@ -663,7 +663,7 @@ Allowed options)",
bool CommandLineInterface::processInput()
{
ReadFile::Callback fileReader = [this](string const& _path)
ReadCallback::Callback fileReader = [this](string const& _path)
{
try
{
@ -683,25 +683,25 @@ bool CommandLineInterface::processInput()
}
}
if (!isAllowed)
return ReadFile::Result{false, "File outside of allowed directories."};
return ReadCallback::Result{false, "File outside of allowed directories."};
else if (!boost::filesystem::exists(path))
return ReadFile::Result{false, "File not found."};
return ReadCallback::Result{false, "File not found."};
else if (!boost::filesystem::is_regular_file(canonicalPath))
return ReadFile::Result{false, "Not a valid file."};
return ReadCallback::Result{false, "Not a valid file."};
else
{
auto contents = dev::contentsString(canonicalPath.string());
m_sourceCodes[path.string()] = contents;
return ReadFile::Result{true, contents};
return ReadCallback::Result{true, contents};
}
}
catch (Exception const& _exception)
{
return ReadFile::Result{false, "Exception in read callback: " + boost::diagnostic_information(_exception)};
return ReadCallback::Result{false, "Exception in read callback: " + boost::diagnostic_information(_exception)};
}
catch (...)
{
return ReadFile::Result{false, "Unknown exception in read callback."};
return ReadCallback::Result{false, "Unknown exception in read callback."};
}
};

12
solc/jsonCompiler.cpp
View File

@ -41,9 +41,9 @@ typedef void (*CStyleReadFileCallback)(char const* _path, char** o_contents, cha
namespace
{
ReadFile::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullptr)
ReadCallback::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullptr)
{
ReadFile::Callback readCallback;
ReadCallback::Callback readCallback;
if (_readCallback)
{
readCallback = [=](string const& _path)
@ -51,23 +51,23 @@ ReadFile::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullp
char* contents_c = nullptr;
char* error_c = nullptr;
_readCallback(_path.c_str(), &contents_c, &error_c);
ReadFile::Result result;
ReadCallback::Result result;
result.success = true;
if (!contents_c && !error_c)
{
result.success = false;
result.contentsOrErrorMessage = "File not found.";
result.responseOrErrorMessage = "File not found.";
}
if (contents_c)
{
result.success = true;
result.contentsOrErrorMessage = string(contents_c);
result.responseOrErrorMessage = string(contents_c);
free(contents_c);
}
if (error_c)
{
result.success = false;
result.contentsOrErrorMessage = string(error_c);
result.responseOrErrorMessage = string(error_c);
free(error_c);
}
return result;