Merge pull request #11334 from ethereum/smt_abstract_function

[SMTChecker] Abstract function smtchecker natspec

Changelog.md

@@ -6,6 +6,7 @@ Language Features:
 
 
 Compiler Features:
+ * SMTChecker: Function definitions can be annotated with the custom Natspec tag ``custom:smtchecker abstract-function-nondet`` to be abstracted by a nondeterministic value when called.
  * Standard JSON / combined JSON: New artifact "functionDebugData" that contains bytecode offsets of entry points of functions and potentially more information in the future.
  * Yul Optimizer: Evaluate ``keccak256(a, c)``, when the value at memory location ``a`` is known at compile time and ``c`` is a constant ``<= 32``.
 

docs/smtchecker.rst

@@ -503,6 +503,18 @@ which has the following form:
 
 .. _smtchecker_engines:
 
+Natspec Function Abstraction
+============================
+
+Certain functions including common math methods such as ``pow``
+and ``sqrt`` may be too complex to be analyzed in a fully automated way.
+These functions can be annotated with Natspec tags that indicate to the
+SMTChecker that these functions should be abstracted. This means that the
+body of the function is not used, and when called, the function will:
+
+- Return a nondeterministic value, and either keep the state variables unchanged if the abstracted function is view/pure, or also set the state variables to nondeterministic values otherwise. This can be used via the annotation ``/// @custom:smtchecker abstract-function-nondet``.
+- Act as an uninterpreted function. This means that the semantics of the function (given by the body) are ignored, and the only property this function has is that given the same input it guarantees the same output. This is currently under development and will be available via the annotation ``/// @custom:smtchecker abstract-function-uf``.
+
 Model Checking Engines
 ======================
 

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 && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var);
+	conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_contract));
 
 	FunctionDefinition const* function = _function ? _function : _contract.constructor();
 	if (function)
-		for (auto var: function->parameters())
-			conj = conj && m_context.variable(*var)->valueAtIndex(0) == currentValue(*var);
+		conj = conj && currentEqualInitialVarsConstraints(applyMap(function->parameters(), [](auto&& _var) -> VariableDeclaration const* { return _var.get(); }));
 
 	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.

test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_1.sol

@@ -0,0 +1,17 @@
+contract C {
+	/// @custom:smtchecker abstract-function-nondet
+	function f(uint x) internal pure returns (uint) {
+		return x;
+	}
+	function g(uint y) public pure {
+		uint z = f(y);
+		// Generally holds, but here it doesn't because function
+		// `f` has been abstracted by nondeterministic values.
+		assert(z == y);
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (297-311): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol

@@ -0,0 +1,43 @@
+contract C {
+	function e(uint _e) public pure {
+		// Without abstracting function `pow` the solver
+		// fails to prove that `++i` does not overflow.
+		for (uint i = 0; i < _e; ++i)
+			pow(_e, _e);
+	}
+
+	function pow(uint base, uint exponent) internal pure returns (uint) {
+		if (base == 0) {
+			return 0;
+		}
+		if (exponent == 0) {
+			return 1;
+		}
+		if (exponent == 1) {
+			return base;
+		}
+		uint y = 1;
+		while(exponent > 1) {
+			if(exponent % 2 == 0) {
+				base = base * base;
+				exponent = exponent / 2;
+			} else {
+				y = base * y;
+				base = base * base;
+				exponent = (exponent - 1) / 2;
+			}
+		}
+		return base * y;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 4984: (176-179): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4281: (435-447): CHC: Division by zero might happen here.
+// Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4281: (495-507): CHC: Division by zero might happen here.
+// Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 3944: (579-591): CHC: Underflow (resulting value less than 0) might happen here.
+// Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_with_abstraction.sol

@@ -0,0 +1,35 @@
+contract C {
+	function e(uint _e) public pure {
+		// Without abstracting function `pow` the solver
+		// fails to prove that `++i` does not overflow.
+		for (uint i = 0; i < _e; ++i)
+			pow(_e, _e);
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function pow(uint base, uint exponent) internal pure returns (uint) {
+		if (base == 0) {
+			return 0;
+		}
+		if (exponent == 0) {
+			return 1;
+		}
+		if (exponent == 1) {
+			return base;
+		}
+		uint y = 1;
+		while(exponent > 1) {
+			if(exponent % 2 == 0) {
+				base = base * base;
+				exponent = exponent / 2;
+			} else {
+				y = base * y;
+				base = base * base;
+				exponent = (exponent - 1) / 2;
+			}
+		}
+		return base * y;
+	}
+}
+// ====
+// SMTEngine: chc

test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_empty.sol

@@ -0,0 +1,11 @@
+contract C {
+	/// @custom:smtchecker
+	function f(uint x) internal pure returns (uint) {
+		return x;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 3130: (38-102): Unknown option for "custom:smtchecker": ""
+// Warning 3130: (38-102): Unknown option for "custom:smtchecker": ""

test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_error_1.sol

@@ -0,0 +1,11 @@
+contract C {
+	/// @custom:smtchecker abstract-function
+	function f(uint x) internal pure returns (uint) {
+		return x;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function"
+// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function"

test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive.sol

@@ -0,0 +1,32 @@
+contract C {
+	uint x;
+	uint y;
+
+	function g(uint _x) public {
+		f1(_x);
+		// If the body of function `f` is ignored while keeping the state,
+		// the assertion is true and not reporting it would be a false negative.
+		// However, since `f` can change the state, the state variables are also
+		// assigned nondeterministic values after a call to `f`.
+		// Therefore the assertion below should fail.
+		assert(x == 0);
+
+		f2(_x);
+		assert(y == 0); // should fail
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function f1(uint _x) internal {
+		x = _x;
+	}
+
+	function f2(uint _y) internal {
+		y = _y;
+	}
+
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 6328: (400-414): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call
+// Warning 6328: (429-443): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 1\n_x = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n    C.f1(1) -- internal call\n    C.f2(1) -- internal call

test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol

@@ -0,0 +1,29 @@
+contract C {
+	uint x;
+	uint y;
+
+	function g(uint _x) public {
+		uint z = f1(_x);
+		assert(x == 0); // should hold because f1 is pure
+		assert(z == _x); // should hold but f1 was abstracted as nondet, so it fails
+
+		uint t = f2(_x);
+		assert(y == 0); // should hold because f1 is pure and f2 is view
+		assert(t == _x); // should hold
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function f1(uint _x) internal pure returns (uint) {
+		return _x;
+	}
+
+	function f2(uint _y) internal view returns (uint) {
+		return _y;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 2018: (33-335): Function state mutability can be restricted to view
+// Warning 2018: (457-524): Function state mutability can be restricted to pure
+// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\nz = 1\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call

test/libsolidity/smtCheckerTests/natspec/unsafe_assert_remains_unsafe.sol

@@ -0,0 +1,27 @@
+contract C {
+	uint x;
+	uint y;
+
+	function g(uint _x) public {
+		f1(_x);
+		assert(x > 0); // should fail
+
+		f2(_x);
+		assert(y > 0); // should fail
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function f1(uint _x) internal {
+		x = _x;
+	}
+
+	function f2(uint _y) internal {
+		y = _y;
+	}
+
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 6328: (74-87): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call
+// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call\n    C.f2(0) -- internal call

test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol

@@ -14,7 +14,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (134-140): CHC: Error trying to invoke SMT solver.
 // Warning 4984: (134-140): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (143-146): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 2661: (134-140): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/types/array_literal_7.sol

@@ -18,6 +18,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (226-254): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f()
-// Warning 6328: (315-335): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f()
+// Warning 6328: (226-254): CHC: Assertion violation happens here.
+// Warning 6328: (315-335): CHC: Assertion violation happens here.