[SMTChecker] Support inheritance and resolve overrides

Changelog.md

@@ -7,6 +7,7 @@ Compiler Features:
  * Code Generator: Use SELFBALANCE for ``address(this).balance`` if using Istanbul EVM
  * SMTChecker: Add break/continue support to the CHC engine.
  * SMTChecker: Support assignments to multi-dimensional arrays and mappings.
+ * SMTChecker: Support inheritance and function overriding.
  * EWasm: Experimental EWasm binary output.
 
 

libsolidity/formal/BMC.cpp

@@ -108,14 +108,16 @@ bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall)
 
 bool BMC::visit(ContractDefinition const& _contract)
 {
-	SMTEncoder::visit(_contract);
+	initContract(_contract);
 
 	/// Check targets created by state variable initialization.
 	smt::Expression constraints = m_context.assertions();
 	checkVerificationTargets(constraints);
 	m_verificationTargets.clear();
 
-	return true;
+	SMTEncoder::visit(_contract);
+
+	return false;
 }
 
 void BMC::endVisit(ContractDefinition const& _contract)

libsolidity/formal/CHC.cpp

@@ -62,8 +62,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	reset();
 
-	if (!SMTEncoder::visit(_contract))
-		return false;
+	initContract(_contract);
 
 	m_stateVariables = _contract.stateVariablesIncludingInherited();
 
@@ -89,7 +88,6 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	// 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());
@@ -108,7 +106,8 @@ bool CHC::visit(ContractDefinition const& _contract)
 		connectBlocks(constructorPred, interface());
 	}
 
-	return true;
+	SMTEncoder::visit(_contract);
+	return false;
 }
 
 void CHC::endVisit(ContractDefinition const& _contract)

libsolidity/formal/CVC4Interface.cpp

@@ -50,8 +50,7 @@ void CVC4Interface::pop()
 
 void CVC4Interface::declareVariable(string const& _name, Sort const& _sort)
 {
-	if (!m_variables.count(_name))
-		m_variables.insert({_name, m_context.mkVar(_name.c_str(), cvc4Sort(_sort))});
+	m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(_sort));
 }
 
 void CVC4Interface::addAssertion(Expression const& _expr)

libsolidity/formal/SMTEncoder.cpp

@@ -36,12 +36,37 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 
 bool SMTEncoder::visit(ContractDefinition const& _contract)
 {
-	solAssert(m_currentContract == nullptr, "");
-	m_currentContract = &_contract;
+	solAssert(m_currentContract, "");
 
-	initializeStateVariables(_contract);
+	for (auto const& node: _contract.subNodes())
+		if (!dynamic_pointer_cast<FunctionDefinition>(node))
+			node->accept(*this);
 
-	return true;
+	vector<FunctionDefinition const*> resolvedFunctions = _contract.definedFunctions();
+	for (auto const& base: _contract.annotation().linearizedBaseContracts)
+		for (auto const& baseFunction: base->definedFunctions())
+		{
+			if (baseFunction->isConstructor())
+				continue;
+			bool overridden = false;
+			for (auto const& function: resolvedFunctions)
+				if (
+					function->name() == baseFunction->name() &&
+					FunctionType(*function).asCallableFunction(false)->
+						hasEqualParameterTypes(*FunctionType(*baseFunction).asCallableFunction(false))
+				)
+				{
+					overridden = true;
+					break;
+				}
+			if (!overridden)
+				resolvedFunctions.push_back(baseFunction);
+		}
+
+	for (auto const& function: resolvedFunctions)
+		function->accept(*this);
+
+	return false;
 }
 
 void SMTEncoder::endVisit(ContractDefinition const& _contract)
@@ -512,6 +537,14 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	}
 }
 
+void SMTEncoder::initContract(ContractDefinition const& _contract)
+{
+	solAssert(m_currentContract == nullptr, "");
+	m_currentContract = &_contract;
+
+	initializeStateVariables(_contract);
+}
+
 void SMTEncoder::initFunction(FunctionDefinition const& _function)
 {
 	solAssert(m_callStack.empty(), "");

libsolidity/formal/SMTEncoder.h

@@ -107,6 +107,7 @@ protected:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void initContract(ContractDefinition const& _contract);
 	void initFunction(FunctionDefinition const& _function);
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);

libsolidity/formal/Z3Interface.cpp

@@ -54,18 +54,20 @@ void Z3Interface::declareVariable(string const& _name, Sort const& _sort)
 {
 	if (_sort.kind == Kind::Function)
 		declareFunction(_name, _sort);
-	else if (!m_constants.count(_name))
-		m_constants.insert({_name, m_context.constant(_name.c_str(), z3Sort(_sort))});
+	else if (m_constants.count(_name))
+		m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(_sort));
+	else
+		m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(_sort)));
 }
 
 void Z3Interface::declareFunction(string const& _name, Sort const& _sort)
 {
 	solAssert(_sort.kind == smt::Kind::Function, "");
-	if (!m_functions.count(_name))
-	{
-		FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
-		m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain))});
-	}
+	FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
+	if (m_functions.count(_name))
+		m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain));
+	else
+		m_functions.emplace(_name, m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain)));
 }
 
 void Z3Interface::addAssertion(Expression const& _expr)

test/libsolidity/smtCheckerTests/inheritance/functions_1.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+// 2 warnings, A.f and A.g
+contract A {
+	uint x;
+
+	function f() public view {
+		assert(x == 1);
+	}
+	function g() public view {
+		assert(x == 1);
+	}
+}
+
+// 2 warnings, B.f and A.g
+contract B is A {
+	function f() public view {
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (113-127): Assertion violation happens here
+// Warning: (162-176): Assertion violation happens here
+// Warning: (259-273): Assertion violation happens here
+// Warning: (162-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/functions_2.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+// 2 warnings, A.f and A.g
+contract A {
+	uint x;
+
+	function f() public view {
+		assert(x == 1);
+	}
+	function g() public view {
+		assert(x == 1);
+	}
+}
+
+// 2 warnings, B.f and A.g
+contract B is A {
+	uint y;
+
+	function f() public view {
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (113-127): Assertion violation happens here
+// Warning: (162-176): Assertion violation happens here
+// Warning: (269-283): Assertion violation happens here
+// Warning: (162-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/inheritance/functions_3.sol

@@ -0,0 +1,47 @@
+pragma experimental SMTChecker;
+
+// 2 warnings, A.f and A.g
+contract A {
+	uint x;
+
+	function f() public view {
+		assert(x == 1);
+	}
+	function g() public view {
+		assert(x == 1);
+	}
+}
+
+// 3 warnings, B.f, B.h, A.g
+contract B is A {
+	uint y;
+
+	function f() public view {
+		assert(x == 0);
+	}
+	function h() public view {
+		assert(x == 2);
+	}
+}
+
+// 4 warnings, C.f, C.i, B.h, A.g
+contract C is B {
+	uint z;
+
+	function f() public view {
+		assert(x == 0);
+	}
+	function i() public view {
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (113-127): Assertion violation happens here
+// Warning: (162-176): Assertion violation happens here
+// Warning: (271-285): Assertion violation happens here
+// Warning: (320-334): Assertion violation happens here
+// Warning: (162-176): Assertion violation happens here
+// Warning: (434-448): Assertion violation happens here
+// Warning: (483-497): Assertion violation happens here
+// Warning: (320-334): Assertion violation happens here
+// Warning: (162-176): Assertion violation happens here