cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #13130 from ethereum/check-overflow-after-add-sub-operations

Browse Source 
Check overflow after add sub operations
This commit is contained in:
chriseth
2022-06-27 15:33:57 +02:00
committed by GitHub
parent 2397f09b79 4fd5c11af7
commit b70e064e8f
49 changed files with 450 additions and 434 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/cmdlineTests/asm_json/output
+63 -76
View File
@@ -1300,14 +1300,14 @@ EVM assembly:
},
{
"begin": 1211,
"end": 1516,
"end": 1402,
"name": "tag",
"source": 1,
"value": "10"
},
{
"begin": 1211,
"end": 1516,
"end": 1402,
"name": "JUMPDEST",
"source": 1
},
@@ -1423,159 +1423,146 @@ EVM assembly:
"source": 1
},
{
"begin": 1458,
"end": 1459,
"begin": 1347,
"end": 1348,
"name": "DUP3",
"source": 1
},
{
"begin": 1390,
"end": 1456,
"name": "PUSH",
"source": 1,
"value": "FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
},
{
"begin": 1386,
"end": 1460,
"name": "SUB",
"source": 1
},
{
"begin": 1383,
"end": 1384,
"begin": 1344,
"end": 1345,
"name": "DUP3",
"source": 1
},
{
"begin": 1380,
"end": 1461,
"begin": 1340,
"end": 1349,
"name": "ADD",
"source": 1
},
{
"begin": 1333,
"end": 1349,
"name": "SWAP1",
"source": 1
},
{
"begin": 1333,
"end": 1349,
"name": "POP",
"source": 1
},
{
"begin": 1368,
"end": 1371,
"name": "DUP1",
"source": 1
},
{
"begin": 1365,
"end": 1366,
"name": "DUP3",
"source": 1
},
{
"begin": 1362,
"end": 1372,
"name": "GT",
"source": 1
},
{
"begin": 1377,
"end": 1484,
"begin": 1359,
"end": 1395,
"name": "ISZERO",
"source": 1
},
{
"begin": 1377,
"end": 1484,
"begin": 1359,
"end": 1395,
"name": "PUSH [tag]",
"source": 1,
"value": "37"
},
{
"begin": 1377,
"end": 1484,
"begin": 1359,
"end": 1395,
"name": "JUMPI",
"source": 1
},
{
"begin": 1464,
"end": 1482,
"begin": 1375,
"end": 1393,
"name": "PUSH [tag]",
"source": 1,
"value": "38"
},
{
"begin": 1464,
"end": 1482,
"begin": 1375,
"end": 1393,
"name": "PUSH [tag]",
"source": 1,
"value": "18"
},
{
"begin": 1464,
"end": 1482,
"begin": 1375,
"end": 1393,
"jumpType": "[in]",
"name": "JUMP",
"source": 1
},
{
"begin": 1464,
"end": 1482,
"begin": 1375,
"end": 1393,
"name": "tag",
"source": 1,
"value": "38"
},
{
"begin": 1464,
"end": 1482,
"begin": 1375,
"end": 1393,
"name": "JUMPDEST",
"source": 1
},
{
"begin": 1377,
"end": 1484,
"begin": 1359,
"end": 1395,
"name": "tag",
"source": 1,
"value": "37"
},
{
"begin": 1377,
"end": 1484,
"begin": 1359,
"end": 1395,
"name": "JUMPDEST",
"source": 1
},
{
"begin": 1508,
"end": 1509,
"name": "DUP3",
"source": 1
},
{
"begin": 1505,
"end": 1506,
"name": "DUP3",
"source": 1
},
{
"begin": 1501,
"end": 1510,
"name": "ADD",
"source": 1
},
{
"begin": 1494,
"end": 1510,
"name": "SWAP1",
"source": 1
},
{
"begin": 1494,
"end": 1510,
"name": "POP",
"source": 1
},
{
"begin": 1211,
"end": 1516,
"end": 1402,
"name": "SWAP3",
"source": 1
},
{
"begin": 1211,
"end": 1516,
"end": 1402,
"name": "SWAP2",
"source": 1
},
{
"begin": 1211,
"end": 1516,
"end": 1402,
"name": "POP",
"source": 1
},
{
"begin": 1211,
"end": 1516,
"end": 1402,
"name": "POP",
"source": 1
},
{
"begin": 1211,
"end": 1516,
"end": 1402,
"jumpType": "[out]",
"name": "JUMP",
"source": 1
test/cmdlineTests/asm_json_no_pretty_print/output
+1 -1
View File
File diff suppressed because one or more lines are too long
test/cmdlineTests/optimizer_array_sload/output
+4 -3
View File
@@ -49,16 +49,17 @@ object "Arraysum_34" {
{
/// @src 0:80:429 "contract Arraysum {..."
mstore(_2, _2)
let _4 := sload(add(18569430475105882587588266137607568536673111973893317399460219858819262702947, var_i))
if gt(var_sum, not(_4))
let sum := add(var_sum, sload(add(18569430475105882587588266137607568536673111973893317399460219858819262702947, var_i)))
if gt(var_sum, sum)
{
mstore(_2, shl(224, 0x4e487b71))
mstore(_1, 0x11)
revert(_2, 0x24)
}
/// @src 0:407:423 "sum += values[i]"
var_sum := /** @src 0:80:429 "contract Arraysum {..." */ add(var_sum, _4)
var_sum := sum
}
/// @src 0:80:429 "contract Arraysum {..."
let memPos := mload(64)
mstore(memPos, var_sum)
return(memPos, 32)
test/cmdlineTests/optimizer_inliner_dynamic_reference/output
+35 -37
View File
@@ -150,75 +150,73 @@ sub_0: assembly {
jump // in
tag_25:
jump // out
/* "#utility.yul":196:421 */
/* "#utility.yul":196:418 */
tag_22:
/* "#utility.yul":236:239 */
0x00
/* "#utility.yul":267:268 */
/* "#utility.yul":261:270 */
dup1
dup3
/* "#utility.yul":263:269 */
not
/* "#utility.yul":260:261 */
add
/* "#utility.yul":282:292 */
dup1
dup3
/* "#utility.yul":257:270 */
gt
/* "#utility.yul":254:390 */
/* "#utility.yul":279:412 */
iszero
tag_30
jumpi
/* "#utility.yul":312:322 */
/* "#utility.yul":334:344 */
0x4e487b71
/* "#utility.yul":307:310 */
/* "#utility.yul":329:332 */
0xe0
/* "#utility.yul":303:323 */
/* "#utility.yul":325:345 */
shl
/* "#utility.yul":300:301 */
/* "#utility.yul":322:323 */
0x00
/* "#utility.yul":293:324 */
/* "#utility.yul":315:346 */
mstore
/* "#utility.yul":347:351 */
/* "#utility.yul":369:373 */
0x11
/* "#utility.yul":344:345 */
/* "#utility.yul":366:367 */
0x04
/* "#utility.yul":337:352 */
/* "#utility.yul":359:374 */
mstore
/* "#utility.yul":375:379 */
/* "#utility.yul":397:401 */
0x24
/* "#utility.yul":372:373 */
/* "#utility.yul":394:395 */
0x00
/* "#utility.yul":365:380 */
/* "#utility.yul":387:402 */
revert
/* "#utility.yul":254:390 */
/* "#utility.yul":279:412 */
tag_30:
/* "#utility.yul":196:418 */
swap3
swap2
pop
pop
/* "#utility.yul":406:415 */
add
swap1
/* "#utility.yul":196:421 */
jump // out
/* "#utility.yul":426:553 */
/* "#utility.yul":423:550 */
tag_26:
/* "#utility.yul":487:497 */
/* "#utility.yul":484:494 */
0x4e487b71
/* "#utility.yul":482:485 */
/* "#utility.yul":479:482 */
0xe0
/* "#utility.yul":478:498 */
/* "#utility.yul":475:495 */
shl
/* "#utility.yul":475:476 */
/* "#utility.yul":472:473 */
0x00
/* "#utility.yul":468:499 */
/* "#utility.yul":465:496 */
mstore
/* "#utility.yul":518:522 */
/* "#utility.yul":515:519 */
0x51
/* "#utility.yul":515:516 */
/* "#utility.yul":512:513 */
0x04
/* "#utility.yul":508:523 */
/* "#utility.yul":505:520 */
mstore
/* "#utility.yul":542:546 */
/* "#utility.yul":539:543 */
0x24
/* "#utility.yul":539:540 */
/* "#utility.yul":536:537 */
0x00
/* "#utility.yul":532:547 */
/* "#utility.yul":529:544 */
revert
auxdata: <AUXDATA REMOVED>
test/cmdlineTests/optimizer_inliner_dynamic_reference_constructor/output
+35 -37
View File
@@ -155,75 +155,73 @@ sub_0: assembly {
jump // in
tag_21:
jump // out
/* "#utility.yul":196:421 */
/* "#utility.yul":196:418 */
tag_19:
/* "#utility.yul":236:239 */
0x00
/* "#utility.yul":267:268 */
/* "#utility.yul":261:270 */
dup1
dup3
/* "#utility.yul":263:269 */
not
/* "#utility.yul":260:261 */
add
/* "#utility.yul":282:292 */
dup1
dup3
/* "#utility.yul":257:270 */
gt
/* "#utility.yul":254:390 */
/* "#utility.yul":279:412 */
iszero
tag_26
jumpi
/* "#utility.yul":312:322 */
/* "#utility.yul":334:344 */
0x4e487b71
/* "#utility.yul":307:310 */
/* "#utility.yul":329:332 */
0xe0
/* "#utility.yul":303:323 */
/* "#utility.yul":325:345 */
shl
/* "#utility.yul":300:301 */
/* "#utility.yul":322:323 */
0x00
/* "#utility.yul":293:324 */
/* "#utility.yul":315:346 */
mstore
/* "#utility.yul":347:351 */
/* "#utility.yul":369:373 */
0x11
/* "#utility.yul":344:345 */
/* "#utility.yul":366:367 */
0x04
/* "#utility.yul":337:352 */
/* "#utility.yul":359:374 */
mstore
/* "#utility.yul":375:379 */
/* "#utility.yul":397:401 */
0x24
/* "#utility.yul":372:373 */
/* "#utility.yul":394:395 */
0x00
/* "#utility.yul":365:380 */
/* "#utility.yul":387:402 */
revert
/* "#utility.yul":254:390 */
/* "#utility.yul":279:412 */
tag_26:
/* "#utility.yul":196:418 */
swap3
swap2
pop
pop
/* "#utility.yul":406:415 */
add
swap1
/* "#utility.yul":196:421 */
jump // out
/* "#utility.yul":426:553 */
/* "#utility.yul":423:550 */
tag_22:
/* "#utility.yul":487:497 */
/* "#utility.yul":484:494 */
0x4e487b71
/* "#utility.yul":482:485 */
/* "#utility.yul":479:482 */
0xe0
/* "#utility.yul":478:498 */
/* "#utility.yul":475:495 */
shl
/* "#utility.yul":475:476 */
/* "#utility.yul":472:473 */
0x00
/* "#utility.yul":468:499 */
/* "#utility.yul":465:496 */
mstore
/* "#utility.yul":518:522 */
/* "#utility.yul":515:519 */
0x51
/* "#utility.yul":515:516 */
/* "#utility.yul":512:513 */
0x04
/* "#utility.yul":508:523 */
/* "#utility.yul":505:520 */
mstore
/* "#utility.yul":542:546 */
/* "#utility.yul":539:543 */
0x24
/* "#utility.yul":539:540 */
/* "#utility.yul":536:537 */
0x00
/* "#utility.yul":532:547 */
/* "#utility.yul":529:544 */
revert
auxdata: <AUXDATA REMOVED>
test/cmdlineTests/standard_debug_info_in_evm_asm_via_ir_location/output.json
+52 -61
View File
@@ -120,9 +120,7 @@ sub_0: assembly {
eq
tag_14
jumpi
/* \"C\":117:119 41 */
0x01
/* \"C\":79:428 contract C... */
add
swap2
dup3
@@ -312,54 +310,51 @@ sub_0: assembly {
jumpi
/* \"C\":290:298 immutVar */
immutable(\"0xe4b1702d9298fee62dfeccc57d322a463ad55ca201256d01f62b45b2e1c21c10\")
sub(shl(0xff, 0x01), 0x2a)
/* \"C\":117:119 41 */
dup1
0x29
add
swap1
dup2
sgt
slt
0x01
and
tag_14
jumpi
/* \"C\":79:428 contract C... */
0x20
/* \"C\":117:119 41 */
swap3
pop
0x29
add
/* \"C\":79:428 contract C... */
dup2
mstore
return
/* \"C\":117:119 41 */
tag_1:
swap2
swap1
swap2
0x00
dup2
dup4
dup3
add
swap4
dup5
slt
swap2
slt
swap1
dup1
iszero
sub(shl(0xff, 0x01), 0x01)
dup4
swap1
sub
dup5
sgt
and
tag_40
jumpi
shl(0xff, 0x01)
dup3
swap1
sub
dup4
slt
and
tag_40
swap2
iszero
and
or
tag_38
jumpi
add
swap1
jump\t// out
tag_40:
tag_38:
mstore(0x00, shl(0xe0, 0x4e487b71))
mstore(0x04, 0x11)
revert(0x00, 0x24)
@@ -410,18 +405,19 @@ sub_0: assembly {
mload
/* \"C\":147:149 42 */
mstore(0x80, 0x2a)
sub(shl(0xff, 0x01), 0x04)
/* \"D\":91:166 contract D is C(3)... */
dup2
sgt
0x01
and
tag_7
jumpi
dup1
/* \"D\":107:108 3 */
0x03
/* \"D\":91:166 contract D is C(3)... */
add
swap1
dup2
slt
0x01
and
tag_7
jumpi
0x00
sstore
mload(0x40)
@@ -503,9 +499,7 @@ sub_0: assembly {
eq
tag_14
jumpi
/* \"C\":117:119 41 */
0x01
/* \"D\":91:166 contract D is C(3)... */
add
swap2
dup3
@@ -695,54 +689,51 @@ sub_0: assembly {
jumpi
/* \"C\":290:298 immutVar */
immutable(\"0xe4b1702d9298fee62dfeccc57d322a463ad55ca201256d01f62b45b2e1c21c10\")
sub(shl(0xff, 0x01), 0x2a)
/* \"C\":117:119 41 */
dup1
0x29
add
swap1
dup2
sgt
slt
0x01
and
tag_14
jumpi
/* \"D\":91:166 contract D is C(3)... */
0x20
/* \"C\":117:119 41 */
swap3
pop
0x29
add
/* \"D\":91:166 contract D is C(3)... */
dup2
mstore
return
/* \"C\":117:119 41 */
tag_1:
swap2
swap1
swap2
0x00
dup2
dup4
dup3
add
swap4
dup5
slt
swap2
slt
swap1
dup1
iszero
sub(shl(0xff, 0x01), 0x01)
dup4
swap1
sub
dup5
sgt
and
tag_40
jumpi
shl(0xff, 0x01)
dup3
swap1
sub
dup4
slt
and
tag_40
swap2
iszero
and
or
tag_38
jumpi
add
swap1
jump\t// out
tag_40:
tag_38:
mstore(0x00, shl(0xe0, 0x4e487b71))
mstore(0x04, 0x11)
revert(0x00, 0x24)
test/cmdlineTests/standard_debug_info_in_yul_location/output.json
+49 -50
View File
@@ -354,13 +354,15 @@ object \"C_54\" {
function checked_add_t_int256(x, y) -> sum {
x := cleanup_t_int256(x)
y := cleanup_t_int256(y)
// overflow, if x >= 0 and y > (maxValue - x)
if and(iszero(slt(x, 0)), sgt(y, sub(0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff, x))) { panic_error_0x11() }
// underflow, if x < 0 and y < (minValue - x)
if and(slt(x, 0), slt(y, sub(0x8000000000000000000000000000000000000000000000000000000000000000, x))) { panic_error_0x11() }
sum := add(x, y)
// overflow, if x >= 0 and sum < y
// underflow, if x < 0 and sum >= y
if or(
and(iszero(slt(x, 0)), slt(sum, y)),
and(slt(x, 0), iszero(slt(sum, y)))
) { panic_error_0x11() }
}
/// @ast-id 30
@@ -656,13 +658,14 @@ object \"C_54\" {
/// @src 0:297:305 \"immutVar\"
let _4 := loadimmutable(\"8\")
/// @src 0:79:435 \"contract C...\"
if and(1, sgt(_4, sub(shl(255, 1), 42)))
let sum := add(/** @src 0:124:126 \"41\" */ 0x29, /** @src 0:79:435 \"contract C...\" */ _4)
if and(1, slt(sum, _4))
{
mstore(_3, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(_3, 0x24)
}
mstore(_1, add(/** @src 0:124:126 \"41\" */ 0x29, /** @src 0:79:435 \"contract C...\" */ _4))
mstore(_1, sum)
return(_1, 32)
}
case 0x793816ec {
@@ -742,20 +745,15 @@ object \"C_54\" {
}
function checked_add_int256(x, y) -> sum
{
let _1 := slt(x, 0)
if and(iszero(_1), sgt(y, sub(sub(shl(255, 1), 1), x)))
{
mstore(0, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(0, 0x24)
}
if and(_1, slt(y, sub(shl(255, 1), x)))
{
mstore(0, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(0, 0x24)
}
sum := add(x, y)
let _1 := slt(sum, y)
let _2 := slt(x, 0)
if or(and(iszero(_2), _1), and(_2, iszero(_1)))
{
mstore(0, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(0, 0x24)
}
}
}
data \".metadata\" hex\"<BYTECODE REMOVED>\"
@@ -893,13 +891,15 @@ object \"D_72\" {
function checked_add_t_int256(x, y) -> sum {
x := cleanup_t_int256(x)
y := cleanup_t_int256(y)
// overflow, if x >= 0 and y > (maxValue - x)
if and(iszero(slt(x, 0)), sgt(y, sub(0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff, x))) { panic_error_0x11() }
// underflow, if x < 0 and y < (minValue - x)
if and(slt(x, 0), slt(y, sub(0x8000000000000000000000000000000000000000000000000000000000000000, x))) { panic_error_0x11() }
sum := add(x, y)
// overflow, if x >= 0 and sum < y
// underflow, if x < 0 and sum >= y
if or(
and(iszero(slt(x, 0)), slt(sum, y)),
and(slt(x, 0), iszero(slt(sum, y)))
) { panic_error_0x11() }
}
function shift_left_0(value) -> newValue {
@@ -1185,13 +1185,15 @@ object \"D_72\" {
function checked_add_t_int256(x, y) -> sum {
x := cleanup_t_int256(x)
y := cleanup_t_int256(y)
// overflow, if x >= 0 and y > (maxValue - x)
if and(iszero(slt(x, 0)), sgt(y, sub(0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff, x))) { panic_error_0x11() }
// underflow, if x < 0 and y < (minValue - x)
if and(slt(x, 0), slt(y, sub(0x8000000000000000000000000000000000000000000000000000000000000000, x))) { panic_error_0x11() }
sum := add(x, y)
// overflow, if x >= 0 and sum < y
// underflow, if x < 0 and sum >= y
if or(
and(iszero(slt(x, 0)), slt(sum, y)),
and(slt(x, 0), iszero(slt(sum, y)))
) { panic_error_0x11() }
}
/// @ast-id 30
@@ -1460,13 +1462,14 @@ object \"D_72\" {
/// @src 0:154:156 \"42\"
mstore(128, 0x2a)
/// @src 1:91:166 \"contract D is C(3)...\"
if and(1, sgt(value, sub(shl(255, 1), 4)))
let sum := add(/** @src 1:107:108 \"3\" */ 0x03, /** @src 1:91:166 \"contract D is C(3)...\" */ value)
if and(1, slt(sum, value))
{
mstore(/** @src -1:-1:-1 */ 0, /** @src 1:91:166 \"contract D is C(3)...\" */ shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(/** @src -1:-1:-1 */ 0, /** @src 1:91:166 \"contract D is C(3)...\" */ 0x24)
}
sstore(/** @src -1:-1:-1 */ 0, /** @src 1:91:166 \"contract D is C(3)...\" */ add(/** @src 1:107:108 \"3\" */ 0x03, /** @src 1:91:166 \"contract D is C(3)...\" */ value))
sstore(/** @src -1:-1:-1 */ 0, /** @src 1:91:166 \"contract D is C(3)...\" */ sum)
let _2 := mload(64)
let _3 := datasize(\"D_72_deployed\")
codecopy(_2, dataoffset(\"D_72_deployed\"), _3)
@@ -1493,13 +1496,14 @@ object \"D_72\" {
/// @src 0:297:305 \"immutVar\"
let _4 := loadimmutable(\"8\")
/// @src 1:91:166 \"contract D is C(3)...\"
if and(1, sgt(_4, sub(shl(255, 1), 42)))
let sum := add(/** @src 0:124:126 \"41\" */ 0x29, /** @src 1:91:166 \"contract D is C(3)...\" */ _4)
if and(1, slt(sum, _4))
{
mstore(_3, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(_3, 0x24)
}
mstore(_1, add(/** @src 0:124:126 \"41\" */ 0x29, /** @src 1:91:166 \"contract D is C(3)...\" */ _4))
mstore(_1, sum)
return(_1, 32)
}
case 0x793816ec {
@@ -1579,20 +1583,15 @@ object \"D_72\" {
}
function checked_add_int256(x, y) -> sum
{
let _1 := slt(x, 0)
if and(iszero(_1), sgt(y, sub(sub(shl(255, 1), 1), x)))
{
mstore(0, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(0, 0x24)
}
if and(_1, slt(y, sub(shl(255, 1), x)))
{
mstore(0, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(0, 0x24)
}
sum := add(x, y)
let _1 := slt(sum, y)
let _2 := slt(x, 0)
if or(and(iszero(_2), _1), and(_2, iszero(_1)))
{
mstore(0, shl(224, 0x4e487b71))
mstore(4, 0x11)
revert(0, 0x24)
}
}
}
data \".metadata\" hex\"<BYTECODE REMOVED>\"
test/formal/checked_int_add.py
+10 -5
View File
@@ -1,4 +1,4 @@
from opcodes import AND, ISZERO, SGT, SLT, SUB
from opcodes import AND, ISZERO, SGT, SLT, ADD
from rule import Rule
from util import BVSignedMax, BVSignedMin, BVSignedUpCast
from z3 import BitVec, BVAddNoOverflow, BVAddNoUnderflow, Not
@@ -25,16 +25,21 @@ while type_bits <= n_bits:
# cast to full n_bits values
X = BVSignedUpCast(X_short, n_bits)
Y = BVSignedUpCast(Y_short, n_bits)
sum_ = ADD(X, Y)
# Constants
maxValue = BVSignedMax(type_bits, n_bits)
minValue = BVSignedMin(type_bits, n_bits)
# Overflow and underflow checks in YulUtilFunction::overflowCheckedIntAddFunction
overflow_check = AND(ISZERO(SLT(X, 0)), SGT(Y, SUB(maxValue, X)))
underflow_check = AND(SLT(X, 0), SLT(Y, SUB(minValue, X)))
if type_bits == 256:
overflow_check = AND(ISZERO(SLT(X, 0)), SLT(sum_, Y))
underflow_check = AND(SLT(X, 0), ISZERO(SLT(sum_, Y)))
else:
overflow_check = SGT(sum_, maxValue)
underflow_check = SLT(sum_, minValue)
type_bits += 8
rule.check(actual_overflow, overflow_check != 0)
rule.check(actual_underflow, underflow_check != 0)
type_bits *= 2
test/formal/checked_int_sub.py
+10 -5
View File
@@ -1,4 +1,4 @@
from opcodes import AND, ADD, ISZERO, SLT, SGT
from opcodes import AND, ISZERO, SLT, SGT, SUB
from rule import Rule
from util import BVSignedMax, BVSignedMin, BVSignedUpCast
from z3 import BitVec, BVSubNoOverflow, BVSubNoUnderflow, Not
@@ -25,16 +25,21 @@ while type_bits <= n_bits:
# cast to full n_bits values
X = BVSignedUpCast(X_short, n_bits)
Y = BVSignedUpCast(Y_short, n_bits)
diff = SUB(X, Y)
# Constants
maxValue = BVSignedMax(type_bits, n_bits)
minValue = BVSignedMin(type_bits, n_bits)
# Overflow and underflow checks in YulUtilFunction::overflowCheckedIntSubFunction
underflow_check = AND(ISZERO(SLT(Y, 0)), SLT(X, ADD(minValue, Y)))
overflow_check = AND(SLT(Y, 0), SGT(X, ADD(maxValue, Y)))
if type_bits == 256:
underflow_check = AND(ISZERO(SLT(Y, 0)), SGT(diff, X))
overflow_check = AND(SLT(Y, 0), SLT(diff, X))
else:
underflow_check = SLT(diff, minValue)
overflow_check = SGT(diff, maxValue)
type_bits += 8
rule.check(actual_underflow, underflow_check != 0)
rule.check(actual_overflow, overflow_check != 0)
type_bits *= 2
test/formal/checked_uint_add.py
+8 -4
View File
@@ -1,4 +1,4 @@
from opcodes import GT, SUB
from opcodes import GT, ADD
from rule import Rule
from util import BVUnsignedMax, BVUnsignedUpCast
from z3 import BitVec, BVAddNoOverflow, Not
@@ -24,13 +24,17 @@ while type_bits <= n_bits:
# cast to full n_bits values
X = BVUnsignedUpCast(X_short, n_bits)
Y = BVUnsignedUpCast(Y_short, n_bits)
sum_ = ADD(X, Y)
# Constants
maxValue = BVUnsignedMax(type_bits, n_bits)
# Overflow check in YulUtilFunction::overflowCheckedIntAddFunction
overflow_check = GT(X, SUB(maxValue, Y))
if type_bits == 256:
overflow_check = GT(X, sum_)
else:
overflow_check = GT(sum_, maxValue)
type_bits += 8
rule.check(overflow_check != 0, actual_overflow)
type_bits *= 2
test/formal/checked_uint_sub.py
+8 -4
View File
@@ -1,4 +1,4 @@
from opcodes import LT
from opcodes import SUB, GT
from rule import Rule
from util import BVUnsignedMax, BVUnsignedUpCast
from z3 import BVSubNoUnderflow, BitVec, Not
@@ -24,13 +24,17 @@ while type_bits <= n_bits:
# cast to full n_bits values
X = BVUnsignedUpCast(X_short, n_bits)
Y = BVUnsignedUpCast(Y_short, n_bits)
diff = SUB(X, Y)
# Constants
maxValue = BVUnsignedMax(type_bits, n_bits)
# Overflow check in YulUtilFunction::overflowCheckedIntSubFunction
overflow_check = LT(X, Y)
if type_bits == 256:
overflow_check = GT(diff, X)
else:
overflow_check = GT(diff, maxValue)
type_bits += 8
rule.check(overflow_check != 0, actual_overflow)
type_bits *= 2
test/libsolidity/semanticTests/array/copying/array_copy_target_leftover.sol
+3 -3
View File
@@ -19,6 +19,6 @@ contract c {
// compileToEwasm: also
// ----
// test() -> 0xffffffff, 0x0000000000000000000000000a00090008000700060005000400030002000100, 0x0000000000000000000000000000000000000000000000000000000000000000
// gas irOptimized: 124757
// gas legacy: 186184
// gas legacyOptimized: 165682
// gas irOptimized: 124817
// gas legacy: 186028
// gas legacyOptimized: 165692
test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_storage.sol
+4 -4
View File
@@ -38,10 +38,10 @@ contract c {
// compileViaYul: true
// ----
// test1(uint256[][]): 0x20, 2, 0x40, 0x40, 2, 23, 42 -> 2, 65
// gas irOptimized: 180766
// gas irOptimized: 180769
// test2(uint256[][2]): 0x20, 0x40, 0x40, 2, 23, 42 -> 2, 65
// gas irOptimized: 157564
// gas irOptimized: 157567
// test3(uint256[2][]): 0x20, 2, 23, 42, 23, 42 -> 2, 65
// gas irOptimized: 134630
// gas irOptimized: 134633
// test4(uint256[2][2]): 23, 42, 23, 42 -> 65
// gas irOptimized: 111268
// gas irOptimized: 111271
test/libsolidity/semanticTests/array/copying/array_nested_memory_to_storage.sol
+6 -6
View File
@@ -38,12 +38,12 @@ contract Test {
}
// ----
// test() -> 24
// gas irOptimized: 226694
// gas legacy: 227133
// gas legacyOptimized: 226547
// gas irOptimized: 226700
// gas legacy: 227121
// gas legacyOptimized: 226557
// test1() -> 3
// test2() -> 6
// test3() -> 24
// gas irOptimized: 133254
// gas legacy: 134295
// gas legacyOptimized: 133383
// gas irOptimized: 133260
// gas legacy: 134283
// gas legacyOptimized: 133393
test/libsolidity/semanticTests/array/dynamic_array_cleanup.sol
+3 -3
View File
@@ -14,9 +14,9 @@ contract c {
// ----
// storageEmpty -> 1
// fill() ->
// gas irOptimized: 519616
// gas legacy: 521710
// gas legacyOptimized: 516922
// gas irOptimized: 519490
// gas legacy: 521584
// gas legacyOptimized: 517027
// storageEmpty -> 0
// halfClear() ->
// storageEmpty -> 0
test/libsolidity/semanticTests/array/fixed_array_cleanup.sol
+3 -3
View File
@@ -12,9 +12,9 @@ contract c {
// ----
// storageEmpty -> 1
// fill() ->
// gas irOptimized: 465440
// gas legacy: 471400
// gas legacyOptimized: 467400
// gas irOptimized: 465380
// gas legacy: 471280
// gas legacyOptimized: 467500
// storageEmpty -> 0
// clear() ->
// storageEmpty -> 1
test/libsolidity/semanticTests/array/pop/array_pop_array_transition.sol
+2 -2
View File
@@ -23,7 +23,7 @@ contract c {
}
// ----
// test() -> 1, 2, 3
// gas irOptimized: 2280132
// gas irOptimized: 2280147
// gas legacy: 2273434
// gas legacyOptimized: 2261820
// gas legacyOptimized: 2261844
// storageEmpty -> 1
test/libsolidity/semanticTests/array/pop/array_pop_uint16_transition.sol
+2 -2
View File
@@ -18,7 +18,7 @@ contract c {
}
// ----
// test() -> 38, 28, 18
// gas irOptimized: 186364
// gas irOptimized: 186370
// gas legacy: 189492
// gas legacyOptimized: 178294
// gas legacyOptimized: 178318
// storageEmpty -> 1
test/libsolidity/semanticTests/array/pop/array_pop_uint24_transition.sol
+2 -2
View File
@@ -18,7 +18,7 @@ contract c {
}
// ----
// test() -> 20, 10
// gas irOptimized: 158009
// gas irOptimized: 158020
// gas legacy: 159279
// gas legacyOptimized: 152921
// gas legacyOptimized: 152937
// storageEmpty -> 1
test/libsolidity/semanticTests/array/pop/byte_array_pop_long_storage_empty.sol
+3 -3
View File
@@ -16,7 +16,7 @@ contract c {
}
// ----
// test() -> true
// gas irOptimized: 180539
// gas legacy: 228685
// gas legacyOptimized: 209662
// gas irOptimized: 176111
// gas legacy: 224093
// gas legacyOptimized: 205152
// storageEmpty -> 1
test/libsolidity/semanticTests/array/push/byte_array_push_transition.sol
+2 -2
View File
@@ -15,6 +15,6 @@ contract c {
}
// ----
// test() -> 0
// gas irOptimized: 173650
// gas irOptimized: 174126
// gas legacy: 216790
// gas legacyOptimized: 203886
// gas legacyOptimized: 204003
test/libsolidity/semanticTests/constructor_with_params_diamond_inheritance.sol
+3 -3
View File
@@ -21,9 +21,9 @@ contract D is B, C {
}
// ----
// constructor(): 2, 0 ->
// gas irOptimized: 154366
// gas legacy: 170665
// gas legacyOptimized: 145396
// gas irOptimized: 154331
// gas legacy: 170115
// gas legacyOptimized: 145429
// i() -> 2
// j() -> 2
// k() -> 1
test/libsolidity/semanticTests/constructor_with_params_inheritance.sol
+3 -3
View File
@@ -12,8 +12,8 @@ contract D is C {
}
// ----
// constructor(): 2, 0 ->
// gas irOptimized: 123982
// gas legacy: 139250
// gas legacyOptimized: 119367
// gas irOptimized: 123966
// gas legacy: 138700
// gas legacyOptimized: 119400
// i() -> 2
// k() -> 1
test/libsolidity/semanticTests/events/event_dynamic_array_storage.sol
+3 -3
View File
@@ -13,6 +13,6 @@ contract C {
// ----
// createEvent(uint256): 42 ->
// ~ emit E(uint256[]): 0x20, 0x03, 0x2a, 0x2b, 0x2c
// gas irOptimized: 113517
// gas legacy: 116393
// gas legacyOptimized: 114415
// gas irOptimized: 113514
// gas legacy: 116381
// gas legacyOptimized: 114425
test/libsolidity/semanticTests/events/event_dynamic_array_storage_v2.sol
+3 -3
View File
@@ -14,6 +14,6 @@ contract C {
// ----
// createEvent(uint256): 42 ->
// ~ emit E(uint256[]): 0x20, 0x03, 0x2a, 0x2b, 0x2c
// gas irOptimized: 113517
// gas legacy: 116393
// gas legacyOptimized: 114415
// gas irOptimized: 113514
// gas legacy: 116381
// gas legacyOptimized: 114425
test/libsolidity/semanticTests/events/event_dynamic_nested_array_storage_v2.sol
+2 -2
View File
@@ -16,5 +16,5 @@ contract C {
// createEvent(uint256): 42 ->
// ~ emit E(uint256[][]): 0x20, 0x02, 0x40, 0xa0, 0x02, 0x2a, 0x2b, 0x02, 0x2c, 0x2d
// gas irOptimized: 185145
// gas legacy: 187621
// gas legacyOptimized: 184551
// gas legacy: 187603
// gas legacyOptimized: 184566
test/libsolidity/semanticTests/externalContracts/base64.sol
+9 -9
View File
@@ -33,9 +33,9 @@ contract test {
// EVMVersion: >=constantinople
// ----
// constructor()
// gas irOptimized: 443542
// gas legacy: 765640
// gas legacyOptimized: 541810
// gas irOptimized: 444190
// gas legacy: 757857
// gas legacyOptimized: 539866
// encode_inline_asm(bytes): 0x20, 0 -> 0x20, 0
// encode_inline_asm(bytes): 0x20, 1, "f" -> 0x20, 4, "Zg=="
// encode_inline_asm(bytes): 0x20, 2, "fo" -> 0x20, 4, "Zm8="
@@ -51,10 +51,10 @@ contract test {
// encode_no_asm(bytes): 0x20, 5, "fooba" -> 0x20, 8, "Zm9vYmE="
// encode_no_asm(bytes): 0x20, 6, "foobar" -> 0x20, 8, "Zm9vYmFy"
// encode_inline_asm_large()
// gas irOptimized: 1385042
// gas legacy: 1652033
// gas legacyOptimized: 1201033
// gas irOptimized: 1382042
// gas legacy: 1646033
// gas legacyOptimized: 1206033
// encode_no_asm_large()
// gas irOptimized: 3335099
// gas legacy: 4777077
// gas legacyOptimized: 2890077
// gas irOptimized: 3311099
// gas legacy: 4723077
// gas legacyOptimized: 2909077
test/libsolidity/semanticTests/externalContracts/deposit_contract.sol
+3 -3
View File
@@ -176,9 +176,9 @@ contract DepositContract is IDepositContract, ERC165 {
}
// ----
// constructor()
// gas irOptimized: 1433406
// gas legacy: 2435803
// gas legacyOptimized: 1775425
// gas irOptimized: 1432633
// gas legacy: 2427722
// gas legacyOptimized: 1773892
// supportsInterface(bytes4): 0x0 -> 0
// supportsInterface(bytes4): 0xffffffff00000000000000000000000000000000000000000000000000000000 -> false # defined to be false by ERC-165 #
// supportsInterface(bytes4): 0x01ffc9a700000000000000000000000000000000000000000000000000000000 -> true # ERC-165 id #
test/libsolidity/semanticTests/externalContracts/prbmath_signed.sol
+3 -3
View File
@@ -48,9 +48,9 @@ contract test {
}
// ----
// constructor()
// gas irOptimized: 1878547
// gas legacy: 2478955
// gas legacyOptimized: 1877737
// gas irOptimized: 1876171
// gas legacy: 2471603
// gas legacyOptimized: 1876669
// div(int256,int256): 3141592653589793238, 88714123 -> 35412542528203691288251815328
// gas irOptimized: 22137
// gas legacy: 22767
test/libsolidity/semanticTests/externalContracts/prbmath_unsigned.sol
+3 -3
View File
@@ -48,9 +48,9 @@ contract test {
}
// ----
// constructor()
// gas irOptimized: 1737100
// gas legacy: 2248594
// gas legacyOptimized: 1749096
// gas irOptimized: 1735588
// gas legacy: 2241243
// gas legacyOptimized: 1748028
// div(uint256,uint256): 3141592653589793238, 88714123 -> 35412542528203691288251815328
// gas irOptimized: 22004
// gas legacy: 22497
test/libsolidity/semanticTests/externalContracts/ramanujan_pi.sol
+3 -3
View File
@@ -33,9 +33,9 @@ contract test {
}
// ----
// constructor()
// gas irOptimized: 438112
// gas legacy: 671453
// gas legacyOptimized: 480242
// gas irOptimized: 422763
// gas legacy: 654526
// gas legacyOptimized: 474842
// prb_pi() -> 3141592656369545286
// gas irOptimized: 57478
// gas legacy: 98903
test/libsolidity/semanticTests/externalContracts/snark.sol
+1 -1
View File
@@ -297,5 +297,5 @@ contract Test {
// verifyTx() -> true
// ~ emit Verified(string): 0x20, 0x16, "Successfully verified."
// gas irOptimized: 95261
// gas legacy: 113731
// gas legacy: 113239
// gas legacyOptimized: 83670
test/libsolidity/semanticTests/externalContracts/strings.sol
+6 -6
View File
@@ -49,9 +49,9 @@ contract test {
}
// ----
// constructor()
// gas irOptimized: 691317
// gas legacy: 1127730
// gas legacyOptimized: 753807
// gas irOptimized: 678980
// gas legacy: 1103242
// gas legacyOptimized: 745184
// toSlice(string): 0x20, 11, "hello world" -> 11, 0xa0
// gas irOptimized: 22660
// gas legacy: 23190
@@ -69,6 +69,6 @@ contract test {
// gas legacy: 31621
// gas legacyOptimized: 27914
// benchmark(string,bytes32): 0x40, 0x0842021, 8, "solidity" -> 0x2020
// gas irOptimized: 2040019
// gas legacy: 4356286
// gas legacyOptimized: 2268278
// gas irOptimized: 2017767
// gas legacy: 4294510
// gas legacyOptimized: 2327982
test/libsolidity/semanticTests/functionCall/external_call_to_nonexisting.sol
+3 -3
View File
@@ -23,9 +23,9 @@ contract C {
// ----
// constructor(), 1 ether ->
// gas irOptimized: 270677
// gas legacy: 464030
// gas legacyOptimized: 304049
// gas irOptimized: 270449
// gas legacy: 456680
// gas legacyOptimized: 302975
// f(uint256): 0 -> FAILURE
// f(uint256): 1 -> FAILURE
// f(uint256): 2 -> FAILURE
test/libsolidity/semanticTests/functionCall/external_call_to_nonexisting_debugstrings.sol
+3 -3
View File
@@ -26,9 +26,9 @@ contract C {
// revertStrings: debug
// ----
// constructor(), 1 ether ->
// gas irOptimized: 428679
// gas legacy: 832976
// gas legacyOptimized: 509560
// gas irOptimized: 428444
// gas legacy: 825625
// gas legacyOptimized: 508492
// f(uint256): 0 -> FAILURE, hex"08c379a0", 0x20, 37, "Target contract does not contain", " code"
// f(uint256): 1 -> FAILURE, hex"08c379a0", 0x20, 37, "Target contract does not contain", " code"
// f(uint256): 2 -> FAILURE, hex"08c379a0", 0x20, 37, "Target contract does not contain", " code"
test/libsolidity/semanticTests/functionCall/failed_create.sol
+3 -3
View File
@@ -17,9 +17,9 @@ contract C {
// EVMVersion: >=byzantium
// ----
// constructor(), 20 wei
// gas irOptimized: 184221
// gas irOptimized: 184005
// gas legacy: 294335
// gas legacyOptimized: 174279
// gas legacyOptimized: 173427
// f(uint256): 20 -> 1370859564726510389319704988634906228201275401179
// x() -> 1
// f(uint256): 20 -> FAILURE
@@ -27,7 +27,7 @@ contract C {
// stack(uint256): 1023 -> FAILURE
// gas irOptimized: 260987
// gas legacy: 483942
// gas legacyOptimized: 298807
// gas legacyOptimized: 302349
// x() -> 1
// stack(uint256): 10 -> 693016686122178122849713379390321835634789309880
// x() -> 2
test/libsolidity/semanticTests/functionTypes/store_function.sol
+2 -2
View File
@@ -27,5 +27,5 @@ contract C {
// ----
// t() -> 9
// gas irOptimized: 99064
// gas legacy: 158955
// gas legacyOptimized: 108788
// gas legacy: 152137
// gas legacyOptimized: 107793
test/libsolidity/semanticTests/immutable/use_scratch.sol
+2 -2
View File
@@ -16,7 +16,7 @@ contract C {
// ----
// constructor(): 3 ->
// gas irOptimized: 125477
// gas legacy: 209361
// gas legacyOptimized: 139324
// gas legacy: 202011
// gas legacyOptimized: 139552
// f() -> 84, 23
// m(uint256): 3 -> 7
test/libsolidity/semanticTests/salted_create/salted_create_with_value.sol
+3 -3
View File
@@ -21,6 +21,6 @@ contract A {
// EVMVersion: >=constantinople
// ----
// f(), 10 ether -> 3007, 3008, 3009
// gas irOptimized: 257206
// gas legacy: 422501
// gas legacyOptimized: 287472
// gas irOptimized: 268645
// gas legacy: 402016
// gas legacyOptimized: 288087
test/libsolidity/semanticTests/userDefinedValueType/erc20.sol
+3 -3
View File
@@ -113,9 +113,9 @@ contract ERC20 {
// ----
// constructor()
// ~ emit Transfer(address,address,uint256): #0x00, #0x1212121212121212121212121212120000000012, 0x14
// gas irOptimized: 364503
// gas legacy: 860880
// gas legacyOptimized: 420959
// gas irOptimized: 362054
// gas legacy: 852973
// gas legacyOptimized: 419237
// totalSupply() -> 20
// gas irOptimized: 23415
// gas legacy: 23653
test/libsolidity/semanticTests/using/using_global_invisible.sol
+1 -1
View File
@@ -40,4 +40,4 @@ contract D {
// ----
// library: "A":L
// test() -> 3
// gas legacy: 130369
// gas legacy: 123521
test/libsolidity/semanticTests/various/erc20.sol
+3 -3
View File
@@ -96,9 +96,9 @@ contract ERC20 {
// ----
// constructor()
// ~ emit Transfer(address,address,uint256): #0x00, #0x1212121212121212121212121212120000000012, 0x14
// gas irOptimized: 357114
// gas legacy: 832643
// gas legacyOptimized: 416135
// gas irOptimized: 357746
// gas legacy: 824737
// gas legacyOptimized: 414462
// totalSupply() -> 20
// gas irOptimized: 23415
// gas legacy: 23524
test/libsolidity/semanticTests/various/value_complex.sol
+3 -3
View File
@@ -20,7 +20,7 @@ contract test {
// ----
// constructor(), 20 wei ->
// gas irOptimized: 176219
// gas legacy: 265006
// gas legacyOptimized: 182842
// gas irOptimized: 176003
// gas legacy: 257656
// gas legacyOptimized: 183070
// sendAmount(uint256): 5 -> 8
test/libsolidity/semanticTests/various/value_insane.sol
+3 -3
View File
@@ -19,7 +19,7 @@ contract test {
// ----
// constructor(), 20 wei ->
// gas irOptimized: 177083
// gas legacy: 266728
// gas legacyOptimized: 184762
// gas irOptimized: 176867
// gas legacy: 259378
// gas legacyOptimized: 183682
// sendAmount(uint256): 5 -> 8
test/libsolidity/semanticTests/viaYul/array_memory_index_access.sol
+3 -3
View File
@@ -26,9 +26,9 @@ contract C {
// index(uint256): 10 -> true
// index(uint256): 20 -> true
// index(uint256): 0xFF -> true
// gas irOptimized: 135578
// gas legacy: 247324
// gas legacyOptimized: 149578
// gas irOptimized: 135584
// gas legacy: 244264
// gas legacyOptimized: 152128
// accessIndex(uint256,int256): 10, 1 -> 2
// accessIndex(uint256,int256): 10, 0 -> 1
// accessIndex(uint256,int256): 10, 11 -> FAILURE, hex"4e487b71", 0x32
test/libsolidity/semanticTests/viaYul/array_storage_index_access.sol
+14 -14
View File
@@ -17,32 +17,32 @@ contract C {
// test_indices(uint256): 1 ->
// test_indices(uint256): 129 ->
// gas irOptimized: 3018687
// gas legacy: 3070431
// gas legacyOptimized: 3010325
// gas legacy: 3068883
// gas legacyOptimized: 3011615
// test_indices(uint256): 5 ->
// gas irOptimized: 372543
// gas legacy: 369211
// gas legacyOptimized: 366089
// gas legacy: 369151
// gas legacyOptimized: 366139
// test_indices(uint256): 10 ->
// test_indices(uint256): 15 ->
// gas irOptimized: 72860
// test_indices(uint256): 0xFF ->
// gas irOptimized: 3410255
// gas legacy: 3512637
// gas legacyOptimized: 3395047
// gas legacy: 3509577
// gas legacyOptimized: 3397597
// test_indices(uint256): 1000 ->
// gas irOptimized: 18206122
// gas legacy: 18611999
// gas legacyOptimized: 18166944
// gas legacy: 18599999
// gas legacyOptimized: 18176944
// test_indices(uint256): 129 ->
// gas irOptimized: 2756955
// gas legacy: 2771961
// gas legacyOptimized: 2714999
// gas legacy: 2770413
// gas legacyOptimized: 2716289
// test_indices(uint256): 128 ->
// gas irOptimized: 411903
// gas legacy: 466504
// gas legacyOptimized: 416888
// gas legacy: 464968
// gas legacyOptimized: 418168
// test_indices(uint256): 1 ->
// gas irOptimized: 368571
// gas legacy: 363401
// gas legacyOptimized: 361799
// gas legacy: 363389
// gas legacyOptimized: 361809
test/libsolidity/semanticTests/viaYul/array_storage_index_zeroed_test.sol
+12 -12
View File
@@ -52,18 +52,18 @@ contract C {
// ----
// test_zeroed_indicies(uint256): 1 ->
// test_zeroed_indicies(uint256): 5 ->
// gas irOptimized: 131192
// gas legacy: 132331
// gas legacyOptimized: 129514
// gas irOptimized: 131177
// gas legacy: 132301
// gas legacyOptimized: 129539
// test_zeroed_indicies(uint256): 10 ->
// gas irOptimized: 174810
// gas legacy: 177248
// gas legacyOptimized: 172062
// gas irOptimized: 174780
// gas legacy: 177188
// gas legacyOptimized: 172112
// test_zeroed_indicies(uint256): 15 ->
// gas irOptimized: 198070
// gas legacy: 201828
// gas legacyOptimized: 194352
// gas irOptimized: 198025
// gas legacy: 201738
// gas legacyOptimized: 194427
// test_zeroed_indicies(uint256): 0xFF ->
// gas irOptimized: 6098680
// gas legacy: 6160863
// gas legacyOptimized: 6024902
// gas irOptimized: 6097915
// gas legacy: 6159333
// gas legacyOptimized: 6026177