Merge pull request #7121 from ethereum/smt_chc_functions

[SMTChecker] CHC blocks for functions and asserts

Changelog.md

@@ -24,9 +24,11 @@ Compiler Features:
  * Standard JSON Interface: Provide secondary error locations (e.g. the source position of other conflicting declarations).
  * SMTChecker: Do not erase knowledge about storage pointers if another storage pointer is assigned.
  * SMTChecker: Support string literal type.
+ * SMTChecker: New Horn-based algorithm that proves assertions via multi-transaction contract invariants.
  * Standard JSON Interface: Provide AST even on errors if ``--error-recovery`` commandline switch or StandardCompiler `settings.parserErrorRecovery` is true.
  * Yul Optimizer: Do not inline function if it would result in expressions being duplicated that are not cheap.
 
+
 Bugfixes:
  * ABI decoder: Ensure that decoded arrays always point to distinct memory locations.
  * Code Generator: Treat dynamically encoded but statically sized arrays and structs in calldata properly.

libsolidity/formal/CHC.cpp

@@ -135,6 +135,44 @@ bool CHC::visit(FunctionDefinition const& _function)
 	solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
 	m_currentFunction = &_function;
 
+	initFunction(_function);
+
+	// Store the constraints related to variable initialization.
+	smt::Expression const& initAssertions = m_context.assertions();
+
+	createFunctionBlock(*m_currentFunction);
+
+	// Rule Interface -> FunctionEntry, uses no constraints.
+	smt::Expression interfaceFunction = smt::Expression::implies(
+		interface(),
+		predicateCurrent(m_currentFunction)
+	);
+	m_interface->addRule(
+		interfaceFunction,
+		m_interfacePredicate->currentName() + "_to_" + m_predicates.at(m_currentFunction)->currentName()
+	);
+
+	pushBlock(predicateCurrent(m_currentFunction));
+
+	createFunctionBlock(m_currentFunction->body());
+
+	// Rule FunctionEntry -> FunctionBody, also no constraints.
+	smt::Expression functionBody = smt::Expression::implies(
+		predicateEntry(m_currentFunction),
+		predicateBodyCurrent(&m_currentFunction->body())
+	);
+	m_interface->addRule(
+		functionBody,
+		m_predicates.at(m_currentFunction)->currentName() + "_to_" + m_predicates.at(&m_currentFunction->body())->currentName()
+	);
+
+	pushBlock(predicateBodyCurrent(&m_currentFunction->body()));
+	// We need to re-add the constraints that were created for initialization of variables.
+	m_context.addAssertion(initAssertions);
+
+	solAssert(m_functionBlocks == 0, "");
+	m_functionBlocks = 2;
+
 	SMTEncoder::visit(*m_currentFunction);
 
 	return false;
@@ -146,7 +184,36 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		return;
 
 	solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented");
+
+	// Create Function Exit block.
+	createFunctionBlock(*m_currentFunction);
+
+	// Rule FunctionBody -> FunctionExit.
+	smt::Expression bodyFunction = smt::Expression::implies(
+		predicateEntry(&_function.body()) && m_context.assertions(),
+		predicateCurrent(&_function)
+	);
+	m_interface->addRule(
+		bodyFunction,
+		m_predicates.at(&_function.body())->currentName() + "_to_" + m_predicates.at(&_function.body())->currentName()
+	);
+
+	// Rule FunctionExit -> Interface, uses no constraints.
+	smt::Expression functionInterface = smt::Expression::implies(
+		predicateCurrent(&_function),
+		interface()
+	);
+	m_interface->addRule(
+		functionInterface,
+		m_predicates.at(&_function)->currentName() + "_to_" + m_interfacePredicate->currentName()
+	);
+
 	m_currentFunction = nullptr;
+	solAssert(m_path.size() == m_functionBlocks, "");
+	for (unsigned i = 0; i < m_path.size(); ++i)
+		m_context.popSolver();
+	m_functionBlocks = 0;
+	m_path.clear();
 
 	SMTEncoder::endVisit(_function);
 }
@@ -155,8 +222,30 @@ bool CHC::visit(IfStatement const& _if)
 {
 	solAssert(m_currentFunction, "");
 
+	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
+	m_unknownFunctionCallSeen = false;
+
 	SMTEncoder::visit(_if);
 
+	if (m_unknownFunctionCallSeen)
+		eraseKnowledge();
+
+	m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
+
+	return false;
+}
+
+bool CHC::visit(WhileStatement const& _while)
+{
+	eraseKnowledge();
+	m_context.resetVariables(touchedVariables(_while));
+	return false;
+}
+
+bool CHC::visit(ForStatement const& _for)
+{
+	eraseKnowledge();
+	m_context.resetVariables(touchedVariables(_for));
 	return false;
 }
 
@@ -164,20 +253,74 @@ void CHC::endVisit(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
 
-	if (_funCall.annotation().kind == FunctionCallKind::FunctionCall)
+	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
 	{
-		FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+		SMTEncoder::endVisit(_funCall);
-		if (funType.kind() == FunctionType::Kind::Assert)
+		return;
-			visitAssert(_funCall);
 	}
 
-	SMTEncoder::endVisit(_funCall);
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	switch (funType.kind())
+	{
+	case FunctionType::Kind::Assert:
+		visitAssert(_funCall);
+		SMTEncoder::endVisit(_funCall);
+		break;
+	case FunctionType::Kind::Internal:
+	case FunctionType::Kind::External:
+	case FunctionType::Kind::DelegateCall:
+	case FunctionType::Kind::BareCall:
+	case FunctionType::Kind::BareCallCode:
+	case FunctionType::Kind::BareDelegateCall:
+	case FunctionType::Kind::BareStaticCall:
+	case FunctionType::Kind::Creation:
+	case FunctionType::Kind::KECCAK256:
+	case FunctionType::Kind::ECRecover:
+	case FunctionType::Kind::SHA256:
+	case FunctionType::Kind::RIPEMD160:
+	case FunctionType::Kind::BlockHash:
+	case FunctionType::Kind::AddMod:
+	case FunctionType::Kind::MulMod:
+		SMTEncoder::endVisit(_funCall);
+		unknownFunctionCall(_funCall);
+		break;
+	default:
+		SMTEncoder::endVisit(_funCall);
+		break;
+	}
 
 	createReturnedExpressions(_funCall);
 }
 
-void CHC::visitAssert(FunctionCall const&)
+void CHC::visitAssert(FunctionCall const& _funCall)
 {
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() == 1, "");
+	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
+
+	solAssert(!m_path.empty(), "");
+
+	smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
+	smt::Expression assertionError = smt::Expression::implies(
+		m_path.back() && m_context.assertions() && currentPathConditions() && assertNeg,
+		error()
+	);
+	string predicateName = "assert_" + to_string(_funCall.id());
+	m_interface->addRule(assertionError, predicateName + "_to_error");
+
+	m_verificationTargets.push_back(&_funCall);
+}
+
+void CHC::unknownFunctionCall(FunctionCall const&)
+{
+	/// Function calls are not handled at the moment,
+	/// so always erase knowledge.
+	/// TODO remove when function calls get predicates/blocks.
+	eraseKnowledge();
+
+	/// Used to erase outer scope knowledge in loops and ifs.
+	/// TODO remove when function calls get predicates/blocks.
+	m_unknownFunctionCallSeen = true;
 }
 
 void CHC::reset()
@@ -186,6 +329,13 @@ void CHC::reset()
 	m_stateVariables.clear();
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
+	m_unknownFunctionCallSeen = false;
+}
+
+void CHC::eraseKnowledge()
+{
+	resetStateVariables();
+	m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
 }
 
 bool CHC::shouldVisit(ContractDefinition const& _contract) const
@@ -208,13 +358,25 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 	return false;
 }
 
+void CHC::pushBlock(smt::Expression const& _block)
+{
+	m_context.pushSolver();
+	m_path.push_back(_block);
+}
+
+void CHC::popBlock()
+{
+	m_context.popSolver();
+	m_path.pop_back();
+}
+
 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());
+	return sort(*m_currentContract->constructor());
 }
 
 smt::SortPointer CHC::interfaceSort()
@@ -226,14 +388,41 @@ smt::SortPointer CHC::interfaceSort()
 	);
 }
 
-smt::SortPointer CHC::functionSort(FunctionDefinition const& _function)
+smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 {
+	if (m_nodeSorts.count(&_function))
+		return m_nodeSorts.at(&_function);
+
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	auto const& funType = dynamic_cast<FunctionType const&>(*_function.type());
+	vector<smt::SortPointer> varSorts;
-	return make_shared<smt::FunctionSort>(
+	for (auto const& var: _function.parameters() + _function.returnParameters())
-		smt::smtSort(funType.parameterTypes()),
+		varSorts.push_back(smt::smtSort(*var->type()));
+	auto sort = make_shared<smt::FunctionSort>(
+		m_stateSorts + varSorts,
 		boolSort
 	);
+	return m_nodeSorts[&_function] = move(sort);
+}
+
+smt::SortPointer CHC::sort(Block const& _block)
+{
+	if (m_nodeSorts.count(&_block))
+		return m_nodeSorts.at(&_block);
+
+	solAssert(_block.scope() == m_currentFunction, "");
+
+	auto fSort = dynamic_pointer_cast<smt::FunctionSort>(sort(*m_currentFunction));
+	solAssert(fSort, "");
+
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	vector<smt::SortPointer> varSorts;
+	for (auto const& var: m_currentFunction->localVariables())
+		varSorts.push_back(smt::smtSort(*var->type()));
+	auto functionBodySort = make_shared<smt::FunctionSort>(
+		fSort->domain + varSorts,
+		boolSort
+	);
+	return m_nodeSorts[&_block] = move(functionBodySort);
 }
 
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(smt::SortPointer _sort, string const& _name)
@@ -273,6 +462,81 @@ smt::Expression CHC::error()
 	return (*m_errorPredicate)({});
 }
 
+void CHC::createFunctionBlock(FunctionDefinition const& _function)
+{
+	if (m_predicates.count(&_function))
+	{
+		m_predicates.at(&_function)->increaseIndex();
+		m_interface->registerRelation(m_predicates.at(&_function)->currentValue());
+	}
+	else
+		m_predicates[&_function] = createBlock(
+			sort(_function),
+			predicateName(_function)
+		);
+}
+
+void CHC::createFunctionBlock(Block const& _block)
+{
+	solAssert(_block.scope() == m_currentFunction, "");
+	if (m_predicates.count(&_block))
+	{
+		m_predicates.at(&_block)->increaseIndex();
+		m_interface->registerRelation(m_predicates.at(&_block)->currentValue());
+	}
+	else
+		m_predicates[&_block] = createBlock(
+			sort(_block),
+			predicateName(*m_currentFunction) + "_body"
+		);
+}
+
+vector<smt::Expression> CHC::currentFunctionVariables()
+{
+	solAssert(m_currentFunction, "");
+	vector<smt::Expression> paramExprs;
+	for (auto const& var: m_stateVariables)
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return paramExprs;
+}
+
+vector<smt::Expression> CHC::currentBlockVariables()
+{
+	solAssert(m_currentFunction, "");
+	vector<smt::Expression> paramExprs;
+	for (auto const& var: m_currentFunction->localVariables())
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return currentFunctionVariables() + paramExprs;
+}
+
+string CHC::predicateName(FunctionDefinition const& _function)
+{
+	string functionName = _function.isConstructor() ?
+		"constructor" :
+		_function.isFallback() ?
+			"fallback" :
+			"function_" + _function.name();
+	return functionName + "_" + to_string(_function.id());
+}
+
+smt::Expression CHC::predicateCurrent(ASTNode const* _node)
+{
+	return (*m_predicates.at(_node))(currentFunctionVariables());
+}
+
+smt::Expression CHC::predicateBodyCurrent(ASTNode const* _node)
+{
+	return (*m_predicates.at(_node))(currentBlockVariables());
+}
+
+smt::Expression CHC::predicateEntry(ASTNode const* _node)
+{
+	solAssert(!m_path.empty(), "");
+	return (*m_predicates.at(_node))(m_path.back().arguments);
+}
+
 bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
 {
 	smt::CheckResult result;

libsolidity/formal/CHC.h

@@ -58,23 +58,30 @@ private:
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	bool visit(IfStatement const& _node) override;
+	bool visit(WhileStatement const&) override;
+	bool visit(ForStatement const&) override;
 	void endVisit(FunctionCall const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void unknownFunctionCall(FunctionCall const& _funCall);
 	//@}
 
 	/// Helpers.
 	//@{
 	void reset();
+	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
+	void pushBlock(smt::Expression const& _block);
+	void popBlock();
 	//@}
 
 	/// Sort helpers.
 	//@{
 	smt::SortPointer constructorSort();
 	smt::SortPointer interfaceSort();
-	smt::SortPointer functionSort(FunctionDefinition const& _function);
+	smt::SortPointer sort(FunctionDefinition const& _function);
+	smt::SortPointer sort(Block const& _block);
 	//@}
 
 	/// Predicate helpers.
@@ -88,6 +95,33 @@ private:
 	smt::Expression interface();
 	/// Error predicate over current variables.
 	smt::Expression error();
+
+	/// Creates a block for the given _function or increases its SSA index
+	/// if the block already exists which in practice creates a new function.
+	/// The predicate parameters are _function input and output parameters.
+	void createFunctionBlock(FunctionDefinition const& _function);
+	/// Creates a block for the given _function or increases its SSA index
+	/// if the block already exists which in practice creates a new function.
+	/// The predicate parameters are m_currentFunction input, output
+	/// and local variables.
+	void createFunctionBlock(Block const& _block);
+
+	/// @returns the current symbolic values of the current function's
+	/// input and output parameters.
+	std::vector<smt::Expression> currentFunctionVariables();
+	/// @returns the samve as currentFunctionVariables plus
+	/// local variables.
+	std::vector<smt::Expression> currentBlockVariables();
+
+	/// @returns the predicate name for a given function.
+	std::string predicateName(FunctionDefinition const& _function);
+	/// @returns a predicate application over the current function's parameters.
+	smt::Expression predicateCurrent(ASTNode const* _node);
+	/// @returns a predicate application over the current function's parameters plus local variables.
+	smt::Expression predicateBodyCurrent(ASTNode const* _node);
+	/// Predicate for block _node over the variables at the latest
+	/// block entry.
+	smt::Expression predicateEntry(ASTNode const* _node);
 	//@}
 
 	/// Solver related.
@@ -109,6 +143,9 @@ private:
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
 	std::unique_ptr<smt::SymbolicVariable> m_errorPredicate;
+
+	/// Maps AST nodes to their predicates.
+	std::unordered_map<ASTNode const*, std::shared_ptr<smt::SymbolicVariable>> m_predicates;
 	//@}
 
 	/// Variables.
@@ -119,6 +156,9 @@ private:
 	/// State variables.
 	/// Used to create all predicates.
 	std::vector<VariableDeclaration const*> m_stateVariables;
+
+	/// Input sorts for AST nodes.
+	std::map<ASTNode const*, smt::SortPointer> m_nodeSorts;
 	//@}
 
 	/// Verification targets.
@@ -132,6 +172,13 @@ private:
 	/// Control-flow.
 	//@{
 	FunctionDefinition const* m_currentFunction = nullptr;
+
+	/// Number of basic blocks created for the body of the current function.
+	unsigned m_functionBlocks = 0;
+	/// The current control flow path.
+	std::vector<smt::Expression> m_path;
+	/// Whether a function call was seen in the current scope.
+	bool m_unknownFunctionCallSeen = false;
 	//@}
 
 	/// CHC solver.

test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+
+	function f() public {
+		if (x == 0)
+			x = 1;
+	}
+
+	function g() public {
+		if (x == 1)
+			x = 2;
+	}
+
+	function h() public {
+		if (x == 2)
+			x = 0;
+	}
+
+	// This function shows that (x < 9) is not inductive and
+	// a stronger invariant is needed to be found.
+	// (x < 3) is the one found in the end.
+	function j() public {
+		if (x == 7)
+			x = 100;
+	}
+
+	function i() public view {
+		assert(x < 9);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+
+	function f() public {
+		if (x == 0)
+			x = 1;
+	}
+
+	function g() public {
+		if (x == 1)
+			x = 2;
+	}
+
+	function h() public {
+		if (x == 2)
+			x = 0;
+	}
+
+	function j() public {
+		if (x < 2)
+			x = 100;
+	}
+
+	// Fails due to j.
+	function i() public view {
+		assert(x < 2);
+	}
+}
+// ----
+// Warning: (311-324): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol

@@ -15,6 +15,10 @@ contract C
 		assert(x > 0);
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (136-149): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol

@@ -20,6 +20,10 @@ contract C
 	function f() m n public {
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (170-183): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol

@@ -17,6 +17,10 @@ contract C
 	function f() m public {
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (156-170): Assertion violation happens here