Abstract function smtchecker natspec

libsolidity/formal/CHC.cpp

@@ -219,9 +219,20 @@ bool CHC::visit(FunctionDefinition const& _function)
 	if (!m_currentContract)
 		return false;
 
-	if (!_function.isImplemented())
+	if (
+		!_function.isImplemented() ||
+		abstractAsNondet(_function)
+	)
 	{
-		addRule(summary(_function), "summary_function_" + to_string(_function.id()));
+		smtutil::Expression conj(true);
+		if (
+			_function.stateMutability() == StateMutability::Pure ||
+			_function.stateMutability() == StateMutability::View
+		)
+			conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_function));
+
+		conj = conj && errorFlag().currentValue() == 0;
+		addRule(smtutil::Expression::implies(conj, summary(_function)), "summary_function_" + to_string(_function.id()));
 		return false;
 	}
 
@@ -262,7 +273,10 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (!m_currentContract)
 		return;
 
-	if (!_function.isImplemented())
+	if (
+		!_function.isImplemented() ||
+		abstractAsNondet(_function)
+	)
 		return;
 
 	solAssert(m_currentFunction && m_currentContract, "");
@@ -1001,6 +1015,37 @@ set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
 	return verificationTargetsIds;
 }
 
+optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(string const& _option)
+{
+	static map<string, CHCNatspecOption> options{
+		{"abstract-function-nondet", CHCNatspecOption::AbstractFunctionNondet}
+	};
+	if (options.count(_option))
+		return options.at(_option);
+	return {};
+}
+
+set<CHC::CHCNatspecOption> CHC::smtNatspecTags(FunctionDefinition const& _function)
+{
+	set<CHC::CHCNatspecOption> options;
+	string smtStr = "custom:smtchecker";
+	for (auto const& [tag, value]: _function.annotation().docTags)
+		if (tag == smtStr)
+		{
+			string const& content = value.content;
+			if (auto option = natspecOptionFromString(content))
+				options.insert(*option);
+			else
+				m_errorReporter.warning(3130_error, _function.location(), "Unknown option for \"" + smtStr + "\": \"" + content + "\"");
+		}
+	return options;
+}
+
+bool CHC::abstractAsNondet(FunctionDefinition const& _function)
+{
+	return smtNatspecTags(_function).count(CHCNatspecOption::AbstractFunctionNondet);
+}
+
 SortPointer CHC::sort(FunctionDefinition const& _function)
 {
 	return functionBodySort(_function, m_currentContract, state());
@@ -1213,13 +1258,11 @@ smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract,
 {
 	smtutil::Expression conj = state().state() == state().state(0);
 	conj = conj && errorFlag().currentValue() == 0;
-	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
+	conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_contract));
-		conj = conj && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var);
 
 	FunctionDefinition const* function = _function ? _function : _contract.constructor();
 	if (function)
-		for (auto var: function->parameters())
+		conj = conj && currentEqualInitialVarsConstraints(applyMap(function->parameters(), [](auto&& _var) -> VariableDeclaration const* { return _var.get(); }));
-			conj = conj && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var);
 
 	return conj;
 }
@@ -1254,6 +1297,13 @@ vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const&
 	return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
 }
 
+smtutil::Expression CHC::currentEqualInitialVarsConstraints(vector<VariableDeclaration const*> const& _vars) const
+{
+	return fold(_vars, smtutil::Expression(true), [this](auto&& _conj, auto _var) {
+		return move(_conj) && currentValue(*_var) == m_context.variable(*_var)->valueAtIndex(0);
+	});
+}
+
 string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract)
 {
 	string prefix;

libsolidity/formal/CHC.h

@@ -70,6 +70,11 @@ public:
 	/// the constructor.
 	std::vector<std::string> unhandledQueries() const;
 
+	enum class CHCNatspecOption
+	{
+		AbstractFunctionNondet
+	};
+
 private:
 	/// Visitor functions.
 	//@{
@@ -123,6 +128,19 @@ private:
 	std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot);
 	//@}
 
+	/// SMT Natspec and abstraction helpers.
+	//@{
+	/// @returns a CHCNatspecOption enum if _option is a valid SMTChecker Natspec value
+	/// or nullopt otherwise.
+	static std::optional<CHCNatspecOption> natspecOptionFromString(std::string const& _option);
+	/// @returns which SMTChecker options are enabled by @a _function's Natspec via
+	/// `@custom:smtchecker <option>` or nullopt if none is used.
+	std::set<CHCNatspecOption> smtNatspecTags(FunctionDefinition const& _function);
+	/// @returns true if _function is Natspec annotated to be abstracted by
+	/// nondeterministic values.
+	bool abstractAsNondet(FunctionDefinition const& _function);
+	//@}
+
 	/// Sort helpers.
 	//@{
 	smtutil::SortPointer sort(FunctionDefinition const& _function);
@@ -183,6 +201,9 @@ private:
 	std::vector<smtutil::Expression> currentStateVariables();
 	std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract);
 
+	/// @returns \bigwedge currentValue(_vars[i]) == initialState(_var[i])
+	smtutil::Expression currentEqualInitialVarsConstraints(std::vector<VariableDeclaration const*> const& _vars) const;
+
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
 	/// @returns a predicate application after checking the predicate's type.

libsolidity/formal/SMTEncoder.cpp

@@ -2307,13 +2307,13 @@ void SMTEncoder::mergeVariables(smtutil::Expression const& _condition, VariableI
 	}
 }
 
-smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl)
+smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl) const
 {
 	solAssert(m_context.knownVariable(_decl), "");
 	return m_context.variable(_decl)->currentValue();
 }
 
-smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, unsigned _index)
+smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, unsigned _index) const
 {
 	solAssert(m_context.knownVariable(_decl), "");
 	return m_context.variable(_decl)->valueAtIndex(_index);

libsolidity/formal/SMTEncoder.h

@@ -314,10 +314,10 @@ protected:
 
 	/// @returns an expression denoting the value of the variable declared in @a _decl
 	/// at the current point.
-	smtutil::Expression currentValue(VariableDeclaration const& _decl);
+	smtutil::Expression currentValue(VariableDeclaration const& _decl) const;
 	/// @returns an expression denoting the value of the variable declared in @a _decl
 	/// at the given index. Does not ensure that this index exists.
-	smtutil::Expression valueAtIndex(VariableDeclaration const& _decl, unsigned _index);
+	smtutil::Expression valueAtIndex(VariableDeclaration const& _decl, unsigned _index) const;
 	/// Returns the expression corresponding to the AST node.
 	/// If _targetType is not null apply conversion.
 	/// Throws if the expression does not exist.