Merge pull request #10836 from ethereum/smt_fix_cex_inheritance

Fix inheritance bug in CHC cex

libsolidity/formal/CHC.cpp

@@ -936,9 +936,9 @@ SortPointer CHC::sort(ASTNode const* _node)
 	return functionBodySort(*m_currentFunction, m_currentContract, state());
 }
 
-Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node)
+Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node, ContractDefinition const* _contractContext)
 {
-	auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node);
+	auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext);
 	m_interface->registerRelation(block->functor());
 	return block;
 }
@@ -1081,7 +1081,8 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType,
 		sort(_node),
 		"block_" + uniquePrefix() + "_" + _prefix + predicateName(_node),
 		_predType,
-		_node
+		_node,
+		m_currentContract
 	);
 
 	solAssert(m_currentFunction, "");
@@ -1094,7 +1095,8 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co
 		functionSort(_function, &_contract, state()),
 		"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
 		_type,
-		&_function
+		&_function,
+		&_contract
 	);
 }
 
@@ -1104,6 +1106,7 @@ Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract
 		constructorSort(_contract, state()),
 		_prefix + "_" + contractSuffix(_contract) + "_" + uniquePrefix(),
 		PredicateType::ConstructorSummary,
+		&_contract,
 		&_contract
 	);
 }

libsolidity/formal/CHC.h

@@ -126,7 +126,7 @@ private:
 	/// Predicate helpers.
 	//@{
 	/// @returns a new block of given _sort and _name.
-	Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr);
+	Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr, ContractDefinition const* _contractContext = nullptr);
 
 	/// Creates summary predicates for all functions of all contracts
 	/// in a given _source.

libsolidity/formal/Predicate.cpp

@@ -40,7 +40,8 @@ Predicate const* Predicate::create(
 	string _name,
 	PredicateType _type,
 	EncodingContext& _context,
-	ASTNode const* _node
+	ASTNode const* _node,
+	ContractDefinition const* _contractContext
 )
 {
 	smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context};
@@ -49,18 +50,20 @@ Predicate const* Predicate::create(
 	return &m_predicates.emplace(
 		std::piecewise_construct,
 		std::forward_as_tuple(functorName),
-		std::forward_as_tuple(move(predicate), _type, _node)
+		std::forward_as_tuple(move(predicate), _type, _node, _contractContext)
 	).first->second;
 }
 
 Predicate::Predicate(
 	smt::SymbolicFunctionVariable&& _predicate,
 	PredicateType _type,
-	ASTNode const* _node
+	ASTNode const* _node,
+	ContractDefinition const* _contractContext
 ):
 	m_predicate(move(_predicate)),
 	m_type(_type),
-	m_node(_node)
+	m_node(_node),
+	m_contractContext(_contractContext)
 {
 }
 
@@ -130,18 +133,8 @@ FunctionCall const* Predicate::programFunctionCall() const
 
 optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
 {
-	if (auto const* fun = programFunction())
-		return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
-	if (auto const* contract = programContract())
-		return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract);
-
-	auto const* node = m_node;
-	while (auto const* scopable = dynamic_cast<Scopable const*>(node))
-	{
-		node = scopable->scope();
-		if (auto const* fun = dynamic_cast<FunctionDefinition const*>(node))
-			return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
-	}
+	if (m_contractContext)
+		return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*m_contractContext);
 
 	return nullopt;
 }

libsolidity/formal/Predicate.h

@@ -55,13 +55,15 @@ public:
 		std::string _name,
 		PredicateType _type,
 		smt::EncodingContext& _context,
-		ASTNode const* _node = nullptr
+		ASTNode const* _node = nullptr,
+		ContractDefinition const* _contractContext = nullptr
 	);
 
 	Predicate(
 		smt::SymbolicFunctionVariable&& _predicate,
 		PredicateType _type,
-		ASTNode const* _node = nullptr
+		ASTNode const* _node = nullptr,
+		ContractDefinition const* _contractContext = nullptr
 	);
 
 	/// Predicate should not be copiable.
@@ -166,6 +168,12 @@ private:
 	/// nullptr if this predicate is not associated with a specific program AST node.
 	ASTNode const* m_node = nullptr;
 
+	/// The ContractDefinition that contains this predicate.
+	/// nullptr if this predicate is not associated with a specific contract.
+	/// This is unfortunately necessary because of virtual resolution for
+	/// function nodes.
+	ContractDefinition const* m_contractContext = nullptr;
+
 	/// Maps the name of the predicate to the actual Predicate.
 	/// Used in counterexample generation.
 	static std::map<std::string, Predicate> m_predicates;

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract B {
+	uint x;
+	function f() public view {
+		assert(x == 0);
+	}
+}
+
+contract C is B {
+	uint y;
+	function g() public {
+		x = 1;
+		f();
+	}
+}
+// ----
+// Warning 6328: (85-99): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n    B.f() -- internal call\nState: y = 0, x = 1\nB.f()

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal view {
+		assert(x == 0);
+	}
+}
+
+contract B is A {
+	uint a;
+	uint b;
+}
+
+contract C is B {
+	uint y;
+	uint z;
+	uint w;
+	function g() public {
+		x = 1;
+		f();
+	}
+}
+// ----
+// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, z = 0, w = 0, a = 0, b = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, z = 0, w = 0, a = 0, b = 0, x = 0\nC.g()\n    A.f() -- internal call