From 3118fb366656a4af2066ab75b77aaefcf2bee25e Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Wed, 6 Oct 2021 11:51:22 +0200
Subject: [PATCH] Add invariants option to CLI and JSON

---
 libsolidity/interface/StandardCompiler.cpp | 23 +++++++++++++++++++++-
 solc/CommandLineParser.cpp                 | 21 ++++++++++++++++++++
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 66f5dc4e5..da28cf29f 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -445,7 +445,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");
 }
 
@@ -987,6 +987,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"];
diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp
index 6b1fc1526..22d92d463 100644
--- a/solc/CommandLineParser.cpp
+++ b/solc/CommandLineParser.cpp
@@ -78,6 +78,7 @@ static string const g_strMetadataLiteral = "metadata-literal";
 static string const g_strModelCheckerContracts = "model-checker-contracts";
 static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks";
 static string const g_strModelCheckerEngine = "model-checker-engine";
+static string const g_strModelCheckerInvariants = "model-checker-invariants";
 static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
 static string const g_strModelCheckerSolvers = "model-checker-solvers";
 static string const g_strModelCheckerTargets = "model-checker-targets";
@@ -801,6 +802,13 @@ General Information)").c_str(),
 			po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
 			"Select model checker engine."
 		)
+		(
+			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(),
 			"Show all unproved targets separately."
@@ -1253,6 +1261,18 @@ bool CommandLineParser::processArgs()
 		m_options.modelChecker.settings.engine = *engine;
 	}
 
+	if (m_args.count(g_strModelCheckerInvariants))
+	{
+		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;
 
@@ -1288,6 +1308,7 @@ bool CommandLineParser::processArgs()
 		m_args.count(g_strModelCheckerContracts) ||
 		m_args.count(g_strModelCheckerDivModNoSlacks) ||
 		m_args.count(g_strModelCheckerEngine) ||
+		m_args.count(g_strModelCheckerInvariants) ||
 		m_args.count(g_strModelCheckerShowUnproved) ||
 		m_args.count(g_strModelCheckerSolvers) ||
 		m_args.count(g_strModelCheckerTargets) ||