Check that a + b does not overflow.
(a: BitVecRef, b: BitVecRef, signed: bool = False)
| 1972 | |
| 1973 | |
| 1974 | def BVAddNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool = False) -> BoolRef: |
| 1975 | """Check that a + b does not overflow.""" |
| 1976 | sort = a._sort |
| 1977 | if not isinstance(sort, BitVecSortRef): |
| 1978 | raise TypeError("BVAddNoOverflow requires BitVecRef") |
| 1979 | w = sort._width |
| 1980 | if signed: |
| 1981 | # Signed: extend to w+1, add, check fits in w signed range |
| 1982 | ea = SignExt(1, a) |
| 1983 | eb = SignExt(1, b) |
| 1984 | s = ea + eb |
| 1985 | upper = BitVecVal((1 << (w - 1)) - 1, w + 1) |
| 1986 | return s <= upper |
| 1987 | else: |
| 1988 | ea = ZeroExt(1, a) |
| 1989 | eb = ZeroExt(1, b) |
| 1990 | s = ea + eb |
| 1991 | upper = BitVecVal((1 << w) - 1, w + 1) |
| 1992 | return ULE(s, upper) |
| 1993 | |
| 1994 | |
| 1995 | def BVAddNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: |