Merge pull request #12167 from ethereum/smt_merge_query_entry_points

[SMTChecker] Merge all entry points for a target

libsolidity/formal/CHC.cpp

@@ -1623,28 +1623,23 @@ void CHC::checkVerificationTargets()
 	// Also, all possible contexts in which an external function can be called has been recorded (m_queryPlaceholders).
 	// Here we combine every context in which an external function can be called with all possible verification conditions
 	// in its call graph. Each such combination forms a unique verification target.
-	vector<CHCVerificationTarget> verificationTargets;
+	map<unsigned, vector<CHCQueryPlaceholder>> targetEntryPoints;
 	for (auto const& [function, placeholders]: m_queryPlaceholders)
 	{
 		auto functionTargets = transactionVerificationTargetsIds(function);
 		for (auto const& placeholder: placeholders)
 			for (unsigned id: functionTargets)
-			{
-				auto const& target = m_verificationTargets.at(id);
-				verificationTargets.push_back(CHCVerificationTarget{
-					{target.type, placeholder.fromPredicate, placeholder.constraints && placeholder.errorExpression == target.errorId},
-					target.errorId,
-					target.errorNode
-				});
-			}
+				targetEntryPoints[id].push_back(placeholder);
 	}
 
 	set<unsigned> checkedErrorIds;
-	for (auto const& target: verificationTargets)
+	for (auto const& [targetId, placeholders]: targetEntryPoints)
 	{
 		string errorType;
 		ErrorId errorReporterId;
 
+		auto const& target = m_verificationTargets.at(targetId);
+
 		if (target.type == VerificationTargetType::PopEmptyArray)
 		{
 			solAssert(dynamic_cast<FunctionCall const*>(target.errorNode), "");
@@ -1692,7 +1687,7 @@ void CHC::checkVerificationTargets()
 		else
 			solAssert(false, "");
 
-		checkAndReportTarget(target, errorReporterId, errorType + " happens here.", errorType + " might happen here.");
+		checkAndReportTarget(target, placeholders, errorReporterId, errorType + " happens here.", errorType + " might happen here.");
 		checkedErrorIds.insert(target.errorId);
 	}
 
@@ -1750,7 +1745,7 @@ void CHC::checkVerificationTargets()
 		{
 			set<unsigned> seenErrors;
 			msg += "<errorCode> = 0 -> no errors\n";
-			for (auto const& target: verificationTargets)
+			for (auto const& [id, target]: m_verificationTargets)
 				if (!seenErrors.count(target.errorId))
 				{
 					seenErrors.insert(target.errorId);
@@ -1785,6 +1780,7 @@ void CHC::checkVerificationTargets()
 
 void CHC::checkAndReportTarget(
 	CHCVerificationTarget const& _target,
+	vector<CHCQueryPlaceholder> const& _placeholders,
 	ErrorId _errorReporterId,
 	string _satMsg,
 	string _unknownMsg
@@ -1794,7 +1790,12 @@ void CHC::checkAndReportTarget(
 		return;
 
 	createErrorBlock();
-	connectBlocks(_target.value, error(), _target.constraints);
+	for (auto const& placeholder: _placeholders)
+		connectBlocks(
+			placeholder.fromPredicate,
+			error(),
+			placeholder.constraints && placeholder.errorExpression == _target.errorId
+		);
 	auto const& location = _target.errorNode->location();
 	auto [result, invariant, model] = query(error(), location);
 	if (result == CheckResult::UNSATISFIABLE)

libsolidity/formal/CHC.h

@@ -252,11 +252,13 @@ private:
 	void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTargetType _type, smtutil::Expression const& _errorCondition);
 
 	void checkVerificationTargets();
-	// Forward declaration. Definition is below.
+	// Forward declarations. Definitions are below.
 	struct CHCVerificationTarget;
+	struct CHCQueryPlaceholder;
 	void checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target);
 	void checkAndReportTarget(
 		CHCVerificationTarget const& _target,
+		std::vector<CHCQueryPlaceholder> const& _placeholders,
 		langutil::ErrorId _errorReporterId,
 		std::string _satMsg,
 		std::string _unknownMsg = ""

test/cmdlineTests/model_checker_invariants_all/err

@@ -7,7 +7,6 @@ Warning: Return value of low-level calls not used.
 Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
 (x <= 0)
 Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
-(!(x <= 0) || (x' <= 0))
 ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
 ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
 <errorCode> = 0 -> no errors

test/cmdlineTests/model_checker_invariants_contract_reentrancy/err

@@ -7,7 +7,6 @@ Warning: Return value of low-level calls not used.
 Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
 (x <= 0)
 Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
-(!(x <= 0) || (x' <= 0))
 ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
 ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
 <errorCode> = 0 -> no errors

test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json

@@ -7,7 +7,6 @@
 ","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
 (x <= 0)
 Reentrancy property(ies) for A:test:
-(!(x <= 0) || (x' <= 0))
 ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
 ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
 <errorCode> = 0 -> no errors
@@ -18,7 +17,6 @@ Reentrancy property(ies) for A:test:
 ","message":"Contract invariant(s) for A:test:
 (x <= 0)
 Reentrancy property(ies) for A:test:
-(!(x <= 0) || (x' <= 0))
 ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
 ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
 <errorCode> = 0 -> no errors

test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol

@@ -25,8 +25,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreInv: yes
 // ----
 // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (302-333): CHC: Assertion violation might happen here.
-// Info 1180: Contract invariant(s) for :C:\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\nReentrancy property(ies) for :C:\n((!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)))\n((!(<errorCode> = 1) || !((kec + ((- 1) * keccak256(data))) = 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)) && (!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(_kec == kec)\n<errorCode> = 2 -> Assertion failed at assert(kec == keccak256(_data))\n
 // Warning 4661: (302-333): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol

@@ -15,5 +15,5 @@ contract C is B {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n    B.f() -- internal call\nState: y = 0, x = 1\nB.f()
+// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n    B.f() -- internal call
 // Info 1180: Contract invariant(s) for :B:\n(x <= 0)\n

test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol

@@ -15,5 +15,4 @@ contract C is B {
 // ====
 // SMTEngine: all
 // SMTSolvers: z3
-// ----
-// Info 1180: Contract invariant(s) for :C:\n(!(x <= 1) && !(x >= 3))\n
+// SMTIgnoreInv: yes

test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol

@@ -25,4 +25,6 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 2072: (249-255): Unused local variable.
-// Warning 6328: (271-295): CHC: Assertion violation happens here.
+// Warning 1218: (271-295): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (271-295): CHC: Assertion violation might happen here.
+// Warning 4661: (271-295): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol

@@ -25,4 +25,4 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 2072: (255-261): Unused local variable.
-// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)))\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (!(x' >= 3) || ((x' + ((- 1) * x)) = 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
+// Info 1180: Reentrancy property(ies) for :C:\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (!(x' >= 3) || ((x' + ((- 1) * x)) = 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n