claripy
claripy copied to clipboard
Widening operator doesn't widen
Errant Behavior: In (at least) the following case, widening has no effect, although the interval being widened to has a value not included in the first interval:
Interval a covers 32-bit values 0x000003E8 through 0xFFFFFFFF and interval b covers 32-bit values 0x000003E9 thru 0x00000000. Interval c is the widening of a to b:
a = StridedInterval(None, 32, 1, 1000, 0xFFFFFFFF)
b = StridedInterval(None, 32, 1, 1001, 0)
c = a.widen(b)
The value 0 is not included in interval a, but is included in interval b:
(Pdb) p a.solution(0)
False
(Pdb) p b.solution(0)
True
Yet widening a to b just results in a, and 0 isn't included:
(Pdb) p a.identical(c)
True
(Pdb) p c.solution(0)
False
Expected behavior: I expect c to be some interval wider than a which includes all values of b (in particular: 0), something like <32>0x1[0x3e8, 0]
or <32>0x1[0,0xFFFFFFFF]
.