replaced almost all instances of SMTchecker to SolCMC

Author: furmak331

libsolidity/ast/ExperimentalFeatures.h

@@ -30,7 +30,7 @@ namespace solidity::frontend
 enum class ExperimentalFeature
 {
 	ABIEncoderV2, // new ABI encoder that makes use of Yul
-	SMTChecker,
+	SolCMC,
 	Test,
 	TestOnlyAnalysis,
 	Solidity
@@ -39,14 +39,14 @@ enum class ExperimentalFeature
 static std::set<ExperimentalFeature> const ExperimentalFeatureWithoutWarning =
 {
 	ExperimentalFeature::ABIEncoderV2,
-	ExperimentalFeature::SMTChecker,
+	ExperimentalFeature::SolCMC,
 	ExperimentalFeature::TestOnlyAnalysis,
 };
 
 static std::map<std::string, ExperimentalFeature> const ExperimentalFeatureNames =
 {
 	{ "ABIEncoderV2", ExperimentalFeature::ABIEncoderV2 },
-	{ "SMTChecker", ExperimentalFeature::SMTChecker },
+	{ "SolCMC", ExperimentalFeature::SolCMC },
 	{ "__test", ExperimentalFeature::Test },
 	{ "__testOnlyAnalysis", ExperimentalFeature::TestOnlyAnalysis },
 	{ "solidity", ExperimentalFeature::Solidity }

libsolidity/formal/CHC.h

@@ -179,11 +179,11 @@ class CHC: public SMTEncoder
 
 	/// SMT Natspec and abstraction helpers.
 	//@{
-	/// @returns a CHCNatspecOption enum if _option is a valid SMTChecker Natspec value
+	/// @returns a CHCNatspecOption enum if _option is a valid SolCMC Natspec value
 	/// or nullopt otherwise.
 	static std::optional<CHCNatspecOption> natspecOptionFromString(std::string const& _option);
-	/// @returns which SMTChecker options are enabled by @a _function's Natspec via
-	/// `@custom:smtchecker <option>` or nullopt if none is used.
+	/// @returns which SolCMC options are enabled by @a _function's Natspec via
+	/// `@custom:SolCMC <option>` or nullopt if none is used.
 	std::set<CHCNatspecOption> smtNatspecTags(FunctionDefinition const& _function);
 	/// @returns true if _function is Natspec annotated to be abstracted by
 	/// nondeterministic values.

libsolidity/formal/ModelChecker.cpp

@@ -55,7 +55,7 @@ ModelChecker::ModelChecker(
 bool ModelChecker::isPragmaPresent(std::vector<std::shared_ptr<SourceUnit>> const& _sources)
 {
 	return ranges::any_of(_sources, [](auto _source) {
-		return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker);
+		return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SolCMC);
 	});
 }
 
@@ -94,14 +94,14 @@ void ModelChecker::checkRequestedSourcesAndContracts(std::vector<std::shared_ptr
 void ModelChecker::analyze(SourceUnit const& _source)
 {
 	// TODO This should be removed for 0.9.0.
-	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
+	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SolCMC))
 	{
 		PragmaDirective const* smtPragma = nullptr;
 		for (auto node: _source.nodes())
 			if (auto pragma = std::dynamic_pointer_cast<PragmaDirective>(node))
 				if (
 					pragma->literals().size() >= 2 &&
-					pragma->literals().at(1) == "SMTChecker"
+					pragma->literals().at(1) == "SolCMC"
 				)
 				{
 					smtPragma = pragma.get();
@@ -111,8 +111,8 @@ void ModelChecker::analyze(SourceUnit const& _source)
 		m_uniqueErrorReporter.warning(
 			5523_error,
 			smtPragma->location(),
-			"The SMTChecker pragma has been deprecated and will be removed in the future. "
-			"Please use the \"model checker engine\" compiler setting to activate the SMTChecker instead. "
+			"The SolCMC pragma has been deprecated and will be removed in the future. "
+			"Please use the \"model checker engine\" compiler setting to activate the SolCMC instead. "
 			"If the pragma is enabled, all engines will be used."
 		);
 	}
@@ -144,7 +144,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
 		m_errorReporter.warning(
 			5724_error,
 			{},
-			"SMTChecker: " +
+			"SolCMC: " +
 			std::to_string(m_unsupportedErrorReporter.errors().size()) +
 			" unsupported language feature(s)."
 			" Enable the model checker option \"show unsupported\" to see all of them."
@@ -188,7 +188,7 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er
 		_errorReporter.warning(
 			4902_error,
 			SourceLocation(),
-			"Solver cvc5 was selected for SMTChecker but it is not available."
+			"Solver cvc5 was selected for SolCMC but it is not available."
 		);
 	}
 
@@ -199,9 +199,9 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er
 			4458_error,
 			SourceLocation(),
 #if defined(__linux) || defined(__APPLE__)
-			"Solver Eldarica was selected for SMTChecker but it was not found in the system."
+			"Solver Eldarica was selected for SolCMC but it was not found in the system."
 #else
-			"Solver Eldarica was selected for SMTChecker but it is only supported on Linux and MacOS."
+			"Solver Eldarica was selected for SolCMC but it is only supported on Linux and MacOS."
 #endif
 		);
 	}
@@ -212,7 +212,7 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er
 		_errorReporter.warning(
 			8158_error,
 			SourceLocation(),
-			"Solver z3 was selected for SMTChecker but it is not available."
+			"Solver z3 was selected for SolCMC but it is not available."
 		);
 	}
 

libsolidity/formal/ModelCheckerSettings.h

@@ -47,7 +47,7 @@ struct ModelCheckerContracts
 	bool operator!=(ModelCheckerContracts const& _other) const noexcept { return !(*this == _other); }
 	bool operator==(ModelCheckerContracts const& _other) const noexcept { return contracts == _other.contracts; }
 
-	/// Represents which contracts should be analyzed by the SMTChecker
+	/// Represents which contracts should be analyzed by the SolCMC
 	/// as the most derived.
 	/// The key is the source file. If the map is empty, all sources must be analyzed.
 	/// For each source, contracts[source] represents the contracts in that source

libsolidity/formal/SMTEncoder.cpp

@@ -347,7 +347,7 @@ bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
 	m_unsupportedErrors.warning(
 		7737_error,
 		_inlineAsm.location(),
-		"Inline assembly may cause SMTChecker to produce spurious warnings (false positives)."
+		"Inline assembly may cause SolCMC to produce spurious warnings (false positives)."
 	);
 	return false;
 }

libsolidity/interface/CompilerStack.cpp

@@ -654,7 +654,7 @@ bool CompilerStack::analyzeLegacy(bool _noErrorsSoFar)
 
 	if (noErrors)
 	{
-		// Run SMTChecker
+		// Run SolCMC
 
 		auto allSources = util::applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; });
 		if (ModelChecker::isPragmaPresent(allSources))

solc/CommandLineParser.cpp

@@ -860,8 +860,8 @@ General Information)").c_str(),
 	;
 	desc.add(optimizerOptions);
 
-	po::options_description smtCheckerOptions("Model Checker Options");
-	smtCheckerOptions.add_options()
+	po::options_description SolCMCOptions("Model Checker Options");
+	SolCMCOptions.add_options()
 		(
 			g_strModelCheckerContracts.c_str(),
 			po::value<std::string>()->value_name("default,<source>:<contract>")->default_value("default"),
@@ -894,7 +894,7 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerPrintQuery.c_str(),
-			"Print the queries created by the SMTChecker in the SMTLIB2 format."
+			"Print the queries created by the SolCMC in the SMTLIB2 format."
 		)
 		(
 			g_strModelCheckerShowProvedSafe.c_str(),
@@ -934,7 +934,7 @@ General Information)").c_str(),
 			"Default is 1."
 		)
 	;
-	desc.add(smtCheckerOptions);
+	desc.add(SolCMCOptions);
 
 	desc.add_options()(g_strInputFile.c_str(), po::value<std::vector<std::string>>(), "input file");
 	return desc;

test/InteractiveTests.h

@@ -29,7 +29,7 @@
 #include <test/libsolidity/OptimizedIRCachingTest.h>
 #include <test/libsolidity/SyntaxTest.h>
 #include <test/libsolidity/SemanticTest.h>
-#include <test/libsolidity/SMTCheckerTest.h>
+#include <test/libsolidity/SolCMCTest.h>
 #include <test/libyul/ControlFlowGraphTest.h>
 #include <test/libyul/SSAControlFlowGraphTest.h>
 #include <test/libyul/EVMCodeTransformTest.h>
@@ -83,7 +83,7 @@ Testsuite const g_interactiveTestsuites[] = {
 	{"JSON AST",                    "libsolidity", "ASTJSON",                       false, false, &ASTJSONTest::create},
 	{"JSON ABI",                    "libsolidity", "ABIJson",                       false, false, &ABIJsonTest::create},
 	{"JSON Natspec",                "libsolidity", "natspecJSON",                   false, false, &NatspecJSONTest::create},
-	{"SMT Checker",                 "libsolidity", "smtCheckerTests",               true,  false, &SMTCheckerTest::create},
+	{"SMT Checker",                 "libsolidity", "SolCMCTests",               true,  false, &SolCMCTest::create},
 	{"Gas Estimates",               "libsolidity", "gasTests",                      false, false, &GasTest::create},
 	{"Memory Guard",                "libsolidity", "memoryGuardTests",              false, false, &MemoryGuardTest::create},
 	{"AST Properties",              "libsolidity", "astPropertyTests",              false, false, &ASTPropertyTest::create},

test/tools/fuzzer_common.cpp

@@ -68,7 +68,7 @@ void FuzzerUtil::testCompilerJsonInterface(std::string const& _input, bool _opti
 void FuzzerUtil::forceSMT(StringMap& _input)
 {
 	// Add SMT checker pragma if not already present in source
-	static auto constexpr smtPragma = "pragma experimental SMTChecker;";
+	static auto constexpr smtPragma = "pragma experimental SolCMC;";
 	for (auto &sourceUnit: _input)
 		if (sourceUnit.second.find(smtPragma) == std::string::npos)
 			sourceUnit.second += smtPragma;

test/tools/ossfuzz/SolidityGenerator.cpp

@@ -134,7 +134,7 @@ std::string PragmaGenerator::visit()
 {
 	static constexpr const char* preamble = R"(
 		pragma solidity >= 0.0.0;
-		pragma experimental SMTChecker;
+		pragma experimental SolCMC;
 	)";
 	// Choose equally at random from coder v1 and v2
 	std::string abiPragma = "pragma abicoder v" +