solidity/libsolidity/formal/Invariants.cpp

87 lines
2.6 KiB
C++
Raw Normal View History

/*
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/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsolidity/formal/Invariants.h>
#include <libsolidity/formal/ExpressionFormatter.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolutil/Algorithms.h>
#include <boost/algorithm/string.hpp>
using namespace std;
using boost::algorithm::starts_with;
using namespace solidity;
using namespace solidity::smtutil;
using namespace solidity::frontend::smt;
namespace solidity::frontend::smt
{
map<Predicate const*, set<string>> collectInvariants(
smtutil::Expression const& _proof,
set<Predicate const*> const& _predicates,
ModelCheckerInvariants const& _invariantsSetting
)
{
set<string> targets;
if (_invariantsSetting.has(InvariantType::Contract))
targets.insert("interface_");
if (_invariantsSetting.has(InvariantType::Reentrancy))
targets.insert("nondet_interface_");
map<string, pair<smtutil::Expression, smtutil::Expression>> equalities;
// Collect equalities where one of the sides is a predicate we're interested in.
util::BreadthFirstSearch<smtutil::Expression const*>{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) {
if (_expr->name == "=")
for (auto const& t: targets)
{
auto arg0 = _expr->arguments.at(0);
auto arg1 = _expr->arguments.at(1);
if (starts_with(arg0.name, t))
equalities.insert({arg0.name, {arg0, move(arg1)}});
else if (starts_with(arg1.name, t))
equalities.insert({arg1.name, {arg1, move(arg0)}});
}
for (auto const& arg: _expr->arguments)
_addChild(&arg);
});
map<Predicate const*, set<string>> invariants;
for (auto pred: _predicates)
{
auto predName = pred->functor().name;
if (!equalities.count(predName))
continue;
solAssert(pred->contextContract(), "");
auto const& [predExpr, invExpr] = equalities.at(predName);
static set<string> const ignore{"true", "false"};
auto r = substitute(invExpr, pred->expressionSubstitution(predExpr));
// No point in reporting true/false as invariants.
if (!ignore.count(r.name))
invariants[pred].insert(toSolidityStr(r));
}
return invariants;
}
}