mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
87 lines
2.6 KiB
C++
87 lines
2.6 KiB
C++
/*
|
|
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;
|
|
}
|
|
|
|
}
|