refactor

ethereum · Jan 11, 2024 · 460a51f · 460a51f
1 parent df1b15e
commit 460a51f
Show file tree

Hide file tree

Showing 13 changed files with 144 additions and 53 deletions.
diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh
@@ -63,7 +63,7 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  z3_version="4.12.4"
+  z3_version="4.12.1"
   z3_dir="z3-${z3_version}-x64-osx-10.16"
   z3_package="${z3_dir}.zip"
   wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}"

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -75,7 +75,7 @@ configure_file("${PROJECT_SOURCE_DIR}/cmake/templates/license.h.in" include/lice
 
 include(EthOptions)
 configure_project(TESTS)
-set(LATEST_Z3_VERSION "4.12.4")
+set(LATEST_Z3_VERSION "4.12.1")
 set(MINIMUM_Z3_VERSION "4.8.16")
 find_package(Z3)
 if (${Z3_FOUND})

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
@@ -940,8 +940,6 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co
 	for (auto const* var: _contract.stateVariables())
 		m_context.variable(*var)->increaseIndex();
 
-	auto error = errorFlag().increaseIndex();
-
 	Predicate const& callPredicate = *createSymbolicBlock(
 		nondetInterfaceSort(_contract, state()),
 		"nondet_call_" + uniquePrefix(),
@@ -950,7 +948,7 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co
 		m_currentContract
 	);
 	auto postCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
-	std::vector<smtutil::Expression> stateExprs{error, address, state().abi(), state().bytesConcat(), state().crypto()};
+    std::vector<smtutil::Expression> stateExprs = commonStateExpressions(errorFlag().increaseIndex(), address);
 
 	auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState);
 	auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
@@ -1024,16 +1022,14 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 			m_context.variable(*var)->increaseIndex();
 	}
 
-	auto error = errorFlag().increaseIndex();
-
 	Predicate const& callPredicate = *createSymbolicBlock(
 		nondetInterfaceSort(*m_currentContract, state()),
 		"nondet_call_" + uniquePrefix(),
 		PredicateType::ExternalCallUntrusted,
 		&_funCall
 	);
 	auto postCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables();
-	std::vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().bytesConcat(), state().crypto()};
+	std::vector<smtutil::Expression> stateExprs = commonStateExpressions(errorFlag().increaseIndex(), state().thisAddress());
 
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
 	auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
@@ -1464,7 +1460,9 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 					auto errorPost = errorFlag().increaseIndex();
 					auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
 
-					std::vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().bytesConcat(), state().crypto(), state().tx(), state().state(1)};
+					std::vector<smtutil::Expression> args =	commonStateExpressions(errorPost, state().thisAddress());
+					args.push_back(state().tx());
+					args.push_back(state().state(1));
 					args += state1 +
 						applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
 						std::vector<smtutil::Expression>{state().state(2)} +
@@ -1829,7 +1827,9 @@ smtutil::Expression CHC::predicate(
 
 	errorFlag().increaseIndex();
 
-	std::vector<smtutil::Expression> args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().bytesConcat(), state().crypto(), state().tx(), state().state()};
+	std::vector<smtutil::Expression> args =	commonStateExpressions(errorFlag().currentValue(), _contractAddressValue);
+	args.push_back(state().tx());
+	args.push_back(state().state());
 
 	auto const* contract = _funDef->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
@@ -2176,7 +2176,8 @@ void CHC::checkAndReportTarget(
 			predicates.insert(pred);
 		for (auto const* pred: m_nondetInterfaces | ranges::views::values)
 			predicates.insert(pred);
-		std::map<Predicate const*, std::set<std::string>> invariants = collectInvariants(invariant, predicates, m_settings.invariants);
+		std::map<Predicate const*, std::set<std::string>> invariants =
+            collectInvariants(invariant, predicates, m_settings.invariants, state().hasBytesConcatFunction());
 		for (auto pred: invariants | ranges::views::keys)
 			m_invariants[pred] += std::move(invariants.at(pred));
 	}
@@ -2257,7 +2258,7 @@ std::optional<std::string> CHC::generateCounterexample(CHCSolverInterface::CexGr
 		{
 			auto stateVars = summaryPredicate->stateVariables();
 			solAssert(stateVars.has_value(), "");
-			auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
+			auto stateValues = summaryPredicate->summaryStateValues(summaryArgs, state().hasBytesConcatFunction());
 			solAssert(stateValues.size() == stateVars->size(), "");
 
 			if (first)
@@ -2268,11 +2269,11 @@ std::optional<std::string> CHC::generateCounterexample(CHCSolverInterface::CexGr
 
 				if (auto calledFun = summaryPredicate->programFunction())
 				{
-					auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
+					auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs, state().hasBytesConcatFunction());
 					auto const& inParams = calledFun->parameters();
 					if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
 						localState += inStr + "\n";
-					auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
+					auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs, state().hasBytesConcatFunction());
 					auto const& outParams = calledFun->returnParameters();
 					if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
 						localState += outStr + "\n";
@@ -2311,8 +2312,7 @@ std::optional<std::string> CHC::generateCounterexample(CHCSolverInterface::CexGr
 					path.emplace_back("State: " + modelMsg);
 			}
 		}
-
-		std::string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
+		std::string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider, state().hasBytesConcatFunction());
 
 		std::list<std::string> calls;
 		auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void {
@@ -2486,3 +2486,11 @@ void CHC::decreaseBalanceFromOptionsValue(Expression const& _value)
 {
 	state().addBalance(state().thisAddress(), 0 - expr(_value));
 }
+
+
+std::vector<smtutil::Expression> CHC::commonStateExpressions(smtutil::Expression error, smtutil::Expression address)
+{
+	if (state().hasBytesConcatFunction())
+		return {error, address, state().abi(), state().bytesConcat(), state().crypto()};
+	return {error, address, state().abi(), state().crypto()};
+}
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
@@ -362,6 +362,8 @@ class CHC: public SMTEncoder
 
 	/// Adds constraints that decrease the balance of the caller by _value.
 	void decreaseBalanceFromOptionsValue(Expression const& _value);
+
+    std::vector<smtutil::Expression> commonStateExpressions(smtutil::Expression error, smtutil::Expression address);
 	//@}
 
 	/// Predicates.

diff --git a/libsolidity/formal/Invariants.cpp b/libsolidity/formal/Invariants.cpp
@@ -36,7 +36,8 @@ namespace solidity::frontend::smt
 std::map<Predicate const*, std::set<std::string>> collectInvariants(
 	smtutil::Expression const& _proof,
 	std::set<Predicate const*> const& _predicates,
-	ModelCheckerInvariants const& _invariantsSetting
+	ModelCheckerInvariants const& _invariantsSetting,
+    bool _hasBytesConcatFunction
 )
 {
 	std::set<std::string> targets;
@@ -74,7 +75,7 @@ std::map<Predicate const*, std::set<std::string>> collectInvariants(
 		auto const& [predExpr, invExpr] = equalities.at(predName);
 
 		static std::set<std::string> const ignore{"true", "false"};
-		auto r = substitute(invExpr, pred->expressionSubstitution(predExpr));
+		auto r = substitute(invExpr, pred->expressionSubstitution(predExpr, _hasBytesConcatFunction));
 		// No point in reporting true/false as invariants.
 		if (!ignore.count(r.name))
 			invariants[pred].insert(toSolidityStr(r));

diff --git a/libsolidity/formal/Invariants.h b/libsolidity/formal/Invariants.h
@@ -31,7 +31,8 @@ namespace solidity::frontend::smt
 std::map<Predicate const*, std::set<std::string>> collectInvariants(
 	smtutil::Expression const& _proof,
 	std::set<Predicate const*> const& _predicates,
-	ModelCheckerInvariants const& _invariantsSettings
+	ModelCheckerInvariants const& _invariantsSettings,
+    bool _hasBytesConcatFunction
 );
 
 }
diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp
@@ -213,6 +213,7 @@ bool Predicate::isNondetInterface() const
 std::string Predicate::formatSummaryCall(
 	std::vector<smtutil::Expression> const& _args,
 	langutil::CharStreamProvider const& _charStreamProvider,
+    bool _includeBytesConcatFunctions,
 	bool _appendTxVars
 ) const
 {
@@ -285,7 +286,7 @@ std::string Predicate::formatSummaryCall(
 		}
 
 		// Here we are interested in txData from the summary predicate.
-		auto txValues = readTxVars(_args.at(5));
+		auto txValues = readTxVars(_args.at(txValuesIndex(_includeBytesConcatFunctions)));
 		std::vector<std::string> values;
 		for (auto const& _var: txVars)
 			if (auto v = txValues.at(_var))
@@ -303,7 +304,7 @@ std::string Predicate::formatSummaryCall(
 	auto const* fun = programFunction();
 	solAssert(fun, "");
 
-	auto first = _args.begin() + 7 + static_cast<int>(stateVars->size());
+	auto first = _args.begin() + (long)firstArgIndex(_includeBytesConcatFunctions) + static_cast<int>(stateVars->size());
 	auto last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
@@ -335,7 +336,7 @@ std::string Predicate::formatSummaryCall(
 	return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel;
 }
 
-std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vector<smtutil::Expression> const& _args) const
+std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vector<smtutil::Expression> const& _args, bool _includeBytesConcatFunctions) const
 {
 	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
@@ -347,12 +348,12 @@ std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vecto
 	std::vector<smtutil::Expression>::const_iterator stateLast;
 	if (auto const* function = programFunction())
 	{
-		stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
+		stateFirst = _args.begin() + (long)firstArgIndex(_includeBytesConcatFunctions) + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else if (programContract())
 	{
-		stateFirst = _args.begin() + 8 + static_cast<int>(stateVars->size());
+		stateFirst = _args.begin() + (long)firstStateVarIndex(_includeBytesConcatFunctions) + static_cast<int>(stateVars->size());
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else if (programVariable())
@@ -369,7 +370,7 @@ std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vecto
 	return formatExpressions(stateArgs, stateTypes);
 }
 
-std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::vector<smtutil::Expression> const& _args) const
+std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::vector<smtutil::Expression> const& _args, bool _includeBytesConcatFunctions) const
 {
 	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in postInputVars.
@@ -381,7 +382,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::v
 
 	auto const& inParams = function->parameters();
 
-	auto first = _args.begin() + 7 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
+	auto first = _args.begin() + (long)firstArgIndex(_includeBytesConcatFunctions) + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
 	auto last = first + static_cast<int>(inParams.size());
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -393,7 +394,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::v
 	return formatExpressions(inValues, inTypes);
 }
 
-std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const
+std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::vector<smtutil::Expression> const& _args, bool _includeBytesConcatFunctions) const
 {
 	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in outputVars.
@@ -405,7 +406,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::
 
 	auto const& inParams = function->parameters();
 
-	auto first = _args.begin() + 7 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
+	auto first = _args.begin() + (long)firstArgIndex(_includeBytesConcatFunctions) + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 
@@ -441,7 +442,7 @@ std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclarati
 	return {formatExpressions(outValuesInScope, outTypes), localVarsInScope};
 }
 
-std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const
+std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Expression const& _predExpr, bool _includeBytesConcatFunctions) const
 {
 	std::map<std::string, std::string> subst;
 	std::string predName = functor().name;
@@ -457,11 +458,12 @@ std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Ex
 	// invariant over its state, for example `x <= 0`.
 	if (isInterface())
 	{
+        size_t argsIndexShift = firstArgIndex(_includeBytesConcatFunctions);
 		solAssert(starts_with(predName, "interface"), "");
 		subst[_predExpr.arguments.at(0).name] = "address(this)";
-		solAssert(nArgs == stateVars.size() + 5, "");
+		solAssert(nArgs == stateVars.size() + argsIndexShift, "");
 		for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i)
-			subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 5)->name();
+			subst[_predExpr.arguments.at(i).name] = stateVars.at(i - argsIndexShift)->name();
 	}
 	// The signature of a nondet interface predicate is
 	// nondet_interface(error, this, abiFunctions, bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
@@ -475,7 +477,7 @@ std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Ex
 		solAssert(starts_with(predName, "nondet_interface"), "");
 		subst[_predExpr.arguments.at(0).name] = "<errorCode>";
 		subst[_predExpr.arguments.at(1).name] = "address(this)";
-		solAssert(nArgs == stateVars.size() * 2 + 7, "");
+		solAssert(nArgs == stateVars.size() * 2 + firstArgIndex(_includeBytesConcatFunctions), "");
 		for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s)
 			subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'";
 		for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s)

diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h
@@ -159,27 +159,28 @@ class Predicate
 	std::string formatSummaryCall(
 		std::vector<smtutil::Expression> const& _args,
 		langutil::CharStreamProvider const& _charStreamProvider,
+        bool _includeBytesConcatFunctions,
 		bool _appendTxVars = false
 	) const;
 
 	/// @returns the values of the state variables from _args at the point
 	/// where this summary was reached.
-	std::vector<std::optional<std::string>> summaryStateValues(std::vector<smtutil::Expression> const& _args) const;
+	std::vector<std::optional<std::string>> summaryStateValues(std::vector<smtutil::Expression> const& _args, bool _includeBytesConcatFunctions) const;
 
 	/// @returns the values of the function input variables from _args at the point
 	/// where this summary was reached.
-	std::vector<std::optional<std::string>> summaryPostInputValues(std::vector<smtutil::Expression> const& _args) const;
+	std::vector<std::optional<std::string>> summaryPostInputValues(std::vector<smtutil::Expression> const& _args, bool _includeBytesConcatFunctions) const;
 
 	/// @returns the values of the function output variables from _args at the point
 	/// where this summary was reached.
-	std::vector<std::optional<std::string>> summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const;
+	std::vector<std::optional<std::string>> summaryPostOutputValues(std::vector<smtutil::Expression> const& _args, bool _includeBytesConcatFunctions) const;
 
 	/// @returns the values of the local variables used by this predicate.
 	std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclaration const*>> localVariableValues(std::vector<smtutil::Expression> const& _args) const;
 
 	/// @returns a substitution map from the arguments of _predExpr
 	/// to a Solidity-like expression.
-	std::map<std::string, std::string> expressionSubstitution(smtutil::Expression const& _predExpr) const;
+	std::map<std::string, std::string> expressionSubstitution(smtutil::Expression const& _predExpr, bool _includeBytesConcatFunctions) const;
 
 private:
 	/// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants.
@@ -196,6 +197,13 @@ class Predicate
 
 	std::map<std::string, std::optional<std::string>> readTxVars(smtutil::Expression const& _tx) const;
 
+    /// @returns index at which transaction values start in args list
+	size_t txValuesIndex(bool _includeBytesConcatFunctions) const { return _includeBytesConcatFunctions ? 5 : 4; }
+	/// @returns index at which transaction values start in args list
+    size_t firstArgIndex(bool _includeBytesConcatFunctions) const { return _includeBytesConcatFunctions ? 7 : 6; }
+	/// @returns index at which transaction values start in args list
+    size_t firstStateVarIndex(bool _includeBytesConcatFunctions) const { return _includeBytesConcatFunctions ? 8 : 7; }
+
 	/// The actual SMT expression.
 	smt::SymbolicFunctionVariable m_predicate;