solang-parser 0.2.1

Solang Solidity Parser
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

from opcodes import GT, SUB
from rule import Rule
from util import BVUnsignedMax, BVUnsignedUpCast
from z3 import BitVec, BVAddNoOverflow, Not

"""
Overflow checked unsigned integer addition.
"""

n_bits = 256
type_bits = 8

while type_bits <= n_bits:

	rule = Rule()

	# Input vars
	X_short = BitVec('X', type_bits)
	Y_short = BitVec('Y', type_bits)

	# Z3's overflow condition
	actual_overflow = Not(BVAddNoOverflow(X_short, Y_short, False))

	# cast to full n_bits values
	X = BVUnsignedUpCast(X_short, n_bits)
	Y = BVUnsignedUpCast(Y_short, n_bits)

	# Constants
	maxValue = BVUnsignedMax(type_bits, n_bits)

	# Overflow check in YulUtilFunction::overflowCheckedIntAddFunction
	overflow_check = GT(X, SUB(maxValue, Y))

	rule.check(overflow_check != 0, actual_overflow)

	type_bits *= 2