Merge pull request ethereum#8323 from ethereum/smt_split_3

[SMTChecker] CHC support to internal function calls

Changelog.md

@@ -43,6 +43,7 @@ Compiler Features:
  * Code Generator: Use ``calldatacopy`` instead of ``codecopy`` to zero out memory past input.
  * Debug: Provide reason strings for compiler-generated internal reverts when using the ``--revert-strings`` option or the ``settings.debug.revertStrings`` setting on ``debug`` mode.
  * Yul Optimizer: Prune functions that call each other but are otherwise unreferenced.
+ * SMTChecker: CHC support to internal function calls.
 
 
 Bugfixes:

libsolidity/formal/BMC.cpp

@@ -432,12 +432,6 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 			m_context.newValue(*param);
 			m_context.setUnknownValue(*param);
 		}
-
-		m_errorReporter.warning(
-			_funCall.location(),
-			"Assertion checker does not support recursive function calls.",
-			SecondarySourceLocation().append("Starting from function:", funDef->location())
-		);
 	}
 	else
 	{

libsolidity/formal/CHC.cpp

@@ -459,6 +459,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		break;
 	case FunctionType::Kind::Internal:
+		internalFunctionCall(_funCall);
+		break;
 	case FunctionType::Kind::External:
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCall:
@@ -525,6 +527,39 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	m_context.addAssertion(m_error.currentValue() == previousError);
 }
 
+void CHC::internalFunctionCall(FunctionCall const& _funCall)
+{
+	solAssert(m_currentContract, "");
+
+	auto const* function = functionCallToDefinition(_funCall);
+	if (function)
+	{
+		if (m_currentFunction && !m_currentFunction->isConstructor())
+			m_callGraph[m_currentFunction].insert(function);
+		else
+			m_callGraph[m_currentContract].insert(function);
+		auto const* contract = function->annotation().contract;
+
+		// Libraries can have constants as their "state" variables,
+		// so we need to ensure they were constructed correctly.
+		if (contract->isLibrary())
+			m_context.addAssertion(interface(*contract));
+	}
+
+	auto previousError = m_error.currentValue();
+
+	m_context.addAssertion(predicate(_funCall));
+
+	connectBlocks(
+		m_currentBlock,
+		(m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract),
+		(m_error.currentValue() > 0)
+	);
+	m_context.addAssertion(m_error.currentValue() == 0);
+	m_error.increaseIndex();
+	m_context.addAssertion(m_error.currentValue() == previousError);
+}
+
 void CHC::unknownFunctionCall(FunctionCall const&)
 {
 	/// Function calls are not handled at the moment,
@@ -580,12 +615,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 
 bool CHC::shouldVisit(FunctionDefinition const& _function) const
 {
-	if (
-		_function.isPublic() &&
-		_function.isImplemented()
-	)
-		return true;
-	return false;
+	return _function.isImplemented();
 }
 
 void CHC::setCurrentBlock(
@@ -919,6 +949,34 @@ smt::Expression CHC::predicate(
 	return _block(_arguments);
 }
 
+smt::Expression CHC::predicate(FunctionCall const& _funCall)
+{
+	auto const* function = functionCallToDefinition(_funCall);
+	if (!function)
+		return smt::Expression(true);
+
+	m_error.increaseIndex();
+	vector<smt::Expression> args{m_error.currentValue()};
+	auto const* contract = function->annotation().contract;
+
+	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
+	args += symbolicArguments(_funCall);
+	for (auto const& var: m_stateVariables)
+		m_context.variable(*var)->increaseIndex();
+	args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
+
+	auto const& returnParams = function->returnParameters();
+	for (auto param: returnParams)
+		if (m_context.knownVariable(*param))
+			m_context.variable(*param)->increaseIndex();
+		else
+			createVariable(*param);
+	for (auto const& var: function->returnParameters())
+		args.push_back(m_context.variable(*var)->currentValue());
+
+	return (*m_summaries.at(contract).at(function))(args);
+}
+
 void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 {
 	m_interface->addRule(_rule, _ruleName);

libsolidity/formal/CHC.h

@@ -76,6 +76,7 @@ class CHC: public SMTEncoder
 	void endVisit(Continue const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void internalFunctionCall(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
 	//@}
 
@@ -164,6 +165,8 @@ class CHC: public SMTEncoder
 	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block);
 	/// @returns a predicate application over @param _arguments.
 	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const& _arguments);
+	/// @returns the summary predicate for the called function.
+	smt::Expression predicate(FunctionCall const& _funCall);
 	/// @returns a predicate that defines a constructor summary.
 	smt::Expression summary(ContractDefinition const& _contract);
 	/// @returns a predicate that defines a function summary.

libsolidity/formal/SMTEncoder.cpp

@@ -673,7 +673,6 @@ void SMTEncoder::visitAssert(FunctionCall const& _funCall)
 	auto const& args = _funCall.arguments();
 	solAssert(args.size() == 1, "");
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
-	addPathImpliedExpression(expr(*args.front()));
 }
 
 void SMTEncoder::visitRequire(FunctionCall const& _funCall)

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol

@@ -6,23 +6,17 @@ contract c {
 		x = x + 1;
 		return x;
 	}
-	function g(bool a) public returns (bool) {
+	function g() public returns (bool) {
 		bool b;
-		if (a) {
-			x = 0;
-			b = (f() == 0) && (f() == 0);
-			assert(x == 1);
-			assert(!b);
-		} else {
 			x = 100;
-			b = (f() > 0) && (f() > 0);
+			b = f() > 0;
 			assert(x == 102);
 			// Should fail.
 			assert(!b);
-		}
 		return b;
 	}
 }
 // ----
 // Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (362-372): Assertion violation happens here
+// Warning: (202-218): Assertion violation happens here
+// Warning: (242-252): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol

@@ -19,4 +19,6 @@ contract A is B {
 	}
 }
 // ----
+// Warning: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (265-270): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (253-271): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol

@@ -26,4 +26,6 @@ contract A is B2, B1 {
 }
 // ----
 // Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (330-348): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol

@@ -26,4 +26,6 @@ contract A is B2, B1 {
 }
 // ----
 // Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (214-219): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (342-347): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (330-348): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -31,4 +31,7 @@ contract A is B2, B1 {
 // Warning: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (262-267): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (262-267): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (174-179): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (362-378): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol

@@ -26,4 +26,5 @@ contract A is B {
 }
 // ----
 // Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (356-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol

@@ -14,3 +14,4 @@ contract A is C {
 }
 // ----
 // Warning: (148-162): Assertion violation happens here
+// Warning: (166-182): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol

@@ -9,5 +9,3 @@ contract C {
     }
 }
 // ----
-// Warning: (99-107): Assertion checker does not support recursive function calls.
-// Warning: (141-144): Assertion checker does not support recursive function calls.

test/libsolidity/smtCheckerTests/functions/function_inline_chain.sol

@@ -2,40 +2,22 @@ pragma experimental SMTChecker;
 
 contract C
 {
-	uint x;
 	uint y;
-	uint z;
 
 	function f() public {
-		if (x == 1)
-			x = 2;
-		else
-			x = 1;
-		g();
+		if (y != 1)
+			g();
 		assert(y == 1);
 	}
 
-	function g() public {
+	function g() internal {
 		y = 1;
 		h();
-		assert(z == 1);
 	}
 
-	function h() public {
-		z = 1;
-		x = 1;
+	function h() internal {
 		f();
-		// This fails for the following calls to the contract:
-		// h()
-		// g() h()
-		// It does not fail for f() g() h() because in that case
-		// h() will not inline f() since it already is in the callstack.
-		assert(x == 1);
+		assert(y == 1);
 	}
 }
 // ----
-// Warning: (271-274): Assertion checker does not support recursive function calls.
-// Warning: (140-143): Assertion checker does not support recursive function calls.
-// Warning: (483-497): Assertion violation happens here
-// Warning: (201-204): Assertion checker does not support recursive function calls.
-// Warning: (483-497): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_recursive.sol

@@ -14,4 +14,3 @@ contract C
 }
 
 // ----
-// Warning: (111-114): Assertion checker does not support recursive function calls.

test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol

@@ -22,5 +22,4 @@ contract C
 	}
 }
 // ----
-// Warning: (206-209): Assertion checker does not support recursive function calls.
-// Warning: (111-114): Assertion checker does not support recursive function calls.
+// Warning: (130-144): Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C{
+    uint x;
+	constructor(uint y) public {
+		assert(x == 0);
+		x = 1;
+	}
+    function f() public {
+		assert(x == 1);
+		++x;
+		g();
+		assert(x == 1);
+    }
+
+	function g() internal {
+		assert(x == 2);
+		--x;
+		assert(x == 1);
+	}
+}
+// ----
+// Warning: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (245-248): Underflow (resulting value less than 0) happens here

test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C{
+    uint x;
+	constructor(uint y) public {
+		assert(x == 1);
+		x = 1;
+	}
+    function f() public {
+		assert(x == 2);
+		++x;
+		g();
+		assert(x == 2);
+    }
+
+	function g() internal {
+		assert(x == 3);
+		--x;
+		assert(x == 2);
+	}
+}
+// ----
+// Warning: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (145-159): Assertion violation happens here
+// Warning: (163-166): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (227-241): Assertion violation happens here
+// Warning: (252-266): Assertion violation happens here
+// Warning: (177-191): Assertion violation happens here
+// Warning: (227-241): Assertion violation happens here
+// Warning: (245-248): Underflow (resulting value less than 0) happens here
+// Warning: (252-266): Assertion violation happens here
+// Warning: (89-103): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal {
+		assert(x == 1);
+		--x;
+	}
+}
+
+contract C is A {
+	constructor() public {
+		assert(x == 0);
+		++x;
+		f();
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (100-103): Underflow (resulting value less than 0) happens here
+// Warning: (100-103): Underflow (resulting value less than 0) happens here

test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1_fail.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal {
+		assert(x == 2);
+		--x;
+	}
+}
+
+contract C is A {
+	constructor() public {
+		assert(x == 1);
+		++x;
+		f();
+		assert(x == 1);
+	}
+}
+// ----
+// Warning: (82-96): Assertion violation happens here
+// Warning: (100-103): Underflow (resulting value less than 0) happens here
+// Warning: (82-96): Assertion violation happens here
+// Warning: (100-103): Underflow (resulting value less than 0) happens here
+// Warning: (155-169): Assertion violation happens here
+// Warning: (82-96): Assertion violation happens here
+// Warning: (187-201): Assertion violation happens here