Add invariants to ModelCheckerSettings

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,6 +148,7 @@ struct ModelCheckerSettings
 	/// might prefer the precise encoding.
 	bool divModNoSlacks = false;
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
+	ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
 	bool showUnproved = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
 	ModelCheckerTargets targets = ModelCheckerTargets::Default();
@@ -135,6 +161,7 @@ struct ModelCheckerSettings
 			contracts == _other.contracts &&
 			divModNoSlacks == _other.divModNoSlacks &&
 			engine == _other.engine &&
+			invariants == _other.invariants &&
 			showUnproved == _other.showUnproved &&
 			solvers == _other.solvers &&
 			targets == _other.targets &&