Change CHC encoding to functions forest instead of explicit CFG

libsolidity/formal/CHC.cpp

@@ -27,6 +27,8 @@
 
 #include <libsolidity/ast/TypeProvider.h>
 
+#include <libsolutil/Algorithms.h>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::langutil;
@@ -75,16 +77,39 @@ void CHC::analyze(SourceUnit const& _source)
 	m_context.setAssertionAccumulation(false);
 	m_variableUsage.setFunctionInlining(false);
 
+	resetSourceAnalysis();
+
 	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");
-	addRule(genesis, genesis.name);
 
-	_source.accept(*this);
+	set<SourceUnit const*, IdCompare> sources;
+	sources.insert(&_source);
+	for (auto const& source: _source.referencedSourceUnits(true))
+		sources.insert(source);
+	for (auto const* source: sources)
+		defineInterfacesAndSummaries(*source);
+	for (auto const* source: sources)
+		source->accept(*this);
+
+	for (auto const& [scope, target]: m_verificationTargets)
+	{
+		auto assertions = transactionAssertions(scope);
+		for (auto const* assertion: assertions)
+		{
+			createErrorBlock();
+			connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
+			auto [result, model] = query(error(), assertion->location());
+			// This should be fine but it's a bug in the old compiler
+			(void)model;
+			if (result == smt::CheckResult::UNSATISFIABLE)
+				m_safeAssertions.insert(assertion);
+		}
+	}
 }
 
 vector<string> CHC::unhandledQueries() const
@@ -97,26 +122,15 @@ vector<string> CHC::unhandledQueries() const
 
 bool CHC::visit(ContractDefinition const& _contract)
 {
-	if (!shouldVisit(_contract))
+	resetContractAnalysis();
-		return false;
-
-	reset();
 
 	initContract(_contract);
 
-	m_stateVariables = _contract.stateVariablesIncludingInherited();
+	m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
-
+	m_stateSorts = stateSorts(_contract);
-	for (auto const& var: m_stateVariables)
-		// SMT solvers do not support function types as arguments.
-		if (var->type()->category() == Type::Category::Function)
-			m_stateSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
-		else
-			m_stateSorts.push_back(smt::smtSort(*var->type()));
 
 	clearIndices(&_contract);
 
-	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);
@@ -125,10 +139,12 @@ bool CHC::visit(ContractDefinition const& _contract)
 		boolSort
 	);
 
+	string suffix = _contract.name() + "_" + to_string(_contract.id());
 	m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix);
-	m_constructorPredicate = createSymbolicBlock(constructorSort(), "implicit_constructor_" + to_string(_contract.id()));
+	m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix);
+	m_implicitConstructorPredicate = createSymbolicBlock(interfaceSort(), "implicit_constructor_" + suffix);
 	auto stateExprs = currentStateVariables();
-	setCurrentBlock(*m_interfacePredicate, &stateExprs);
+	setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
 
 	SMTEncoder::visit(_contract);
 	return false;
@@ -136,33 +152,33 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 void CHC::endVisit(ContractDefinition const& _contract)
 {
-	if (!shouldVisit(_contract))
-		return;
-
 	for (auto const& var: m_stateVariables)
 	{
 		solAssert(m_context.knownVariable(*var), "");
+		auto const& symbVar = m_context.variable(*var);
+		symbVar->resetIndex();
 		m_context.setZeroValue(*var);
+		symbVar->increaseIndex();
 	}
-	auto genesisPred = (*m_genesisPredicate)({});
+	auto implicitConstructor = (*m_implicitConstructorPredicate)(initialStateVariables());
-	auto implicitConstructor = (*m_constructorPredicate)(currentStateVariables());
+	connectBlocks(genesis(), implicitConstructor);
-	connectBlocks(genesisPred, implicitConstructor);
 	m_currentBlock = implicitConstructor;
+	m_context.addAssertion(m_error.currentValue() == 0);
 
 	if (auto constructor = _contract.constructor())
 		constructor->accept(*this);
 	else
 		inlineConstructorHierarchy(_contract);
 
-	connectBlocks(m_currentBlock, interface());
+	auto summary = predicate(*m_constructorSummaryPredicate, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables());
+	connectBlocks(m_currentBlock, summary);
 
-	for (unsigned i = 0; i < m_verificationTargets.size(); ++i)
+	clearIndices(m_currentContract, nullptr);
-	{
+	auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
-		auto const& target = m_verificationTargets.at(i);
+	setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
-		auto errorAppl = error(i + 1);
+
-		if (query(errorAppl, target->location()))
+	addVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
-			m_safeAssertions.insert(target);
+	connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
-	}
 
 	SMTEncoder::endVisit(_contract);
 }
@@ -182,7 +198,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 		return false;
 	}
 
-	solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
+	solAssert(!m_currentFunction, "Function inlining should not happen in CHC.");
 	m_currentFunction = &_function;
 
 	initFunction(_function);
@@ -193,7 +209,17 @@ bool CHC::visit(FunctionDefinition const& _function)
 	auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
 	auto bodyPred = predicate(*bodyBlock);
 
+	if (_function.isConstructor())
 		connectBlocks(m_currentBlock, functionPred);
+	else
+		connectBlocks(genesis(), functionPred);
+
+	m_context.addAssertion(m_error.currentValue() == 0);
+	for (auto const* var: m_stateVariables)
+		m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
+	for (auto const& var: _function.parameters())
+		m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
+
 	connectBlocks(functionPred, bodyPred);
 
 	setCurrentBlock(*bodyBlock);
@@ -225,18 +251,30 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		// This is done in endVisit(ContractDefinition).
 		if (_function.isConstructor())
 		{
-			auto constructorExit = createSymbolicBlock(interfaceSort(), "constructor_exit_" + to_string(_function.id()));
+			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
-			connectBlocks(m_currentBlock, predicate(*constructorExit, currentStateVariables()));
+			auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
+			connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables()));
+
 			clearIndices(m_currentContract, m_currentFunction);
-			auto stateExprs = currentStateVariables();
+			auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
 			setCurrentBlock(*constructorExit, &stateExprs);
 		}
 		else
 		{
-			connectBlocks(m_currentBlock, interface());
+			auto assertionError = m_error.currentValue();
-			clearIndices(m_currentContract, m_currentFunction);
+			auto sum = summary(_function);
-			auto stateExprs = currentStateVariables();
+			connectBlocks(m_currentBlock, sum);
-			setCurrentBlock(*m_interfacePredicate, &stateExprs);
+
+			auto iface = interface();
+
+			auto stateExprs = initialStateVariables();
+			setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
+
+			if (_function.isPublic())
+			{
+				addVerificationTarget(&_function, m_currentBlock, sum, assertionError);
+				connectBlocks(m_currentBlock, iface, sum && (assertionError == 0));
+			}
 		}
 		m_currentFunction = nullptr;
 	}
@@ -468,12 +506,23 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	solAssert(args.size() == 1, "");
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
 
-	createErrorBlock();
+	solAssert(m_currentContract, "");
+	solAssert(m_currentFunction, "");
+	if (m_currentFunction->isConstructor())
+		m_functionAssertions[m_currentContract].insert(&_funCall);
+	else
+		m_functionAssertions[m_currentFunction].insert(&_funCall);
 
-	smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
+	auto previousError = m_error.currentValue();
-	connectBlocks(m_currentBlock, error(), currentPathConditions() && assertNeg);
+	m_error.increaseIndex();
 
-	m_verificationTargets.push_back(&_funCall);
+	connectBlocks(
+		m_currentBlock,
+		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
+		currentPathConditions() && !m_context.expression(*args.front())->currentValue() && (m_error.currentValue() == _funCall.id())
+	);
+
+	m_context.addAssertion(m_error.currentValue() == previousError);
 }
 
 void CHC::unknownFunctionCall(FunctionCall const&)
@@ -488,15 +537,23 @@ void CHC::unknownFunctionCall(FunctionCall const&)
 	m_unknownFunctionCallSeen = true;
 }
 
-void CHC::reset()
+void CHC::resetSourceAnalysis()
+{
+	m_verificationTargets.clear();
+	m_safeAssertions.clear();
+	m_functionAssertions.clear();
+	m_callGraph.clear();
+	m_summaries.clear();
+}
+
+void CHC::resetContractAnalysis()
 {
 	m_stateSorts.clear();
 	m_stateVariables.clear();
-	m_verificationTargets.clear();
-	m_safeAssertions.clear();
 	m_unknownFunctionCallSeen = false;
 	m_breakDest = nullptr;
 	m_continueDest = nullptr;
+	m_error.resetIndex();
 }
 
 void CHC::eraseKnowledge()
@@ -521,17 +578,6 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 	}
 }
 
-
-bool CHC::shouldVisit(ContractDefinition const& _contract) const
-{
-	if (
-		_contract.isLibrary() ||
-		_contract.isInterface()
-	)
-		return false;
-	return true;
-}
-
 bool CHC::shouldVisit(FunctionDefinition const& _function) const
 {
 	if (
@@ -547,6 +593,7 @@ void CHC::setCurrentBlock(
 	vector<smt::Expression> const* _arguments
 )
 {
+	if (m_context.solverStackHeigh() > 0)
 		m_context.popSolver();
 	solAssert(m_currentContract, "");
 	clearIndices(m_currentContract, m_currentFunction);
@@ -557,10 +604,42 @@ void CHC::setCurrentBlock(
 		m_currentBlock = predicate(_block);
 }
 
+set<Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
+{
+	set<Expression const*, IdCompare> assertions;
+	solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
+		assertions.insert(m_functionAssertions[function].begin(), m_functionAssertions[function].end());
+		for (auto const* called: m_callGraph[function])
+		_addChild(called);
+	});
+	return assertions;
+}
+
+vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
+{
+	vector<VariableDeclaration const*> stateVars;
+	for (auto const& contract: _contract.annotation().linearizedBaseContracts)
+		for (auto var: contract->stateVariables())
+			stateVars.push_back(var);
+	return stateVars;
+}
+
+vector<smt::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
+{
+	vector<smt::SortPointer> stateSorts;
+	for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract))
+		stateSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
+	return stateSorts;
+}
+
 smt::SortPointer CHC::constructorSort()
 {
-	// TODO this will change once we support function calls.
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	return interfaceSort();
+	auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
+	return make_shared<smt::FunctionSort>(
+		vector<smt::SortPointer>{intSort} + m_stateSorts,
+		boolSort
+	);
 }
 
 smt::SortPointer CHC::interfaceSort()
@@ -572,20 +651,38 @@ smt::SortPointer CHC::interfaceSort()
 	);
 }
 
+smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
+{
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	return make_shared<smt::FunctionSort>(
+		stateSorts(_contract),
+		boolSort
+	);
+}
+
+/// A function in the symbolic CFG requires:
+/// - Index of failed assertion. 0 means no assertion failed.
+/// - 2 sets of state variables:
+///   - State variables at the beginning of the current function, immutable
+///   - Current state variables
+///    At the beginning of the function these must equal set 1
+/// - 2 sets of input variables:
+///   - Input variables at the beginning of the current function, immutable
+///   - Current input variables
+///    At the beginning of the function these must equal set 1
+/// - 1 set of output variables
 smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 {
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	vector<smt::SortPointer> varSorts;
+	auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
-	for (auto const& var: _function.parameters() + _function.returnParameters())
+	vector<smt::SortPointer> inputSorts;
-	{
+	for (auto const& var: _function.parameters())
-		// SMT solvers do not support function types as arguments.
+		inputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
-		if (var->type()->category() == Type::Category::Function)
+	vector<smt::SortPointer> outputSorts;
-			varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
+	for (auto const& var: _function.returnParameters())
-		else
+		outputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
-			varSorts.push_back(smt::smtSort(*var->type()));
-	}
 	return make_shared<smt::FunctionSort>(
-		m_stateSorts + varSorts,
+		vector<smt::SortPointer>{intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
 		boolSort
 	);
 }
@@ -601,19 +698,31 @@ smt::SortPointer CHC::sort(ASTNode const* _node)
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	vector<smt::SortPointer> varSorts;
 	for (auto const& var: m_currentFunction->localVariables())
-	{
+		varSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
-		// SMT solvers do not support function types as arguments.
-		if (var->type()->category() == Type::Category::Function)
-			varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
-		else
-			varSorts.push_back(smt::smtSort(*var->type()));
-	}
 	return make_shared<smt::FunctionSort>(
 		fSort->domain + varSorts,
 		boolSort
 	);
 }
 
+smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
+{
+	auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
+	auto sorts = stateSorts(_contract);
+
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
+	vector<smt::SortPointer> inputSorts, outputSorts;
+	for (auto const& var: _function.parameters())
+		inputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
+	for (auto const& var: _function.returnParameters())
+		outputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
+	return make_shared<smt::FunctionSort>(
+		vector<smt::SortPointer>{intSort} + sorts + inputSorts + sorts + outputSorts,
+		boolSort
+	);
+}
+
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
 {
 	auto block = make_unique<smt::SymbolicFunctionVariable>(
@@ -625,12 +734,33 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPoin
 	return block;
 }
 
+void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
+{
+	for (auto const& node: _source.nodes())
+		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
+			for (auto const* base: contract->annotation().linearizedBaseContracts)
+			{
+				string suffix = base->name() + "_" + to_string(base->id());
+				m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix);
+				for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
+					if (!m_context.knownVariable(*var))
+						createVariable(*var);
+				for (auto const* function: base->definedFunctions())
+					m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
+			}
+}
+
 smt::Expression CHC::interface()
 {
 	vector<smt::Expression> paramExprs;
 	for (auto const& var: m_stateVariables)
 		paramExprs.push_back(m_context.variable(*var)->currentValue());
-	return (*m_interfacePredicate)(paramExprs);
+	return (*m_interfaces.at(m_currentContract))(paramExprs);
+}
+
+smt::Expression CHC::interface(ContractDefinition const& _contract)
+{
+	return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract));
 }
 
 smt::Expression CHC::error()
@@ -643,6 +773,27 @@ smt::Expression CHC::error(unsigned _idx)
 	return m_errorPredicate->functionValueAtIndex(_idx)({});
 }
 
+smt::Expression CHC::summary(ContractDefinition const&)
+{
+	return (*m_constructorSummaryPredicate)(
+		vector<smt::Expression>{m_error.currentValue()} +
+		currentStateVariables()
+	);
+}
+
+smt::Expression CHC::summary(FunctionDefinition const& _function)
+{
+	vector<smt::Expression> args{m_error.currentValue()};
+	auto contract = _function.annotation().contract;
+	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables();
+	for (auto const& var: _function.parameters())
+		args.push_back(m_context.variable(*var)->valueAtIndex(0));
+	args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
+	for (auto const& var: _function.returnParameters())
+		args.push_back(m_context.variable(*var)->currentValue());
+	return (*m_summaries.at(m_currentContract).at(&_function))(args);
+}
+
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
 {
 	return createSymbolicBlock(sort(_node),
@@ -653,6 +804,15 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node,
 		predicateName(_node));
 }
 
+unique_ptr<smt::SymbolicFunctionVariable> CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
+{
+	return createSymbolicBlock(summarySort(_function, _contract),
+		"summary_" +
+		uniquePrefix() +
+		"_" +
+		predicateName(&_function, &_contract));
+}
+
 void CHC::createErrorBlock()
 {
 	solAssert(m_errorPredicate, "");
@@ -669,6 +829,28 @@ void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to
 	addRule(edge, _from.name + "_to_" + _to.name);
 }
 
+vector<smt::Expression> CHC::initialStateVariables()
+{
+	return stateVariablesAtIndex(0);
+}
+
+vector<smt::Expression> CHC::stateVariablesAtIndex(int _index)
+{
+	solAssert(m_currentContract, "");
+	vector<smt::Expression> exprs;
+	for (auto const& var: m_stateVariables)
+		exprs.push_back(m_context.variable(*var)->valueAtIndex(_index));
+	return exprs;
+}
+
+vector<smt::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
+{
+	vector<smt::Expression> exprs;
+	for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract))
+		exprs.push_back(m_context.variable(*var)->valueAtIndex(_index));
+	return exprs;
+}
+
 vector<smt::Expression> CHC::currentStateVariables()
 {
 	solAssert(m_currentContract, "");
@@ -680,11 +862,22 @@ vector<smt::Expression> CHC::currentStateVariables()
 
 vector<smt::Expression> CHC::currentFunctionVariables()
 {
-	vector<smt::Expression> paramExprs;
+	vector<smt::Expression> initInputExprs;
-	if (m_currentFunction)
+	vector<smt::Expression> mutableInputExprs;
-		for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
+	for (auto const& var: m_currentFunction->parameters())
-			paramExprs.push_back(m_context.variable(*var)->currentValue());
+	{
-	return currentStateVariables() + paramExprs;
+		initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
+		mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
+	}
+	vector<smt::Expression> returnExprs;
+	for (auto const& var: m_currentFunction->returnParameters())
+		returnExprs.push_back(m_context.variable(*var)->currentValue());
+	return vector<smt::Expression>{m_error.currentValue()} +
+		initialStateVariables() +
+		initInputExprs +
+		currentStateVariables() +
+		mutableInputExprs +
+		returnExprs;
 }
 
 vector<smt::Expression> CHC::currentBlockVariables()
@@ -696,7 +889,7 @@ vector<smt::Expression> CHC::currentBlockVariables()
 	return currentFunctionVariables() + paramExprs;
 }
 
-string CHC::predicateName(ASTNode const* _node)
+string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract)
 {
 	string prefix;
 	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
@@ -705,7 +898,12 @@ string CHC::predicateName(ASTNode const* _node)
 		if (!funDef->name().empty())
 			prefix += "_" + funDef->name() + "_";
 	}
-	return prefix + to_string(_node->id());
+	else if (m_currentFunction && !m_currentFunction->name().empty())
+		prefix += m_currentFunction->name();
+
+	auto contract = _contract ? _contract : m_currentContract;
+	solAssert(contract, "");
+	return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
 }
 
 smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
@@ -726,7 +924,7 @@ void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 	m_interface->addRule(_rule, _ruleName);
 }
 
-bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
+pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
 {
 	smt::CheckResult result;
 	vector<string> values;
@@ -736,7 +934,7 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _
 	case smt::CheckResult::SATISFIABLE:
 		break;
 	case smt::CheckResult::UNSATISFIABLE:
-		return true;
+		break;
 	case smt::CheckResult::UNKNOWN:
 		break;
 	case smt::CheckResult::CONFLICTING:
@@ -746,7 +944,12 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _
 		m_outerErrorReporter.warning(_location, "Error trying to invoke SMT solver.");
 		break;
 	}
-	return false;
+	return {result, values};
+}
+
+void CHC::addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
+{
+	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{VerificationTarget::Type::Assert, _from, _constraints}, _errorId});
 }
 
 string CHC::uniquePrefix()

libsolidity/formal/CHC.h

@@ -79,22 +79,38 @@ private:
 	void unknownFunctionCall(FunctionCall const& _funCall);
 	//@}
 
+	struct IdCompare
+	{
+		bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
+		{
+			return lhs->id() < rhs->id();
+		}
+	};
+
 	/// Helpers.
 	//@{
-	void reset();
+	void resetSourceAnalysis();
+	void resetContractAnalysis();
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
-	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
 	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
+	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
+	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
 	//@}
 
 	/// Sort helpers.
 	//@{
+	static std::vector<smt::SortPointer> stateSorts(ContractDefinition const& _contract);
 	smt::SortPointer constructorSort();
 	smt::SortPointer interfaceSort();
+	static smt::SortPointer interfaceSort(ContractDefinition const& _const);
 	smt::SortPointer sort(FunctionDefinition const& _function);
 	smt::SortPointer sort(ASTNode const* _block);
+	/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
+	/// The _contract is also needed because the same function might be in many contracts due to inheritance,
+	/// where the sort changes because the set of state variables might change.
+	static smt::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract);
 	//@}
 
 	/// Predicate helpers.
@@ -102,14 +118,24 @@ private:
 	/// @returns a new block of given _sort and _name.
 	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
 
+	/// Creates summary predicates for all functions of all contracts
+	/// in a given _source.
+	void defineInterfacesAndSummaries(SourceUnit const& _source);
+
+	/// Genesis predicate.
+	smt::Expression genesis() { return (*m_genesisPredicate)({}); }
 	/// Interface predicate over current variables.
 	smt::Expression interface();
+	smt::Expression interface(ContractDefinition const& _contract);
 	/// Error predicate over current variables.
 	smt::Expression error();
 	smt::Expression error(unsigned _idx);
 
 	/// Creates a block for the given _node.
 	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
+	/// Creates a call block for the given function _function from contract _contract.
+	/// The contract is needed here because of inheritance.
+	std::unique_ptr<smt::SymbolicFunctionVariable> createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
 
 	/// Creates a new error block to be used by an assertion.
 	/// Also registers the predicate.
@@ -117,6 +143,11 @@ private:
 
 	void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
 
+	/// @returns the symbolic values of the state variables at the beginning
+	/// of the current transaction.
+	std::vector<smt::Expression> initialStateVariables();
+	std::vector<smt::Expression> stateVariablesAtIndex(int _index);
+	std::vector<smt::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
 	/// @returns the current symbolic values of the current state variables.
 	std::vector<smt::Expression> currentStateVariables();
 
@@ -128,19 +159,26 @@ private:
 	std::vector<smt::Expression> currentBlockVariables();
 
 	/// @returns the predicate name for a given node.
-	std::string predicateName(ASTNode const* _node);
+	std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
 	/// @returns a predicate application over the current scoped variables.
 	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block);
 	/// @returns a predicate application over @param _arguments.
 	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const& _arguments);
+	/// @returns a predicate that defines a constructor summary.
+	smt::Expression summary(ContractDefinition const& _contract);
+	/// @returns a predicate that defines a function summary.
+	smt::Expression summary(FunctionDefinition const& _function);
 	//@}
 
 	/// Solver related.
 	//@{
 	/// Adds Horn rule to the solver.
 	void addRule(smt::Expression const& _rule, std::string const& _ruleName);
-	/// @returns true if query is unsatisfiable (safe).
+	/// @returns <true, empty> if query is unsatisfiable (safe).
-	bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
+	/// @returns <false, model> otherwise.
+	std::pair<smt::CheckResult, std::vector<std::string>> query(smt::Expression const& _query, langutil::SourceLocation const& _location);
+
+	void addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
 	//@}
 
 	/// Misc.
@@ -157,15 +195,29 @@ private:
 
 	/// Implicit constructor predicate.
 	/// Explicit constructors are handled as functions.
-	std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorPredicate;
+	std::unique_ptr<smt::SymbolicFunctionVariable> m_implicitConstructorPredicate;
+
+	/// Constructor summary predicate, exists after the constructor
+	/// (implicit or explicit) and before the interface.
+	std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorSummaryPredicate;
 
 	/// Artificial Interface predicate.
 	/// Single entry block for all functions.
-	std::unique_ptr<smt::SymbolicFunctionVariable> m_interfacePredicate;
+	std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_interfaces;
 
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
 	std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;
+
+	/// Function predicates.
+	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>>> m_summaries;
+
+	smt::SymbolicIntVariable m_error{
+		TypeProvider::uint256(),
+		TypeProvider::uint256(),
+		"error",
+		m_context
+	};
 	//@}
 
 	/// Variables.
@@ -180,7 +232,12 @@ private:
 
 	/// Verification targets.
 	//@{
-	std::vector<Expression const*> m_verificationTargets;
+	struct CHCVerificationTarget: VerificationTarget
+	{
+		smt::Expression errorId;
+	};
+
+	std::map<ASTNode const*, CHCVerificationTarget, IdCompare> m_verificationTargets;
 
 	/// Assertions proven safe.
 	std::set<Expression const*> m_safeAssertions;
@@ -190,6 +247,10 @@ private:
 	//@{
 	FunctionDefinition const* m_currentFunction = nullptr;
 
+	std::map<ASTNode const*, std::set<ASTNode const*, IdCompare>, IdCompare> m_callGraph;
+
+	std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
+
 	/// The current block.
 	smt::Expression m_currentBlock = smt::Expression(true);
 

libsolidity/formal/EncodingContext.h

@@ -140,6 +140,7 @@ public:
 	void pushSolver();
 	void popSolver();
 	void addAssertion(Expression const& _e);
+	unsigned solverStackHeigh() { return m_assertions.size(); } const
 	SolverInterface* solver()
 	{
 		solAssert(m_solver, "");

libsolidity/formal/ModelChecker.cpp

@@ -29,9 +29,9 @@ ModelChecker::ModelChecker(
 	ReadCallback::Callback const& _smtCallback,
 	smt::SMTSolverChoice _enabledSolvers
 ):
+	m_context(),
 	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers)
-	m_context()
 {
 }
 

libsolidity/formal/ModelChecker.h

@@ -62,14 +62,14 @@ public:
 	static smt::SMTSolverChoice availableSolvers();
 
 private:
+	/// Stores the context of the encoding.
+	smt::EncodingContext m_context;
+
 	/// Bounded Model Checker engine.
 	BMC m_bmc;
 
 	/// Constrained Horn Clauses engine.
 	CHC m_chc;
-
-	/// Stores the context of the encoding.
-	smt::EncodingContext m_context;
 };
 
 }

libsolidity/formal/Z3Interface.h

@@ -58,11 +58,11 @@ private:
 	z3::sort z3Sort(smt::Sort const& _sort);
 	z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
 
-	std::map<std::string, z3::expr> m_constants;
-	std::map<std::string, z3::func_decl> m_functions;
-
 	z3::context m_context;
 	z3::solver m_solver;
+
+	std::map<std::string, z3::expr> m_constants;
+	std::map<std::string, z3::func_decl> m_functions;
 };
 
 }

test/libsolidity/smtCheckerTests/functions/library_constant.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+library l1 {
+
+	uint private constant TON = 1000;
+	function f1() public pure {
+		assert(TON == 1000);
+		assert(TON == 2000);
+	}
+	function f2(uint x, uint y) internal pure returns (uint) {
+		return x + y;
+	}
+}
+
+contract C {
+	function f(uint x) public pure {
+		uint z = l1.f2(x, 1);
+		assert(z == x + 1);
+	}
+}
+// ----
+// Warning: (136-155): Assertion violation happens here
+// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (300-302): Assertion checker does not yet implement type type(library l1)
+// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/functions/library_constant_2.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+library l1 {
+
+	uint private constant TON = 1000;
+	function f1() public pure {
+		assert(TON == 1000);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/loop_nested.sol

@@ -17,3 +17,8 @@ contract Simple {
 }
 // ====
 // SMTSolvers: z3
+// ----
+// Warning: (172-187): Error trying to invoke SMT solver.
+// Warning: (195-209): Error trying to invoke SMT solver.
+// Warning: (172-187): Assertion violation happens here
+// Warning: (195-209): Assertion violation happens here

test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol

@@ -14,3 +14,8 @@ contract Simple {
 }
 // ====
 // SMTSolvers: z3
+// ----
+// Warning: (164-179): Error trying to invoke SMT solver.
+// Warning: (187-201): Error trying to invoke SMT solver.
+// Warning: (164-179): Assertion violation happens here
+// Warning: (187-201): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol

@@ -12,12 +12,12 @@ contract LoopFor2 {
 			b[i] = i + 1;
 			c[i] = b[i];
 		}
+		// This is safe but too hard to solve currently.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
-// ====
-// SMTSolvers: z3
 // ----
-// Warning: (312-331): Assertion violation happens here
+// Warning: (316-336): Assertion violation happens here
+// Warning: (363-382): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -12,13 +12,13 @@ contract LoopFor2 {
 			b[i] = i + 1;
 			c[i] = b[i];
 		}
+		// This is safe but too hard to prove currently.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
-// ====
-// SMTSolvers: z3
 // ----
-// Warning: (290-309): Assertion violation happens here
+// Warning: (317-337): Assertion violation happens here
-// Warning: (313-332): Assertion violation happens here
+// Warning: (341-360): Assertion violation happens here
+// Warning: (364-383): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol

@@ -13,5 +13,5 @@ contract C
 		assert(a[1][1] == 0);
 	}
 }
-// ====
+// ----
-// SMTSolvers: z3
+// Warning: (184-204): Assertion violation happens here