Merge remote-tracking branch 'origin/develop' into HEAD

This commit is contained in:
chriseth 2019-12-05 16:44:26 +01:00
commit e061f1e743
22 changed files with 201 additions and 28 deletions

View File

@ -47,6 +47,7 @@ Compiler Features:
Language Features: Language Features:
* Allow to obtain the selector of public or external library functions via a member ``.selector``. * Allow to obtain the selector of public or external library functions via a member ``.selector``.
* Parser: Allow splitting string and hexadecimal string literals into multiple parts. * Parser: Allow splitting string and hexadecimal string literals into multiple parts.
* Inline Assembly: Support referencing other constants.
Compiler Features: Compiler Features:
@ -66,7 +67,7 @@ Bugfixes:
* SMTChecker: Fix internal error when using arrays or mappings of functions. * SMTChecker: Fix internal error when using arrays or mappings of functions.
* SMTChecker: Fix internal error in array of structs type. * SMTChecker: Fix internal error in array of structs type.
* Yul: Consider infinite loops and recursion to be not removable. * Yul: Consider infinite loops and recursion to be not removable.
* Version Checker: 0.5.x-prerelease will match `pragma solidity ^0.5`.
### 0.5.13 (2019-11-14) ### 0.5.13 (2019-11-14)

View File

@ -86,7 +86,7 @@ but for quicker feedback, you might want to run specific tests.
Solidity includes different types of tests, most of them bundled into the Solidity includes different types of tests, most of them bundled into the
`Boost C++ Test Framework <https://www.boost.org/doc/libs/1_69_0/libs/test/doc/html/index.html>`_ application ``soltest``. `Boost C++ Test Framework <https://www.boost.org/doc/libs/1_69_0/libs/test/doc/html/index.html>`_ application ``soltest``.
Running ``build/test/soltest` or its wrapper ``scripts/soltest.sh`` is sufficient for most changes. Running ``build/test/soltest`` or its wrapper ``scripts/soltest.sh`` is sufficient for most changes.
Some tests require the ``evmone`` library, others require ``libz3``. Some tests require the ``evmone`` library, others require ``libz3``.
@ -113,7 +113,7 @@ See especially:
If you are running this in plain Command Prompt, use ``.\build\test\Release\soltest.exe -- --no-smt``. If you are running this in plain Command Prompt, use ``.\build\test\Release\soltest.exe -- --no-smt``.
To run a subset of tests, you can use filters: To run a subset of tests, you can use filters:
``./scripts/soltest.sh -t TestSuite/TestName, ``./scripts/soltest.sh -t TestSuite/TestName``,
where ``TestName`` can be a wildcard ``*``. where ``TestName`` can be a wildcard ``*``.
For example, here is an example test you might run; For example, here is an example test you might run;

View File

@ -105,8 +105,19 @@ bool SemVerMatchExpression::MatchComponent::matches(SemVerVersion const& _versio
didCompare = true; didCompare = true;
cmp = _version.numbers[i] - version.numbers[i]; cmp = _version.numbers[i] - version.numbers[i];
} }
if (cmp == 0 && !_version.prerelease.empty() && didCompare) if (cmp == 0 && !_version.prerelease.empty() && didCompare)
{
cmp = -1; cmp = -1;
for (unsigned i = levelsPresent; i < 3; i++)
{
if (_version.numbers[i] > 0)
{
cmp = 0;
break;
}
}
}
switch (prefix) switch (prefix)
{ {

View File

@ -39,6 +39,8 @@ set(sources
ast/ASTForward.h ast/ASTForward.h
ast/ASTJsonConverter.cpp ast/ASTJsonConverter.cpp
ast/ASTJsonConverter.h ast/ASTJsonConverter.h
ast/ASTUtils.cpp
ast/ASTUtils.h
ast/ASTVisitor.h ast/ASTVisitor.h
ast/ExperimentalFeatures.h ast/ExperimentalFeatures.h
ast/Types.cpp ast/Types.cpp

View File

@ -22,6 +22,7 @@
#include <libsolidity/analysis/TypeChecker.h> #include <libsolidity/analysis/TypeChecker.h>
#include <libsolidity/ast/AST.h> #include <libsolidity/ast/AST.h>
#include <libsolidity/ast/ASTUtils.h>
#include <libsolidity/ast/TypeProvider.h> #include <libsolidity/ast/TypeProvider.h>
#include <libyul/AsmAnalysis.h> #include <libyul/AsmAnalysis.h>
@ -658,6 +659,8 @@ bool TypeChecker::visit(InlineAssembly const& _inlineAssembly)
solAssert(var->type(), "Expected variable type!"); solAssert(var->type(), "Expected variable type!");
if (var->isConstant()) if (var->isConstant())
{ {
var = rootVariableDeclaration(*var);
if (!var->value()) if (!var->value())
{ {
m_errorReporter.typeError(_identifier.location, "Constant has no value."); m_errorReporter.typeError(_identifier.location, "Constant has no value.");
@ -668,7 +671,7 @@ bool TypeChecker::visit(InlineAssembly const& _inlineAssembly)
type(*var->value())->category() != Type::Category::RationalNumber type(*var->value())->category() != Type::Category::RationalNumber
)) ))
{ {
m_errorReporter.typeError(_identifier.location, "Only direct number constants are supported by inline assembly."); m_errorReporter.typeError(_identifier.location, "Only direct number constants and references to such constants are supported by inline assembly.");
return size_t(-1); return size_t(-1);
} }
else if (_context == yul::IdentifierContext::LValue) else if (_context == yul::IdentifierContext::LValue)

View File

@ -0,0 +1,42 @@
/*
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/ast/AST.h>
#include <libsolidity/ast/ASTUtils.h>
namespace dev
{
namespace solidity
{
VariableDeclaration const* rootVariableDeclaration(VariableDeclaration const& _varDecl)
{
solAssert(_varDecl.isConstant(), "Constant variable expected");
VariableDeclaration const* rootDecl = &_varDecl;
Identifier const* identifier;
while ((identifier = dynamic_cast<Identifier const*>(rootDecl->value().get())))
{
auto referencedVarDecl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration);
solAssert(referencedVarDecl && referencedVarDecl->isConstant(), "Identifier is not referencing a variable declaration");
rootDecl = referencedVarDecl;
}
return rootDecl;
}
}
}

View File

@ -0,0 +1,30 @@
/*
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
namespace dev
{
namespace solidity
{
/// Find the topmost referenced variable declaration when the given variable
/// declaration value is an identifier. Works only for constant variable declarations.
VariableDeclaration const* rootVariableDeclaration(VariableDeclaration const& _varDecl);
}
}

View File

@ -21,6 +21,7 @@
*/ */
#include <libsolidity/ast/AST.h> #include <libsolidity/ast/AST.h>
#include <libsolidity/ast/ASTUtils.h>
#include <libsolidity/ast/TypeProvider.h> #include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/codegen/CompilerUtils.h> #include <libsolidity/codegen/CompilerUtils.h>
#include <libsolidity/codegen/ContractCompiler.h> #include <libsolidity/codegen/ContractCompiler.h>
@ -668,6 +669,7 @@ bool ContractCompiler::visit(InlineAssembly const& _inlineAssembly)
{ {
if (variable->isConstant()) if (variable->isConstant())
{ {
variable = rootVariableDeclaration(*variable);
u256 value; u256 value;
if (variable->value()->annotation().type->category() == Type::Category::RationalNumber) if (variable->value()->annotation().type->category() == Type::Category::RationalNumber)
{ {

View File

@ -29,14 +29,17 @@ using namespace dev::solidity;
BMC::BMC( BMC::BMC(
smt::EncodingContext& _context, smt::EncodingContext& _context,
ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses, ErrorReporter& _errorReporter,
ReadCallback::Callback const& _smtCallback map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
): ):
SMTEncoder(_context), SMTEncoder(_context),
m_outerErrorReporter(_errorReporter), m_outerErrorReporter(_errorReporter),
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses, _smtCallback)) m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers))
{ {
#if defined (HAVE_Z3) || defined (HAVE_CVC4) #if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (_enabledSolvers.some())
if (!_smtlib2Responses.empty()) if (!_smtlib2Responses.empty())
m_errorReporter.warning( m_errorReporter.warning(
"SMT-LIB2 query responses were given in the auxiliary input, " "SMT-LIB2 query responses were given in the auxiliary input, "

View File

@ -57,7 +57,8 @@ public:
smt::EncodingContext& _context, smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter, langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses, std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
); );
void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions); void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);

View File

@ -36,17 +36,23 @@ CHC::CHC(
smt::EncodingContext& _context, smt::EncodingContext& _context,
ErrorReporter& _errorReporter, ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses, map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
): ):
SMTEncoder(_context), SMTEncoder(_context),
#ifdef HAVE_Z3 #ifdef HAVE_Z3
m_interface(make_shared<smt::Z3CHCInterface>()), m_interface(
_enabledSolvers.z3 ?
dynamic_pointer_cast<smt::CHCSolverInterface>(make_shared<smt::Z3CHCInterface>()) :
dynamic_pointer_cast<smt::CHCSolverInterface>(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback))
),
#else #else
m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback)), m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback)),
#endif #endif
m_outerErrorReporter(_errorReporter) m_outerErrorReporter(_errorReporter)
{ {
(void)_smtlib2Responses; (void)_smtlib2Responses;
(void)_enabledSolvers;
(void)_smtCallback; (void)_smtCallback;
} }

View File

@ -50,7 +50,8 @@ public:
smt::EncodingContext& _context, smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter, langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses, std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
); );
void analyze(SourceUnit const& _sources); void analyze(SourceUnit const& _sources);

View File

@ -25,10 +25,11 @@ using namespace dev::solidity;
ModelChecker::ModelChecker( ModelChecker::ModelChecker(
ErrorReporter& _errorReporter, ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses, map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
): ):
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback), m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback), m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
m_context() m_context()
{ {
} }

View File

@ -25,6 +25,7 @@
#include <libsolidity/formal/BMC.h> #include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/CHC.h> #include <libsolidity/formal/CHC.h>
#include <libsolidity/formal/EncodingContext.h> #include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h> #include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h> #include <liblangutil/ErrorReporter.h>
@ -43,10 +44,13 @@ namespace solidity
class ModelChecker class ModelChecker
{ {
public: public:
/// @param _enabledSolvers represents a runtime choice of which SMT solvers
/// should be used, even if all are available. The default choice is to use all.
ModelChecker( ModelChecker(
langutil::ErrorReporter& _errorReporter, langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses, std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback = ReadCallback::Callback() ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All()
); );
void analyze(SourceUnit const& _sources); void analyze(SourceUnit const& _sources);

View File

@ -32,16 +32,20 @@ using namespace dev::solidity::smt;
SMTPortfolio::SMTPortfolio( SMTPortfolio::SMTPortfolio(
map<h256, string> const& _smtlib2Responses, map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback ReadCallback::Callback const& _smtCallback,
SMTSolverChoice _enabledSolvers
) )
{ {
m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses, _smtCallback)); m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses, _smtCallback));
#ifdef HAVE_Z3 #ifdef HAVE_Z3
if (_enabledSolvers.z3)
m_solvers.emplace_back(make_unique<smt::Z3Interface>()); m_solvers.emplace_back(make_unique<smt::Z3Interface>());
#endif #endif
#ifdef HAVE_CVC4 #ifdef HAVE_CVC4
if (_enabledSolvers.cvc4)
m_solvers.emplace_back(make_unique<smt::CVC4Interface>()); m_solvers.emplace_back(make_unique<smt::CVC4Interface>());
#endif #endif
(void)_enabledSolvers;
} }
void SMTPortfolio::reset() void SMTPortfolio::reset()

View File

@ -44,7 +44,8 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable
public: public:
SMTPortfolio( SMTPortfolio(
std::map<h256, std::string> const& _smtlib2Responses, std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback ReadCallback::Callback const& _smtCallback,
SMTSolverChoice _enabledSolvers
); );
void reset() override; void reset() override;

View File

@ -36,6 +36,21 @@ namespace solidity
namespace smt namespace smt
{ {
struct SMTSolverChoice
{
bool cvc4 = false;
bool z3 = false;
static constexpr SMTSolverChoice All() { return {true, true}; }
static constexpr SMTSolverChoice CVC4() { return {true, false}; }
static constexpr SMTSolverChoice Z3() { return {false, true}; }
static constexpr SMTSolverChoice None() { return {false, false}; }
bool none() { return !some(); }
bool some() { return cvc4 || z3; }
bool all() { return cvc4 && z3; }
};
enum class CheckResult enum class CheckResult
{ {
SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR

View File

@ -70,6 +70,8 @@ BOOST_AUTO_TEST_CASE(positive_range)
{"*", "1.2.3-foo"}, {"*", "1.2.3-foo"},
{"1.0.0 - 2.0.0", "1.2.3"}, {"1.0.0 - 2.0.0", "1.2.3"},
{"1.0.0", "1.0.0"}, {"1.0.0", "1.0.0"},
{"1.0", "1.0.0"},
{"1", "1.0.0"},
{">=*", "0.2.4"}, {">=*", "0.2.4"},
{"*", "1.2.3"}, {"*", "1.2.3"},
{">=1.0.0", "1.0.0"}, {">=1.0.0", "1.0.0"},
@ -82,6 +84,8 @@ BOOST_AUTO_TEST_CASE(positive_range)
{"<=2.0.0", "0.2.9"}, {"<=2.0.0", "0.2.9"},
{"<2.0.0", "1.9999.9999"}, {"<2.0.0", "1.9999.9999"},
{"<2.0.0", "0.2.9"}, {"<2.0.0", "0.2.9"},
{"<1.0", "1.0.0-pre"},
{"<1", "1.0.0-pre"},
{">= 1.0.0", "1.0.0"}, {">= 1.0.0", "1.0.0"},
{">= 1.0.0", "1.0.1"}, {">= 1.0.0", "1.0.1"},
{">= 1.0.0", "1.1.0"}, {">= 1.0.0", "1.1.0"},
@ -137,6 +141,10 @@ BOOST_AUTO_TEST_CASE(positive_range)
{"^0.1.2", "0.1.2"}, {"^0.1.2", "0.1.2"},
{"^0.1", "0.1.2"}, {"^0.1", "0.1.2"},
{"^1.2", "1.4.2"}, {"^1.2", "1.4.2"},
{"^1.2", "1.2.1-pre"},
{"^1.2", "1.2.0"},
{"^1", "1.2.0-pre"},
{"^1", "1.2.0"},
{"<=1.2.3", "1.2.3-beta"}, {"<=1.2.3", "1.2.3-beta"},
{">1.2", "1.3.0-beta"}, {">1.2", "1.3.0-beta"},
{"<1.2.3", "1.2.3-beta"}, {"<1.2.3", "1.2.3-beta"},
@ -158,6 +166,8 @@ BOOST_AUTO_TEST_CASE(negative_range)
// Positive range tests // Positive range tests
vector<pair<string, string>> tests = { vector<pair<string, string>> tests = {
{"1.0.0 - 2.0.0", "2.2.3"}, {"1.0.0 - 2.0.0", "2.2.3"},
{"1.0", "1.0.0-pre"},
{"1", "1.0.0-pre"},
{"^1.2.3", "1.2.3-pre"}, {"^1.2.3", "1.2.3-pre"},
{"^1.2", "1.2.0-pre"}, {"^1.2", "1.2.0-pre"},
{"^1.2.3", "1.2.3-beta"}, {"^1.2.3", "1.2.3-beta"},

View File

@ -0,0 +1,26 @@
contract C {
uint constant a = 2;
uint constant aa = a;
uint constant aaa = aa;
bytes2 constant b = 0xabcd;
bytes2 constant bb = b;
bytes3 constant c = "abc";
bytes3 constant cc = c;
bytes3 constant ccc = cc;
bytes3 constant cccc = ccc;
bool constant d = true;
bool constant dd = d;
address payable constant e = 0x1212121212121212121212121212121212121212;
address payable constant ee = e;
function f() public pure returns (uint w, bytes2 x, bytes3 y, bool z, address t) {
assembly {
w := aaa
x := bb
y := cccc
z := dd
t := ee
}
}
}
// ----
// f() -> 2, left(0xabcd), left(0x616263), true, 0x1212121212121212121212121212121212121212

View File

@ -7,4 +7,4 @@ contract C {
} }
} }
// ---- // ----
// TypeError: (115-116): Only direct number constants are supported by inline assembly. // TypeError: (115-116): Only direct number constants and references to such constants are supported by inline assembly.

View File

@ -0,0 +1,11 @@
contract C {
bytes32 constant x = keccak256("abc");
bytes32 constant y = x;
function f() public pure returns (uint t) {
assembly {
t := y
}
}
}
// ----
// TypeError: (168-169): Only direct number constants and references to such constants are supported by inline assembly.

View File

@ -8,4 +8,3 @@ contract C {
} }
} }
// ---- // ----
// TypeError: (134-135): Only direct number constants are supported by inline assembly.