Merge pull request #10828 from ethereum/smt_cex_value

[SMTChecker] Add msgvalue to cex if > 0

Changelog.md

@@ -16,6 +16,7 @@ Compiler Features:
  * SMTChecker: Support try/catch statements.
  * SMTChecker: Output internal and trusted external function calls in a counterexample's transaction trace.
  * SMTChecker: Synthesize untrusted functions called externally.
+ * SMTChecker: Show ``msg.value`` in counterexample transaction traces when greater than 0.
  * Standard JSON: New option ``modelCheckerSettings.targets`` allows specifying which targets should be checked. The valid options are ``all``, ``constantCondition``,
    ``underflow``, ``overflow``, ``divByZero``, ``balance``, ``assert``, ``popEmptyArray``, where the default is ``all``. Multiple targets can be chosen at the same time,
    separated by a comma without spaces: ``underflow,overflow,assert``.

libsolidity/formal/Predicate.cpp

@@ -21,8 +21,10 @@
 #include <libsolidity/formal/SMTEncoder.h>
 
 #include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/TypeProvider.h>
 
 #include <boost/algorithm/string/join.hpp>
+#include <range/v3/view.hpp>
 #include <utility>
 
 using namespace std;
@@ -187,19 +189,29 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
 {
 	solAssert(isSummary(), "");
 
-	if (auto contract = programContract())
-		return contract->name() + ".constructor()";
-
 	if (auto funCall = programFunctionCall())
 		return funCall->location().text();
 
+	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// Here we are interested in preInputVars to format the function call,
+	/// and in txData to retrieve `msg.value`.
+
+	string value;
+	if (auto v = readTxVars(_args.at(4)).at("msg.value"))
+	{
+		bigint x(*v);
+		if (x > 0)
+			value = "{ value: " + *v + " }";
+	}
+
+	if (auto contract = programContract())
+		return contract->name() + ".constructor()" + value;
+
 	auto stateVars = stateVariables();
 	solAssert(stateVars.has_value(), "");
 	auto const* fun = programFunction();
 	solAssert(fun, "");
 
-	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
-	/// Here we are interested in preInputVars.
 	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size());
 	auto last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -221,7 +233,7 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
 		fun->isReceive() ? "receive" :
 		fun->name();
 	solAssert(fun->annotation().contract, "");
-	return fun->annotation().contract->name() + "." + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
+	return fun->annotation().contract->name() + "." + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + value;
 
 }
 
@@ -336,7 +348,9 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
 	if (smt::isArray(*_type))
 	{
 		auto const& arrayType = dynamic_cast<ArrayType const&>(*_type);
-		solAssert(_expr.name == "tuple_constructor", "");
+		if (_expr.name != "tuple_constructor")
+			return {};
+
 		auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
 		solAssert(tupleSort.components.size() == 2, "");
 
@@ -446,3 +460,26 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
 
 	solAssert(false, "");
 }
+
+map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _tx) const
+{
+	map<string, TypePointer> const txVars{
+		{"block.chainid", TypeProvider::uint256()},
+		{"block.coinbase", TypeProvider::address()},
+		{"block.difficulty", TypeProvider::uint256()},
+		{"block.gaslimit", TypeProvider::uint256()},
+		{"block.number", TypeProvider::uint256()},
+		{"block.timestamp", TypeProvider::uint256()},
+		{"blockhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
+		{"msg.data", TypeProvider::bytesMemory()},
+		{"msg.sender", TypeProvider::address()},
+		{"msg.sig", TypeProvider::uint256()},
+		{"msg.value", TypeProvider::uint256()},
+		{"tx.gasprice", TypeProvider::uint256()},
+		{"tx.origin", TypeProvider::address()}
+	};
+	map<string, optional<string>> vars;
+	for (auto&& [i, v]: txVars | ranges::views::enumerate)
+		vars.emplace(v.first, expressionToString(_tx.arguments.at(i), v.second));
+	return vars;
+}

libsolidity/formal/Predicate.h

@@ -154,6 +154,8 @@ class Predicate
 	/// and false if at least one element could not be built.
 	bool fillArray(smtutil::Expression const& _expr, std::vector<std::string>& _array, ArrayType const& _type) const;
 
+	std::map<std::string, std::optional<std::string>> readTxVars(smtutil::Expression const& _tx) const;
+
 	/// The actual SMT expression.
 	smt::SymbolicFunctionVariable m_predicate;
 

libsolidity/formal/SymbolicState.cpp

@@ -128,19 +128,23 @@ smtutil::Expression SymbolicState::txMember(string const& _member) const
 
 smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _function) const
 {
-	smtutil::Expression conj = smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::uint(160)) &&
-		smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
+	smtutil::Expression conj = smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::address()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.difficulty"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.number"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.timestamp"), TypeProvider::uint256()) &&
-		smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::uint(160)) &&
-		smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::uint(160));
+		smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::address()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("msg.value"), TypeProvider::uint256()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::address()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("tx.gasprice"), TypeProvider::uint256());
 
 	if (_function.isPartOfExternalInterface())
 	{
 		auto sig = TypeProvider::function(_function)->externalIdentifier();
 		conj = conj && m_tx.member("msg.sig") == sig;
+		if (!_function.isPayable())
+			conj = conj && m_tx.member("msg.value") == 0;
 
 		auto b0 = sig >> (3 * 8);
 		auto b1 = (sig & 0x00ff0000) >> (2 * 8);

libsolidity/formal/SymbolicState.h

@@ -189,13 +189,13 @@ class SymbolicState
 	BlockchainVariable m_tx{
 		"tx",
 		{
-			{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
 			{"block.chainid", smtutil::SortProvider::uintSort},
 			{"block.coinbase", smt::smtSort(*TypeProvider::address())},
 			{"block.difficulty", smtutil::SortProvider::uintSort},
 			{"block.gaslimit", smtutil::SortProvider::uintSort},
 			{"block.number", smtutil::SortProvider::uintSort},
 			{"block.timestamp", smtutil::SortProvider::uintSort},
+			{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
 			// TODO gasleft
 			{"msg.data", smt::smtSort(*TypeProvider::bytesMemory())},
 			{"msg.sender", smt::smtSort(*TypeProvider::address())},

test/cmdlineTests/standard_model_checker_engine_bmc/output.json

@@ -1,4 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x058094a9af015b518e634e27c9b42140d8b77dd0f915986a1e2fbed694cdb7de":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x1b0b95f75c7c1f14af97d9682c4b88edc51efc5b3bb09e7fd6f39bc6274879d7":"(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -17,7 +17,7 @@
 (declare-fun |expr_9_0| () Int)
 (declare-fun |expr_10_1| () Bool)
 
-(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (implies (and true true) true) (and (= expr_9_0 0) (and (implies (and true true) (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))) (not expr_10_1)))
+(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (implies (and true true) true) (and (= expr_9_0 0) (and (implies (and true true) (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 3017696395)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))) (not expr_10_1)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (check-sat)