Merge pull request #16019 from ethereum/smt-more-refactoring

blishko · web-flow · commit 7526fbcd0622 · 2025-04-23T12:53:04.000+02:00
SMTChecker: Clean up includes and remove unused functionality
diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp
@@ -25,7 +25,8 @@
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
 
-#include <range/v3/algorithm/find_if.hpp>
+#include <range/v3/view/transform.hpp>
+#include <range/v3/view/zip.hpp>
 
 #include <array>
 #include <fstream>
diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h
@@ -20,10 +20,7 @@
 
 
 #include <libsmtutil/BMCSolverInterface.h>
-#include <libsolidity/interface/ReadFile.h>
-#include <libsolutil/FixedHash.h>
 
-#include <map>
 #include <vector>
 
 namespace solidity::smtutil
diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
@@ -26,7 +26,8 @@
 #include <libsolutil/CommonData.h>
 
 #include <range/v3/algorithm/all_of.hpp>
-#include <range/v3/view.hpp>
+#include <range/v3/range/conversion.hpp>
+#include <range/v3/view/split.hpp>
 
 #include <cstdio>
 #include <map>
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt
@@ -137,8 +137,6 @@ set(sources
 	formal/SymbolicTypes.h
 	formal/SymbolicVariables.cpp
 	formal/SymbolicVariables.h
-	formal/VariableUsage.cpp
-	formal/VariableUsage.h
 	formal/Z3CHCSmtLib2Interface.cpp
 	formal/Z3CHCSmtLib2Interface.h
 	formal/Z3SMTLib2Interface.cpp
diff --git a/libsolidity/formal/ArraySlicePredicate.cpp b/libsolidity/formal/ArraySlicePredicate.cpp
@@ -18,6 +18,8 @@
 
 #include <libsolidity/formal/ArraySlicePredicate.h>
 
+#include <libsolidity/formal/SymbolicVariables.h>
+
 #include <liblangutil/Exceptions.h>
 
 using namespace solidity;
diff --git a/libsolidity/formal/ArraySlicePredicate.h b/libsolidity/formal/ArraySlicePredicate.h
@@ -16,9 +16,9 @@
 */
 // SPDX-License-Identifier: GPL-3.0
 
-#include <libsolidity/formal/EncodingContext.h>
+#pragma once
+
 #include <libsolidity/formal/Predicate.h>
-#include <libsolidity/formal/SymbolicVariables.h>
 
 #include <libsmtutil/Sorts.h>
 
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
@@ -80,7 +80,6 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
 	m_context.setSolver(m_interface.get());
 	m_context.reset();
 	m_context.setAssertionAccumulation(true);
-	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 	auto const& sources = sourceDependencies(_source);
 	createFreeConstants(sources);
 	createStateVariables(sources);
diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp
@@ -18,12 +18,19 @@
 
 #include <libsolidity/formal/EncodingContext.h>
 
+#include <libsolidity/ast/AST.h>
+
 #include <libsolidity/formal/SymbolicTypes.h>
 
 using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::frontend::smt;
 
+bool EncodingContext::IdCompare::operator()(ASTNode const* lhs, ASTNode const* rhs) const
+{
+	return lhs->id() < rhs->id();
+}
+
 EncodingContext::EncodingContext():
 	m_state(*this)
 {
diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h
@@ -68,10 +68,7 @@ class EncodingContext
 
 	struct IdCompare
 	{
-		bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
-		{
-			return lhs->id() < rhs->id();
-		}
+		bool operator()(ASTNode const* lhs, ASTNode const* rhs) const;
 	};
 
 	/// Variables.
diff --git a/libsolidity/formal/ExpressionFormatter.cpp b/libsolidity/formal/ExpressionFormatter.cpp
@@ -20,6 +20,8 @@
 
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsolidity/ast/AST.h>
+
 #include <libsolutil/Algorithms.h>
 #include <libsolutil/CommonData.h>
 
diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp
@@ -28,7 +28,7 @@
 
 #include <boost/algorithm/string/join.hpp>
 
-#include <range/v3/view.hpp>
+#include <range/v3/view/enumerate.hpp>
 #include <utility>
 
 using namespace solidity;
diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h
@@ -19,7 +19,8 @@
 #pragma once
 
 
-#include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/ASTForward.h>
+#include <libsolidity/ast/Types.h>
 
 #include <libsmtutil/SolverInterface.h>
 #include <libsmtutil/Sorts.h>
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
@@ -756,7 +756,6 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
 	m_context.pushSolver();
 	createStateVariables(_contract);
 	clearIndices(m_currentContract, nullptr);
-	m_variableUsage.setCurrentContract(_contract);
 	m_checked = true;
 }
 
@@ -2813,14 +2812,6 @@ Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
 	return expr;
 }
 
-std::set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
-{
-	std::vector<CallableDeclaration const*> callStack;
-	for (auto const& call: m_callStack)
-		callStack.push_back(call.first);
-	return m_variableUsage.touchedVariables(_node, callStack);
-}
-
 Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const
 {
 	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
@@ -27,7 +27,6 @@
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/ModelCheckerSettings.h>
 #include <libsolidity/formal/SymbolicVariables.h>
-#include <libsolidity/formal/VariableUsage.h>
 
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/ASTVisitor.h>
@@ -454,7 +453,6 @@ class SMTEncoder: public ASTConstVisitor
 		smtutil::Expression constraints;
 	};
 
-	smt::VariableUsage m_variableUsage;
 	bool m_arrayAssignmentHappened = false;
 
 	/// Stores the instances of an Uninterpreted Function applied to arguments.
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
@@ -20,6 +20,7 @@
 
 #include <libsolidity/formal/EncodingContext.h>
 
+#include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/TypeProvider.h>
 #include <libsolidity/ast/Types.h>
 #include <libsolutil/CommonData.h>
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
@@ -19,7 +19,6 @@
 #pragma once
 
 #include <libsolidity/formal/SymbolicVariables.h>
-#include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/Types.h>
 
 namespace solidity::frontend::smt
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
@@ -18,6 +18,8 @@
 
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsolidity/ast/AST.h>
+
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h
