From 36def3ef6ef3dce9687f3d61ecabbe3cd226a0a6 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 12 Apr 2021 13:47:24 +0200 Subject: [PATCH] tests for free constants --- .../file_level/constant_easy.sol | 12 ++++ .../constant_string_at_file_level.sol | 41 ++++++++++++ .../constants_at_file_level_referencing.sol | 64 +++++++++++++++++++ .../file_level/file_level_call_via_module.sol | 26 ++++++++ .../file_level/free_constant_1.sol | 2 +- .../file_level/free_constant_2.sol | 2 +- .../free_function_and_constant_1.sol | 6 +- .../same_constants_different_files.sol | 37 +++++++++++ 8 files changed, 185 insertions(+), 5 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/file_level/constant_easy.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol diff --git a/test/libsolidity/smtCheckerTests/file_level/constant_easy.sol b/test/libsolidity/smtCheckerTests/file_level/constant_easy.sol new file mode 100644 index 000000000..73dc2a861 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol b/test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol new file mode 100644 index 000000000..a40fbc216 --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol b/test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol new file mode 100644 index 000000000..4082885b9 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol b/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol new file mode 100644 index 000000000..facedf003 --- /dev/null +++ b/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" diff --git a/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol index 11c4428b0..ccf6700ef 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol +++ b/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) diff --git a/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol b/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol index 1e937c303..3419624c7 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol index 2ac197bbe..d9c07ea13 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol b/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol new file mode 100644 index 000000000..da222be4f --- /dev/null +++ b/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.