SMTChecker: add insufficient funds verification target for CHC engine

ethereum · May 14, 2024 · f0c8c93 · f0c8c93
1 parent ff81bac
commit f0c8c93
Show file tree

Hide file tree

Showing 26 changed files with 124 additions and 91 deletions.
diff --git a/Changelog.md b/Changelog.md
@@ -5,7 +5,7 @@ Language Features:
 
 
 Compiler Features:
-
+* SMTChecker: Create balance check verification target for CHC engine.
 
 Bugfixes:
  * Commandline Interface: Fix ICE when the optimizer is disabled and an empty/blank string is used for ``--yul-optimizations`` sequence.

diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
@@ -1050,6 +1050,12 @@ void BMC::checkDivByZero(BMCVerificationTarget& _target)
 void BMC::checkBalance(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTargetType::Balance, "");
+
+	if (
+		m_solvedTargets.count(_target.expression) &&
+		m_solvedTargets.at(_target.expression).count(VerificationTargetType::Balance)
+	)
+		return;
 	checkCondition(
 		_target,
 		_target.constraints && _target.value,

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
@@ -607,6 +607,22 @@ void CHC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		unknownFunctionCall(_funCall);
 		break;
+	case FunctionType::Kind::Send:
+	case FunctionType::Kind::Transfer:
+	{
+		auto value = _funCall.arguments().front();
+		solAssert(value, "");
+		smtutil::Expression thisBalance = state().balance();
+
+		verificationTargetEncountered(
+			&_funCall,
+			VerificationTargetType::Balance,
+			thisBalance < expr(*value)
+		);
+
+		SMTEncoder::endVisit(_funCall);
+		break;
+	}
 	case FunctionType::Kind::KECCAK256:
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
@@ -2013,6 +2029,8 @@ std::pair<std::string, ErrorId> CHC::targetDescription(CHCVerificationTarget con
 		return {"Division by zero", 4281_error};
 	else if (_target.type == VerificationTargetType::Assert)
 		return {"Assertion violation", 6328_error};
+	else if (_target.type == VerificationTargetType::Balance)
+		return {"Insufficient funds", 8656_error};
 	else
 		solAssert(false);
 }

diff --git a/test/cmdlineTests/model_checker_targets_all_all_engines/err b/test/cmdlineTests/model_checker_targets_all_all_engines/err
@@ -88,21 +88,11 @@ test.f(0x0, 1)
 13 | 		arr[x];
    | 		^^^^^^
 
+Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+
 Warning: BMC: Condition is always true.
  --> model_checker_targets_all_all_engines/input.sol:6:11:
   |
 6 | 		require(x >= 0);
   | 		        ^^^^^^
 Note: Callstack:
-
-Warning: BMC: Insufficient funds happens here.
-  --> model_checker_targets_all_all_engines/input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
diff --git a/test/cmdlineTests/model_checker_targets_all_chc/err b/test/cmdlineTests/model_checker_targets_all_chc/err
@@ -87,3 +87,5 @@ test.f(0x0, 1)
    |
 13 | 		arr[x];
    | 		^^^^^^
+
+Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/cmdlineTests/model_checker_targets_balance_chc/err b/test/cmdlineTests/model_checker_targets_balance_chc/err
@@ -0,0 +1 @@
+Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/cmdlineTests/model_checker_targets_default_all_engines/err b/test/cmdlineTests/model_checker_targets_default_all_engines/err
@@ -58,21 +58,11 @@ test.f(0x0, 1)
 13 | 		arr[x];
    | 		^^^^^^
 
+Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+
 Warning: BMC: Condition is always true.
  --> model_checker_targets_default_all_engines/input.sol:6:11:
   |
 6 | 		require(x >= 0);
   | 		        ^^^^^^
 Note: Callstack:
-
-Warning: BMC: Insufficient funds happens here.
-  --> model_checker_targets_default_all_engines/input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
diff --git a/test/cmdlineTests/model_checker_targets_default_chc/err b/test/cmdlineTests/model_checker_targets_default_chc/err
@@ -57,3 +57,5 @@ test.f(0x0, 1)
    |
 13 | 		arr[x];
    | 		^^^^^^
+
+Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json
@@ -1,4 +1,16 @@
 {
+    "errors": [
+        {
+            "component": "general",
+            "errorCode": "1391",
+            "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.
+
+",
+            "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.",
+            "severity": "info",
+            "type": "Info"
+        }
+    ],
     "sources": {
         "A": {
             "id": 0

diff --git a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json
@@ -148,6 +148,16 @@ test.f(0x0, 1)",
             },
             "type": "Warning"
         },
+        {
+            "component": "general",
+            "errorCode": "1391",
+            "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.
+
+",
+            "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.",
+            "severity": "info",
+            "type": "Info"
+        },
         {
             "component": "general",
             "errorCode": "6838",
@@ -172,45 +182,6 @@ Note: Callstack:
                 "start": 159
             },
             "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "1236",
-            "formattedMessage": "Warning: BMC: Insufficient funds happens here.
-  --> A:11:7:
-   |
-11 | \t\t\t\t\t\ta.transfer(x);
-   | \t\t\t\t\t\t^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
-
-",
-            "message": "BMC: Insufficient funds happens here.",
-            "secondarySourceLocations": [
-                {
-                    "message": "Counterexample:
-  a = 0
-  x = 0
-"
-                },
-                {
-                    "message": "Callstack:"
-                },
-                {
-                    "message": ""
-                }
-            ],
-            "severity": "warning",
-            "sourceLocation": {
-                "end": 237,
-                "file": "A",
-                "start": 224
-            },
-            "type": "Warning"
         }
     ],
     "sources": {

diff --git a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json
@@ -147,6 +147,16 @@ test.f(0x0, 1)",
                 "start": 283
             },
             "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "1391",
+            "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.
+
+",
+            "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.",
+            "severity": "info",
+            "type": "Info"
         }
     ],
     "sources": {

diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
@@ -19,5 +19,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (280-314): CHC: Assertion violation happens here.
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 1236: (175-190): BMC: Insufficient funds happens here.
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
@@ -16,8 +16,7 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (193-226): CHC: Assertion violation might happen here.
+// Warning 8656: (141-156): CHC: Insufficient funds happens here.
+// Warning 6328: (193-226): CHC: Assertion violation happens here.
 // Warning 6328: (245-279): CHC: Assertion violation happens here.
 // Warning 6328: (298-332): CHC: Assertion violation happens here.
-// Warning 1236: (141-156): BMC: Insufficient funds happens here.
-// Warning 4661: (193-226): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol
@@ -18,4 +18,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
@@ -20,5 +20,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (258-274): CHC: Assertion violation happens here.
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 1236: (33-46): BMC: Insufficient funds happens here.
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
@@ -23,5 +23,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (315-331): CHC: Assertion violation happens here.
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 1236: (87-100): BMC: Insufficient funds happens here.
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol
@@ -21,6 +21,6 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.
+// Warning 8656: (54-67): CHC: Insufficient funds happens here.
 // Warning 6328: (282-298): CHC: Assertion violation happens here.
 // Warning 6328: (317-331): CHC: Assertion violation happens here.
-// Warning 1236: (54-67): BMC: Insufficient funds happens here.
diff --git a/...heckerTests/blockchain_state/transfer.sol → ...ckerTests/blockchain_state/transfer_1.sol b/...heckerTests/blockchain_state/transfer.sol → ...ckerTests/blockchain_state/transfer_1.sol
@@ -12,5 +12,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (166-201): CHC: Assertion violation happens here.
-// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol
@@ -0,0 +1,14 @@
+contract C {
+	address payable recipient;
+	uint amount;
+
+	function shouldHold() public {
+		uint tempAmount = address(this).balance;
+		recipient.transfer(tempAmount);
+		recipient.transfer(amount);
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol
@@ -0,0 +1,11 @@
+contract C {
+	address payable recipient;
+
+	function shouldFail() public {
+		recipient.transfer(1);
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8656: (76-97): CHC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol
@@ -0,0 +1,12 @@
+contract C {
+	address payable recipient;
+
+	function f() public payable {
+		require(msg.value > 1);
+		recipient.transfer(1);
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_state.sol b/test/libsolidity/smtCheckerTests/functions/this_state.sol
@@ -1,14 +1,14 @@
 contract C
 {
-    uint public x;
-    function g() public {
+	uint public x;
+	function g() public {
 		x = 0;
-        this.h();
+		this.h();
 		assert(x == 2);
-    }
-    function h() public {
-        x = 2;
-    }
+	}
+	function h() public {
+		x = 2;
+	}
 }
 // ====
 // SMTEngine: all

diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol
@@ -11,5 +11,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 8656: (98-113): CHC: Insufficient funds happens here.
 // Warning 6328: (162-186): CHC: Assertion violation happens here.
-// Warning 1236: (98-113): BMC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
@@ -15,6 +15,6 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 8656: (184-199): CHC: Insufficient funds happens here.
+// Warning 8656: (203-218): CHC: Insufficient funds happens here.
 // Warning 6328: (262-291): CHC: Assertion violation happens here.
-// Warning 1236: (184-199): BMC: Insufficient funds happens here.
-// Warning 1236: (203-218): BMC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol
@@ -13,5 +13,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
@@ -12,6 +12,6 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 8656: (101-116): CHC: Insufficient funds happens here.
+// Warning 8656: (120-136): CHC: Insufficient funds happens here.
 // Warning 6328: (180-204): CHC: Assertion violation happens here.
-// Warning 1236: (101-116): BMC: Insufficient funds happens here.
-// Warning 1236: (120-136): BMC: Insufficient funds happens here.