Merge pull request #10614 from blishko/smt-overidden-modifiers

[SMTChecker] Fix analysis of overriding modifiers

Changelog.md

@@ -3,6 +3,9 @@
 Compiler Features:
  * SMTChecker: Support ABI functions as uninterpreted functions.
 
+Bugfixes:
+ * SMTChecker: Fix false negatives in overriding modifiers.
+
 
 ### 0.8.0 (2020-12-16)
 

libsolidity/formal/CHC.cpp

@@ -821,7 +821,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 	{
 		for (auto const& var: _function->parameters() + _function->returnParameters())
 			m_context.variable(*var)->increaseIndex();
-		for (auto const& var: localVariablesIncludingModifiers(*_function))
+		for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
 			m_context.variable(*var)->increaseIndex();
 	}
 
@@ -898,7 +898,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						createVariable(*var);
 					for (auto var: function->returnParameters())
 						createVariable(*var);
-					for (auto const* var: localVariablesIncludingModifiers(*function))
+					for (auto const* var: localVariablesIncludingModifiers(*function, contract))
 						createVariable(*var);
 
 					m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));

libsolidity/formal/PredicateInstance.cpp

@@ -179,7 +179,7 @@ vector<smtutil::Expression> currentBlockVariables(FunctionDefinition const& _fun
 {
 	return currentFunctionVariablesForDefinition(_function, _contract, _context) +
 		applyMap(
-			SMTEncoder::localVariablesIncludingModifiers(_function),
+			SMTEncoder::localVariablesIncludingModifiers(_function, _contract),
 			[&](auto _var) { return _context.variable(*_var)->currentValue(); }
 		);
 }

libsolidity/formal/PredicateSort.cpp

@@ -84,7 +84,7 @@ SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefini
 
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
 	return make_shared<FunctionSort>(
-		fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function), smtSort),
+		fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort),
 		SortProvider::boolSort
 	);
 }

libsolidity/formal/SMTEncoder.cpp

@@ -208,7 +208,11 @@ void SMTEncoder::visitFunctionOrModifier()
 		if (dynamic_cast<ContractDefinition const*>(refDecl))
 			visitFunctionOrModifier();
 		else if (auto modifierDef = dynamic_cast<ModifierDefinition const*>(refDecl))
-			inlineModifierInvocation(modifierInvocation.get(), modifierDef);
+		{
+			solAssert(*modifierInvocation->name().annotation().requiredLookup == VirtualLookup::Virtual, "");
+			ModifierDefinition const& modifier = modifierDef->resolveVirtual(*m_currentContract);
+			inlineModifierInvocation(modifierInvocation.get(), &modifier);
+		}
 		else
 			solAssert(false, "");
 	}
@@ -2162,7 +2166,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 
 	vector<VariableDeclaration const*> localVars;
 	if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function))
-		localVars = localVariablesIncludingModifiers(*fun);
+		localVars = localVariablesIncludingModifiers(*fun, m_currentContract);
 	else
 		localVars = _function.localVariables();
 	for (auto const& variable: localVars)
@@ -2205,7 +2209,7 @@ void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
 
 void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
 {
-	for (auto const& variable: localVariablesIncludingModifiers(_function))
+	for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
 		createVariable(*variable);
 
 	for (auto const& param: _function.parameters())
@@ -2218,7 +2222,7 @@ void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
 
 void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
 {
-	for (auto const& variable: localVariablesIncludingModifiers(_function))
+	for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
 	{
 		solAssert(m_context.knownVariable(*variable), "");
 		m_context.setZeroValue(*variable);
@@ -2481,7 +2485,7 @@ void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefin
 	{
 		for (auto const& var: _function->parameters() + _function->returnParameters())
 			m_context.variable(*var)->resetIndex();
-		for (auto const& var: localVariablesIncludingModifiers(*_function))
+		for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
 			m_context.variable(*var)->resetIndex();
 	}
 	m_context.state().reset();
@@ -2638,12 +2642,12 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
 	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
 }
 
-vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function)
+vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
 {
-	return _function.localVariables() + modifiersVariables(_function);
+	return _function.localVariables() + modifiersVariables(_function, _contract);
 }
 
-vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function)
+vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract)
 {
 	struct BlockVars: ASTConstVisitor
 	{
@@ -2664,10 +2668,12 @@ vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefini
 			continue;
 
 		visited.insert(modifier);
-		if (modifier->isImplemented())
+		solAssert(_contract, "No contract context provided for modifier analysis!");
+		auto const& actualModifier = modifier->resolveVirtual(*_contract);
+		if (actualModifier.isImplemented())
 		{
-			vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
+			vars += applyMap(actualModifier.parameters(), [](auto _var) { return _var.get(); });
-			vars += BlockVars(modifier->body()).vars;
+			vars += BlockVars(actualModifier.body()).vars;
 		}
 	}
 	return vars;

libsolidity/formal/SMTEncoder.h

@@ -74,8 +74,8 @@ public:
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
 
-	static std::vector<VariableDeclaration const*> localVariablesIncludingModifiers(FunctionDefinition const& _function);
+	static std::vector<VariableDeclaration const*> localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract);
-	static std::vector<VariableDeclaration const*> modifiersVariables(FunctionDefinition const& _function);
+	static std::vector<VariableDeclaration const*> modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract);
 
 	/// @returns the SourceUnit that contains _scopable.
 	static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);

test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	uint s;
+
+	function f() public mod(s) {}
+	modifier mod(uint x) virtual;
+}
+
+contract B is A {
+	modifier mod(uint x) override {
+		require(x == 42);
+		_;
+		assert(x == 42); // should hold
+		assert(x == 0); // should fail
+	}
+
+	function set(uint x) public {
+		s = x;
+	}
+}
+// ----
+// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\ns = 42\n\n\n\nTransaction trace:\nconstructor()\nState: s = 0\nset(42)\nState: s = 42\nf()

test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	bool s;
+
+	function f() public view mod {
+		assert(s); // holds for C, but fails for B
+	}
+	modifier mod() virtual;
+}
+
+contract B is A {
+	modifier mod() virtual override {
+		s = false;
+		_;
+	}
+}
+
+contract C is B {
+	modifier mod() override {
+		s = true;
+		_;
+	}
+}
+// ----
+// Warning 5740: (95-144): Unreachable code.
+// Warning 6328: (99-108): CHC: Assertion violation happens here.\nCounterexample:\ns = false\n\n\n\nTransaction trace:\nconstructor()\nState: s = false\nf()

test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	bool s;
+
+	function f() public view mod {
+		assert(s); // holds for B
+		assert(!s); // fails for B
+	}
+	modifier mod() virtual;
+}
+
+contract B is A {
+	modifier mod() virtual override {
+		bool x = true;
+		s = x;
+		_;
+	}
+}
+// ----
+// Warning 5740: (95-156): Unreachable code.
+// Warning 6328: (127-137): CHC: Assertion violation happens here.\nCounterexample:\ns = true\n\n\n\nTransaction trace:\nconstructor()\nState: s = false\nf()

test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol

@@ -0,0 +1,42 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	int x = 0;
+
+	function f() public view mod() {
+		assert(x != 0); // fails for A
+		assert(x != 1); // fails for B
+		assert(x != 2); // fails for C
+		assert(x != 3); // fails for D
+	}
+
+	modifier mod() virtual {
+		_;
+	}
+}
+
+contract B is A {
+	modifier mod() virtual override {
+		x = 1;
+		_;
+	}
+}
+
+contract C is A {
+	modifier mod() virtual override {
+		x = 2;
+		_;
+	}
+}
+
+contract D is B,C {
+	modifier mod() virtual override (B,C){
+		x = 3;
+		_;
+	}
+}
+// ----
+// Warning 6328: (104-118): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
+// Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
+// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
+// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()