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

Supply scanner to model checker.

Browse Source
This commit is contained in:
chriseth 2021-07-01 17:28:06 +02:00
parent 01dc77e5a2
commit e3525b81d0
11 changed files with 61 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
libsolidity/formal/BMC.cpp
View File

@ -22,6 +22,9 @@
#include <libsmtutil/SMTPortfolio.h>
#include <liblangutil/CharStream.h>
#include <liblangutil/CharStreamProvider.h>
#ifdef HAVE_Z3_DLOPEN
#include <z3_version.h>
#endif
@ -38,9 +41,10 @@ BMC::BMC(
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smtutil::SMTSolverChoice _enabledSolvers,
ModelCheckerSettings const& _settings
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings),
SMTEncoder(_context, _settings, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)),
m_outerErrorReporter(_errorReporter)
{
@ -650,7 +654,12 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
if (uf->annotation().type->isValueType())
{
expressionsToEvaluate.emplace_back(expr(*uf));
// TODO expressionNames.push_back(uf->location().text());
string expressionName;
if (uf->location().hasText())
expressionName = m_charStreamProvider.charStream(*uf->location().sourceName).text(
uf->location()
);
expressionNames.push_back(move(expressionName));
}
return {expressionsToEvaluate, expressionNames};

3
libsolidity/formal/BMC.h
View File

@ -63,7 +63,8 @@ public:
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smtutil::SMTSolverChoice _enabledSolvers,
ModelCheckerSettings const& _settings
ModelCheckerSettings const& _settings,
langutil::CharStreamProvider const& _charStreamProvider
);
void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>> _solvedTargets);

9
libsolidity/formal/CHC.cpp
View File

@ -57,9 +57,10 @@ CHC::CHC(
[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
SMTSolverChoice _enabledSolvers,
ModelCheckerSettings const& _settings
ModelCheckerSettings const& _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings),
SMTEncoder(_context, _settings, _charStreamProvider),
m_outerErrorReporter(_errorReporter),
m_enabledSolvers(_enabledSolvers)
{
@ -1741,7 +1742,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
path.emplace_back("State: " + modelMsg);
}
string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
list<string> calls;
auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void {
@ -1753,7 +1754,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
if (!pred->isConstructorSummary())
for (unsigned v: callGraph[node])
_dfs(node, v, depth + 1, _dfs);
calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node)));
calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider));
if (pred->isInternalCall())
calls.front() += " -- internal call";
else if (pred->isExternalCallTrusted())

3
libsolidity/formal/CHC.h
View File

@ -57,7 +57,8 @@ public:
std::map<util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smtutil::SMTSolverChoice _enabledSolvers,
ModelCheckerSettings const& _settings
ModelCheckerSettings const& _settings,
langutil::CharStreamProvider const& _charStreamProvider
);
void analyze(SourceUnit const& _sources);

5
libsolidity/formal/ModelChecker.cpp
View File

@ -32,6 +32,7 @@ using namespace solidity::frontend;
ModelChecker::ModelChecker(
ErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider,
map<h256, string> const& _smtlib2Responses,
ModelCheckerSettings _settings,
ReadCallback::Callback const& _smtCallback,
@ -40,8 +41,8 @@ ModelChecker::ModelChecker(
m_errorReporter(_errorReporter),
m_settings(_settings),
m_context(),
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings)
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings, _charStreamProvider),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings, _charStreamProvider)
{
}

1
libsolidity/formal/ModelChecker.h
View File

@ -49,6 +49,7 @@ public:
/// should be used, even if all are available. The default choice is to use all.
ModelChecker(
langutil::ErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider,
std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
ModelCheckerSettings _settings = ModelCheckerSettings{},
ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),

17
libsolidity/formal/Predicate.cpp
View File

@ -20,6 +20,8 @@
#include <libsolidity/formal/SMTEncoder.h>
#include <liblangutil/CharStreamProvider.h>
#include <liblangutil/CharStream.h>
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/TypeProvider.h>
@ -196,13 +198,20 @@ bool Predicate::isInterface() const
return m_type == PredicateType::Interface;
}
string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) const
string Predicate::formatSummaryCall(
vector<smtutil::Expression> const& _args,
langutil::CharStreamProvider const& _charStreamProvider
) const
{
solAssert(isSummary(), "");
//if (auto funCall = programFunctionCall())
// return funCall->location().text();
// TODO
if (auto funCall = programFunctionCall())
{
if (funCall->location().hasText())
return string(_charStreamProvider.charStream(*funCall->location().sourceName).text(funCall->location()));
else
return {};
}
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in preInputVars to format the function call,

10
libsolidity/formal/Predicate.h
View File

@ -27,6 +27,11 @@
#include <optional>
#include <vector>
namespace solidity::langutil
{
class CharStreamProvider;
}
namespace solidity::frontend
{
@ -142,7 +147,10 @@ public:
/// @returns a formatted string representing a call to this predicate
/// with _args.
std::string formatSummaryCall(std::vector<smtutil::Expression> const& _args) const;
std::string formatSummaryCall(
std::vector<smtutil::Expression> const& _args,
langutil::CharStreamProvider const& _charStreamProvider
) const;
/// @returns the values of the state variables from _args at the point
/// where this summary was reached.

8
libsolidity/formal/SMTEncoder.cpp
View File

@ -30,6 +30,8 @@
#include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/Helpers.h>
#include <liblangutil/CharStreamProvider.h>
#include <range/v3/view.hpp>
#include <boost/range/adaptors.hpp>
@ -45,11 +47,13 @@ using namespace solidity::frontend;
SMTEncoder::SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings
ModelCheckerSettings const& _settings,
langutil::CharStreamProvider const& _charStreamProvider
):
m_errorReporter(m_smtErrors),
m_context(_context),
m_settings(_settings)
m_settings(_settings),
m_charStreamProvider(_charStreamProvider)
{
}

8
libsolidity/formal/SMTEncoder.h
View File

@ -43,6 +43,7 @@ namespace solidity::langutil
{
class ErrorReporter;
struct SourceLocation;
class CharStreamProvider;
}
namespace solidity::frontend
@ -53,7 +54,8 @@ class SMTEncoder: public ASTConstVisitor
public:
SMTEncoder(
smt::EncodingContext& _context,
ModelCheckerSettings const& _settings
ModelCheckerSettings const& _settings,
langutil::CharStreamProvider const& _charStreamProvider
);
/// @returns true if engine should proceed with analysis.
@ -469,6 +471,10 @@ protected:
ModelCheckerSettings const& m_settings;
/// Character stream for each source,
/// used for retrieving source text of expressions for e.g. counter-examples.
langutil::CharStreamProvider const& m_charStreamProvider;
smt::SymbolicState& state();
};

2
libsolidity/interface/CompilerStack.cpp
View File

@ -555,7 +555,7 @@ bool CompilerStack::analyze()
if (noErrors)
{
ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
auto allSources = applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; });
modelChecker.enableAllEnginesIfPragmaPresent(allSources);
modelChecker.checkRequestedSourcesAndContracts(allSources);