[SMTChecker] Add support to constructors

libsolidity/formal/BMC.cpp

@@ -110,11 +110,6 @@ bool BMC::visit(ContractDefinition const& _contract)
 {
 	initContract(_contract);
 
-	/// Check targets created by state variable initialization.
-	smt::Expression constraints = m_context.assertions();
-	checkVerificationTargets(constraints);
-	m_verificationTargets.clear();
-
 	SMTEncoder::visit(_contract);
 
 	return false;
@@ -122,6 +117,17 @@ bool BMC::visit(ContractDefinition const& _contract)
 
 void BMC::endVisit(ContractDefinition const& _contract)
 {
+	if (auto constructor = _contract.constructor())
+		constructor->accept(*this);
+	else
+	{
+		inlineConstructorHierarchy(_contract);
+		/// Check targets created by state variable initialization.
+		smt::Expression constraints = m_context.assertions();
+		checkVerificationTargets(constraints);
+		m_verificationTargets.clear();
+	}
+
 	SMTEncoder::endVisit(_contract);
 }
 
@@ -132,10 +138,14 @@ bool BMC::visit(FunctionDefinition const& _function)
 	solAssert(m_currentContract, "");
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
 	if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end())
-		initializeStateVariables(*contract);
+		createStateVariables(*contract);
 
 	if (m_callStack.empty())
+	{
 		reset();
+		initFunction(_function);
+		resetStateVariables();
+	}
 
 	/// Already visits the children.
 	SMTEncoder::visit(_function);
@@ -447,10 +457,6 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
 		// is that there we don't have `_funCall`.
 		pushCallStack({funDef, &_funCall});
-		// If an internal function is called to initialize
-		// a state variable.
-		if (m_callStack.empty())
-			initFunction(*funDef);
 		funDef->accept(*this);
 	}
 

libsolidity/formal/CHC.cpp

@@ -65,6 +65,15 @@ void CHC::analyze(SourceUnit const& _source)
 	m_context.setAssertionAccumulation(false);
 	m_variableUsage.setFunctionInlining(false);
 
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	auto genesisSort = make_shared<smt::FunctionSort>(
+		vector<smt::SortPointer>(),
+		boolSort
+	);
+	m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
+	auto genesis = (*m_genesisPredicate)({});
+	addRule(genesis, genesis.name);
+
 	_source.accept(*this);
 }
 
@@ -94,10 +103,10 @@ bool CHC::visit(ContractDefinition const& _contract)
 		else
 			m_stateSorts.push_back(smt::smtSort(*var->type()));
 
-	clearIndices();
+	clearIndices(&_contract);
 
-	string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id());
-	m_interfacePredicate = createSymbolicBlock(interfaceSort(), interfaceName);
+	string suffix = _contract.name() + "_" + to_string(_contract.id());
+	m_interfacePredicate = createSymbolicBlock(interfaceSort(), "interface_" + suffix);
 
 	// TODO create static instances for Bool/Int sorts in SolverInterface.
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
@@ -105,27 +114,11 @@ bool CHC::visit(ContractDefinition const& _contract)
 		vector<smt::SortPointer>(),
 		boolSort
 	);
-	m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error");
 
-	// If the contract has a constructor it is handled as a function.
-	// Otherwise we zero-initialize all state vars.
-	if (!_contract.constructor())
-	{
-		string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id());
-		m_constructorPredicate = createSymbolicBlock(constructorSort(), constructorName);
-		smt::Expression constructorPred = (*m_constructorPredicate)({});
-		addRule(constructorPred, constructorName);
-
-		for (auto const& var: m_stateVariables)
-		{
-			auto const& symbVar = m_context.variable(*var);
-			symbVar->increaseIndex();
-			m_interface->declareVariable(symbVar->currentName(), symbVar->sort());
-			m_context.setZeroValue(*symbVar);
-		}
-
-		connectBlocks(constructorPred, interface());
-	}
+	m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix);
+	m_constructorPredicate = createSymbolicBlock(constructorSort(), "implicit_constructor_" + to_string(_contract.id()));
+	auto stateExprs = currentStateVariables();
+	setCurrentBlock(*m_interfacePredicate, &stateExprs);
 
 	SMTEncoder::visit(_contract);
 	return false;
@@ -136,6 +129,23 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	if (!shouldVisit(_contract))
 		return;
 
+	for (auto const& var: m_stateVariables)
+	{
+		solAssert(m_context.knownVariable(*var), "");
+		m_context.setZeroValue(*var);
+	}
+	auto genesisPred = (*m_genesisPredicate)({});
+	auto implicitConstructor = (*m_constructorPredicate)(currentStateVariables());
+	connectBlocks(genesisPred, implicitConstructor);
+	m_currentBlock = implicitConstructor;
+
+	if (auto constructor = _contract.constructor())
+		constructor->accept(*this);
+	else
+		inlineConstructorHierarchy(_contract);
+
+	connectBlocks(m_currentBlock, interface());
+
 	for (unsigned i = 0; i < m_verificationTargets.size(); ++i)
 	{
 		auto const& target = m_verificationTargets.at(i);
@@ -152,6 +162,16 @@ bool CHC::visit(FunctionDefinition const& _function)
 	if (!shouldVisit(_function))
 		return false;
 
+	// This is the case for base constructor inlining.
+	if (m_currentFunction)
+	{
+		solAssert(m_currentFunction->isConstructor(), "");
+		solAssert(_function.isConstructor(), "");
+		solAssert(_function.scope() != m_currentContract, "");
+		SMTEncoder::visit(_function);
+		return false;
+	}
+
 	solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
 	m_currentFunction = &_function;
 
@@ -163,20 +183,11 @@ bool CHC::visit(FunctionDefinition const& _function)
 	auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
 	auto bodyPred = predicate(*bodyBlock);
 
-	// Store the constraints related to variable initialization.
-	smt::Expression const& initAssertions = m_context.assertions();
-	m_context.pushSolver();
-
-	connectBlocks(interface(), functionPred);
+	connectBlocks(m_currentBlock, functionPred);
 	connectBlocks(functionPred, bodyPred);
 
-	m_context.popSolver();
-
 	setCurrentBlock(*bodyBlock);
 
-	// We need to re-add the constraints that were created for initialization of variables.
-	m_context.addAssertion(initAssertions);
-
 	SMTEncoder::visit(*m_currentFunction);
 
 	return false;
@@ -187,10 +198,37 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (!shouldVisit(_function))
 		return;
 
-	connectBlocks(m_currentBlock, interface());
+	// This is the case for base constructor inlining.
+	if (m_currentFunction != &_function)
+	{
+		solAssert(m_currentFunction && m_currentFunction->isConstructor(), "");
+		solAssert(_function.isConstructor(), "");
+		solAssert(_function.scope() != m_currentContract, "");
+	}
+	else
+	{
+		// We create an extra exit block for constructors that simply
+		// connects to the interface in case an explicit constructor
+		// exists in the hierarchy.
+		// It is not connected directly here, as normal functions are,
+		// because of the case where there are only implicit constructors.
+		// This is done in endVisit(ContractDefinition).
+		if (_function.isConstructor())
+		{
+			auto constructorExit = createBlock(&_function, "exit_");
+			connectBlocks(m_currentBlock, predicate(*constructorExit));
+			setCurrentBlock(*constructorExit);
+		}
+		else
+		{
+			connectBlocks(m_currentBlock, interface());
+			clearIndices(m_currentContract, m_currentFunction);
+			auto stateExprs = currentStateVariables();
+			setCurrentBlock(*m_interfacePredicate, &stateExprs);
+		}
+		m_currentFunction = nullptr;
+	}
 
-	solAssert(&_function == m_currentFunction, "");
-	m_currentFunction = nullptr;
 	SMTEncoder::endVisit(_function);
 }
 
@@ -445,7 +483,6 @@ void CHC::reset()
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
 	m_unknownFunctionCallSeen = false;
-	m_blockCounter = 0;
 	m_breakDest = nullptr;
 	m_continueDest = nullptr;
 }
@@ -470,28 +507,31 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 {
 	if (
 		_function.isPublic() &&
-		_function.isImplemented() &&
-		!_function.isConstructor()
+		_function.isImplemented()
 	)
 		return true;
 	return false;
 }
 
-void CHC::setCurrentBlock(smt::SymbolicFunctionVariable const& _block)
+void CHC::setCurrentBlock(
+	smt::SymbolicFunctionVariable const& _block,
+	vector<smt::Expression> const* _arguments
+)
 {
 	m_context.popSolver();
-	clearIndices();
+	solAssert(m_currentContract, "");
+	clearIndices(m_currentContract, m_currentFunction);
 	m_context.pushSolver();
-	m_currentBlock = predicate(_block);
+	if (_arguments)
+		m_currentBlock = predicate(_block, *_arguments);
+	else
+		m_currentBlock = predicate(_block);
 }
 
 smt::SortPointer CHC::constructorSort()
 {
-	solAssert(m_currentContract, "");
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	if (!m_currentContract->constructor())
-		return make_shared<smt::FunctionSort>(vector<smt::SortPointer>{}, boolSort);
-	return sort(*m_currentContract->constructor());
+	// TODO this will change once we support function calls.
+	return interfaceSort();
 }
 
 smt::SortPointer CHC::interfaceSort()
@@ -556,19 +596,6 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPoin
 	return block;
 }
 
-smt::Expression CHC::constructor()
-{
-	solAssert(m_currentContract, "");
-
-	if (!m_currentContract->constructor())
-		return (*m_constructorPredicate)({});
-
-	vector<smt::Expression> paramExprs;
-	for (auto const& var: m_currentContract->constructor()->parameters())
-		paramExprs.push_back(m_context.variable(*var)->currentValue());
-	return (*m_constructorPredicate)(paramExprs);
-}
-
 smt::Expression CHC::interface()
 {
 	vector<smt::Expression> paramExprs;
@@ -613,37 +640,31 @@ void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to
 	addRule(edge, _from.name + "_to_" + _to.name);
 }
 
+vector<smt::Expression> CHC::currentStateVariables()
+{
+	solAssert(m_currentContract, "");
+	vector<smt::Expression> exprs;
+	for (auto const& var: m_stateVariables)
+		exprs.push_back(m_context.variable(*var)->currentValue());
+	return exprs;
+}
+
 vector<smt::Expression> CHC::currentFunctionVariables()
 {
-	solAssert(m_currentFunction, "");
 	vector<smt::Expression> paramExprs;
-	for (auto const& var: m_stateVariables)
-		paramExprs.push_back(m_context.variable(*var)->currentValue());
-	for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
-		paramExprs.push_back(m_context.variable(*var)->currentValue());
-	return paramExprs;
+	if (m_currentFunction)
+		for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
+			paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return currentStateVariables() + paramExprs;
 }
 
 vector<smt::Expression> CHC::currentBlockVariables()
 {
-	solAssert(m_currentFunction, "");
 	vector<smt::Expression> paramExprs;
-	for (auto const& var: m_currentFunction->localVariables())
-		paramExprs.push_back(m_context.variable(*var)->currentValue());
-	return currentFunctionVariables() + paramExprs;
-}
-
-void CHC::clearIndices()
-{
-	for (auto const& var: m_stateVariables)
-		m_context.variable(*var)->resetIndex();
 	if (m_currentFunction)
-	{
-		for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
-			m_context.variable(*var)->resetIndex();
 		for (auto const& var: m_currentFunction->localVariables())
-			m_context.variable(*var)->resetIndex();
-	}
+			paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return currentFunctionVariables() + paramExprs;
 }
 
 string CHC::predicateName(ASTNode const* _node)
@@ -674,7 +695,6 @@ smt::Expression CHC::predicate(
 	return _block(_arguments);
 }
 
-
 void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 {
 	m_interface->addRule(_rule, _ruleName);

libsolidity/formal/CHC.h

@@ -83,7 +83,7 @@ private:
 	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
-	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block);
+	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
 	//@}
 
 	/// Sort helpers.
@@ -99,8 +99,6 @@ private:
 	/// @returns a new block of given _sort and _name.
 	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
 
-	/// Constructor predicate over current variables.
-	smt::Expression constructor();
 	/// Interface predicate over current variables.
 	smt::Expression interface();
 	/// Error predicate over current variables.
@@ -116,17 +114,16 @@ private:
 
 	void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
 
+	/// @returns the current symbolic values of the current state variables.
+	std::vector<smt::Expression> currentStateVariables();
+
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
 	std::vector<smt::Expression> currentFunctionVariables();
-	/// @returns the samve as currentFunctionVariables plus
+	/// @returns the same as currentFunctionVariables plus
 	/// local variables.
 	std::vector<smt::Expression> currentBlockVariables();
 
-	/// Sets the SSA indices of the variables in scope to 0.
-	/// Used when starting a new block.
-	void clearIndices();
-
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node);
 	/// @returns a predicate application over the current scoped variables.
@@ -152,8 +149,11 @@ private:
 
 	/// Predicates.
 	//@{
-	/// Constructor predicate.
-	/// Default constructor sets state vars to 0.
+	/// Genesis predicate.
+	std::unique_ptr<smt::SymbolicFunctionVariable> m_genesisPredicate;
+
+	/// Implicit constructor predicate.
+	/// Explicit constructors are handled as functions.
 	std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorPredicate;
 
 	/// Artificial Interface predicate.

libsolidity/formal/SMTEncoder.cpp

@@ -22,6 +22,7 @@
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <boost/range/adaptors.hpp>
+#include <boost/range/adaptor/reversed.hpp>
 
 using namespace std;
 using namespace dev;
@@ -39,11 +40,28 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 	solAssert(m_currentContract, "");
 
 	for (auto const& node: _contract.subNodes())
-		if (!dynamic_pointer_cast<FunctionDefinition>(node))
+		if (
+			!dynamic_pointer_cast<FunctionDefinition>(node) &&
+			!dynamic_pointer_cast<VariableDeclaration>(node)
+		)
 			node->accept(*this);
 
 	vector<FunctionDefinition const*> resolvedFunctions = _contract.definedFunctions();
 	for (auto const& base: _contract.annotation().linearizedBaseContracts)
+	{
+		// Look for all the constructor invocations bottom up.
+		if (auto const& constructor =  base->constructor())
+			for (auto const& invocation: constructor->modifiers())
+			{
+				auto refDecl = invocation->name()->annotation().referencedDeclaration;
+				if (auto const& baseContract = dynamic_cast<ContractDefinition const*>(refDecl))
+				{
+					solAssert(!m_baseConstructorCalls.count(baseContract), "");
+					m_baseConstructorCalls[baseContract] = invocation.get();
+				}
+			}
+
+		// Check for function overrides.
 		for (auto const& baseFunction: base->definedFunctions())
 		{
 			if (baseFunction->isConstructor())
@@ -62,9 +80,18 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 			if (!overridden)
 				resolvedFunctions.push_back(baseFunction);
 		}
+	}
 
+	// Functions are visited first since they might be used
+	// for state variable initialization which is part of
+	// the constructor.
+	// Constructors are visited as part of the constructor
+	// hierarchy inlining.
 	for (auto const& function: resolvedFunctions)
-		function->accept(*this);
+		if (!function->isConstructor())
+			function->accept(*this);
+
+	// Constructors need to be handled by the engines separately.
 
 	return false;
 }
@@ -73,13 +100,16 @@ void SMTEncoder::endVisit(ContractDefinition const& _contract)
 {
 	m_context.resetAllVariables();
 
+	m_baseConstructorCalls.clear();
+
 	solAssert(m_currentContract == &_contract, "");
 	m_currentContract = nullptr;
 }
 
 void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
 {
-	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
+	// State variables are handled by the constructor.
+	if (_varDecl.isLocalVariable() &&_varDecl.value())
 		assignment(_varDecl, *_varDecl.value());
 }
 
@@ -90,25 +120,22 @@ bool SMTEncoder::visit(ModifierDefinition const&)
 
 bool SMTEncoder::visit(FunctionDefinition const& _function)
 {
-	// Not visited by a function call
-	if (m_callStack.empty())
-		initFunction(_function);
-
 	m_modifierDepthStack.push_back(-1);
+
 	if (_function.isConstructor())
-	{
-		m_errorReporter.warning(
-			_function.location(),
-			"Assertion checker does not yet support constructors."
-		);
-	}
-	else
-	{
-		_function.parameterList().accept(*this);
-		if (_function.returnParameterList())
-			_function.returnParameterList()->accept(*this);
-		visitFunctionOrModifier();
-	}
+		inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
+
+	// Base constructors' parameters should be set by explicit calls,
+	// but the most derived one needs to be initialized.
+	if (_function.scope() == m_currentContract)
+		initializeLocalVariables(_function);
+
+	_function.parameterList().accept(*this);
+	if (_function.returnParameterList())
+		_function.returnParameterList()->accept(*this);
+
+	visitFunctionOrModifier();
+
 	return false;
 }
 
@@ -130,27 +157,87 @@ void SMTEncoder::visitFunctionOrModifier()
 		solAssert(m_modifierDepthStack.back() < int(function.modifiers().size()), "");
 		ASTPointer<ModifierInvocation> const& modifierInvocation = function.modifiers()[m_modifierDepthStack.back()];
 		solAssert(modifierInvocation, "");
-		modifierInvocation->accept(*this);
-		auto const& modifierDef = dynamic_cast<ModifierDefinition const&>(
-			*modifierInvocation->name()->annotation().referencedDeclaration
-		);
-		vector<smt::Expression> modifierArgsExpr;
-		if (auto const* arguments = modifierInvocation->arguments())
-		{
-			auto const& modifierParams = modifierDef.parameters();
-			solAssert(modifierParams.size() == arguments->size(), "");
-			for (unsigned i = 0; i < arguments->size(); ++i)
-				modifierArgsExpr.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
-		}
-		initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
-		pushCallStack({&modifierDef, modifierInvocation.get()});
-		modifierDef.body().accept(*this);
-		popCallStack();
+		auto refDecl = modifierInvocation->name()->annotation().referencedDeclaration;
+		if (dynamic_cast<ContractDefinition const*>(refDecl))
+			visitFunctionOrModifier();
+		else if (auto modifierDef = dynamic_cast<ModifierDefinition const*>(refDecl))
+			inlineModifierInvocation(modifierInvocation.get(), modifierDef);
+		else
+			solAssert(false, "");
 	}
 
 	--m_modifierDepthStack.back();
 }
 
+void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition)
+{
+	solAssert(_invocation, "");
+	_invocation->accept(*this);
+
+	vector<smt::Expression> args;
+	if (auto const* arguments = _invocation->arguments())
+	{
+		auto const& modifierParams = _definition->parameters();
+		solAssert(modifierParams.size() == arguments->size(), "");
+		for (unsigned i = 0; i < arguments->size(); ++i)
+			args.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
+	}
+
+	initializeFunctionCallParameters(*_definition, args);
+
+	pushCallStack({_definition, _invocation});
+	if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
+	{
+		modifier->body().accept(*this);
+		popCallStack();
+	}
+	else if (auto function = dynamic_cast<FunctionDefinition const*>(_definition))
+	{
+		if (function->isImplemented())
+			function->accept(*this);
+		// Functions are popped from the callstack in endVisit(FunctionDefinition)
+	}
+}
+
+void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
+{
+	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
+	auto it = find(begin(hierarchy), end(hierarchy), &_contract);
+	solAssert(it != end(hierarchy), "");
+
+	auto nextBase = it + 1;
+	// Initialize the base contracts here as long as their constructors are implicit,
+	// stop when the first explicit constructor is found.
+	while (nextBase != end(hierarchy))
+	{
+		if (auto baseConstructor = (*nextBase)->constructor())
+		{
+			createLocalVariables(*baseConstructor);
+			// If any subcontract explicitly called baseConstructor, use those arguments.
+			if (m_baseConstructorCalls.count(*nextBase))
+				inlineModifierInvocation(m_baseConstructorCalls.at(*nextBase), baseConstructor);
+			else if (baseConstructor->isImplemented())
+			{
+				// The first constructor found is handled like a function
+				// and its pushed into the callstack there.
+				// This if avoids duplication in the callstack.
+				if (!m_callStack.empty())
+					pushCallStack({baseConstructor, nullptr});
+				baseConstructor->accept(*this);
+				// popped by endVisit(FunctionDefinition)
+			}
+			break;
+		}
+		else
+		{
+			initializeStateVariables(**nextBase);
+			++nextBase;
+		}
+	}
+
+	initializeStateVariables(_contract);
+}
+
 bool SMTEncoder::visit(PlaceholderStatement const&)
 {
 	solAssert(!m_callStack.empty(), "");
@@ -551,20 +638,25 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
 	solAssert(m_currentContract == nullptr, "");
 	m_currentContract = &_contract;
 
-	initializeStateVariables(_contract);
+	m_context.reset();
+	m_context.pushSolver();
+	createStateVariables(_contract);
+	clearIndices(m_currentContract, nullptr);
 }
 
 void SMTEncoder::initFunction(FunctionDefinition const& _function)
 {
 	solAssert(m_callStack.empty(), "");
+	solAssert(m_currentContract, "");
 	m_context.reset();
 	m_context.pushSolver();
 	m_pathConditions.clear();
 	pushCallStack({&_function, nullptr});
 	m_uninterpretedTerms.clear();
-	resetStateVariables();
-	initializeLocalVariables(_function);
+	createStateVariables(*m_currentContract);
+	createLocalVariables(_function);
 	m_arrayAssignmentHappened = false;
+	clearIndices(m_currentContract, &_function);
 }
 
 void SMTEncoder::visitAssert(FunctionCall const& _funCall)
@@ -1239,26 +1331,61 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 			}
 }
 
-void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
+void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
 {
 	for (auto var: _contract.stateVariablesIncludingInherited())
 		createVariable(*var);
 }
 
-void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
+void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
+{
+	for (auto var: _contract.stateVariables())
+	{
+		solAssert(m_context.knownVariable(*var), "");
+		m_context.setZeroValue(*var);
+	}
+
+	for (auto var: _contract.stateVariables())
+		if (var->value())
+		{
+			var->value()->accept(*this);
+			assignment(*var, *var->value());
+		}
+}
+
+void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
 {
 	for (auto const& variable: _function.localVariables())
-		if (createVariable(*variable))
-			m_context.setZeroValue(*variable);
+		createVariable(*variable);
 
 	for (auto const& param: _function.parameters())
-		if (createVariable(*param))
-			m_context.setUnknownValue(*param);
+		createVariable(*param);
 
 	if (_function.returnParameterList())
 		for (auto const& retParam: _function.returnParameters())
-			if (createVariable(*retParam))
-				m_context.setZeroValue(*retParam);
+			createVariable(*retParam);
+}
+
+void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
+{
+	for (auto const& variable: _function.localVariables())
+	{
+		solAssert(m_context.knownVariable(*variable), "");
+		m_context.setZeroValue(*variable);
+	}
+
+	for (auto const& param: _function.parameters())
+	{
+		solAssert(m_context.knownVariable(*param), "");
+		m_context.setUnknownValue(*param);
+	}
+
+	if (_function.returnParameterList())
+		for (auto const& retParam: _function.returnParameters())
+		{
+			solAssert(m_context.knownVariable(*retParam), "");
+			m_context.setZeroValue(*retParam);
+		}
 }
 
 void SMTEncoder::resetStateVariables()
@@ -1438,6 +1565,20 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 		m_context.variable(*var.first)->index() = var.second;
 }
 
+void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
+{
+	solAssert(_contract, "");
+	for (auto var: _contract->stateVariablesIncludingInherited())
+		m_context.variable(*var)->resetIndex();
+	if (_function)
+	{
+		for (auto const& var: _function->parameters() + _function->returnParameters())
+			m_context.variable(*var)->resetIndex();
+		for (auto const& var: _function->localVariables())
+			m_context.variable(*var)->resetIndex();
+	}
+}
+
 Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
 {
 	Expression const* base = &_indexAccess.baseExpression();

libsolidity/formal/SMTEncoder.h

@@ -122,6 +122,12 @@ protected:
 	/// visit depth.
 	void visitFunctionOrModifier();
 
+	/// Inlines a modifier or base constructor call.
+	void inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition);
+
+	/// Inlines the constructor hierarchy into a single constructor.
+	void inlineConstructorHierarchy(ContractDefinition const& _contract);
+
 	/// Defines a new global variable or function.
 	void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
 
@@ -161,7 +167,9 @@ protected:
 
 	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
 
+	void createStateVariables(ContractDefinition const& _contract);
 	void initializeStateVariables(ContractDefinition const& _contract);
+	void createLocalVariables(FunctionDefinition const& _function);
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
 	void resetStateVariables();
@@ -209,6 +217,9 @@ protected:
 	VariableIndices copyVariableIndices();
 	/// Resets the variable indices.
 	void resetVariableIndices(VariableIndices const& _indices);
+	/// Used when starting a new block.
+	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr);
+
 
 	/// @returns variables that are touched in _node's subtree.
 	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
@@ -253,6 +264,8 @@ protected:
 	/// Needs to be a stack because of function calls.
 	std::vector<int> m_modifierDepthStack;
 
+	std::map<ContractDefinition const*, ModifierInvocation const*> m_baseConstructorCalls;
+
 	ContractDefinition const* m_currentContract = nullptr;
 
 	/// Stores the context of the encoding.