From b9b9c229b44510e020b71a3647402eb659ca565b Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 13 Oct 2020 12:47:03 +0100 Subject: [PATCH] New tests --- .../smtCheckerTests/special/blockhash.sol | 1 - .../smtCheckerTests/special/msg_data.sol | 18 +++- .../smtCheckerTests/special/msg_sig.sol | 24 +++++- .../special/tx_data_gasleft_changes.sol | 21 +++++ .../special/tx_data_immutable.sol | 61 +++++++++++++ .../special/tx_data_immutable_fail.sol | 86 +++++++++++++++++++ 6 files changed, 207 insertions(+), 4 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol create mode 100644 test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol create mode 100644 test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol index ca956e6d3..d16cb7dc2 100644 --- a/test/libsolidity/smtCheckerTests/special/blockhash.sol +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -12,4 +12,3 @@ contract C // ---- // Warning 6328: (85-109): CHC: Assertion violation happens here. // Warning 6328: (113-137): CHC: Assertion violation happens here. -// Warning 6328: (155-191): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol index 4c5b24601..9406404e2 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_data.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol @@ -4,7 +4,23 @@ contract C { function f() public payable { assert(msg.data.length > 0); + // Fails since calldata size should be 4 + assert(msg.data.length > 4); + // f's sig is 0x26121ff0 + assert(msg.data[0] == 0x26); + assert(msg.data[1] == 0x12); + assert(msg.data[2] == 0x1f); + assert(msg.data[3] == 0xf0); + } + function g() public payable { + // g's sig is 0xe2179b8e + assert(msg.data[0] == 0xe2); + assert(msg.data[1] == 0x17); + assert(msg.data[2] == 0x9b); + // Fails + assert(msg.data[3] == 0x8f); } } // ---- -// Warning 6328: (79-106): CHC: Assertion violation happens here. +// Warning 6328: (153-180): CHC: Assertion violation happens here. +// Warning 6328: (500-527): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol index 4a7ddacc4..a367049fa 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_sig.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -2,9 +2,29 @@ pragma experimental SMTChecker; contract C { - function f() public payable { + function f() public pure { assert(msg.sig == 0x00000000); + assert(msg.sig == 0x26121ff0); + fi(); + gi(); + } + function fi() internal pure { + assert(msg.sig == 0x26121ff0); + } + function g() public pure { + assert(msg.sig == 0xe2179b8e); + gi(); + } + function gi() internal pure { + // Fails since f can also call gi in which case msg.sig == 0x26121ff0 + assert(msg.sig == 0xe2179b8e); + } + function h() public pure { + // Fails since gi can also call h in which case msg.sig can be f() or g() + assert(msg.sig == 0xe2179b8e); } } // ---- -// Warning 6328: (79-108): CHC: Assertion violation happens here. +// Warning 6328: (76-105): CHC: Assertion violation happens here. +// Warning 6328: (403-432): CHC: Assertion violation happens here. +// Warning 6328: (543-572): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol b/test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol new file mode 100644 index 000000000..11d1940a7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C { + uint gleft; + + function f() public payable { + gleft = gasleft(); + + fi(); + + assert(gleft == gasleft()); + assert(gleft >= gasleft()); + } + + function fi() internal view { + assert(gleft == gasleft()); + } +} +// ---- +// Warning 6328: (124-150): CHC: Assertion violation happens here. +// Warning 6328: (219-245): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol b/test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol new file mode 100644 index 000000000..371897b3b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol @@ -0,0 +1,61 @@ +pragma experimental SMTChecker; + +contract C { + bytes32 bhash; + address coin; + uint dif; + uint glimit; + uint number; + uint tstamp; + bytes mdata; + address sender; + bytes4 sig; + uint value; + uint gprice; + address origin; + + function f() public payable { + bhash = blockhash(12); + coin = block.coinbase; + dif = block.difficulty; + glimit = block.gaslimit; + number = block.number; + tstamp = block.timestamp; + mdata = msg.data; + sender = msg.sender; + sig = msg.sig; + value = msg.value; + gprice = tx.gasprice; + origin = tx.origin; + + fi(); + + assert(bhash == blockhash(12)); + assert(coin == block.coinbase); + assert(dif == block.difficulty); + assert(glimit == block.gaslimit); + assert(number == block.number); + assert(tstamp == block.timestamp); + assert(mdata.length == msg.data.length); + assert(sender == msg.sender); + assert(sig == msg.sig); + assert(value == msg.value); + assert(gprice == tx.gasprice); + assert(origin == tx.origin); + } + + function fi() internal view { + assert(bhash == blockhash(12)); + assert(coin == block.coinbase); + assert(dif == block.difficulty); + assert(glimit == block.gaslimit); + assert(number == block.number); + assert(tstamp == block.timestamp); + assert(mdata.length == msg.data.length); + assert(sender == msg.sender); + assert(sig == msg.sig); + assert(value == msg.value); + assert(gprice == tx.gasprice); + assert(origin == tx.origin); + } +} diff --git a/test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol b/test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol new file mode 100644 index 000000000..3a5b820a0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol @@ -0,0 +1,86 @@ +pragma experimental SMTChecker; + +contract C { + bytes32 bhash; + address coin; + uint dif; + uint glimit; + uint number; + uint tstamp; + bytes mdata; + address sender; + bytes4 sig; + uint value; + uint gprice; + address origin; + + function f() public payable { + bhash = blockhash(12); + coin = block.coinbase; + dif = block.difficulty; + glimit = block.gaslimit; + number = block.number; + tstamp = block.timestamp; + mdata = msg.data; + sender = msg.sender; + sig = msg.sig; + value = msg.value; + gprice = tx.gasprice; + origin = tx.origin; + + fi(); + + assert(bhash == blockhash(122)); + assert(coin != block.coinbase); + assert(dif != block.difficulty); + assert(glimit != block.gaslimit); + assert(number != block.number); + assert(tstamp != block.timestamp); + assert(mdata.length != msg.data.length); + assert(sender != msg.sender); + assert(sig != msg.sig); + assert(value != msg.value); + assert(gprice != tx.gasprice); + assert(origin != tx.origin); + } + + function fi() internal view { + assert(bhash == blockhash(122)); + assert(coin != block.coinbase); + assert(dif != block.difficulty); + assert(glimit != block.gaslimit); + assert(number != block.number); + assert(tstamp != block.timestamp); + assert(mdata.length != msg.data.length); + assert(sender != msg.sender); + assert(sig != msg.sig); + assert(value != msg.value); + assert(gprice != tx.gasprice); + assert(origin != tx.origin); + } +} +// ---- +// Warning 6328: (545-576): CHC: Assertion violation happens here. +// Warning 6328: (580-610): CHC: Assertion violation happens here. +// Warning 6328: (614-645): CHC: Assertion violation happens here. +// Warning 6328: (649-681): CHC: Assertion violation happens here. +// Warning 6328: (685-715): CHC: Assertion violation happens here. +// Warning 6328: (719-752): CHC: Assertion violation happens here. +// Warning 6328: (756-795): CHC: Assertion violation happens here. +// Warning 6328: (799-827): CHC: Assertion violation happens here. +// Warning 6328: (831-853): CHC: Assertion violation happens here. +// Warning 6328: (857-883): CHC: Assertion violation happens here. +// Warning 6328: (887-916): CHC: Assertion violation happens here. +// Warning 6328: (920-947): CHC: Assertion violation happens here. +// Warning 6328: (986-1017): CHC: Assertion violation happens here. +// Warning 6328: (1021-1051): CHC: Assertion violation happens here. +// Warning 6328: (1055-1086): CHC: Assertion violation happens here. +// Warning 6328: (1090-1122): CHC: Assertion violation happens here. +// Warning 6328: (1126-1156): CHC: Assertion violation happens here. +// Warning 6328: (1160-1193): CHC: Assertion violation happens here. +// Warning 6328: (1197-1236): CHC: Assertion violation happens here. +// Warning 6328: (1240-1268): CHC: Assertion violation happens here. +// Warning 6328: (1272-1294): CHC: Assertion violation happens here. +// Warning 6328: (1298-1324): CHC: Assertion violation happens here. +// Warning 6328: (1328-1357): CHC: Assertion violation happens here. +// Warning 6328: (1361-1388): CHC: Assertion violation happens here.