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 #5398 from ethereum/smt_model_scanner

Browse Source 
Add Scanner function that prints source based on SourceLocation
This commit is contained in:
Leonardo 2018-11-13 16:06:10 +01:00 committed by GitHub
commit c21c7e74fe
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 15 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolidity/formal/SMTChecker.cpp
View File

@ -37,9 +37,10 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
{ {
} }
void SMTChecker::analyze(SourceUnit const& _source) void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
{ {
m_variableUsage = make_shared<VariableUsage>(_source); m_variableUsage = make_shared<VariableUsage>(_source);
m_scanner = _scanner;
if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
_source.accept(*this); _source.accept(*this);
} }
@ -753,6 +754,7 @@ void SMTChecker::checkCondition(
vector<string> expressionNames; vector<string> expressionNames;
if (m_functionPath.size()) if (m_functionPath.size())
{ {
solAssert(m_scanner, "");
if (_additionalValue) if (_additionalValue)
{ {
expressionsToEvaluate.emplace_back(*_additionalValue); expressionsToEvaluate.emplace_back(*_additionalValue);

5
libsolidity/formal/SMTChecker.h
View File

@ -25,6 +25,8 @@
#include <libsolidity/interface/ReadFile.h> #include <libsolidity/interface/ReadFile.h>
#include <libsolidity/parsing/Scanner.h>
#include <unordered_map> #include <unordered_map>
#include <string> #include <string>
#include <vector> #include <vector>
@ -42,7 +44,7 @@ class SMTChecker: private ASTConstVisitor
public: public:
SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback); SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
void analyze(SourceUnit const& _sources); void analyze(SourceUnit const& _sources, std::shared_ptr<Scanner> const& _scanner);
private: private:
// TODO: Check that we do not have concurrent reads and writes to a variable, // TODO: Check that we do not have concurrent reads and writes to a variable,
@ -193,6 +195,7 @@ private:
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables; std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
std::vector<smt::Expression> m_pathConditions; std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter; ErrorReporter& m_errorReporter;
std::shared_ptr<Scanner> m_scanner;
/// Stores the current path of function calls. /// Stores the current path of function calls.
std::vector<FunctionDefinition const*> m_functionPath; std::vector<FunctionDefinition const*> m_functionPath;

2
libsolidity/interface/CompilerStack.cpp
View File

@ -284,7 +284,7 @@ bool CompilerStack::analyze()
{ {
SMTChecker smtChecker(m_errorReporter, m_smtQuery); SMTChecker smtChecker(m_errorReporter, m_smtQuery);
for (Source const* source: m_sourceOrder) for (Source const* source: m_sourceOrder)
smtChecker.analyze(*source->ast); smtChecker.analyze(*source->ast, source->scanner);
} }
} }
catch(FatalError const&) catch(FatalError const&)

7
libsolidity/parsing/Scanner.h
View File

@ -162,6 +162,13 @@ public:
/// Do only use in error cases, they are quite expensive. /// Do only use in error cases, they are quite expensive.
std::string lineAtPosition(int _position) const { return m_source.lineAtPosition(_position); } std::string lineAtPosition(int _position) const { return m_source.lineAtPosition(_position); }
std::tuple<int, int> translatePositionToLineColumn(int _position) const { return m_source.translatePositionToLineColumn(_position); } std::tuple<int, int> translatePositionToLineColumn(int _position) const { return m_source.translatePositionToLineColumn(_position); }
std::string sourceAt(SourceLocation const& _location) const
{
solAssert(!_location.isEmpty(), "");
solAssert(m_sourceName && _location.sourceName, "");
solAssert(*m_sourceName == *_location.sourceName, "");
return m_source.source().substr(_location.start, _location.end - _location.start);
}
///@} ///@}
private: private: