Refactor constructor exit

libsolidity/formal/CHC.cpp

@@ -142,12 +142,11 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	else
 		inlineConstructorHierarchy(_contract);
 
-	auto summary = predicate(*m_constructorSummaryPredicate, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables());
+	connectBlocks(m_currentBlock, summary(_contract), m_error.currentValue() == 0);
-	connectBlocks(m_currentBlock, summary);
 
 	clearIndices(m_currentContract, nullptr);
-	auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
+	vector<smtutil::Expression> symbArgs = currentFunctionVariables(*m_currentContract);
-	setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
+	setCurrentBlock(*m_constructorSummaryPredicate, &symbArgs);
 
 	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), m_error.currentValue());
 	connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
@@ -209,6 +208,8 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (!_function.isImplemented())
 		return;
 
+	solAssert(m_currentFunction && m_currentContract, "");
+
 	// This is the case for base constructor inlining.
 	if (m_currentFunction != &_function)
 	{
@@ -228,10 +229,10 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		{
 			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
 			auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
-			connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables()));
+			connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
 
 			clearIndices(m_currentContract, m_currentFunction);
-			auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
+			auto stateExprs = currentFunctionVariables(*m_currentContract);
 			setCurrentBlock(*constructorExit, &stateExprs);
 		}
 		else
@@ -693,6 +694,10 @@ vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract
 
 smtutil::SortPointer CHC::constructorSort()
 {
+	solAssert(m_currentContract, "");
+	if (auto const* constructor = m_currentContract->constructor())
+		return sort(*constructor);
+
 	return make_shared<smtutil::FunctionSort>(
 		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} + m_stateSorts,
 		smtutil::SortProvider::boolSort
@@ -835,7 +840,12 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 					m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
 
-					if (!base->isLibrary() && !base->isInterface() && !function->isConstructor())
+					if (
+						function->isPublic() &&
+						!base->isLibrary() &&
+						!base->isInterface() &&
+						!function->isConstructor()
+					)
 					{
 						auto state1 = stateVariablesAtIndex(1, *base);
 						auto state2 = stateVariablesAtIndex(2, *base);
@@ -880,8 +890,13 @@ smtutil::Expression CHC::error(unsigned _idx)
 	return m_errorPredicate->functionValueAtIndex(_idx)({});
 }
 
-smtutil::Expression CHC::summary(ContractDefinition const&)
+smtutil::Expression CHC::summary(ContractDefinition const& _contract)
 {
+	if (auto const* constructor = _contract.constructor())
+		return (*m_constructorSummaryPredicate)(
+			currentFunctionVariables(*constructor)
+		);
+
 	return (*m_constructorSummaryPredicate)(
 		vector<smtutil::Expression>{m_error.currentValue()} +
 		currentStateVariables()
@@ -977,15 +992,21 @@ vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const&
 }
 
 vector<smtutil::Expression> CHC::currentFunctionVariables()
+{
+	solAssert(m_currentFunction, "");
+	return currentFunctionVariables(*m_currentFunction);
+}
+
+vector<smtutil::Expression> CHC::currentFunctionVariables(FunctionDefinition const& _function)
 {
 	vector<smtutil::Expression> initInputExprs;
 	vector<smtutil::Expression> mutableInputExprs;
-	for (auto const& var: m_currentFunction->parameters())
+	for (auto const& var: _function.parameters())
 	{
 		initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
 		mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
 	}
-	auto returnExprs = applyMap(m_currentFunction->returnParameters(), [this](auto _var) { return currentValue(*_var); });
+	auto returnExprs = applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
 	return vector<smtutil::Expression>{m_error.currentValue()} +
 		initialStateVariables() +
 		initInputExprs +
@@ -994,6 +1015,14 @@ vector<smtutil::Expression> CHC::currentFunctionVariables()
 		returnExprs;
 }
 
+vector<smtutil::Expression> CHC::currentFunctionVariables(ContractDefinition const& _contract)
+{
+	if (auto const* constructor = _contract.constructor())
+		return currentFunctionVariables(*constructor);
+
+	return vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
+}
+
 vector<smtutil::Expression> CHC::currentBlockVariables()
 {
 	if (m_currentFunction)

libsolidity/formal/CHC.h

@@ -164,6 +164,9 @@ private:
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
 	std::vector<smtutil::Expression> currentFunctionVariables();
+	std::vector<smtutil::Expression> currentFunctionVariables(FunctionDefinition const& _function);
+	std::vector<smtutil::Expression> currentFunctionVariables(ContractDefinition const& _contract);
+
 	/// @returns the same as currentFunctionVariables plus
 	/// local variables.
 	std::vector<smtutil::Expression> currentBlockVariables();