Merge pull request #11126 from blishko/smt-no-targets-for-abstract

[SMTChecker] Do not create verification targets for contracts that cannot be deployed.

Changelog.md

@@ -10,6 +10,7 @@ Compiler Features:
 Bugfixes:
  * AST Output: Fix ``kind`` field of ``ModifierInvocation`` for base constructor calls.
  * SMTChecker: Fix false positive and false negative on ``push`` as LHS of a compound assignment.
+ * SMTChecker: Fix false positive in contracts that cannot be deployed.
  * SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available.
 
 

libsolidity/formal/BMC.cpp

@@ -841,7 +841,7 @@ void BMC::addVerificationTarget(
 	Expression const* _expression
 )
 {
-	if (!m_settings.targets.has(_type))
+	if (!m_settings.targets.has(_type) || (m_currentContract && !m_currentContract->canBeDeployed()))
 		return;
 
 	BMCVerificationTarget target{

libsolidity/formal/CHC.cpp

@@ -197,13 +197,17 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	connectBlocks(m_currentBlock, summary(_contract));
 
 	setCurrentBlock(*m_constructorSummaries.at(&_contract));
+
+	solAssert(&_contract == m_currentContract, "");
+	if (_contract.canBeDeployed())
+	{
 		auto constructor = _contract.constructor();
 		auto txConstraints = state().txTypeConstraints();
 		if (!constructor || !constructor->isPayable())
 			txConstraints = txConstraints && state().txNonPayableConstraint();
 		m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
 		connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
-
+	}
 	SMTEncoder::endVisit(_contract);
 }
 
@@ -262,7 +266,8 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (
 		!_function.isConstructor() &&
 		_function.isPublic() &&
-		contractFunctions(*m_currentContract).count(&_function)
+		contractFunctions(*m_currentContract).count(&_function) &&
+		m_currentContract->canBeDeployed()
 	)
 	{
 		auto sum = summary(_function);

test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol

@@ -29,7 +29,6 @@ contract A is B2, B1 {
 // ====
 // SMTIgnoreCex: yes
 // ----
-// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (334-350): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol

@@ -15,4 +15,4 @@ contract C is  A {
 	}
 }
 // ----
-// Warning 6328: (94-108): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
+// Warning 6328: (94-108): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol

@@ -23,6 +23,6 @@ contract A is B {
 // ====
 // SMTIgnoreCex: yes
 // ----
-// Warning 4984: (157-162): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (275-293): CHC: Assertion violation happens here.
+// Warning 4984: (157-162): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (216-221): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol

@@ -23,6 +23,6 @@ contract A is B {
 // ====
 // SMTIgnoreCex: yes
 // ----
-// Warning 4984: (157-163): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 6328: (273-291): CHC: Assertion violation happens here.
+// Warning 4984: (157-163): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4984: (217-222): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol

@@ -4,7 +4,7 @@ abstract contract A {
 	int x = 0;
 
 	function f() public view mod() {
-		assert(x != 0); // fails for A
+		assert(x != 0); // does not hold for A, but A is abstract so it should not be reported
 		assert(x != 1); // fails for B
 		assert(x != 2); // fails for C
 		assert(x != 3); // fails for D
@@ -36,7 +36,6 @@ contract D is B,C {
 	}
 }
 // ----
-// Warning 6328: (104-118): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
+// Warning 6328: (193-207): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nB.constructor()\nState: x = 0\nA.f()
-// Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nB.constructor()\nState: x = 0\nA.f()
+// Warning 6328: (226-240): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()
-// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()
+// Warning 6328: (259-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.f()
-// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.f()

test/libsolidity/smtCheckerTests/verification_target/no_target_for_abstract_constract.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	function f() public pure {
+		assert(false); // A cannot be deployed so this should not be reported
+	}
+}

test/libsolidity/smtCheckerTests/verification_target/no_target_for_constructor_of_abstract_constract.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	constructor() {
+		assert(false); // A cannot be deployed, so this should not be reported
+	}
+}