tests for free constants

test/libsolidity/smtCheckerTests/file_level/constant_easy.sol

@@ -0,0 +1,12 @@
+uint constant x = 42;
+
+contract C {
+	function f() public pure {
+		uint z = x;
+		assert(z == 41);
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (80-95): CHC: Assertion violation happens here.\nCounterexample:\n\nz = 42\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol

@@ -0,0 +1,41 @@
+bytes constant a = "\x03\x01\x02";
+bytes constant b = hex"030102";
+string constant c = "hello";
+uint256 constant x = 56;
+enum ActionChoices {GoLeft, GoRight, GoStraight, Sit}
+ActionChoices constant choices = ActionChoices.GoRight;
+bytes32 constant st = "abc\x00\xff__";
+
+contract C {
+	function f() internal pure returns (bytes memory) {
+		return a;
+	}
+
+	function g() internal pure returns (bytes memory) {
+		return b;
+	}
+
+	function h() internal pure returns (bytes memory) {
+		return bytes(c);
+	}
+
+	function i() internal pure returns (uint, ActionChoices, bytes32) {
+		return (x, choices, st);
+	}
+
+	function p() public pure {
+		assert(f().length == 3); // should hold
+		assert(g().length == 3); // should hold
+		assert(h().length == 5); // should hold
+		(uint w, ActionChoices z, bytes32 t) = i();
+		assert(x == 56); // should hold
+		assert(w == 56); // should hold
+		assert(z == ActionChoices.GoRight); // should hold
+		assert(t == "abc\x00\xff__"); // should hold
+		assert(w == 59); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (968-983): CHC: Assertion violation happens here.\nCounterexample:\n\nw = 56\nz = 1\nt = 44048180624707321370159228589897778088919435935156254407473833945046349512704\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n    C.g() -- internal call\n    C.h() -- internal call\n    C.i() -- internal call

test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol

@@ -0,0 +1,64 @@
+==== Source: s1.sol ====
+
+
+bytes constant a = b;
+bytes constant b = hex"030102";
+
+function fre() pure returns (bytes memory) {
+	return a;
+}
+
+==== Source: s2.sol ====
+
+import "s1.sol";
+
+uint256 constant c = uint8(a[0]) + 2;
+
+contract C {
+	function f() internal pure returns (bytes memory) {
+		return a;
+	}
+
+	function g() internal pure returns (bytes memory) {
+		return b;
+	}
+
+	function h() internal pure returns (uint) {
+		return c;
+	}
+
+	function i() internal pure returns (bytes memory) {
+		return fre();
+	}
+
+	function p() public pure {
+		bytes memory r1 = f();
+		assert(r1[0] == 0x03); // should hold
+		assert(r1[1] == 0x01); // should hold
+		assert(r1[2] == 0x02); // should hold
+		assert(r1[2] == 0x04); // should fail
+
+		bytes memory r2 = g();
+		assert(r2[0] == 0x03); // should hold
+		assert(r2[1] == 0x01); // should hold
+		assert(r2[2] == 0x02); // should hold
+		assert(r2[2] == 0x04); // should fail
+
+		bytes memory r3 = i();
+		assert(r3[0] == 0x03); // should hold
+		assert(r3[1] == 0x01); // should hold
+		assert(r3[2] == 0x02); // should hold
+		assert(r3[2] == 0x04); // should fail
+
+		uint z = h();
+		assert(z == 5); // should hold
+		assert(z == 7); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call
+// Warning 6328: (s2.sol:704-725): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = [3, 1, 2]\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n    C.g() -- internal call
+// Warning 6328: (s2.sol:890-911): CHC: Assertion violation happens here.
+// Warning 6328: (s2.sol:980-994): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol

@@ -0,0 +1,26 @@
+==== Source: a.sol ====
+function f(uint) pure returns (uint) { return 7; }
+function f(bytes memory x) pure returns (uint) { return x.length; }
+==== Source: b.sol ====
+import "a.sol" as M;
+contract C {
+	function f() internal pure returns (uint, uint) {
+		return (M.f(2), M.f("abc"));
+	}
+	function p() public pure {
+		(uint a, uint b) = f();
+		assert(a == 7); // should hold
+		assert(a == 9); // should fail
+		assert(b == 3); // should hold
+		assert(b == 5); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol"
+// Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"
+// Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol::f(2) -- internal call\n        a.sol::f([97, 98, 99]) -- internal call
+// Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol::f(2) -- internal call\n        a.sol::f([97, 98, 99]) -- internal call
+// Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol"
+// Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"

test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol

@@ -7,4 +7,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (125-130): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639894\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639894)
+// Warning 4984: (93-98): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639894\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639894)

test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol

@@ -10,4 +10,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 2018: (220-310): Function state mutability can be restricted to pure
+// Warning 2018: (188-278): Function state mutability can be restricted to pure

test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol

@@ -12,6 +12,6 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (222-234): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    ::fun(_x, []) -- internal call
-// Warning 4984: (222-238): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 115792089237316195423570985008687907853269984665640564039457584007913129632175\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129632175, input)\n    ::fun(_x, []) -- internal call
-// Warning 6368: (347-352): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    ::fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
+// Warning 4984: (190-202): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    ::fun(_x, []) -- internal call
+// Warning 4984: (190-206): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 115792089237316195423570985008687907853269984665640564039457584007913129632175\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129632175, input)\n    ::fun(_x, []) -- internal call
+// Warning 6368: (315-320): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 11, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 11, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    ::fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 11, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call

test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol

@@ -0,0 +1,37 @@
+==== Source: s1.sol ====
+
+
+uint constant a = 89;
+
+function fre() pure returns (uint) {
+	return a;
+}
+
+==== Source: s2.sol ====
+
+import {a as b, fre} from "s1.sol";
+import "s1.sol" as M;
+
+uint256 constant a = 13;
+
+contract C {
+	function f() internal pure returns (uint, uint, uint, uint) {
+		return (a, fre(), M.a, b);
+	}
+	function p() public pure {
+		(uint x, uint y, uint z, uint t) = f();
+		assert(x == 13); // should hold
+		assert(y == 89); // should hold
+		assert(z == 89); // should hold but the SMTChecker does not implement module access
+		assert(t == 89); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
+// Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
+// Warning 6328: (s2.sol:334-349): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 90\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        s1.sol::fre() -- internal call
+// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
+// Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
+// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.