Added tests and support for suffix function with 2 arguments

libsolidity/formal/SMTEncoder.cpp

@@ -3174,10 +3174,24 @@ vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _f
 		firstParam = 1;
 	}
 
-	solAssert((arguments.size() + firstParam) == functionParams.size(), "");
-	for (unsigned i = 0; i < arguments.size(); ++i)
-		args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
-
+	if (_funCall.isSuffixCall() && functionParams.size() == 2)
+	{
+		solAssert(!funType->hasBoundFirstArgument());
+		solAssert(arguments.size() == 1);
+		auto&& literalType = dynamic_cast<RationalNumberType const*>(arguments[0]->annotation().type);
+		solAssert(literalType);
+		auto&& [mantissa, exponent] = literalType->fractionalDecomposition();
+		solAssert(mantissa && exponent);
+		solAssert(!mantissa->isNegative() && !exponent->isNegative());
+		args.emplace_back(mantissa->literalValue(nullptr));
+		args.emplace_back(exponent->literalValue(nullptr));
+	}
+	else
+	{
+		solAssert((arguments.size() + firstParam) == functionParams.size(), "");
+		for (unsigned i = 0; i < arguments.size(); ++i)
+			args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
+	}
 	return args;
 }
 

test/libsolidity/smtCheckerTests/literalSuffixes/division_by_zero_function_single_argument.sol

@@ -0,0 +1,8 @@
+function suffix(uint x) pure suffix returns (uint) { return 1000000 / x; }
+contract C {
+    uint y = 0 suffix;
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4281: (60-71): CHC: Division by zero happens here.

test/libsolidity/smtCheckerTests/literalSuffixes/division_by_zero_function_two_arguments.sol

@@ -0,0 +1,14 @@
+function suffix2(uint m, uint e) pure suffix returns (uint) {
+    return m / e;
+}
+
+contract C {
+    function test() public pure returns (uint x) {
+        x = 1234567890 suffix2;
+    }
+}
+
+// ====
+// SMTEngine: all
+// ----
+// Warning 4281: (73-78): CHC: Division by zero happens here.

test/libsolidity/smtCheckerTests/literalSuffixes/equivalent_function_call_with_single_argument.sol

@@ -0,0 +1,44 @@
+function addressSuffix(address x) pure suffix returns (bytes20) { return ~bytes20(x); }
+
+function boolSuffix(bool x) suffix pure returns (bool) { return !x; }
+
+function bytesSuffix(bytes memory value) pure suffix returns (uint) { return value.length; }
+
+function intSuffix(int x) pure suffix returns (int) { return x + 1; }
+
+function stringSuffix(string memory) suffix pure returns (uint) { return 1; }
+
+contract C {
+    function testAddressSuffix() public pure {
+        assert(
+            0x0000000000000000000000000000000000000001 addressSuffix ==
+            addressSuffix(0x0000000000000000000000000000000000000001)
+        );
+    }
+
+    function testBoolSuffix() public pure {
+        assert(true boolSuffix == boolSuffix(true));
+        assert(false boolSuffix == boolSuffix(false));
+    }
+
+    function testBytes() public pure {
+        assert("zyx" bytesSuffix == bytesSuffix("zyx"));
+        assert(hex"0123456789abcdef" bytesSuffix == bytesSuffix(hex"0123456789abcdef"));
+        assert(unicode"😃" bytesSuffix == bytesSuffix(unicode"😃"));
+    }
+
+    function testStringSuffix() public pure {
+        assert("a" stringSuffix == stringSuffix("a"));
+        assert("abcdef" stringSuffix == stringSuffix("abcdef"));
+        assert("" stringSuffix == stringSuffix(""));
+    }
+
+    function testIntSuffix() public pure {
+        assert(1 intSuffix == intSuffix(1));
+        assert(1 intSuffix + 1 intSuffix == intSuffix(1) + intSuffix(1));
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Info 1391: CHC: 14 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/literalSuffixes/equivalent_function_call_with_two_arguments.sol

@@ -0,0 +1,16 @@
+function suffix(uint m, uint e) pure suffix returns (uint) {
+    return m + e;
+}
+
+contract C {
+    function test() public pure {
+        assert(1.23 suffix == suffix(123, 2));
+        assert(123 suffix == suffix(123, 0));
+        assert(0 suffix == suffix(0, 0));
+    }
+}
+
+// ====
+// SMTEngine: all
+// ----
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/literalSuffixes/equivalent_function_call_with_two_arguments_fail.sol

@@ -0,0 +1,19 @@
+function suffix(uint m, uint e) pure suffix returns (uint) {
+    return m + e;
+}
+
+contract C {
+    function test() public pure {
+        assert(1.23 suffix == suffix(123, 4));
+        assert(123 suffix == suffix(12, 3));
+        assert(0 suffix == suffix(0, 1));
+    }
+}
+
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (137-174): CHC: Assertion violation happens here.
+// Warning 6328: (184-219): CHC: Assertion violation happens here.
+// Warning 6328: (229-261): 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.

test/libsolidity/smtCheckerTests/literalSuffixes/overflow_function_single_argument.sol

@@ -0,0 +1,25 @@
+function intSuffix(int8 x) pure suffix returns (int8) { return x + 1; }
+function uintSuffix(uint y) pure suffix returns (uint) { return y - 1; }
+function constantSuffix(int8) pure suffix returns (int) { return 8; }
+
+contract C {
+    function overflow() public pure {
+        127 intSuffix;
+    }
+
+    function underflow() public pure {
+        0 uintSuffix;
+    }
+
+    function notUnderOverflow() public pure {
+        127 constantSuffix;
+        0 constantSuffix;
+        -127 constantSuffix;
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4984: (63-68): CHC: Overflow (resulting value larger than 127) happens here.
+// Warning 3944: (136-141): CHC: Underflow (resulting value less than 0) happens here.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/literalSuffixes/overflow_function_two_arguments.sol

@@ -0,0 +1,31 @@
+function overflowSuffix(uint8 m, uint8 e) pure suffix returns (uint) {
+    return m + e;
+}
+
+function underflowSuffix(uint8 m, uint8 e) pure suffix returns (uint8) {
+    return m - e;
+}
+
+function constantSuffix(uint8, uint8) pure suffix returns (uint8) {
+    return 1;
+}
+
+contract C {
+    function overflow() public pure {
+        25.5 overflowSuffix;
+    }
+
+    function underflow() public pure {
+        0.01 underflowSuffix;
+    }
+
+    function notUnderOverflow() public pure {
+        25.5 constantSuffix;
+        0.01 constantSuffix;
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4984: (82-87): CHC: Overflow (resulting value larger than 255) happens here.
+// Warning 3944: (176-181): CHC: Underflow (resulting value less than 0) happens here.