cerc-io/solidity
10
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 #7184 from ethereum/smt_fix_scanner

Browse Source 
[SMTChecker] Fix ICE when reporting cex
This commit is contained in:
Leonardo 2019-08-10 21:40:44 +02:00 committed by GitHub
commit f5f2bbb274
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 29 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -28,6 +28,7 @@ Bugfixes:
* SMTChecker: Fix internal error when using compound bitwise assignment operators inside branches.
* SMTChecker: Fix internal error when inlining a function that returns a tuple containing an unsupported type inside a branch.
* SMTChecker: Fix internal error when inlining functions that use state variables and belong to a different source.
* SMTChecker: Fix internal error when reporting counterexamples concerning state variables from different source files.
* View/Pure Checker: Properly detect state variable access through base class.
* Yul analyzer: Check availability of data objects already in analysis phase.
* Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program.

12
liblangutil/SourceLocation.h
View File

@ -22,7 +22,9 @@
#pragma once
#include <libdevcore/Assertions.h>
#include <libdevcore/Common.h> // defines noexcept macro for MSVC
#include <libdevcore/Exceptions.h>
#include <liblangutil/CharStream.h>
#include <memory>
#include <string>
@ -31,6 +33,7 @@
namespace langutil
{
struct SourceLocationError: virtual dev::Exception {};
/**
* Representation of an interval of source positions.
@ -49,6 +52,15 @@ struct SourceLocation
bool isEmpty() const { return start == -1 && end == -1; }
std::string text() const
{
assertThrow(source, SourceLocationError, "Requested text from null source.");
assertThrow(!isEmpty(), SourceLocationError, "Requested text from empty source location.");
assertThrow(start <= end, SourceLocationError, "Invalid source location.");
assertThrow(end <= int(source->source().length()), SourceLocationError, "Invalid source location.");
return source->source().substr(start, end - start);
}
/// @returns the smallest SourceLocation that contains both @param _a and @param _b.
/// Assumes that @param _a and @param _b refer to the same source (exception: if the source of either one
/// is unset, the source of the other will be used for the result, even if that is unset as well).

9
libsolidity/formal/BMC.cpp
View File

@ -43,12 +43,10 @@ BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256
#endif
}
void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner, set<Expression const*> _safeAssertions)
void BMC::analyze(SourceUnit const& _source, set<Expression const*> _safeAssertions)
{
solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
m_scanner = _scanner;
m_safeAssertions += move(_safeAssertions);
m_context.setSolver(m_interface);
m_context.clear();
@ -542,7 +540,7 @@ pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
if (uf->annotation().type->isValueType())
{
expressionsToEvaluate.emplace_back(expr(*uf));
expressionNames.push_back(m_scanner->sourceAt(uf->location()));
expressionNames.push_back(uf->location().text());
}
return {expressionsToEvaluate, expressionNames};
@ -717,14 +715,11 @@ void BMC::checkCondition(
vector<string> expressionNames;
tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
if (callStack.size())
{
solAssert(m_scanner, "");
if (_additionalValue)
{
expressionsToEvaluate.emplace_back(*_additionalValue);
expressionNames.push_back(_additionalValueName);
}
}
smt::CheckResult result;
vector<string> values;
tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);

3
libsolidity/formal/BMC.h
View File

@ -34,7 +34,6 @@
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/Scanner.h>
#include <set>
#include <string>
@ -56,7 +55,7 @@ class BMC: public SMTEncoder
public:
BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner, std::set<Expression const*> _safeAssertions);
void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
/// This is used if the SMT solver is not directly linked into this binary.
/// @returns a list of inputs to the SMT solver that were not part of the argument to

4
libsolidity/formal/CHC.cpp
View File

@ -39,12 +39,10 @@ CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter):
{
}
void CHC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
void CHC::analyze(SourceUnit const& _source)
{
solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
m_scanner = _scanner;
#ifdef HAVE_Z3
auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
solAssert(z3Interface, "");

2
libsolidity/formal/CHC.h
View File

@ -46,7 +46,7 @@ class CHC: public SMTEncoder
public:
CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter);
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
void analyze(SourceUnit const& _sources);
std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }

6
libsolidity/formal/ModelChecker.cpp
View File

@ -29,13 +29,13 @@ ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> cons
{
}
void ModelChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
void ModelChecker::analyze(SourceUnit const& _source)
{
if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
return;
m_chc.analyze(_source, _scanner);
m_bmc.analyze(_source, _scanner, m_chc.safeAssertions());
m_chc.analyze(_source);
m_bmc.analyze(_source, m_chc.safeAssertions());
}
vector<string> ModelChecker::unhandledQueries()

3
libsolidity/formal/ModelChecker.h
View File

@ -28,7 +28,6 @@
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/Scanner.h>
namespace langutil
{
@ -46,7 +45,7 @@ class ModelChecker
public:
ModelChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
void analyze(SourceUnit const& _sources);
/// This is used if the SMT solver is not directly linked into this binary.
/// @returns a list of inputs to the SMT solver that were not part of the argument to

2
libsolidity/formal/SMTEncoder.h
View File

@ -30,7 +30,6 @@
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/Scanner.h>
#include <string>
#include <unordered_map>
@ -231,7 +230,6 @@ protected:
/// warning before the others in case it's needed.
langutil::ErrorReporter m_errorReporter;
langutil::ErrorList m_smtErrors;
std::shared_ptr<langutil::Scanner> m_scanner;
/// Stores the current function/modifier call/invocation path.
std::vector<CallStackEntry> m_callStack;

2
libsolidity/interface/CompilerStack.cpp
View File

@ -373,7 +373,7 @@ bool CompilerStack::analyze()
{
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses);
for (Source const* source: m_sourceOrder)
modelChecker.analyze(*source->ast, source->scanner);
modelChecker.analyze(*source->ast);
m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
}
}

8
test/libsolidity/SMTChecker.cpp
View File

@ -257,8 +257,11 @@ BOOST_AUTO_TEST_CASE(import_base)
pragma solidity >=0.0;
contract Base {
uint x;
function f() internal {
address a;
function f() internal returns (uint) {
a = address(this);
++x;
return 2;
}
}
)"},
@ -268,7 +271,7 @@ BOOST_AUTO_TEST_CASE(import_base)
import "base";
contract Der is Base {
function g(uint y) public {
f();
x += f();
assert(y > x);
}
}
@ -328,6 +331,7 @@ BOOST_AUTO_TEST_CASE(import_library)
}
BOOST_AUTO_TEST_SUITE_END()
}