Add local vars to cex

libsolidity/formal/CHC.cpp

@@ -32,6 +32,8 @@
 #include <libsmtutil/CHCSmtLib2Interface.h>
 #include <libsolutil/Algorithms.h>
 
+#include <range/v3/algorithm/for_each.hpp>
+
 #include <boost/range/adaptor/reversed.hpp>
 
 #ifdef HAVE_Z3_DLOPEN
@@ -130,6 +132,8 @@ bool CHC::visit(ContractDefinition const& _contract)
 	initContract(_contract);
 	clearIndices(&_contract);
 
+	m_scopes.push_back(&_contract);
+
 	m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
 	solAssert(m_currentContract, "");
 
@@ -208,6 +212,10 @@ void CHC::endVisit(ContractDefinition const& _contract)
 		m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
 		connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
 	}
+
+	solAssert(m_scopes.back() == &_contract, "");
+	m_scopes.pop_back();
+
 	SMTEncoder::endVisit(_contract);
 }
 
@@ -223,6 +231,8 @@ bool CHC::visit(FunctionDefinition const& _function)
 	solAssert(!m_currentFunction, "Function inlining should not happen in CHC.");
 	m_currentFunction = &_function;
 
+	m_scopes.push_back(&_function);
+
 	initFunction(_function);
 
 	auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionBlock);
@@ -257,6 +267,9 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	// No inlining.
 	solAssert(m_currentFunction == &_function, "");
 
+	solAssert(m_scopes.back() == &_function, "");
+	m_scopes.pop_back();
+
 	connectBlocks(m_currentBlock, summary(_function));
 	setCurrentBlock(*m_summaries.at(m_currentContract).at(&_function));
 
@@ -282,6 +295,19 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	SMTEncoder::endVisit(_function);
 }
 
+bool CHC::visit(Block const& _block)
+{
+	m_scopes.push_back(&_block);
+	return SMTEncoder::visit(_block);
+}
+
+void CHC::endVisit(Block const& _block)
+{
+	solAssert(m_scopes.back() == &_block, "");
+	m_scopes.pop_back();
+	SMTEncoder::endVisit(_block);
+}
+
 bool CHC::visit(IfStatement const& _if)
 {
 	solAssert(m_currentFunction, "");
@@ -382,6 +408,8 @@ bool CHC::visit(WhileStatement const& _while)
 
 bool CHC::visit(ForStatement const& _for)
 {
+	m_scopes.push_back(&_for);
+
 	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
 	m_unknownFunctionCallSeen = false;
 
@@ -441,6 +469,12 @@ bool CHC::visit(ForStatement const& _for)
 	return false;
 }
 
+void CHC::endVisit(ForStatement const& _for)
+{
+	solAssert(m_scopes.back() == &_for, "");
+	m_scopes.pop_back();
+}
+
 void CHC::endVisit(FunctionCall const& _funCall)
 {
 	auto functionCallKind = *_funCall.annotation().kind;
@@ -552,6 +586,18 @@ void CHC::endVisit(Return const& _return)
 	m_currentBlock = predicate(*returnGhost);
 }
 
+bool CHC::visit(TryCatchClause const& _tryStatement)
+{
+	m_scopes.push_back(&_tryStatement);
+	return SMTEncoder::visit(_tryStatement);
+}
+
+void CHC::endVisit(TryCatchClause const& _tryStatement)
+{
+	solAssert(m_scopes.back() == &_tryStatement, "");
+	m_scopes.pop_back();
+}
+
 bool CHC::visit(TryStatement const& _tryStatement)
 {
 	FunctionCall const* externalCall = dynamic_cast<FunctionCall const*>(&_tryStatement.externalCall());
@@ -975,7 +1021,7 @@ SortPointer CHC::sort(ASTNode const* _node)
 
 Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node, ContractDefinition const* _contractContext)
 {
-	auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext);
+	auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext, m_scopes);
 	m_interface->registerRelation(block->functor());
 	return block;
 }
@@ -1150,7 +1196,11 @@ Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract
 
 void CHC::createErrorBlock()
 {
-	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()), PredicateType::Error);
+	m_errorPredicate = createSymbolicBlock(
+		arity0FunctionSort(),
+		"error_target_" + to_string(m_context.newUniqueId()),
+		PredicateType::Error
+	);
 	m_interface->registerRelation(m_errorPredicate->functor());
 }
 
@@ -1240,6 +1290,7 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 	case PredicateType::ExternalCallUntrusted:
 		return smt::function(_block, m_currentContract, m_context);
 	case PredicateType::FunctionBlock:
+	case PredicateType::FunctionErrorBlock:
 		solAssert(m_currentFunction, "");
 		return functionBlock(_block, *m_currentFunction, m_currentContract, m_context);
 	case PredicateType::Error:
@@ -1375,7 +1426,6 @@ void CHC::verificationTargetEncountered(
 	smtutil::Expression const& _errorCondition
 )
 {
-
 	if (!m_settings.targets.has(_type))
 		return;
 
@@ -1396,13 +1446,18 @@ void CHC::verificationTargetEncountered(
 	auto previousError = errorFlag().currentValue();
 	errorFlag().increaseIndex();
 
-	// create an error edge to the summary
-	solAssert(m_errorDest, "");
+	Predicate const* localBlock = m_currentFunction ?
+		createBlock(m_currentFunction, PredicateType::FunctionErrorBlock) :
+		createConstructorBlock(*m_currentContract, "local_error");
+
+	auto pred = predicate(*localBlock);
 	connectBlocks(
 		m_currentBlock,
-		predicate(*m_errorDest),
+		pred,
 		_errorCondition && errorFlag().currentValue() == errorId
 	);
+	solAssert(m_errorDest, "");
+	addRule(smtutil::Expression::implies(pred, predicate(*m_errorDest)), pred.name);
 
 	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
@@ -1606,6 +1661,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 			first = false;
 			/// Generate counterexample message local to the failed target.
 			localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
+
 			if (auto calledFun = summaryPredicate->programFunction())
 			{
 				auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
@@ -1616,6 +1672,30 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 				auto const& outParams = calledFun->returnParameters();
 				if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
 					localState += outStr + "\n";
+
+				optional<unsigned> localErrorId;
+				solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
+				bfs.run([&](auto _nodeId, auto&& _addChild) {
+					auto const& children = _graph.edges.at(_nodeId);
+					if (
+						children.size() == 1 &&
+						nodePred(children.front())->isFunctionErrorBlock()
+					)
+					{
+						localErrorId = children.front();
+						bfs.abort();
+					}
+					ranges::for_each(children, _addChild);
+				});
+
+				if (localErrorId.has_value())
+				{
+					auto const* localError = nodePred(*localErrorId);
+					solAssert(localError && localError->isFunctionErrorBlock(), "");
+					auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
+					if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
+						localState += localStr + "\n";
+				}
 			}
 		}
 		else

libsolidity/formal/CHC.h

@@ -77,14 +77,19 @@ private:
 	void endVisit(ContractDefinition const& _node) override;
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
+	bool visit(Block const& _block) override;
+	void endVisit(Block const& _block) override;
 	bool visit(IfStatement const& _node) override;
 	bool visit(WhileStatement const&) override;
 	bool visit(ForStatement const&) override;
+	void endVisit(ForStatement const&) override;
 	void endVisit(FunctionCall const& _node) override;
 	void endVisit(Break const& _node) override;
 	void endVisit(Continue const& _node) override;
 	void endVisit(IndexRangeAccess const& _node) override;
 	void endVisit(Return const& _node) override;
+	bool visit(TryCatchClause const&) override;
+	void endVisit(TryCatchClause const&) override;
 	bool visit(TryStatement const& _node) override;
 
 	void pushInlineFrame(CallableDeclaration const& _callable) override;

libsolidity/formal/Predicate.cpp

@@ -41,7 +41,8 @@ Predicate const* Predicate::create(
 	PredicateType _type,
 	EncodingContext& _context,
 	ASTNode const* _node,
-	ContractDefinition const* _contractContext
+	ContractDefinition const* _contractContext,
+	vector<ScopeOpener const*> _scopeStack
 )
 {
 	smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context};
@@ -50,7 +51,7 @@ Predicate const* Predicate::create(
 	return &m_predicates.emplace(
 		std::piecewise_construct,
 		std::forward_as_tuple(functorName),
-		std::forward_as_tuple(move(predicate), _type, _node, _contractContext)
+		std::forward_as_tuple(move(predicate), _type, _node, _contractContext, move(_scopeStack))
 	).first->second;
 }
 
@@ -58,12 +59,14 @@ Predicate::Predicate(
 	smt::SymbolicFunctionVariable&& _predicate,
 	PredicateType _type,
 	ASTNode const* _node,
-	ContractDefinition const* _contractContext
+	ContractDefinition const* _contractContext,
+	vector<ScopeOpener const*> _scopeStack
 ):
 	m_predicate(move(_predicate)),
 	m_type(_type),
 	m_node(_node),
-	m_contractContext(_contractContext)
+	m_contractContext(_contractContext),
+	m_scopeStack(_scopeStack)
 {
 }
 
@@ -102,6 +105,11 @@ ASTNode const* Predicate::programNode() const
 	return m_node;
 }
 
+ContractDefinition const* Predicate::contextContract() const
+{
+	return m_contractContext;
+}
+
 ContractDefinition const* Predicate::programContract() const
 {
 	if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
@@ -153,6 +161,16 @@ bool Predicate::isFunctionSummary() const
 	return m_type == PredicateType::FunctionSummary;
 }
 
+bool Predicate::isFunctionBlock() const
+{
+	return m_type == PredicateType::FunctionBlock;
+}
+
+bool Predicate::isFunctionErrorBlock() const
+{
+	return m_type == PredicateType::FunctionErrorBlock;
+}
+
 bool Predicate::isInternalCall() const
 {
 	return m_type == PredicateType::InternalCall;
@@ -308,6 +326,32 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
 	return formatExpressions(outValues, outTypes);
 }
 
+pair<vector<optional<string>>, vector<VariableDeclaration const*>> Predicate::localVariableValues(vector<smtutil::Expression> const& _args) const
+{
+	/// The signature of a local block predicate is:
+	/// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars).
+	/// Here we are interested in localVars.
+	auto const* function = programFunction();
+	solAssert(function, "");
+
+	auto const& localVars = SMTEncoder::localVariablesIncludingModifiers(*function, m_contractContext);
+	auto first = _args.end() - static_cast<int>(localVars.size());
+	vector<smtutil::Expression> outValues(first, _args.end());
+
+	auto mask = applyMap(
+		localVars,
+		[this](auto _var) {
+			auto varScope = dynamic_cast<ScopeOpener const*>(_var->scope());
+			return find(begin(m_scopeStack), end(m_scopeStack), varScope) != end(m_scopeStack);
+		}
+	);
+	auto localVarsInScope = util::filter(localVars, mask);
+	auto outValuesInScope = util::filter(outValues, mask);
+
+	auto outTypes = applyMap(localVarsInScope, [](auto _var) { return _var->type(); });
+	return {formatExpressions(outValuesInScope, outTypes), localVarsInScope};
+}
+
 vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<Type const*> const& _types) const
 {
 	solAssert(_exprs.size() == _types.size(), "");

libsolidity/formal/Predicate.h

@@ -37,6 +37,7 @@ enum class PredicateType
 	ConstructorSummary,
 	FunctionSummary,
 	FunctionBlock,
+	FunctionErrorBlock,
 	InternalCall,
 	ExternalCallTrusted,
 	ExternalCallUntrusted,
@@ -56,14 +57,16 @@ public:
 		PredicateType _type,
 		smt::EncodingContext& _context,
 		ASTNode const* _node = nullptr,
-		ContractDefinition const* _contractContext = nullptr
+		ContractDefinition const* _contractContext = nullptr,
+		std::vector<ScopeOpener const*> _scopeStack = {}
 	);
 
 	Predicate(
 		smt::SymbolicFunctionVariable&& _predicate,
 		PredicateType _type,
 		ASTNode const* _node = nullptr,
-		ContractDefinition const* _contractContext = nullptr
+		ContractDefinition const* _contractContext = nullptr,
+		std::vector<ScopeOpener const*> _scopeStack = {}
 	);
 
 	/// Predicate should not be copiable.
@@ -89,6 +92,10 @@ public:
 	/// @returns the program node this predicate represents.
 	ASTNode const* programNode() const;
 
+	/// @returns the ContractDefinition of the most derived contract
+	/// being analyzed.
+	ContractDefinition const* contextContract() const;
+
 	/// @returns the ContractDefinition that this predicate represents
 	/// or nullptr otherwise.
 	ContractDefinition const* programContract() const;
@@ -110,6 +117,12 @@ public:
 	/// @returns true if this predicate represents a function summary.
 	bool isFunctionSummary() const;
 
+	/// @returns true if this predicate represents a function block.
+	bool isFunctionBlock() const;
+
+	/// @returns true if this predicate represents a function error block.
+	bool isFunctionErrorBlock() const;
+
 	/// @returns true if this predicate represents an internal function call.
 	bool isInternalCall() const;
 
@@ -143,6 +156,9 @@ public:
 	/// where this summary was reached.
 	std::vector<std::optional<std::string>> summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const;
 
+	/// @returns the values of the local variables used by this predicate.
+	std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclaration const*>> localVariableValues(std::vector<smtutil::Expression> const& _args) const;
+
 private:
 	/// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants.
 	std::vector<std::optional<std::string>> formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<Type const*> const& _types) const;
@@ -177,6 +193,10 @@ private:
 	/// Maps the name of the predicate to the actual Predicate.
 	/// Used in counterexample generation.
 	static std::map<std::string, Predicate> m_predicates;
+
+	/// The scope stack when the predicate was created.
+	/// Used to identify the subset of variables in scope.
+	std::vector<ScopeOpener const*> const m_scopeStack;
 };
 
 }

libsolidity/formal/SMTEncoder.cpp

@@ -192,7 +192,12 @@ void SMTEncoder::visitFunctionOrModifier()
 		if (dynamic_cast<ContractDefinition const*>(refDecl))
 			visitFunctionOrModifier();
 		else if (auto modifier = resolveModifierInvocation(*modifierInvocation, m_currentContract))
+		{
+			m_scopes.push_back(modifier);
 			inlineModifierInvocation(modifierInvocation.get(), modifier);
+			solAssert(m_scopes.back() == modifier, "");
+			m_scopes.pop_back();
+		}
 		else
 			solAssert(false, "");
 	}

libsolidity/formal/SMTEncoder.h

@@ -129,6 +129,7 @@ protected:
 	bool visit(IfStatement const&) override { return false; }
 	bool visit(WhileStatement const&) override { return false; }
 	bool visit(ForStatement const&) override { return false; }
+	void endVisit(ForStatement const&) override {}
 	void endVisit(VariableDeclarationStatement const& _node) override;
 	bool visit(Assignment const& _node) override;
 	void endVisit(Assignment const& _node) override;
@@ -150,6 +151,8 @@ protected:
 	bool visit(InlineAssembly const& _node) override;
 	void endVisit(Break const&) override {}
 	void endVisit(Continue const&) override {}
+	bool visit(TryCatchClause const&) override { return true; }
+	void endVisit(TryCatchClause const&) override {}
 	bool visit(TryStatement const&) override { return false; }
 
 	virtual void pushInlineFrame(CallableDeclaration const&);
@@ -400,6 +403,10 @@ protected:
 
 	/// Stores the current function/modifier call/invocation path.
 	std::vector<CallStackEntry> m_callStack;
+
+	/// Stack of scopes.
+	std::vector<ScopeOpener const*> m_scopes;
+
 	/// Returns true if the current function was not visited by
 	/// a function call.
 	bool isRootFunction();