Fix bug in virtual functions called by constructor.

Changelog.md

@@ -16,9 +16,11 @@ Bugfixes:
  * SMTChecker: Fix internal error on array slices.
  * SMTChecker: Fix internal error on calling public getter on a state variable of type array (possibly nested) of structs.
  * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
+ * SMTChecker: Fix bug in virtual functions called by constructors.
 
 AST Changes:
 
+
 ### 0.8.2 (2021-03-02)
 
 Compiler Features:

libsolidity/formal/CHC.cpp

@@ -139,10 +139,12 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 void CHC::endVisit(ContractDefinition const& _contract)
 {
-	if (auto constructor = _contract.constructor())
+	for (auto base: _contract.annotation().linearizedBaseContracts)
-		constructor->accept(*this);
+	{
-
+		if (auto constructor = base->constructor())
-	defineContractInitializer(_contract);
+			constructor->accept(*this);
+		defineContractInitializer(*base, _contract);
+	}
 
 	auto const& entry = *createConstructorBlock(_contract, "implicit_constructor_entry");
 
@@ -161,7 +163,6 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	// We need to evaluate the base constructor calls (arguments) from derived -> base
 	auto baseArgs = baseArguments(_contract);
 	for (auto base: _contract.annotation().linearizedBaseContracts)
-	{
 		if (base != &_contract)
 		{
 			m_callGraph[&_contract].insert(base);
@@ -183,13 +184,12 @@ void CHC::endVisit(ContractDefinition const& _contract)
 				}
 			}
 		}
-	}
 	m_errorDest = nullptr;
 	// Then call initializer_Base from base -> derived
 	for (auto base: _contract.annotation().linearizedBaseContracts | boost::adaptors::reversed)
 	{
 		errorFlag().increaseIndex();
-		m_context.addAssertion(smt::constructorCall(*m_contractInitializers.at(base), m_context));
+		m_context.addAssertion(smt::constructorCall(*m_contractInitializers.at(&_contract).at(base), m_context));
 		connectBlocks(m_currentBlock, summary(_contract), errorFlag().currentValue() > 0);
 		m_context.addAssertion(errorFlag().currentValue() == 0);
 	}
@@ -953,7 +953,6 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + uniquePrefix() + "_" + suffix, PredicateType::Interface, contract);
 			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract);
 			m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor");
-			m_contractInitializers[contract] = createConstructorBlock(*contract, "contract_initializer");
 
 			for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
 				if (!m_context.knownVariable(*var))
@@ -1001,23 +1000,24 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		}
 }
 
-void CHC::defineContractInitializer(ContractDefinition const& _contract)
+void CHC::defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contextContract)
 {
+	m_contractInitializers[&_contextContract][&_contract] = createConstructorBlock(_contract, "contract_initializer");
 	auto const& implicitConstructorPredicate = *createConstructorBlock(_contract, "contract_initializer_entry");
 
 	auto implicitFact = smt::constructor(implicitConstructorPredicate, m_context);
 	addRule(smtutil::Expression::implies(initialConstraints(_contract), implicitFact), implicitFact.name);
 	setCurrentBlock(implicitConstructorPredicate);
 
-	solAssert(!m_errorDest, "");
+	auto prevErrorDest = m_errorDest;
-	m_errorDest = m_contractInitializers.at(&_contract);
+	m_errorDest = m_contractInitializers.at(&_contextContract).at(&_contract);
 	for (auto var: _contract.stateVariables())
 		if (var->value())
 		{
 			var->value()->accept(*this);
 			assignment(*var, *var->value());
 		}
-	m_errorDest = nullptr;
+	m_errorDest = prevErrorDest;
 
 	auto const& afterInit = *createConstructorBlock(_contract, "contract_initializer_after_init");
 	connectBlocks(m_currentBlock, predicate(afterInit));
@@ -1026,12 +1026,12 @@ void CHC::defineContractInitializer(ContractDefinition const& _contract)
 	if (auto constructor = _contract.constructor())
 	{
 		errorFlag().increaseIndex();
-		m_context.addAssertion(smt::functionCall(*m_summaries.at(&_contract).at(constructor), &_contract, m_context));
+		m_context.addAssertion(smt::functionCall(*m_summaries.at(&_contextContract).at(constructor), &_contextContract, m_context));
-		connectBlocks(m_currentBlock, initializer(_contract), errorFlag().currentValue() > 0);
+		connectBlocks(m_currentBlock, initializer(_contract, _contextContract), errorFlag().currentValue() > 0);
 		m_context.addAssertion(errorFlag().currentValue() == 0);
 	}
 
-	connectBlocks(m_currentBlock, initializer(_contract));
+	connectBlocks(m_currentBlock, initializer(_contract, _contextContract));
 }
 
 smtutil::Expression CHC::interface()
@@ -1055,9 +1055,9 @@ smtutil::Expression CHC::error(unsigned _idx)
 	return m_errorPredicate->functor(_idx)({});
 }
 
-smtutil::Expression CHC::initializer(ContractDefinition const& _contract)
+smtutil::Expression CHC::initializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext)
 {
-	return predicate(*m_contractInitializers.at(&_contract));
+	return predicate(*m_contractInitializers.at(&_contractContext).at(&_contract));
 }
 
 smtutil::Expression CHC::summary(ContractDefinition const& _contract)

libsolidity/formal/CHC.h

@@ -135,7 +135,7 @@ private:
 	/// Creates a CHC system that, for a given contract,
 	/// - initializes its state variables (as 0 or given value, if any).
 	/// - "calls" the explicit constructor function of the contract, if any.
-	void defineContractInitializer(ContractDefinition const& _contract);
+	void defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext);
 
 	/// Interface predicate over current variables.
 	smtutil::Expression interface();
@@ -183,8 +183,8 @@ private:
 	smtutil::Expression predicate(Predicate const& _block);
 	/// @returns the summary predicate for the called function.
 	smtutil::Expression predicate(FunctionCall const& _funCall);
-	/// @returns a predicate that defines a contract initializer.
+	/// @returns a predicate that defines a contract initializer for _contract in the context of _contractContext.
-	smtutil::Expression initializer(ContractDefinition const& _contract);
+	smtutil::Expression initializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext);
 	/// @returns a predicate that defines a constructor summary.
 	smtutil::Expression summary(ContractDefinition const& _contract);
 	/// @returns a predicate that defines a function summary.
@@ -274,7 +274,7 @@ private:
 	std::map<ContractDefinition const*, Predicate const*> m_nondetInterfaces;
 
 	std::map<ContractDefinition const*, Predicate const*> m_constructorSummaries;
-	std::map<ContractDefinition const*, Predicate const*> m_contractInitializers;
+	std::map<ContractDefinition const*, std::map<ContractDefinition const*, Predicate const*>> m_contractInitializers;
 
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.

libsolidity/formal/SMTEncoder.cpp

@@ -2904,8 +2904,7 @@ set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contract
 		auto allFunctions = contractFunctions(_contract);
 		for (auto const* base: _contract.annotation().linearizedBaseContracts)
 			for (auto const* baseFun: base->definedFunctions())
-				if (!baseFun->isConstructor())
+				allFunctions.insert(baseFun);
-					allFunctions.insert(baseFun);
 
 		m_contractFunctionsWithoutVirtual.emplace(&_contract, move(allFunctions));
 

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol

@@ -25,4 +25,4 @@ contract D is C {
 	}
 }
 // ----
-// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\na = 0\n\nTransaction trace:\nD.constructor(0)
+// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 1\n\nTransaction trace:\nD.constructor(1)

test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol

@@ -10,5 +10,7 @@ contract C {
 		assert(h == k);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n    C.fi(data, 39) -- internal call
+// Warning 6328: (229-243): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -29,4 +29,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()\n    s.f() -- untrusted external call
+// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()\n    s.f() -- untrusted external call, synthesized as:\n        C.f() -- reentrant call\n            s.f() -- untrusted external call

test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(9)
+// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(11)

test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+contract A {
+    uint public x;
+    function v() internal virtual {
+        x = 2;
+    }
+    constructor() {
+        v();
+    }
+	function i() public view virtual {
+		assert(x == 2); // should hold
+		assert(x == 10); // should fail
+	}
+}
+
+contract C is A {
+    function v() internal override {
+        x = 10;
+    }
+	function i() public view override {
+		assert(x == 10); // should hold
+		assert(x == 2); // should fail
+	}
+}
+// ----
+// Warning 6328: (231-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i()
+// Warning 6328: (419-433): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i()

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol

@@ -25,5 +25,5 @@ contract D is B, C {
 	}
 }
 // ----
-// Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()
 // Warning 6328: (256-270): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()
+// Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -12,5 +12,3 @@ contract C
 	}
 }
 // ----
-// Warning 4984: (139-144): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 2661: (139-144): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol

@@ -30,4 +30,4 @@ contract C
 }
 // ----
 // Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f(0, 9, false, true)
-// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(9, 0, true, false)
+// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 20\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)

test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol

@@ -7,4 +7,4 @@ contract C  {
 }
 // ----
 // Warning 4281: (110-115): CHC: Division by zero happens here.\nCounterexample:\n\nx = 0\ny = 0\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
-// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
+// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))

test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol

@@ -14,6 +14,6 @@ contract C {
 // Warning 2072: (184-188): Unused local variable.
 // Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
-// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\n\nTransaction trace:\nC.constructor()\nC.f([13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
+// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]\n\nTransaction trace:\nC.constructor()\nC.f([10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10])
 // Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)

test/libsolidity/smtCheckerTests/special/difficulty.sol

@@ -7,4 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 38\n\nTransaction trace:\nC.constructor()\nC.f(38)
+// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 39\n\nTransaction trace:\nC.constructor()\nC.f(39)

test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol

@@ -14,5 +14,5 @@ contract C is A {
 	}
 }
 // ----
-// Warning 6328: (93-107): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
 // Warning 6328: (273-287): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
+// Warning 6328: (93-107): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }

test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol

@@ -7,4 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\na = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1)
+// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 1\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0)

test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol

@@ -12,4 +12,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\nTransaction trace:\nc.constructor()\nc.g(38, 21239)\n    c.f(map, 38, 21239) -- internal call
+// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21238\n\nTransaction trace:\nc.constructor()\nc.g(38, 21238)\n    c.f(map, 38, 21238) -- internal call

test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol

@@ -9,4 +9,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1)
+// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0)