[SMTChecker] Synthesize untrusted functions called externally

Changelog.md

@@ -12,6 +12,7 @@ Compiler Features:
  * SMTChecker: Show contract name in counterexample function call.
  * 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.
 
 Bugfixes:
  * Code Generator: Fix length check when decoding malformed error data in catch clause.

libsolidity/formal/CHC.cpp

@@ -676,6 +676,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
 		function->stateMutability() == StateMutability::Pure ||
 		function->stateMutability() == StateMutability::View;
+
 	if (!usesStaticCall)
 	{
 		state().newState();
@@ -683,13 +684,23 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 			m_context.variable(*var)->increaseIndex();
 	}
 
-	auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
 	auto error = errorFlag().increaseIndex();
+
+	Predicate const& callPredicate = *createSymbolicBlock(
+		nondetInterfaceSort(*m_currentContract, state()),
+		"nondet_call_" + uniquePrefix(),
+		PredicateType::ExternalCallUntrusted,
+		&_funCall
+	);
+	auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
 	vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
+
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
-	// TODO this could instead add the summary of the called function, where that summary
+	auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
-	// basically has the nondet interface of this summary as a constraint.
+
-	m_context.addAssertion(nondet);
+	addRule(smtutil::Expression::implies(nondet, nondetCall), nondetCall.name);
+
+	m_context.addAssertion(nondetCall);
 	solAssert(m_errorDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0);
 	// To capture the possibility of a reentrant call, we record in the call graph that the  current function
@@ -1179,7 +1190,8 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 		return constructor(_block, m_context);
 	case PredicateType::FunctionSummary:
 	case PredicateType::InternalCall:
-	case PredicateType::ExternalCall:
+	case PredicateType::ExternalCallTrusted:
+	case PredicateType::ExternalCallUntrusted:
 		return smt::function(_block, m_currentContract, m_context);
 	case PredicateType::FunctionBlock:
 		solAssert(m_currentFunction, "");
@@ -1256,7 +1268,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	Predicate const& callPredicate = *createSummaryBlock(
 		*function,
 		*calledContract,
-		kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCall
+		kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
 	);
 	auto to = smt::function(callPredicate, calledContract, m_context);
 	addRule(smtutil::Expression::implies(from, to), to.name);
@@ -1561,19 +1573,30 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
 
 		list<string> calls;
-		auto dfs = [&](unsigned node, unsigned depth, auto&& _dfs) -> void {
+		auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void {
 			auto pred = nodePred(node);
+			auto parentPred = nodePred(parent);
 			solAssert(pred && pred->isSummary(), "");
+			solAssert(parentPred && parentPred->isSummary(), "");
+			auto callTraceSize = calls.size();
 			if (!pred->isConstructorSummary())
 				for (unsigned v: callGraph[node])
-					_dfs(v, depth + 1, _dfs);
+					_dfs(node, v, depth + 1, _dfs);
-			calls.push_front(string(depth * 2, ' ') + pred->formatSummaryCall(nodeArgs(node)));
+			calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node)));
 			if (pred->isInternalCall())
 				calls.front() += " -- internal call";
-			else if (pred->isExternalCall())
+			else if (pred->isExternalCallTrusted())
-				calls.front() += " -- external call";
+				calls.front() += " -- trusted external call";
+			else if (pred->isExternalCallUntrusted())
+			{
+				calls.front() += " -- untrusted external call";
+				if (calls.size() > callTraceSize + 1)
+					calls.front() += ", synthesized as:";
+			}
+			else if (pred->isFunctionSummary() && parentPred->isExternalCallUntrusted())
+				calls.front() += " -- reentrant call";
 		};
-		dfs(summaryId, 0, dfs);
+		dfs(summaryId, summaryId, 0, dfs);
 		path.emplace_back(boost::algorithm::join(calls, "\n"));
 	}
 
@@ -1596,7 +1619,14 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
 		q.pop();
 
 		Predicate const* nodePred = Predicate::predicate(_graph.nodes.at(node).name);
-		if (nodePred->isSummary() && (_root == root || nodePred->isInternalCall() || nodePred->isExternalCall()))
+		Predicate const* rootPred = Predicate::predicate(_graph.nodes.at(root).name);
+		if (nodePred->isSummary() && (
+			_root == root ||
+			nodePred->isInternalCall() ||
+			nodePred->isExternalCallTrusted() ||
+			nodePred->isExternalCallUntrusted() ||
+			rootPred->isExternalCallUntrusted()
+		))
 		{
 			calls[root].push_back(node);
 			root = node;

libsolidity/formal/Predicate.cpp

@@ -121,6 +121,11 @@ FunctionDefinition const* Predicate::programFunction() const
 	return nullptr;
 }
 
+FunctionCall const* Predicate::programFunctionCall() const
+{
+	return dynamic_cast<FunctionCall const*>(m_node);
+}
+
 optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
 {
 	if (auto const* fun = programFunction())
@@ -141,7 +146,11 @@ optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
 
 bool Predicate::isSummary() const
 {
-	return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary || m_type == PredicateType::InternalCall || m_type == PredicateType::ExternalCall;
+	return isFunctionSummary() ||
+		isInternalCall() ||
+		isExternalCallTrusted() ||
+		isExternalCallUntrusted() ||
+		isConstructorSummary();
 }
 
 bool Predicate::isFunctionSummary() const
@@ -154,9 +163,14 @@ bool Predicate::isInternalCall() const
 	return m_type == PredicateType::InternalCall;
 }
 
-bool Predicate::isExternalCall() const
+bool Predicate::isExternalCallTrusted() const
 {
-	return m_type == PredicateType::ExternalCall;
+	return m_type == PredicateType::ExternalCallTrusted;
+}
+
+bool Predicate::isExternalCallUntrusted() const
+{
+	return m_type == PredicateType::ExternalCallUntrusted;
 }
 
 bool Predicate::isConstructorSummary() const
@@ -171,10 +185,13 @@ bool Predicate::isInterface() const
 
 string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) const
 {
+	solAssert(isSummary(), "");
+
 	if (auto contract = programContract())
 		return contract->name() + ".constructor()";
 
-	solAssert(isSummary(), "");
+	if (auto funCall = programFunctionCall())
+		return funCall->location().text();
 
 	auto stateVars = stateVariables();
 	solAssert(stateVars.has_value(), "");

libsolidity/formal/Predicate.h

@@ -38,7 +38,8 @@ enum class PredicateType
 	FunctionSummary,
 	FunctionBlock,
 	InternalCall,
-	ExternalCall,
+	ExternalCallTrusted,
+	ExternalCallUntrusted,
 	Error,
 	Custom
 };
@@ -94,6 +95,10 @@ public:
 	/// or nullptr otherwise.
 	FunctionDefinition const* programFunction() const;
 
+	/// @returns the FunctionCall that this predicate represents
+	/// or nullptr otherwise.
+	FunctionCall const* programFunctionCall() const;
+
 	/// @returns the program state variables in the scope of this predicate.
 	std::optional<std::vector<VariableDeclaration const*>> stateVariables() const;
 
@@ -106,8 +111,11 @@ public:
 	/// @returns true if this predicate represents an internal function call.
 	bool isInternalCall() const;
 
-	/// @returns true if this predicate represents an external function call.
+	/// @returns true if this predicate represents a trusted external function call.
-	bool isExternalCall() const;
+	bool isExternalCallTrusted() const;
+
+	/// @returns true if this predicate represents an untrusted external function call.
+	bool isExternalCallUntrusted() const;
 
 	/// @returns true if this predicate represents a constructor summary.
 	bool isConstructorSummary() const;

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol

@@ -34,4 +34,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 1, y = 0, z = 0, s = 0\nC.f()
+// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 1, y = 0, z = 0, s = 0\nC.f()\n    s.f() -- untrusted external call\n    s.f() -- untrusted external call, synthesized as:\n        C.inv() -- reentrant call

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -29,4 +29,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()
+// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()\n    s.f() -- untrusted external call

test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol

@@ -16,4 +16,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (239-253): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)
+// Warning 6328: (239-253): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)\n    D(target).e() -- untrusted external call, synthesized as:\n        C.broken() -- reentrant call

test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)
+// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)\n    D(target).e() -- untrusted external call, synthesized as:\n        C.call(0) -- reentrant call

test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol

@@ -28,4 +28,4 @@ contract C is A {
 }
 // ----
 // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
-// Warning 6328: (385-399): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.call(0)
+// Warning 6328: (385-399): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.call(0)\n    d.d() -- untrusted external call, synthesized as:\n        C.f() -- reentrant call

test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol

@@ -27,4 +27,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, d = 0, lock = false\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0, lock = false\nC.f()
+// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, d = 0, lock = false\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0, lock = false\nC.f()\n    d.d() -- untrusted external call, synthesized as:\n        C.set(1) -- reentrant call

test/libsolidity/smtCheckerTests/functions/functions_external_4.sol

@@ -16,4 +16,4 @@ contract D
 	}
 }
 // ----
-// Warning 6328: (191-206): CHC: Assertion violation happens here.\nCounterexample:\nc = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: c = 0\nD.g(0)
+// Warning 6328: (191-206): CHC: Assertion violation happens here.\nCounterexample:\nc = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: c = 0\nD.g(0)\n    c.f(_y) -- untrusted external call

test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol

@@ -13,4 +13,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (141-156): CHC: Assertion violation happens here.\nCounterexample:\na = 42\nx = 42\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.f(42)\n  C.g(42) -- external call
+// Warning 6328: (141-156): CHC: Assertion violation happens here.\nCounterexample:\na = 42\nx = 42\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.f(42)\n    C.g(42) -- trusted external call

test/libsolidity/smtCheckerTests/imports/import_base.sol

@@ -17,9 +17,11 @@ contract Der is Base {
 		assert(y > x);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 4984: (der:101-109): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (der:113-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 3, a = 7\ny = 0\n\nTransaction trace:\nDer.constructor()\nState: x = 0, a = 0\nDer.g(0)\n  Base.f() -- internal call
+// Warning 6328: (der:113-126): CHC: Assertion violation happens here.
 // Warning 4984: (base:100-103): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (der:101-109): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol

@@ -24,4 +24,4 @@ contract C {
 }
 // ----
 // Warning 2072: (282-288): Unused local variable.
-// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = false, x = 0, d = 0\nC.g()\n  C.g() -- internal call
+// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = false, x = 0, d = 0\nC.g()\n    d.d() -- untrusted external call, synthesized as:\n        C.f() -- reentrant call\n            C.g() -- internal call\n                d.d() -- untrusted external call, synthesized as:\n                    C.h() -- reentrant call

test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol

@@ -5,6 +5,8 @@ contract C  {
 		return x * y;
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.\nCounterexample:\n\nx = (- 3)\ny = 19298681539552699237261830834781317975544997444273427339909597334652188273323\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 3), 19298681539552699237261830834781317975544997444273427339909597334652188273323)
+// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.
-// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 1)\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 1), (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))
+// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.

test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol

@@ -22,6 +22,6 @@ contract C {
 }
 // ----
 // Warning 2519: (197-203): This declaration shadows an existing declaration.
-// Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n    d.d() -- untrusted external call
-// Warning 6328: (306-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 6328: (306-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n    d.d() -- untrusted external call
 // Warning 6328: (426-440): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol

@@ -14,4 +14,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (278-338): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n  C.g() -- external call
+// Warning 6328: (278-338): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n    C.g() -- trusted external call

test/libsolidity/smtCheckerTests/types/address_staticcall.sol

@@ -17,6 +17,7 @@ contract C
 }
 // ====
 // EVMVersion: >spuriousDragon
+// SMTIgnoreCex: yes
 // ----
 // Warning 2072: (224-240): Unused local variable.
-// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 14, 7, 7, 7, 19, 7, 7, 7, 7, 7, 7, 7, 27, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 14, 7, 7, 7, 19, 7, 7, 7, 7, 7, 7, 7, 27, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7])
+// Warning 6328: (266-281): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/address_transfer_2.sol

@@ -13,7 +13,9 @@ contract C
 		assert(a.balance > b.balance);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 39\nb = 38\n\nTransaction trace:\nC.constructor()\nC.f(100, 39, 38)
+// Warning 6328: (295-324): CHC: Assertion violation happens here.
 // Warning 1236: (217-232): BMC: Insufficient funds happens here.
 // Warning 1236: (236-251): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol

@@ -14,5 +14,7 @@ contract C {
 		assert(s1.x == s2.x);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (225-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, a: []}\ns2 = {x: 3, a: [5, 5, 5, 5, 5, 5]}\n\nTransaction trace:\nC.constructor()\nC.f({x: 0, a: []}, {x: 3, a: [5, 5, 5, 5, 5, 5]})
+// Warning 6328: (225-245): CHC: Assertion violation happens here.