Move predicate functions from CHC to PredicateInstance

libsolidity/CMakeLists.txt

@@ -104,6 +104,8 @@ set(sources
 	formal/ModelChecker.h
 	formal/Predicate.cpp
 	formal/Predicate.h
+	formal/PredicateInstance.cpp
+	formal/PredicateInstance.h
 	formal/PredicateSort.cpp
 	formal/PredicateSort.h
 	formal/SMTEncoder.cpp

libsolidity/formal/CHC.cpp

@@ -22,6 +22,7 @@
 #include <libsmtutil/Z3CHCInterface.h>
 #endif
 
+#include <libsolidity/formal/PredicateInstance.h>
 #include <libsolidity/formal/PredicateSort.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
@@ -101,10 +102,9 @@ bool CHC::visit(ContractDefinition const& _contract)
 	m_constructorSummaryPredicate = createSymbolicBlock(
 		constructorSort(*m_currentContract),
 		"summary_constructor_" + contractSuffix(_contract),
+		PredicateType::ConstructorSummary,
 		&_contract
 	);
-	auto stateExprs = currentStateVariables();
-	setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
 
 	SMTEncoder::visit(_contract);
 	return false;
@@ -130,9 +130,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 
 	connectBlocks(m_currentBlock, summary(_contract));
 
-	clearIndices(m_currentContract, nullptr);
+	setCurrentBlock(*m_constructorSummaryPredicate);
-	vector<smtutil::Expression> symbArgs = currentFunctionVariables(*m_currentContract);
-	setCurrentBlock(*m_constructorSummaryPredicate, &symbArgs);
 
 	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), errorFlag().currentValue());
 	connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0);
@@ -163,10 +161,10 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 	initFunction(_function);
 
-	auto functionEntryBlock = createBlock(m_currentFunction);
+	auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionEntry);
-	auto bodyBlock = createBlock(&m_currentFunction->body());
+	auto bodyBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock);
 
-	auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
+	auto functionPred = predicate(*functionEntryBlock);
 	auto bodyPred = predicate(*bodyBlock);
 
 	if (_function.isConstructor())
@@ -218,13 +216,12 @@ void CHC::endVisit(FunctionDefinition const& _function)
 			auto constructorExit = createSymbolicBlock(
 				constructorSort(*m_currentContract),
 				"constructor_exit_" + suffix,
+				PredicateType::ConstructorSummary,
 				m_currentContract
 			);
-			connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
+			connectBlocks(m_currentBlock, predicate(*constructorExit));
 
-			clearIndices(m_currentContract, m_currentFunction);
+			setCurrentBlock(*constructorExit);
-			auto stateExprs = currentFunctionVariables(*m_currentContract);
-			setCurrentBlock(*constructorExit, &stateExprs);
 		}
 		else
 		{
@@ -234,13 +231,13 @@ void CHC::endVisit(FunctionDefinition const& _function)
 
 			auto iface = interface();
 
-			auto stateExprs = initialStateVariables();
+			setCurrentBlock(*m_interfaces.at(m_currentContract));
-			setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
 
+			auto ifacePre = (*m_interfaces.at(m_currentContract))(initialStateVariables());
 			if (_function.isPublic())
 			{
-				addAssertVerificationTarget(&_function, m_currentBlock, sum, assertionError);
+				addAssertVerificationTarget(&_function, ifacePre, sum, assertionError);
-				connectBlocks(m_currentBlock, iface, sum && (assertionError == 0));
+				connectBlocks(ifacePre, iface, sum && (assertionError == 0));
 			}
 		}
 		m_currentFunction = nullptr;
@@ -259,10 +256,10 @@ bool CHC::visit(IfStatement const& _if)
 	solAssert(m_currentFunction, "");
 	auto const& functionBody = m_currentFunction->body();
 
-	auto ifHeaderBlock = createBlock(&_if, "if_header_");
+	auto ifHeaderBlock = createBlock(&_if, PredicateType::FunctionBlock, "if_header_");
-	auto trueBlock = createBlock(&_if.trueStatement(), "if_true_");
+	auto trueBlock = createBlock(&_if.trueStatement(), PredicateType::FunctionBlock, "if_true_");
-	auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), "if_false_") : nullptr;
+	auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), PredicateType::FunctionBlock, "if_false_") : nullptr;
-	auto afterIfBlock = createBlock(&functionBody);
+	auto afterIfBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
 
 	connectBlocks(m_currentBlock, predicate(*ifHeaderBlock));
 
@@ -306,9 +303,9 @@ bool CHC::visit(WhileStatement const& _while)
 	auto const& functionBody = m_currentFunction->body();
 
 	auto namePrefix = string(_while.isDoWhile() ? "do_" : "") + "while";
-	auto loopHeaderBlock = createBlock(&_while, namePrefix + "_header_");
+	auto loopHeaderBlock = createBlock(&_while, PredicateType::FunctionBlock, namePrefix + "_header_");
-	auto loopBodyBlock = createBlock(&_while.body(), namePrefix + "_body_");
+	auto loopBodyBlock = createBlock(&_while.body(), PredicateType::FunctionBlock, namePrefix + "_body_");
-	auto afterLoopBlock = createBlock(&functionBody);
+	auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
 
 	auto outerBreakDest = m_breakDest;
 	auto outerContinueDest = m_continueDest;
@@ -355,11 +352,11 @@ bool CHC::visit(ForStatement const& _for)
 	solAssert(m_currentFunction, "");
 	auto const& functionBody = m_currentFunction->body();
 
-	auto loopHeaderBlock = createBlock(&_for, "for_header_");
+	auto loopHeaderBlock = createBlock(&_for, PredicateType::FunctionBlock, "for_header_");
-	auto loopBodyBlock = createBlock(&_for.body(), "for_body_");
+	auto loopBodyBlock = createBlock(&_for.body(), PredicateType::FunctionBlock, "for_body_");
-	auto afterLoopBlock = createBlock(&functionBody);
+	auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
 	auto postLoop = _for.loopExpression();
-	auto postLoopBlock = postLoop ? createBlock(postLoop, "for_post_") : nullptr;
+	auto postLoopBlock = postLoop ? createBlock(postLoop, PredicateType::FunctionBlock, "for_post_") : nullptr;
 
 	auto outerBreakDest = m_breakDest;
 	auto outerContinueDest = m_continueDest;
@@ -461,7 +458,7 @@ void CHC::endVisit(Break const& _break)
 {
 	solAssert(m_breakDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_breakDest));
-	auto breakGhost = createBlock(&_break, "break_ghost_");
+	auto breakGhost = createBlock(&_break, PredicateType::FunctionBlock, "break_ghost_");
 	m_currentBlock = predicate(*breakGhost);
 }
 
@@ -469,7 +466,7 @@ void CHC::endVisit(Continue const& _continue)
 {
 	solAssert(m_continueDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_continueDest));
-	auto continueGhost = createBlock(&_continue, "continue_ghost_");
+	auto continueGhost = createBlock(&_continue, PredicateType::FunctionBlock, "continue_ghost_");
 	m_currentBlock = predicate(*continueGhost);
 }
 
@@ -726,19 +723,13 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 	}
 }
 
-void CHC::setCurrentBlock(
+void CHC::setCurrentBlock(Predicate const& _block)
-	Predicate const& _block,
-	vector<smtutil::Expression> const* _arguments
-)
 {
 	if (m_context.solverStackHeigh() > 0)
 		m_context.popSolver();
 	solAssert(m_currentContract, "");
 	clearIndices(m_currentContract, m_currentFunction);
 	m_context.pushSolver();
-	if (_arguments)
-		m_currentBlock = predicate(_block, *_arguments);
-	else
 	m_currentBlock = predicate(_block);
 }
 
@@ -767,9 +758,9 @@ SortPointer CHC::sort(ASTNode const* _node)
 	return functionBodySort(*m_currentFunction, m_currentContract);
 }
 
-Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node)
+Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node)
 {
-	auto const* block = Predicate::create(_sort, _name, m_context, _node);
+	auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node);
 	m_interface->registerRelation(block->functor());
 	return block;
 }
@@ -780,8 +771,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
 		{
 			string suffix = contract->name() + "_" + to_string(contract->id());
-			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix);
+			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix, PredicateType::Interface, contract);
-			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix);
+			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
 
 			for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
 				if (!m_context.knownVariable(*var))
@@ -834,16 +825,13 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 smtutil::Expression CHC::interface()
 {
-	auto paramExprs = applyMap(
+	solAssert(m_currentContract, "");
-		m_stateVariables,
+	return interface(*m_currentContract);
-		[this](auto _var) { return m_context.variable(*_var)->currentValue(); }
-	);
-	return (*m_interfaces.at(m_currentContract))(paramExprs);
 }
 
 smtutil::Expression CHC::interface(ContractDefinition const& _contract)
 {
-	return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract));
+	return ::interface(*m_interfaces.at(&_contract), _contract, m_context);
 }
 
 smtutil::Expression CHC::error()
@@ -858,27 +846,12 @@ smtutil::Expression CHC::error(unsigned _idx)
 
 smtutil::Expression CHC::summary(ContractDefinition const& _contract)
 {
-	if (auto const* constructor = _contract.constructor())
+	return constructor(*m_constructorSummaryPredicate, _contract, m_context);
-		return (*m_constructorSummaryPredicate)(
-			currentFunctionVariables(*constructor)
-		);
-
-	return (*m_constructorSummaryPredicate)(
-		vector<smtutil::Expression>{m_error.currentValue()} +
-		currentStateVariables()
-	);
 }
 
 smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	vector<smtutil::Expression> args{m_error.currentValue()};
+	return smt::function(*m_summaries.at(&_contract).at(&_function), _function, &_contract, m_context);
-	auto contract = _function.annotation().contract;
-	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(_contract);
-	args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); });
-	args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(_contract);
-	args += applyMap(_function.parameters(), [this](auto _var) { return currentValue(*_var); });
-	args += applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
-	return (*m_summaries.at(&_contract).at(&_function))(args);
 }
 
 smtutil::Expression CHC::summary(FunctionDefinition const& _function)
@@ -887,11 +860,12 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function)
 	return summary(_function, *m_currentContract);
 }
 
-Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix)
+Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix)
 {
 	auto block = createSymbolicBlock(
 		sort(_node),
 		"block_" + uniquePrefix() + "_" + _prefix + predicateName(_node),
+		_predType,
 		_node
 	);
 
@@ -904,6 +878,7 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co
 	auto block = createSymbolicBlock(
 		functionSort(_function, &_contract),
 		"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
+		PredicateType::FunctionSummary,
 		&_function
 	);
 
@@ -912,7 +887,7 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co
 
 void CHC::createErrorBlock()
 {
-	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()));
+	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()), PredicateType::Error);
 	m_interface->registerRelation(m_errorPredicate->functor());
 }
 
@@ -930,11 +905,6 @@ vector<smtutil::Expression> CHC::initialStateVariables()
 	return stateVariablesAtIndex(0);
 }
 
-vector<smtutil::Expression> CHC::initialStateVariables(ContractDefinition const& _contract)
-{
-	return stateVariablesAtIndex(0, _contract);
-}
-
 vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
 {
 	solAssert(m_currentContract, "");
@@ -960,46 +930,6 @@ vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const&
 	return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
 }
 
-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: _function.parameters())
-	{
-		initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
-		mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
-	}
-	auto returnExprs = applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
-	return vector<smtutil::Expression>{m_error.currentValue()} +
-		initialStateVariables() +
-		initInputExprs +
-		currentStateVariables() +
-		mutableInputExprs +
-		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)
-		return currentFunctionVariables() + applyMap(m_currentFunction->localVariables(), [this](auto _var) { return currentValue(*_var); });
-
-	return currentFunctionVariables();
-}
-
 string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract)
 {
 	string prefix;
@@ -1019,15 +949,31 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
 
 smtutil::Expression CHC::predicate(Predicate const& _block)
 {
-	return _block(currentBlockVariables());
+	switch (_block.type())
-}
-
-smtutil::Expression CHC::predicate(
-	Predicate const& _block,
-	vector<smtutil::Expression> const& _arguments
-)
 	{
-	return _block(_arguments);
+	case PredicateType::Interface:
+		solAssert(m_currentContract, "");
+		return ::interface(_block, *m_currentContract, m_context);
+	case PredicateType::ImplicitConstructor:
+		solAssert(m_currentContract, "");
+		return implicitConstructor(_block, *m_currentContract, m_context);
+	case PredicateType::ConstructorSummary:
+		solAssert(m_currentContract, "");
+		return constructor(_block, *m_currentContract, m_context);
+	case PredicateType::FunctionEntry:
+	case PredicateType::FunctionSummary:
+		solAssert(m_currentFunction, "");
+		return smt::function(_block, *m_currentFunction, m_currentContract, m_context);
+	case PredicateType::FunctionBlock:
+		solAssert(m_currentFunction, "");
+		return functionBlock(_block, *m_currentFunction, m_currentContract, m_context);
+	case PredicateType::Error:
+		return _block({});
+	case PredicateType::NondetInterface:
+		// Nondeterministic interface predicates are handled differently.
+		solAssert(false, "");
+	}
+	solAssert(false, "");
 }
 
 smtutil::Expression CHC::predicate(FunctionCall const& _funCall)

libsolidity/formal/CHC.h

@@ -111,7 +111,7 @@ private:
 	void resetContractAnalysis();
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
-	void setCurrentBlock(Predicate const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
+	void setCurrentBlock(Predicate const& _block);
 	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
 	//@}
 
@@ -124,7 +124,7 @@ private:
 	/// Predicate helpers.
 	//@{
 	/// @returns a new block of given _sort and _name.
-	Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, ASTNode const* _node = nullptr);
+	Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr);
 
 	/// Creates summary predicates for all functions of all contracts
 	/// in a given _source.
@@ -138,7 +138,7 @@ private:
 	smtutil::Expression error(unsigned _idx);
 
 	/// Creates a block for the given _node.
-	Predicate const* createBlock(ASTNode const* _node, std::string const& _prefix = "");
+	Predicate const* createBlock(ASTNode const* _node, PredicateType _predType, std::string const& _prefix = "");
 	/// Creates a call block for the given function _function from contract _contract.
 	/// The contract is needed here because of inheritance.
 	Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
@@ -152,29 +152,16 @@ private:
 	/// @returns the symbolic values of the state variables at the beginning
 	/// of the current transaction.
 	std::vector<smtutil::Expression> initialStateVariables();
-	std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract);
 	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index);
 	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract);
 	/// @returns the current symbolic values of the current state variables.
 	std::vector<smtutil::Expression> currentStateVariables();
 	std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract);
 
-	/// @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();
-
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
-	/// @returns a predicate application over the current scoped variables.
+	/// @returns a predicate application after checking the predicate's type.
 	smtutil::Expression predicate(Predicate const& _block);
-	/// @returns a predicate application over @param _arguments.
-	smtutil::Expression predicate(Predicate const& _block, std::vector<smtutil::Expression> const& _arguments);
 	/// @returns the summary predicate for the called function.
 	smtutil::Expression predicate(FunctionCall const& _funCall);
 	/// @returns a predicate that defines a constructor summary.

libsolidity/formal/Predicate.cpp

@@ -36,6 +36,7 @@ map<string, Predicate> Predicate::m_predicates;
 Predicate const* Predicate::create(
 	SortPointer _sort,
 	string _name,
+	PredicateType _type,
 	EncodingContext& _context,
 	ASTNode const* _node
 )
@@ -46,15 +47,17 @@ Predicate const* Predicate::create(
 	return &m_predicates.emplace(
 		std::piecewise_construct,
 		std::forward_as_tuple(functorName),
-		std::forward_as_tuple(move(predicate), _node)
+		std::forward_as_tuple(move(predicate), _type, _node)
 	).first->second;
 }
 
 Predicate::Predicate(
 	smt::SymbolicFunctionVariable&& _predicate,
+	PredicateType _type,
 	ASTNode const* _node
 ):
 	m_predicate(move(_predicate)),
+	m_type(_type),
 	m_node(_node)
 {
 }

libsolidity/formal/Predicate.h

@@ -30,6 +30,18 @@
 namespace solidity::frontend
 {
 
+enum class PredicateType
+{
+	Interface,
+	NondetInterface,
+	ImplicitConstructor,
+	ConstructorSummary,
+	FunctionEntry,
+	FunctionSummary,
+	FunctionBlock,
+	Error
+};
+
 /**
  * Represents a predicate used by the CHC engine.
  */
@@ -39,12 +51,14 @@ public:
 	static Predicate const* create(
 		smtutil::SortPointer _sort,
 		std::string _name,
+		PredicateType _type,
 		smt::EncodingContext& _context,
 		ASTNode const* _node = nullptr
 	);
 
 	Predicate(
 		smt::SymbolicFunctionVariable&& _predicate,
+		PredicateType _type,
 		ASTNode const* _node = nullptr
 	);
 
@@ -88,6 +102,8 @@ public:
 	/// @returns true if this predicate represents an interface.
 	bool isInterface() const;
 
+	PredicateType type() const { return m_type; }
+
 	/// @returns a formatted string representing a call to this predicate
 	/// with _args.
 	std::string formatSummaryCall(std::vector<std::string> const& _args) const;
@@ -108,6 +124,9 @@ private:
 	/// The actual SMT expression.
 	smt::SymbolicFunctionVariable m_predicate;
 
+	/// The type of this predicate.
+	PredicateType m_type;
+
 	/// The ASTNode that this predicate represents.
 	/// nullptr if this predicate is not associated with a specific program AST node.
 	ASTNode const* m_node = nullptr;

libsolidity/formal/PredicateInstance.cpp

@@ -0,0 +1,120 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/PredicateInstance.h>
+
+#include <libsolidity/formal/EncodingContext.h>
+#include <libsolidity/formal/SMTEncoder.h>
+
+using namespace std;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+
+namespace solidity::frontend::smt
+{
+
+smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return _pred(currentStateVariables(_contract, _context));
+}
+
+smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
+{
+	if (auto const* constructor = _contract.constructor())
+		return _pred(currentFunctionVariables(*constructor, &_contract, _context));
+
+	return _pred(
+		vector<smtutil::Expression>{_context.state().errorFlag().currentValue()} +
+		currentStateVariables(_contract, _context)
+	);
+}
+
+/// Currently it does not have arguments but it will have tx data in the future.
+smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext&)
+{
+	return _pred({});
+}
+
+smtutil::Expression function(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	return _pred(currentFunctionVariables(_function, _contract, _context));
+}
+
+smtutil::Expression functionBlock(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	return _pred(currentBlockVariables(_function, _contract, _context));
+}
+
+/// Helpers
+
+vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return stateVariablesAtIndex(0, _contract, _context);
+}
+
+vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return applyMap(
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
+		[&](auto _var) { return _context.variable(*_var)->valueAtIndex(_index); }
+	);
+}
+
+vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return applyMap(
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
+		[&](auto _var) { return _context.variable(*_var)->currentValue(); }
+	);
+}
+
+vector<smtutil::Expression> currentFunctionVariables(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue()};
+	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
+	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
+	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
+	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
+	exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
+	return exprs;
+}
+
+vector<smtutil::Expression> currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context)
+{
+	return currentFunctionVariables(_function, _contract, _context) +
+		applyMap(
+			_function.localVariables(),
+			[&](auto _var) { return _context.variable(*_var)->currentValue(); }
+		);
+}
+
+}

libsolidity/formal/PredicateInstance.h

@@ -0,0 +1,73 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsolidity/formal/Predicate.h>
+
+namespace solidity::frontend::smt
+{
+
+class EncodingContext;
+
+/**
+ * This file represents the specification for building CHC predicate instances.
+ * The predicates follow the specification in PredicateSort.h.
+ * */
+
+smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+
+smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+
+smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+
+smtutil::Expression function(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+smtutil::Expression functionBlock(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+/// Helpers
+
+std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context);
+
+std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context);
+
+std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context);
+
+std::vector<smtutil::Expression> currentFunctionVariables(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+std::vector<smtutil::Expression> currentBlockVariables(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+}