tests

Author: Leo Alt

libsolidity/formal/CHC.cpp

@@ -1722,15 +1722,24 @@ void CHC::checkVerificationTargets()
 			" Consider increasing the timeout per query."
 		);
 
-	if (m_settings.invariants)
-		for (auto const& [node, invs]: m_invariants)
+	if (!m_settings.invariants.invariants.empty())
+		for (auto const& [pred, invs]: m_invariants)
 		{
+			ASTNode const* node = pred->programNode();
 			string what;
 			if (auto contract = dynamic_cast<ContractDefinition const*>(node))
 				what = contract->fullyQualifiedName();
-			string msg = "Contract invariants and external call properties for " + what + ":\n";
+			string msg = "Inferred inductive properties for " + what + ":\n";
 			for (auto const& inv: invs)
-				msg += inv + "\n";
+			{
+				string invType;
+				if (pred->type() == PredicateType::Interface)
+					invType = "Contract invariant";
+				else if (pred->type() == PredicateType::NondetInterface)
+					invType = "Reentrancy property";
+				solAssert(!invType.empty(), "");
+				msg += invType + ": " + inv + "\n";
+			}
 			m_errorReporter.info(
 				1180_error,
 				node->location(),
@@ -1780,8 +1789,8 @@ void CHC::checkAndReportTarget(
 			predicates.insert(pred);
 		for (auto const* pred: m_nondetInterfaces | ranges::views::values)
 			predicates.insert(pred);
-		for (auto const& [node, invs]: collectInvariants(invariant, predicates))
-			m_invariants[node] += invs;
+		for (auto&& [pred, invs]: collectInvariants(invariant, predicates, m_settings.invariants))
+			m_invariants[pred] += move(invs);
 	}
 	else if (result == CheckResult::SATISFIABLE)
 	{

libsolidity/formal/CHC.h

@@ -380,7 +380,7 @@ class CHC: public SMTEncoder
 	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unprovedTargets;
 
 	/// Inferred invariants.
-	std::map<ASTNode const*, std::set<std::string>, smt::EncodingContext::IdCompare> m_invariants;
+	std::map<Predicate const*, std::set<std::string>, PredicateCompare> m_invariants;
 	//@}
 
 	/// Control-flow.

libsolidity/formal/Invariants.cpp

@@ -34,9 +34,18 @@ using namespace solidity::frontend::smt;
 namespace solidity::frontend::smt
 {
 
-map<ASTNode const*, set<string>> collectInvariants(smtutil::Expression const& _proof, set<Predicate const*> const& _predicates)
+map<Predicate const*, set<string>> collectInvariants(
+	smtutil::Expression const& _proof,
+	set<Predicate const*> const& _predicates,
+	ModelCheckerInvariants const& _invariantsSetting
+)
 {
-	set<string> targets{"interface_", "nondet_interface_"};
+	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>> eqs;
 	// Collect equalities where one of the sides is a predicate we're interested in.
 	BreadthFirstSearch<smtutil::Expression const*>{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) {
@@ -54,7 +63,7 @@ map<ASTNode const*, set<string>> collectInvariants(smtutil::Expression const& _p
 			_addChild(&arg);
 	});
 
-	map<ASTNode const*, set<string>> invariants;
+	map<Predicate const*, set<string>> invariants;
 	for (auto pred: _predicates)
 	{
 		auto predName = pred->functor().name;
@@ -69,7 +78,7 @@ map<ASTNode const*, set<string>> collectInvariants(smtutil::Expression const& _p
 		auto r = substitute(invExpr, pred->expressionSubstitution(predExpr));
 		// No point in reporting true/false as invariants.
 		if (!ignore.count(r.name))
-			invariants[pred->programNode()].insert(toSolidityStr(r));
+			invariants[pred].insert(toSolidityStr(r));
 	}
 	return invariants;
 }

libsolidity/formal/Invariants.h

@@ -18,6 +18,7 @@
 
 #pragma once
 
+#include <libsolidity/formal/ModelCheckerSettings.h>
 #include <libsolidity/formal/Predicate.h>
 
 #include <map>
@@ -27,6 +28,10 @@
 namespace solidity::frontend::smt
 {
 
-std::map<ASTNode const*, std::set<std::string>> collectInvariants(smtutil::Expression const& _proof, std::set<Predicate const*> const& _predicates);
+std::map<Predicate const*, std::set<std::string>> collectInvariants(
+	smtutil::Expression const& _proof,
+	std::set<Predicate const*> const& _predicates,
+	ModelCheckerInvariants const& _invariantsSettings
+);
 
 }

libsolidity/formal/ModelCheckerSettings.cpp

@@ -25,6 +25,40 @@ using namespace std;
 using namespace solidity;
 using namespace solidity::frontend;
 
+map<string, InvariantType> const ModelCheckerInvariants::validInvariants{
+	{"contract", InvariantType::Contract},
+	{"reentrancy", InvariantType::Reentrancy}
+};
+
+std::optional<ModelCheckerInvariants> ModelCheckerInvariants::fromString(string const& _invs)
+{
+	set<InvariantType> chosenInvs;
+	if (_invs == "default")
+	{
+		// The default is that no invariants are reported.
+	}
+	else if (_invs == "all")
+		for (auto&& v: validInvariants | ranges::views::values)
+			chosenInvs.insert(v);
+	else
+		for (auto&& t: _invs | ranges::views::split(',') | ranges::to<vector<string>>())
+		{
+			if (!validInvariants.count(t))
+				return {};
+			chosenInvs.insert(validInvariants.at(t));
+		}
+
+	return ModelCheckerInvariants{chosenInvs};
+}
+
+bool ModelCheckerInvariants::setFromString(string const& _inv)
+{
+	if (!validInvariants.count(_inv))
+		return false;
+	invariants.insert(validInvariants.at(_inv));
+	return true;
+}
+
 using TargetType = VerificationTargetType;
 map<string, TargetType> const ModelCheckerTargets::targetStrings{
 	{"constantCondition", TargetType::ConstantCondition},

libsolidity/formal/ModelCheckerSettings.h

@@ -87,6 +87,31 @@ struct ModelCheckerEngine
 	bool operator==(ModelCheckerEngine const& _other) const noexcept { return bmc == _other.bmc && chc == _other.chc; }
 };
 
+enum class InvariantType { Contract, Reentrancy };
+
+struct ModelCheckerInvariants
+{
+	/// Adds the default targets, that is, all except underflow and overflow.
+	static ModelCheckerInvariants Default() { return *fromString("default"); }
+	/// Adds all targets, including underflow and overflow.
+	static ModelCheckerInvariants All() { return *fromString("all"); }
+
+	static std::optional<ModelCheckerInvariants> fromString(std::string const& _invs);
+
+	bool has(InvariantType _inv) const { return invariants.count(_inv); }
+
+	/// @returns true if the @p _target is valid,
+	/// and false otherwise.
+	bool setFromString(std::string const& _target);
+
+	static std::map<std::string, InvariantType> const validInvariants;
+
+	bool operator!=(ModelCheckerInvariants const& _other) const noexcept { return !(*this == _other); }
+	bool operator==(ModelCheckerInvariants const& _other) const noexcept { return invariants == _other.invariants; }
+
+	std::set<InvariantType> invariants;
+};
+
 enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
 
 struct ModelCheckerTargets
@@ -123,7 +148,7 @@ struct ModelCheckerSettings
 	/// might prefer the precise encoding.
 	bool divModNoSlacks = false;
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
-	bool invariants = false;
+	ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
 	bool showUnproved = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
 	ModelCheckerTargets targets = ModelCheckerTargets::Default();

libsolidity/formal/Predicate.h

@@ -21,6 +21,8 @@
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsolidity/ast/AST.h>
+
 #include <libsmtutil/Sorts.h>
 
 #include <map>
@@ -214,4 +216,12 @@ class Predicate
 	std::vector<ScopeOpener const*> const m_scopeStack;
 };
 
+struct PredicateCompare
+{
+	bool operator()(Predicate const* lhs, Predicate const* rhs) const
+	{
+		return lhs->programNode()->id() < rhs->programNode()->id();
+	}
+};
+
 }

libsolidity/interface/StandardCompiler.cpp

@@ -441,7 +441,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"contracts", "divModNoSlacks", "engine", "showUnproved", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -958,6 +958,27 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("invariants"))
+	{
+		auto const& invariantsArray = modelCheckerSettings["invariants"];
+		if (!invariantsArray.isArray())
+			return formatFatalError("JSONError", "settings.modelChecker.invariants must be an array.");
+
+		ModelCheckerInvariants invariants;
+		for (auto const& i: invariantsArray)
+		{
+			if (!i.isString())
+				return formatFatalError("JSONError", "Every invariant type in settings.modelChecker.invariants must be a string.");
+			if (!invariants.setFromString(i.asString()))
+				return formatFatalError("JSONError", "Invalid model checker invariants requested.");
+		}
+
+		if (invariants.invariants.empty())
+			return formatFatalError("JSONError", "settings.modelChecker.invariants must be a non-empty array.");
+
+		ret.modelCheckerSettings.invariants = invariants;
+	}
+
 	if (modelCheckerSettings.isMember("showUnproved"))
 	{
 		auto const& showUnproved = modelCheckerSettings["showUnproved"];

solc/CommandLineParser.cpp

@@ -746,7 +746,10 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerInvariants.c_str(),
+			po::value<string>()->value_name("default,all,contract,reentrancy")->default_value("default"),
 			"Select whether to report inferred contract inductive invariants."
+			"Multiple types of invariants can be selected at the same time, separated by a comma and no spaces."
+			" By default no invariants are reported."
 		)
 		(
 			g_strModelCheckerShowUnproved.c_str(),
@@ -1170,7 +1173,16 @@ bool CommandLineParser::processArgs()
 	}
 
 	if (m_args.count(g_strModelCheckerInvariants))
-		m_options.modelChecker.settings.invariants = true;
+	{
+		string invsStr = m_args[g_strModelCheckerInvariants].as<string>();
+		optional<ModelCheckerInvariants> invs = ModelCheckerInvariants::fromString(invsStr);
+		if (!invs)
+		{
+			serr() << "Invalid option for --" << g_strModelCheckerInvariants << ": " << invsStr << endl;
+			return false;
+		}
+		m_options.modelChecker.settings.invariants = *invs;
+	}
 
 	if (m_args.count(g_strModelCheckerShowUnproved))
 		m_options.modelChecker.settings.showUnproved = true;

test/libsolidity/SMTCheckerTest.cpp

@@ -59,7 +59,7 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 	if (m_modelCheckerSettings.solvers.none() || m_modelCheckerSettings.engine.none())
 		m_shouldRun = false;
 
-	m_modelCheckerSettings.invariants = true;
+	m_modelCheckerSettings.invariants = ModelCheckerInvariants::All();
 
 	auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "no");
 	if (ignoreCex == "no")