From 397bd7da4fb13ecacdc74d22841a6915b97373c8 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Tue, 12 Oct 2021 11:32:02 +0200
Subject: [PATCH] Add CLI option for smtchecker trusted external calls

---
 libsolidity/interface/StandardCompiler.cpp | 12 +++++++++++-
 solc/CommandLineParser.cpp                 | 17 +++++++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 9ca8de3ea..5339b2a14 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", "invariants", "showUnproved", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -987,6 +987,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("extCalls"))
+	{
+		if (!modelCheckerSettings["extCalls"].isString())
+			return formatFatalError("JSONError", "settings.modelChecker.extCalls must be a string.");
+		std::optional<ModelCheckerExtCalls> extCalls = ModelCheckerExtCalls::fromString(modelCheckerSettings["extCalls"].asString());
+		if (!extCalls)
+			return formatFatalError("JSONError", "Invalid model checker extCalls requested.");
+		ret.modelCheckerSettings.externalCalls = *extCalls;
+	}
+
 	if (modelCheckerSettings.isMember("invariants"))
 	{
 		auto const& invariantsArray = modelCheckerSettings["invariants"];
diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp
index 1a3fbed0e..23f7c4380 100644
--- a/solc/CommandLineParser.cpp
+++ b/solc/CommandLineParser.cpp
@@ -67,6 +67,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_strModelCheckerExtCalls = "model-checker-ext-calls";
 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";
@@ -800,6 +801,12 @@ General Information)").c_str(),
 			po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
 			"Select model checker engine."
 		)
+		(
+			g_strModelCheckerExtCalls.c_str(),
+			po::value<string>()->value_name("untrusted,trusted")->default_value("untrusted"),
+			"Select whether to assume (trusted) that external calls always invoke"
+			" the code given by the type of the contract, if that code is available."
+		)
 		(
 			g_strModelCheckerInvariants.c_str(),
 			po::value<string>()->value_name("default,all,contract,reentrancy")->default_value("default"),
@@ -1219,6 +1226,15 @@ void CommandLineParser::processArgs()
 		m_options.modelChecker.settings.engine = *engine;
 	}
 
+	if (m_args.count(g_strModelCheckerExtCalls))
+	{
+		string mode = m_args[g_strModelCheckerExtCalls].as<string>();
+		optional<ModelCheckerExtCalls> extCallsMode = ModelCheckerExtCalls::fromString(mode);
+		if (!extCallsMode)
+			solThrow(CommandLineValidationError, "Invalid option for --" + g_strModelCheckerExtCalls + ": " + mode);
+		m_options.modelChecker.settings.externalCalls = *extCallsMode;
+	}
+
 	if (m_args.count(g_strModelCheckerInvariants))
 	{
 		string invsStr = m_args[g_strModelCheckerInvariants].as<string>();
@@ -1257,6 +1273,7 @@ void CommandLineParser::processArgs()
 		m_args.count(g_strModelCheckerContracts) ||
 		m_args.count(g_strModelCheckerDivModNoSlacks) ||
 		m_args.count(g_strModelCheckerEngine) ||
+		m_args.count(g_strModelCheckerExtCalls) ||
 		m_args.count(g_strModelCheckerInvariants) ||
 		m_args.count(g_strModelCheckerShowUnproved) ||
 		m_args.count(g_strModelCheckerSolvers) ||