Add Invariants which traverses the proof and collects invariants for the given predicates

libsolidity/formal/Invariants.cpp

@@ -0,0 +1,86 @@
+/*
+	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.
+	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;
+}
+
+}

libsolidity/formal/Invariants.h

@@ -0,0 +1,37 @@
+/*
+	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
+
+#pragma once
+
+#include <libsolidity/formal/ModelCheckerSettings.h>
+#include <libsolidity/formal/Predicate.h>
+
+#include <map>
+#include <set>
+#include <string>
+
+namespace solidity::frontend::smt
+{
+
+std::map<Predicate const*, std::set<std::string>> collectInvariants(
+	smtutil::Expression const& _proof,
+	std::set<Predicate const*> const& _predicates,
+	ModelCheckerInvariants const& _invariantsSettings
+);
+
+}