Merge pull request #11451 from ethereum/smt_report_invariants

[SMTChecker] Report contract invariants

Author: hrkrshnn

Changelog.md

@@ -9,6 +9,7 @@ Compiler Features:
  * Commandline Interface: Add ``--debug-info`` option for selecting how much extra debug information should be included in the produced EVM assembly and Yul code.
  * Commandline Interface: Use different colors when printing errors, warnings and infos.
  * SMTChecker: Output values for ``block.*``, ``msg.*`` and ``tx.*`` variables that are present in the called functions.
+ * SMTChecker: Report contract invariants and reentrancy properties. This can be enabled via the CLI option ``--model-checker-invariants`` or the Standard JSON option ``settings.modelChecker.invariants``.
  * Standard JSON: Accept nested brackets in step sequences passed to ``settings.optimizer.details.yulDetails.optimizerSteps``.
  * Standard JSON: Add ``settings.debug.debugInfo`` option for selecting how much extra debug information should be included in the produced EVM assembly and Yul code.
 

docs/smtchecker.rst

@@ -412,7 +412,7 @@ is already "locked", so it would not be possible to change the value of ``x``,
 regardless of what the unknown called code does.
 
 If we "forget" to use the ``mutex`` modifier on function ``set``, the
-SMTChecker is able to synthesize the behavior of the externally called code so
+SMTChecker is able to synthesize the behaviour of the externally called code so
 that the assertion fails:
 
 .. code-block:: text
@@ -518,6 +518,23 @@ which has the following form:
         "source2.sol": ["contract2", "contract3"]
     }
 
+Reported Inferred Inductive Invariants
+======================================
+
+For properties that were proved safe with the CHC engine,
+the SMTChecker can retrieve inductive invariants that were inferred by the Horn
+solver as part of the proof.
+Currently two types of invariants can be reported to the user:
+
+- Contract Invariants: these are properties over the contract's state variables
+  that are true before and after every possible transaction that the contract may ever run. For example, ``x >= y``, where ``x`` and ``y`` are a contract's state variables.
+- Reentrancy Properties: they represent the behavior of the contract
+  in the presence of external calls to unknown code. These properties can express a relation
+  between the value of the state variables before and after the external call, where the external call is free to do anything, including making reentrant calls to the analyzed contract. Primed variables represent the state variables' values after said external call. Example: ``lock -> x = x'``.
+
+The user can choose the type of invariants to be reported using the CLI option ``--model-checker-invariants "contract,reentrancy"`` or as an array in the field ``settings.modelChecker.invariants`` in the :ref:`JSON input<compiler-api>`.
+By default the SMTChecker does not report invariants.
+
 Division and Modulo With Slack Variables
 ========================================
 

docs/using-the-compiler.rst

@@ -418,6 +418,8 @@ Input Description
           "divModWithSlacks": true,
           // Choose which model checker engine to use: all (default), bmc, chc, none.
           "engine": "chc",
+          // Choose which types of invariants should be reported to the user: contract, reentrancy.
+          "invariants": ["contract", "reentrancy"],
           // Choose whether to output all unproved targets. The default is `false`.
           "showUnproved": true,
           // Choose which solvers should be used, if available.

liblangutil/ErrorReporter.cpp

@@ -261,3 +261,8 @@ void ErrorReporter::info(
 {
 	error(_error, Error::Type::Info, _location, _description);
 }
+
+void ErrorReporter::info(ErrorId _error, string const& _description)
+{
+	error(_error, Error::Type::Info, SourceLocation(), _description);
+}

liblangutil/ErrorReporter.h

@@ -72,6 +72,8 @@ class ErrorReporter
 		std::string const& _description
 	);
 
+	void info(ErrorId _error, std::string const& _description);
+
 	void declarationError(
 		ErrorId _error,
 		SourceLocation const& _location,

liblangutil/UniqueErrorReporter.h

@@ -61,6 +61,20 @@ class UniqueErrorReporter
 		m_errorReporter.warning(_error, _description);
 	}
 
+	void info(ErrorId _error, SourceLocation const& _location, std::string const& _description)
+	{
+		if (!seen(_error, _location, _description))
+		{
+			m_errorReporter.info(_error, _location, _description);
+			markAsSeen(_error, _location, _description);
+		}
+	}
+
+	void info(ErrorId _error, std::string const& _description)
+	{
+		m_errorReporter.info(_error, _description);
+	}
+
 	bool seen(ErrorId _error, SourceLocation const& _location, std::string const& _description) const
 	{
 		if (m_seenErrors.count({_error, _location}))

libsmtutil/CHCSmtLib2Interface.cpp

@@ -87,7 +87,7 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*
 	);
 }
 
-pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
+tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
 {
 	string accumulated{};
 	swap(m_accumulatedOutput, accumulated);
@@ -118,8 +118,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
 	else
 		result = CheckResult::ERROR;
 
-	// TODO collect invariants or counterexamples.
-	return {result, {}};
+	return {result, Expression(true), {}};
 }
 
 void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)

libsmtutil/CHCSmtLib2Interface.h

@@ -44,7 +44,9 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 
 	void addRule(Expression const& _expr, std::string const& _name) override;
 
-	std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
+	/// Takes a function application _expr and checks for reachability.
+	/// @returns solving result, an invariant, and counterexample graph, if possible.
+	std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
 
 	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
 

libsmtutil/CHCSolverInterface.h

@@ -54,8 +54,8 @@ class CHCSolverInterface
 	};
 
 	/// Takes a function application _expr and checks for reachability.
-	/// @returns solving result and a counterexample graph, if possible.
-	virtual std::pair<CheckResult, CexGraph> query(
+	/// @returns solving result, an invariant, and counterexample graph, if possible.
+	virtual std::tuple<CheckResult, Expression, CexGraph> query(
 		Expression const& _expr
 	) = 0;
 

libsmtutil/SolverInterface.h

@@ -23,7 +23,9 @@
 
 #include <libsolutil/Common.h>
 #include <libsolutil/Numeric.h>
+#include <libsolutil/CommonData.h>
 
+#include <range/v3/algorithm/all_of.hpp>
 #include <range/v3/view.hpp>
 
 #include <cstdio>
@@ -305,6 +307,64 @@ class Expression
 		);
 	}
 
+	static bool sameSort(std::vector<Expression> const& _args)
+	{
+		if (_args.empty())
+			return true;
+
+		auto sort = _args.front().sort;
+		return ranges::all_of(
+			_args,
+			[&](auto const& _expr){ return _expr.sort->kind == sort->kind; }
+		);
+	}
+
+	static Expression mkAnd(std::vector<Expression> _args)
+	{
+		smtAssert(!_args.empty(), "");
+		smtAssert(sameSort(_args), "");
+
+		auto sort = _args.front().sort;
+		if (sort->kind == Kind::BitVector)
+			return Expression("bvand", std::move(_args), sort);
+
+		smtAssert(sort->kind == Kind::Bool, "");
+		return Expression("and", std::move(_args), Kind::Bool);
+	}
+
+	static Expression mkOr(std::vector<Expression> _args)
+	{
+		smtAssert(!_args.empty(), "");
+		smtAssert(sameSort(_args), "");
+
+		auto sort = _args.front().sort;
+		if (sort->kind == Kind::BitVector)
+			return Expression("bvor", std::move(_args), sort);
+
+		smtAssert(sort->kind == Kind::Bool, "");
+		return Expression("or", std::move(_args), Kind::Bool);
+	}
+
+	static Expression mkPlus(std::vector<Expression> _args)
+	{
+		smtAssert(!_args.empty(), "");
+		smtAssert(sameSort(_args), "");
+
+		auto sort = _args.front().sort;
+		smtAssert(sort->kind == Kind::BitVector || sort->kind == Kind::Int, "");
+		return Expression("+", std::move(_args), sort);
+	}
+
+	static Expression mkMul(std::vector<Expression> _args)
+	{
+		smtAssert(!_args.empty(), "");
+		smtAssert(sameSort(_args), "");
+
+		auto sort = _args.front().sort;
+		smtAssert(sort->kind == Kind::BitVector || sort->kind == Kind::Int, "");
+		return Expression("*", std::move(_args), sort);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		if (_a.sort->kind == Kind::BitVector)