Fix CHC false positives when using branches inside modifiers

Changelog.md

@@ -19,6 +19,7 @@ Bugfixes:
  * SMTChecker: Fix false negative in modifier applied multiple times.
  * SMTChecker: Fix internal error in the BMC engine when inherited contract from a different source unit has private state variables.
  * SMTChecker: Fix internal error when ``array.push()`` is used as the LHS of an assignment.
+ * SMTChecker: Fix CHC false positives when branches are used inside modifiers.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

libsolidity/formal/CHC.cpp

@@ -746,7 +746,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: _function->localVariables())
+		for (auto const& var: localVariablesIncludingModifiers(*_function))
 			m_context.variable(*var)->increaseIndex();
 	}
 
@@ -821,7 +821,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						createVariable(*var);
 					for (auto var: function->returnParameters())
 						createVariable(*var);
-					for (auto const* var: function->localVariables())
+					for (auto const* var: localVariablesIncludingModifiers(*function))
 						createVariable(*var);
 
 					m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));

libsolidity/formal/PredicateInstance.cpp

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

libsolidity/formal/PredicateSort.cpp

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

libsolidity/formal/SMTEncoder.cpp

@@ -1989,7 +1989,12 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 				m_arrayAssignmentHappened = true;
 		}
 
-	for (auto const& variable: _function.localVariables())
+	vector<VariableDeclaration const*> localVars;
+	if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function))
+		localVars = localVariablesIncludingModifiers(*fun);
+	else
+		localVars = _function.localVariables();
+	for (auto const& variable: localVars)
 		if (createVariable(*variable))
 		{
 			m_context.newValue(*variable);
@@ -2029,7 +2034,7 @@ void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
 
 void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
 {
-	for (auto const& variable: _function.localVariables())
+	for (auto const& variable: localVariablesIncludingModifiers(_function))
 		createVariable(*variable);
 
 	for (auto const& param: _function.parameters())
@@ -2042,7 +2047,7 @@ void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
 
 void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
 {
-	for (auto const& variable: _function.localVariables())
+	for (auto const& variable: localVariablesIncludingModifiers(_function))
 	{
 		solAssert(m_context.knownVariable(*variable), "");
 		m_context.setZeroValue(*variable);
@@ -2297,7 +2302,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: _function->localVariables())
+		for (auto const& var: localVariablesIncludingModifiers(*_function))
 			m_context.variable(*var)->resetIndex();
 	}
 	m_context.state().reset();
@@ -2432,6 +2437,38 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
 	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
 }
 
+vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function)
+{
+	return _function.localVariables() + modifiersVariables(_function);
+}
+
+vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function)
+{
+	struct BlockVars: ASTConstVisitor
+	{
+		BlockVars(Block const& _block) { _block.accept(*this); }
+		void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); }
+		vector<VariableDeclaration const*> vars;
+	};
+
+	vector<VariableDeclaration const*> vars;
+	set<ModifierDefinition const*> visited;
+	for (auto invok: _function.modifiers())
+	{
+		if (!invok)
+			continue;
+		auto decl = invok->name()->annotation().referencedDeclaration;
+		auto const* modifier = dynamic_cast<ModifierDefinition const*>(decl);
+		if (!modifier || visited.count(modifier))
+			continue;
+
+		visited.insert(modifier);
+		vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
+		vars += BlockVars(modifier->body()).vars;
+	}
+	return vars;
+}
+
 SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
 {
 	for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))

libsolidity/formal/SMTEncoder.h

@@ -71,6 +71,9 @@ 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*> modifiersVariables(FunctionDefinition const& _function);
+
 	/// @returns the SourceUnit that contains _scopable.
 	static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);
 

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract C {
+    uint x;
+    modifier m(uint z) {
+		uint y = 3;
+        if (z == 10)
+            x = 2 + y;
+        _;
+        if (z == 10)
+            x = 4 + y;
+    }
+    function f() m(10) internal {
+        x = 3;
+    }
+    function g() public {
+        x = 0;
+        f();
+        assert(x == 7);
+        // Fails
+        assert(x == 6);
+    }
+}
+// ----
+// Warning 6328: (359-373): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract C {
+    uint x;
+    modifier m(uint z) {
+		uint y = 3;
+        if (z == 10)
+            x = 2 + y;
+        _;
+        if (z == 10)
+            x = 4 + y;
+    }
+    function f() m(10) m(12) internal {
+        x = 3;
+    }
+    function g() public {
+        x = 0;
+        f();
+        assert(x == 3);
+        // Fails
+        assert(x == 6);
+    }
+}
+// ----
+// Warning 6328: (365-379): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract C {
+    uint x;
+    modifier m(uint z) {
+		uint y = 3;
+        if (z == 10)
+            x = 2 + y;
+        _;
+        if (z == 10)
+            x = 4 + y;
+    }
+    function f() m(8) internal {
+        x = 3;
+    }
+    function g() public {
+        x = 0;
+        f();
+        assert(x == 3);
+        // Fails
+        assert(x == 6);
+    }
+}
+// ----
+// Warning 6328: (358-372): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract C {
+    uint x;
+    modifier m(uint z) {
+		uint y = 3;
+        if (z >= 10)
+            x = 2 + y;
+        _;
+        if (z >= 10)
+            x = 4 + y;
+    }
+    function f() m(10) m(12) internal {
+        x = 3;
+    }
+    function g() public {
+        x = 0;
+        f();
+        assert(x == 7);
+        // Fails
+        assert(x == 6);
+    }
+}
+// ----
+// Warning 6328: (365-379): CHC: Assertion violation happens here.