Merge pull request #7107 from ethereum/smt_chc_constructor_interface

[SMTChecker] Add CHC constructor/interface/error blocks

libsolidity/formal/CHC.cpp

@@ -65,6 +65,52 @@ bool CHC::visit(ContractDefinition const& _contract)
 	if (!SMTEncoder::visit(_contract))
 		return false;
 
+	m_stateVariables = _contract.stateVariablesIncludingInherited();
+
+	for (auto const& var: m_stateVariables)
+		// SMT solvers do not support function types as arguments.
+		if (var->type()->category() == Type::Category::Function)
+			m_stateSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
+		else
+			m_stateSorts.push_back(smt::smtSort(*var->type()));
+
+	string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id());
+	m_interfacePredicate = createBlock(interfaceSort(),	interfaceName);
+
+	// TODO create static instances for Bool/Int sorts in SolverInterface.
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	auto errorFunctionSort = make_shared<smt::FunctionSort>(
+		vector<smt::SortPointer>(),
+		boolSort
+	);
+	m_errorPredicate = createBlock(errorFunctionSort, "error");
+
+	// If the contract has a constructor it is handled as a function.
+	// Otherwise we zero-initialize all state vars.
+	// TODO take into account state vars init values.
+	if (!_contract.constructor())
+	{
+		string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id());
+		m_constructorPredicate = createBlock(constructorSort(), constructorName);
+
+		for (auto const& var: m_stateVariables)
+		{
+			auto const& symbVar = m_context.variable(*var);
+			symbVar->increaseIndex();
+			m_interface->declareVariable(symbVar->currentName(), *symbVar->sort());
+			m_context.setZeroValue(*symbVar);
+		}
+
+		smt::Expression constructorAppl = (*m_constructorPredicate)({});
+		m_interface->addRule(constructorAppl, constructorName);
+
+		smt::Expression constructorInterface = smt::Expression::implies(
+			constructorAppl && m_context.assertions(),
+			interface()
+		);
+		m_interface->addRule(constructorInterface, constructorName + "_to_" + interfaceName);
+	}
+
 	return true;
 }
 
@@ -73,6 +119,11 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	if (!shouldVisit(_contract))
 		return;
 
+	auto errorAppl = (*m_errorPredicate)({});
+	for (auto const& target: m_verificationTargets)
+		if (query(errorAppl, target->location()))
+			m_safeAssertions.insert(target);
+
 	SMTEncoder::endVisit(_contract);
 }
 
@@ -131,6 +182,8 @@ void CHC::visitAssert(FunctionCall const&)
 
 void CHC::reset()
 {
+	m_stateSorts.clear();
+	m_stateVariables.clear();
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
 }
@@ -155,6 +208,71 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 	return false;
 }
 
+smt::SortPointer CHC::constructorSort()
+{
+	solAssert(m_currentContract, "");
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	if (!m_currentContract->constructor())
+		return make_shared<smt::FunctionSort>(vector<smt::SortPointer>{}, boolSort);
+	return functionSort(*m_currentContract->constructor());
+}
+
+smt::SortPointer CHC::interfaceSort()
+{
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	return make_shared<smt::FunctionSort>(
+		m_stateSorts,
+		boolSort
+	);
+}
+
+smt::SortPointer CHC::functionSort(FunctionDefinition const& _function)
+{
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	auto const& funType = dynamic_cast<FunctionType const&>(*_function.type());
+	return make_shared<smt::FunctionSort>(
+		smt::smtSort(funType.parameterTypes()),
+		boolSort
+	);
+}
+
+unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(smt::SortPointer _sort, string const& _name)
+{
+	auto block = make_unique<smt::SymbolicFunctionVariable>(
+		_sort,
+		_name,
+		m_context
+	);
+	m_interface->registerRelation(block->currentValue());
+	return block;
+}
+
+smt::Expression CHC::constructor()
+{
+	solAssert(m_currentContract, "");
+
+	if (!m_currentContract->constructor())
+		return (*m_constructorPredicate)({});
+
+	vector<smt::Expression> paramExprs;
+	for (auto const& var: m_currentContract->constructor()->parameters())
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return (*m_constructorPredicate)(paramExprs);
+}
+
+smt::Expression CHC::interface()
+{
+	vector<smt::Expression> paramExprs;
+	for (auto const& var: m_stateVariables)
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return (*m_interfacePredicate)(paramExprs);
+}
+
+smt::Expression CHC::error()
+{
+	return (*m_errorPredicate)({});
+}
+
 bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
 {
 	smt::CheckResult result;

libsolidity/formal/CHC.h

@@ -70,12 +70,57 @@ private:
 	bool shouldVisit(FunctionDefinition const& _function) const;
 	//@}
 
+	/// Sort helpers.
+	//@{
+	smt::SortPointer constructorSort();
+	smt::SortPointer interfaceSort();
+	smt::SortPointer functionSort(FunctionDefinition const& _function);
+	//@}
+
+	/// Predicate helpers.
+	//@{
+	/// @returns a new block of given _sort and _name.
+	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(smt::SortPointer _sort, std::string const& _name);
+
+	/// Constructor predicate over current variables.
+	smt::Expression constructor();
+	/// Interface predicate over current variables.
+	smt::Expression interface();
+	/// Error predicate over current variables.
+	smt::Expression error();
+	//@}
+
 	/// Solver related.
 	//@{
 	/// @returns true if query is unsatisfiable (safe).
 	bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
 	//@}
 
+	/// Predicates.
+	//@{
+	/// Constructor predicate.
+	/// Default constructor sets state vars to 0.
+	std::unique_ptr<smt::SymbolicVariable> m_constructorPredicate;
+
+	/// Artificial Interface predicate.
+	/// Single entry block for all functions.
+	std::unique_ptr<smt::SymbolicVariable> m_interfacePredicate;
+
+	/// Artificial Error predicate.
+	/// Single error block for all assertions.
+	std::unique_ptr<smt::SymbolicVariable> m_errorPredicate;
+	//@}
+
+	/// Variables.
+	//@{
+	/// State variables sorts.
+	/// Used by all predicates.
+	std::vector<smt::SortPointer> m_stateSorts;
+	/// State variables.
+	/// Used to create all predicates.
+	std::vector<VariableDeclaration const*> m_stateVariables;
+	//@}
+
 	/// Verification targets.
 	//@{
 	std::vector<Expression const*> m_verificationTargets;

libsolidity/formal/SMTEncoder.cpp

@@ -40,6 +40,7 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 	m_currentContract = &_contract;
 
 	initializeStateVariables(_contract);
+
 	return true;
 }