"""
This file contains an abstract domain IntBound for word-sized integers. This is
used to perform abstract interpretation on traces, specifically the integer
operations on them.

The abstract domain tracks a (signed) upper and lower bound (both ends
inclusive) for every integer variable in the trace. It also tracks which bits
of a range are known 0 or known 1 (the remaining bits are unknown. The ranges
and the known bits feed back into each other, ie we can improve the range if
some upper bits have known values, and we can learn some known bits from the
range too. Every instance of IntBound represents a set of concrete integers.

We do the analysis at the same time as optimization. We initialize all integer
variables to have an unknown range, with no known bits. Then we proceed along
the trace and improve the ranges. We can shrink ranges if we see integer
comparisons followed by guards. We can learn some bits of an integer if there
are bit-operations such as `and` (masking out some bits), followed by a guard.

For every operation in the trace we use a "transfer function" that computes an
IntBound instance for the result of that operation, given the IntBounds of the
arguments. Those functions are called `..._bound`, eg `add_bound`, `and_bound`,
`neg_bound`, etc. Applying the transfer functions while we encounter them along
the trace is forwards reasoning.

We can also reason backwards (but we only do that in a limited way). Here's an
example:

i1 = int_add(i0, 1)
i2 = int_lt(i1, 100)
guard_true(i2)

At the last guard we learn that i1 < 100 must be true, and from that we can
conclude that i0 < 99 in the rest of the trace (this is not quite true due to
possible overflow of the int_add).

More generally, when we shrink (ie make more precise) an IntBound instance due
to a guard, we can often conclude something about earlier variables in the
trace. To reason backwards we look at the operation that created a variable and
then compute the implications.

The reason for having both a range and known bits are that each of them is good
for different situations. Range knownledge is useful for comparisons and
"linear" operations like additions, subtractions, multiplications, etc.
Knowledge about certain bits is good for bit twiddling code, bitfields, stuff
like that.
"""

import sys
from rpython.rlib.rarithmetic import ovfcheck, LONG_BIT, maxint, is_valid_int, r_uint, intmask
from rpython.rlib.objectmodel import we_are_translated, always_inline
from rpython.rtyper.lltypesystem import lltype
from rpython.rtyper.lltypesystem.lloperation import llop
from rpython.jit.metainterp.resoperation import rop, ResOperation
from rpython.jit.metainterp.optimize import InvalidLoop
from rpython.jit.metainterp.optimizeopt.info import AbstractInfo, INFO_NONNULL,\
     INFO_UNKNOWN, INFO_NULL
from rpython.jit.metainterp.history import ConstInt


MAXINT = maxint
MININT = -maxint - 1

IS_64_BIT = sys.maxint > 2**32

TNUM_UNKNOWN = r_uint(0), r_uint(-1)
TNUM_KNOWN_ZERO = r_uint(0), r_uint(0)
TNUM_KNOWN_BITWISEONE = r_uint(-1), r_uint(0)
TNUM_ONLY_VALUE_DEFAULT = r_uint(0)
TNUM_ONLY_MASK_UNKNOWN = r_uint(-1)
TNUM_ONLY_MASK_DEFAULT = TNUM_ONLY_MASK_UNKNOWN


class IntBound(AbstractInfo):
    """
    Abstract domain representation of an integer,
    approximating via integer bounds and known-bits
    tri-state numbers.
    """
    _attrs_ = ('upper', 'lower', 'tvalue', 'tmask')

    def __init__(self, lower=MININT, upper=MAXINT,
                 tvalue=TNUM_ONLY_VALUE_DEFAULT,
                 tmask=TNUM_ONLY_MASK_DEFAULT,
                 do_shrinking=True):
        """
        Instantiates an abstract representation of integer.
        The default parameters set this abstract int to
        contain all integers.

        It is recommended to use the indirect constructors
        below instead of this one.
        """

        self.lower = lower
        self.upper = upper

        # known-bit analysis using tristate/knownbits numbers:
        # every bit can be either 0, 1, or unknown (?).
        # the encoding of these three states is:
        # value       0 1 ?
        # tvalue bit  0 1 0
        # tmask bit   0 0 1
        # the combination tvalue=tmask=1 is forbidden
        assert is_valid_tnum(tvalue, tmask)
        self.tvalue = tvalue
        self.tmask = tmask         # bit=1 means unknown

        # check for unexpected overflows:
        if not we_are_translated():
            assert type(upper) is not long or is_valid_int(upper)
            assert type(lower) is not long or is_valid_int(lower)

        if do_shrinking:
            self.shrink()
            assert self._debug_check()

    @staticmethod
    def from_constant(value):
        """
        Constructs an abstract integer that represents a constant (a completely
        known integer).
        """
        # this one does NOT require a r_uint for `value`.
        assert not isinstance(value, r_uint)
        tvalue = value
        tmask = 0
        bvalue = value
        do_shrinking = False
        if not isinstance(value, int):
            # workaround for AddressAsInt / symbolic ints
            # by CF
            tvalue = 0
            tmask = -1
            bvalue = 0
            do_shrinking = True
        b = IntBound(lower=bvalue,
                     upper=bvalue,
                     tvalue=r_uint(tvalue),
                     tmask=r_uint(tmask), do_shrinking=do_shrinking)
        return b

    @staticmethod
    def unbounded():
        """
        Constructs an abstract integer that is completely unknown (e.g. it
        contains every integer).
        """
        return IntBound(do_shrinking=False)

    @staticmethod
    def nonnegative():
        """
        Construct a non-negative abstract integer.
        """
        return IntBound(lower=0)

    @staticmethod
    def from_knownbits(tvalue, tmask, do_unmask=False):
        """
        Constructs an abstract integer where the bits determined by `tvalue`
        and `tmask` are (un-)known. tvalue and tmask must be r_uints.
        """
        assert isinstance(tvalue, r_uint) and isinstance(tmask, r_uint)
        if do_unmask:
            tvalue = unmask_zero(tvalue, tmask)
        return IntBound(tvalue=tvalue,
                        tmask=tmask)

    # ____________________________________________________________
    # a bunch of slightly artificial methods that are needed to make some of
    # the Z3 proofs in test_z3intbound possible, they are overridden there

    @staticmethod
    @always_inline
    def new(lower, upper, tvalue, tmask):
        """ helper factory to construct a new IntBound. overridden in
        test_z3intbound """
        return IntBound(lower, upper, tvalue, tmask)

    intmask = staticmethod(intmask)
    r_uint = staticmethod(r_uint)

    @staticmethod
    @always_inline
    def _add_check_overflow(a, b, value_if_overflow):
        """ returns a + b, or value_if_overflow if that (signed) addition would
        overflow """
        try:
            return ovfcheck(a + b)
        except OverflowError:
            return value_if_overflow

    @staticmethod
    @always_inline
    def _sub_check_overflow(a, b, value_if_overflow):
        """ returns a - b, or value_if_overflow if that (signed) subtraction would
        overflow """
        try:
            return ovfcheck(a - b)
        except OverflowError:
            return value_if_overflow

    @staticmethod
    @always_inline
    def _urshift(a, b):
        return r_uint(a) >> r_uint(b)

    # ____________________________________________________________

    @staticmethod
    def _to_dec_or_hex_str_heuristics(num):
        # a few formatting heuristics
        if -1000 <= num <= 1000:
            return str(num)
        if num == MININT:
            return "MININT"
        if num == MAXINT:
            return "MAXINT"
        if num >= 0:
            diff = MAXINT - num
            if diff < 1000:
                return "MAXINT - %s" % diff
        else:
            diff = -(MININT - num) # can't overflow because num < 0
            if diff < 1000:
                return "MININT + %s" % diff
        uintnum = r_uint(num)
        if uintnum & (uintnum - 1) == 0:
            # power of two, use hex
            return hex(num)
        # format number as decimal if fewer than 6 significant
        # digits, otherwise use hex
        curr = num
        exp10 = 0
        while curr % 10 == 0:
            curr //= 10
            exp10 += 1
        s = str(num)
        if len(s) - exp10 >= 6:
            return hex(num)
        return s

    def _are_knownbits_implied(self):
        """ return True if the knownbits of self are a direct consequence of
        the range of self (and thus carry no extra information) """
        tvalue, tmask = self._tnum_implied_by_bounds()
        return self.tmask == tmask and self.tvalue == tvalue

    def _are_bounds_implied(self):
        """ return True if the bounds of self are a direct consequence of the
        knownbits of self (and thus carry no extra information) """
        lower = self._get_minimum_signed_by_knownbits()
        upper = self._get_maximum_signed_by_knownbits()
        return self.lower == lower and self.upper == upper

    def __repr__(self):
        if self.is_unbounded():
            return "IntBound.unbounded()"
        if self.lower == 0 and self.upper == MAXINT and self._are_knownbits_implied():
            return "IntBound.nonnegative()"
        if self.is_constant():
            return "IntBound.from_constant(%s)" % self._to_dec_or_hex_str_heuristics(self.get_constant_int())
        s_bounds = "%s, %s" % (self._to_dec_or_hex_str_heuristics(self.lower),
                               self._to_dec_or_hex_str_heuristics(self.upper))

        if self._are_knownbits_implied():
            return "IntBound(%s)" % s_bounds

        s_tnum = "r_uint(%s), r_uint(%s)" % (bin(intmask(self.tvalue)), bin(intmask(self.tmask)))
        if self._are_bounds_implied():
            return "IntBound.from_knownbits(%s)" % s_tnum
        return "IntBound(%s, %s)" % (s_bounds, s_tnum)

    def __str__(self):
        if self.is_constant():
            return '(%s)' % self._to_dec_or_hex_str_heuristics(self.get_constant_int())
        if self.lower == 0 and self.upper == 1:
            return '(bool)'
        if self.lower == MININT:
            lower = ''
        else:
            lower = '%s <= ' % self._to_dec_or_hex_str_heuristics(self.lower)
        if self.upper == MAXINT:
            upper = ''
        else:
            upper = ' <= %s' % self._to_dec_or_hex_str_heuristics(self.upper)
        s = self.knownbits_string()
        if "0" not in s and "1" not in s:
            s = '?'
        else:
            # replace the longest sequence of same characters by ...
            prev_char = s[0]
            count = 0
            max_length = 0
            max_char = '\x00'
            start_pos = 0
            max_pos = -1
            for pos, char in enumerate(s):
                if char == prev_char:
                    count += 1
                else:
                    if count > max_length:
                        max_length = count
                        max_char = prev_char
                        max_pos = start_pos
                    prev_char = char
                    count = 1
                    start_pos = pos
            if count > max_length:
                max_length = count
                max_char = prev_char
                max_pos = start_pos
            if max_length > 5:
                assert max_pos >= 0
                s = s[:max_pos] + max_char + "..." + max_char + s[max_pos + max_length:]
            s = '0b' + s
        return '(%s%s%s)' % (lower, s, upper)

    def set_tvalue_tmask(self, tvalue, tmask):
        changed = self.tvalue != tvalue or self.tmask != tmask
        if changed:
            self.tvalue = tvalue
            self.tmask = tmask
            self.shrink()
        return changed

    def make_le(self, other):
        """
        Sets the bounds of `self` so that it only contains values lower than or
        equal to the values contained in `other`. Returns `True` iff the bound
        was updated. Will raise InvalidLoop if the resulting interval is empty.
        Mutates `self`.
        """
        return self.make_le_const(other.upper)

    def make_le_const(self, value):
        """
        Sets the bounds of `self` so that it only contains values lower than or
        equal to `value`. Returns `True` iff the bound was updated. Will raise
        InvalidLoop if the resulting interval is empty.
        Mutates `self`.
        """
        if value < self.upper:
            if value < self.lower:
                raise InvalidLoop
            self.upper = value
            self.shrink()
            return True
        return False

    def make_lt(self, other):
        """
        Sets the bounds of `self` so that it only contains values lower than
        the values contained in `other`. Returns `True` iff the bound was
        updated. Will raise InvalidLoop if the resulting interval is empty.
        (Mutates `self`.)
        """
        return self.make_lt_const(other.upper)

    def make_lt_const(self, value):
        """
        Sets the bounds of `self` so that it only contains values lower than
        `value`. Returns `True` iff the bound was updated. Will raise
        InvalidLoop if the resulting interval is empty. (Mutates `self`.)
        """
        if value == MININT:
            raise InvalidLoop("intbound can't be made smaller than MININT")
        return self.make_le_const(value - 1)

    def make_ge(self, other):
        """
        Sets the bounds of `self` so that it only contains values greater than
        or equal to the values contained in `other`. Returns `True` iff the
        bound was updated. Will raise InvalidLoop if the resulting interval is
        empty. (Mutates `self`.)
        """
        return self.make_ge_const(other.lower)

    def make_ge_const(self, value):
        """
        Sets the bounds of `self` so that it only contains values greater than
        or equal to `value`. Returns `True` iff the bound was updated. Will
        raise InvalidLoop if the resulting interval is empty. (Mutates `self`.)
        """
        if value > self.lower:
            if value > self.upper:
                raise InvalidLoop
            self.lower = value
            self.shrink()
            return True
        return False

    def make_gt(self, other):
        """
        Sets the bounds of `self` so that it only contains values greater than
        the values contained in `other`. Returns `True` iff the bound was
        updated. Will raise InvalidLoop if the resulting interval is empty.
        (Mutates `self`.)
        """
        return self.make_gt_const(other.lower)

    def make_gt_const(self, value):
        """
        Sets the bounds of `self` so that it only contains values greater than
        `value`. Returns `True` iff the bound was updated. Will raise
        InvalidLoop if the resulting interval is empty. (Mutates `self`.)
        """
        if value == MAXINT:
            raise InvalidLoop
        return self.make_ge_const(value + 1)

    def make_eq_const(self, intval):
        """
        Sets the properties of this abstract integer
        so that it is constant and equals `intval`.
        (Mutates `self`.)
        """
        if not self.contains(intval):
            raise InvalidLoop("constant int is outside of interval")
        self.upper = intval
        self.lower = intval
        self.tvalue = r_uint(intval)
        self.tmask = r_uint(0)

    def make_ne_const(self, intval):
        if self.lower < intval == self.upper:
            self.upper -= 1
            self.shrink()
            return True
        if self.lower == intval < self.upper:
            self.lower += 1
            self.shrink()
            return True
        return False

    def is_constant(self):
        """
        Returns `True` iff this abstract integer
        does contain only one concrete integer.
        """
        # both the bounds and the tnum encode the concrete integer
        res = self.lower == self.upper
        assert res == (self.tmask == r_uint(0))
        if res:
            assert self.lower == intmask(self.tvalue)
        return res

    def get_constant_int(self):
        """
        Returns the only integer contained in this abstract integer. Caller
        needs to check that `.is_constant()` returns True, before calling.
        """
        assert self.is_constant()
        return self.lower

    def known_eq_const(self, value):
        """
        Returns `True` iff this abstract integer contains only one (1) integer
        that does equal `value`.
        """
        if not self.is_constant():
            return False
        else:
            return self.lower == value

    def known_lt_const(self, value):
        """
        Returns `True` iff each number contained in this abstract integer is
        lower than `value`.
        """
        return self.upper < value

    def known_le_const(self, value):
        """
        Returns `True` iff each number contained in this abstract integer is
        lower than or equal to `value`.
        """
        return self.upper <= value

    def known_gt_const(self, value):
        """
        Returns `True` iff each number contained in this abstract integer is
        greater than `value`.
        """
        return self.lower > value

    def known_ge_const(self, value):
        """
        Returns `True` iff each number contained in this abstract integer is
        greater than equal to `value`.
        """
        return self.lower >= value

    def known_lt(self, other):
        """
        Returns `True` iff each number contained in this abstract integer is
        lower than each integer contained in `other`.
        """
        return self.known_lt_const(other.lower)

    def known_le(self, other):
        """
        Returns `True` iff each number contained in this abstract integer is
        lower than or equal to each integer contained in `other`.
        """
        return self.known_le_const(other.lower)

    def known_gt(self, other):
        """
        Returns `True` iff each number contained in this abstract integer is
        greater than each integer contained in `other`.
        """
        return other.known_lt(self)

    def known_ge(self, other):
        """
        Returns `True` iff each number contained in this abstract integer is
        greater than or equal to each integer contained in `other`.
        """
        return other.known_le(self)

    def known_ne(self, other):
        """ return True if the sets of numbers self and other must be disjoint.
        """
        # easy cases part 1: ranges don't overlap
        if self.known_lt(other):
            return True
        if self.known_gt(other):
            return True
        # easy case part 2: check whether the knownbits contradict
        both_known = self.tmask | other.tmask
        if unmask_zero(self.tvalue, both_known) != unmask_zero(other.tvalue, both_known):
            return True
        # for more complicated interactions between ranges and knownbits use
        # the logic in intersect
        newself = self.clone()
        try:
            newself.intersect(other)
        except InvalidLoop:
            return True
        return False

    def known_nonnegative(self):
        """
        Returns `True` if this abstract integer only contains numbers greater
        than or equal to `0` (zero).
        """
        return 0 <= self.lower

    def make_unsigned_le(self, other):
        if other.known_nonnegative():
            return self.intersect_const(0, other.upper)
        return False

    def make_unsigned_lt(self, other):
        if other.known_nonnegative():
            assert other.upper >= 0
            if other.upper == 0:
                raise InvalidLoop
            return self.intersect_const(0, other.upper - 1)
        return False

    def make_unsigned_ge(self, other):
        if other.upper < 0:
            changed = self.make_lt_const(0)
            return self.make_ge(other) or changed
        if self.known_nonnegative() and other.known_nonnegative():
            return self.make_ge(other)
        return False

    def make_unsigned_gt(self, other):
        if other.upper < 0:
            changed = self.make_lt_const(0)
            return self.make_gt(other) or changed
        if self.known_nonnegative() and other.known_nonnegative():
            return self.make_gt(other)
        return False

    def _known_same_sign(self, other):
        # return True if self and other are both either known non-negative or
        # both known negative
        if self.known_nonnegative() and other.known_nonnegative():
            return True
        return self.known_lt_const(0) and other.known_lt_const(0)

    def known_unsigned_lt(self, other):
        """
        Returns `True` iff each unsigned integer contained in this abstract
        integer is lower than each unsigned integer contained in `other`.
        """
        # if they have the same sign, we can reason with signed comparison
        # see test_uint_cmp_equivalent_int_cmp_if_same_sign
        if self._known_same_sign(other) and self.known_lt(other):
            return True
        other_min_unsigned_by_knownbits = other.get_minimum_unsigned_by_knownbits()
        self_max_unsigned_by_knownbits = self.get_maximum_unsigned_by_knownbits()
        return self_max_unsigned_by_knownbits < other_min_unsigned_by_knownbits

    def known_unsigned_le(self, other):
        """
        Returns `True` iff each unsigned integer contained in this abstract
        integer is lower or equal than each unsigned integer contained in
        `other`. """
        # if they have the same sign, we can reason with signed comparison
        if self._known_same_sign(other) and self.known_le(other):
            return True
        other_min_unsigned_by_knownbits = other.get_minimum_unsigned_by_knownbits()
        self_max_unsigned_by_knownbits = self.get_maximum_unsigned_by_knownbits()
        return self_max_unsigned_by_knownbits <= other_min_unsigned_by_knownbits

    def known_unsigned_gt(self, other):
        """
        Returns `True` iff each unsigned integer contained in this abstract
        integer is greater than each unsigned integer contained in `other`.
        """
        return other.known_unsigned_lt(self)

    def known_unsigned_ge(self, other):
        """
        Returns `True` iff each unsigned integer contained in this abstract
        integer is greater or equal than each unsigned integer contained in
        `other`.
        """
        return other.known_unsigned_le(self)

    def get_minimum_unsigned_by_knownbits(self):
        """
        Returns the minimum unsigned number, but only using the knownbits as
        information."""
        return unmask_zero(self.tvalue, self.tmask)

    def get_maximum_unsigned_by_knownbits(self):
        """
        returns the maximum unsigned number, but only using the knownbits as
        information."""
        return unmask_one(self.tvalue, self.tmask)

    def _get_minimum_signed_by_knownbits(self):
        """ for internal use only!
        returns the minimum signed number, but only using the knownbits as
        information."""
        return self.intmask(self.tvalue | msbonly(self.tmask))

    def _get_maximum_signed_by_knownbits(self):
        """ for internal use only!
        returns the maximum signed number, but only using the knownbits as
        information."""
        unsigned_mask = self.tmask & ~msbonly(self.tmask)
        return self.intmask(self.tvalue | unsigned_mask)

    def _get_minimum_signed_by_knownbits_atleast(self, threshold=MININT):
        """ for internal use only!
        return the smallest number permitted by the known bits that is above
        (or equal) threshold. will raise InvalidLoop if no such number exists.
        """
        if self._get_maximum_signed_by_knownbits() < threshold:
            raise InvalidLoop("threshold and knownbits don't overlap")
        min_by_knownbits = self._get_minimum_signed_by_knownbits()
        if min_by_knownbits > self.upper:
            raise InvalidLoop("range and knownbits don't overlap")
        if min_by_knownbits >= threshold:
            return min_by_knownbits
        # see "Sharpening Constraint Programming
        #      approaches for Bit-Vector Theory"
        u_min_threshold = r_uint(threshold)
        # create our working value, the to-be minimum
        working_min, cl2set, set2cl = self._helper_min_max_prepare(u_min_threshold)
        if working_min == u_min_threshold:
            return threshold
        elif cl2set > set2cl:
            return self._helper_min_case1(working_min, cl2set)
        else:
            return self._helper_min_case2(working_min, set2cl)

    @always_inline
    def _helper_min_max_prepare(self, u_threshold):
        working_value = u_threshold # start at given threshold
        working_value &= unmask_one(self.tvalue, self.tmask) # clear known 0s
        working_value |= self.tvalue # set known 1s
        # inspect changed bits
        cl2set = ~u_threshold & working_value
        set2cl = u_threshold & ~working_value
        return working_value, cl2set, set2cl

    @always_inline
    def _helper_min_case1(self, working_min, cl2set):
        # we have set the correct bit already
        clear_mask = leading_zeros_mask(self._urshift(cl2set, 1))
        working_min &= clear_mask | ~self.tmask
        return self.intmask(working_min)

    @always_inline
    def _helper_min_case2(self, working_min, set2cl):
        # flip the sign bit to handle -1 -> 0 overflow
        working_min = flip_msb(working_min)
        # we have to find the proper bit to set...
        possible_bits = ~working_min \
                        & self.tmask \
                        & leading_zeros_mask(set2cl)
        bit_to_set = lowest_set_bit_only(possible_bits)
        working_min |= bit_to_set
        # and clear all lower than that
        clear_mask = leading_zeros_mask(bit_to_set) \
                     | bit_to_set | ~self.tmask
        working_min &= clear_mask
        return self.intmask(flip_msb(working_min))

    def _get_maximum_signed_by_knownbits_atmost(self, threshold=MAXINT):
        """ for internal use only!
        return the largest number permitted by the known bits that is below or
        equal to threshold. will raise InvalidLoop if no such number exists.
        """
        if self._get_minimum_signed_by_knownbits() > threshold:
            raise InvalidLoop("threshold and knownbits don't overlap")
        max_by_knownbits = self._get_maximum_signed_by_knownbits()
        if max_by_knownbits < self.lower:
            raise InvalidLoop("range and knownbits don't overlap")
        if max_by_knownbits <= threshold:
            return max_by_knownbits
        # see "Sharpening Constraint Programming
        #      approaches for Bit-Vector Theory"
        u_max_threshold = r_uint(threshold)
        # now create our working value, the to-be maximum
        working_max, cl2set, set2cl = self._helper_min_max_prepare(u_max_threshold)
        if working_max == u_max_threshold:
            return threshold
        elif cl2set < set2cl:
            # we have cleared the right bit already
            result = self._helper_max_case1(working_max, set2cl)
        else:
            result = self._helper_max_case2(working_max, cl2set)
        assert result <= threshold
        return result

    def _helper_max_case1(self, working_max, set2cl):
        # we have cleared the right bit already
        set_mask = next_pow2_m1(self._urshift(set2cl, 1)) & self.tmask
        working_max |= set_mask
        return self.intmask(working_max)

    def _helper_max_case2(self, working_max, cl2set):
        # flip the sign bit to handle 1 -> 0 overflow
        working_max = flip_msb(working_max)
        # find the right bit to clear
        possible_bits = working_max \
                        & self.tmask \
                        & leading_zeros_mask(cl2set)
        bit_to_clear = lowest_set_bit_only(possible_bits)
        working_max &= ~bit_to_clear
        # and set all lower than that
        set_mask = next_pow2_m1(self._urshift(bit_to_clear, 1)) & self.tmask
        working_max |= set_mask
        return self.intmask(flip_msb(working_max))


    def _get_minimum_signed(self):
        """ for tests only """
        ret_b = self.lower
        result = self._get_minimum_signed_by_knownbits_atleast(ret_b)
        assert isinstance(result, int)
        return result

    def _get_maximum_signed(self):
        """ for tests only """
        ret_b = self.upper
        result = self._get_maximum_signed_by_knownbits_atmost(ret_b)
        assert isinstance(result, int)
        return result

    def intersect(self, other):
        """
        Mutates `self` so that it contains integers that are contained in
        `self` and `other`, and only those. Basically intersection of sets.
        Throws InvalidLoop if `self` and `other` "disagree", meaning the result
        would not contain any integers.
        """
        if self.known_gt(other) or self.known_lt(other):
            # they don't overlap, which makes the loop invalid
            # this never happens in regular linear traces, but it can happen in
            # combination with unrolling/loop peeling
            raise InvalidLoop("two integer ranges don't overlap")

        r = self.intersect_const(other.lower, other.upper, do_shrinking=False)

        tvalue, tmask, valid = self._tnum_intersect(other.tvalue, other.tmask)
        if not valid:
            raise InvalidLoop("knownbits contradict each other")
        # calculate intersect value and mask
        if self.tmask != tmask:
            # this can also raise InvalidLoop, if the ranges and knownbits
            # contradict in more complicated ways
            r = self.set_tvalue_tmask(tvalue, tmask) # this shrinks
            assert r
        elif r:
            # we didn't shrink yet
            self.shrink()
            assert self._debug_check()
        return r

    @always_inline
    def _tnum_intersect(self, other_tvalue, other_tmask):
        union_val = self.tvalue | other_tvalue
        either_known = self.tmask & other_tmask
        both_known = self.tmask | other_tmask
        unmasked_self = unmask_zero(self.tvalue, both_known)
        unmasked_other = unmask_zero(other_tvalue, both_known)
        tvalue = unmask_zero(union_val, either_known)
        valid = unmasked_self == unmasked_other
        return tvalue, either_known, valid

    def intersect_const(self, lower, upper, do_shrinking=True):
        """
        Mutates `self` so that it contains integers that are contained in
        `self` and the range [`lower`, `upper`], and only those. Basically
        intersection of sets.
        """
        changed = False
        if lower > self.lower:
            if lower > self.upper:
                raise InvalidLoop
            self.lower = lower
            changed = True
        if upper < self.upper:
            if upper < self.lower:
                raise InvalidLoop
            self.upper = upper
            changed = True
        if changed and do_shrinking:
            self.shrink()
        return changed

    def add(self, value):
        return self.add_bound(self.from_constant(value))

    def add_bound(self, other):
        """
        Adds the `other` abstract integer to `self` and returns the result.
        Must be correct in the presence of possible overflows.
        (Does not mutate `self`.)
        """

        tvalue, tmask = self._tnum_add(other)

        # the lower and upper logic is proven in test_prove_add_bounds_logic
        try:
            lower = ovfcheck(self.lower + other.lower)
        except OverflowError:
            return IntBound.from_knownbits(tvalue, tmask)
        try:
            upper = ovfcheck(self.upper + other.upper)
        except OverflowError:
            return IntBound.from_knownbits(tvalue, tmask)
        return IntBound(lower, upper, tvalue, tmask)

    @always_inline
    def _tnum_add(self, other):
        sum_values = self.tvalue + other.tvalue
        sum_masks = self.tmask + other.tmask
        all_carries = sum_values + sum_masks
        val_carries = all_carries ^ sum_values
        tmask = self.tmask | other.tmask | val_carries
        tvalue = unmask_zero(sum_values, tmask)
        return tvalue, tmask

    def add_bound_cannot_overflow(self, other):
        """ returns True if self + other can never overflow """
        try:
            ovfcheck(self.upper + other.upper)
            ovfcheck(self.lower + other.lower)
        except OverflowError:
            return False
        return True

    def add_bound_no_overflow(self, other):
        """ return the bound that self + other must have, if no overflow occured,
        eg after an int_add_ovf(...), guard_no_overflow() """
        tvalue, tmask = self._tnum_add(other)

        # returning add_bound is always correct, but let's improve the range
        lower = self._add_check_overflow(self.lower, other.lower, MININT)
        upper = self._add_check_overflow(self.upper, other.upper, MAXINT)
        return self.new(lower, upper, tvalue, tmask)

    def sub_bound(self, other):
        """
        Subtracts the `other` abstract integer from `self` and returns the
        result. (Does not mutate `self`.)
        """
        tvalue, tmask = self._tnum_sub(other)
        # the lower and upper logic is proven in test_prove_sub_bound_logic
        try:
            lower = ovfcheck(self.lower - other.upper)
        except OverflowError:
            return IntBound.from_knownbits(tvalue, tmask)
        try:
            upper = ovfcheck(self.upper - other.lower)
        except OverflowError:
            return IntBound.from_knownbits(tvalue, tmask)
        return IntBound(lower, upper, tvalue, tmask)

    def _tnum_sub(self, other):
        diff_values = self.tvalue - other.tvalue
        val_borrows = (diff_values + self.tmask) ^ (diff_values - other.tmask)
        tmask = self.tmask | other.tmask | val_borrows
        tvalue = unmask_zero(diff_values, tmask)
        return tvalue, tmask

    def sub_bound_cannot_overflow(self, other):
        try:
            ovfcheck(self.lower - other.upper)
            ovfcheck(self.upper - other.lower)
        except OverflowError:
            return False
        return True

    def sub_bound_no_overflow(self, other):
        """ return the bound that self - other must have, if no overflow occured,
        eg after an int_sub_ovf(...), guard_no_overflow() """
        tvalue, tmask = self._tnum_sub(other)
        # returning sub_bound is always correct, but let's improve the range
        lower = self._sub_check_overflow(self.lower, other.upper, MININT)
        upper = self._sub_check_overflow(self.upper, other.lower, MAXINT)
        return self.new(lower, upper, tvalue, tmask)

    def mul_bound(self, other):
        """
        Multiplies the `other` abstract
        integer with `self` and returns the
        result.
        (Does not mutate `self`.)
        """
        try:
            vals = (ovfcheck(self.upper * other.upper),
                    ovfcheck(self.upper * other.lower),
                    ovfcheck(self.lower * other.upper),
                    ovfcheck(self.lower * other.lower))
            return IntBound(min4(vals), max4(vals))
        except OverflowError:
            return IntBound.unbounded()
    mul_bound_no_overflow = mul_bound # can be improved

    def mul_bound_cannot_overflow(self, other):
        try:
            ovfcheck(self.upper * other.upper)
            ovfcheck(self.upper * other.lower)
            ovfcheck(self.lower * other.upper)
            ovfcheck(self.lower * other.lower)
        except OverflowError:
            return False
        return True

    def py_div_bound(self, other):
        """
        Divides this abstract integer by the
        `other` abstract integer and returns
        the result.
        (Does not mutate `self`.)
        """
        # we need to make sure that the 0 is not in the interval because
        # otherwise [-4, 4] / [-4, 4] would return [-1, 1], which is nonsense
        # see test_knownbits_div_bug. the first part of the check is not
        # enough, because 0 could be excluded by the known bits
        if not other.contains(0) and not (other.lower < 0 < other.upper):
            try:
                # this gives the bounds for 'int_py_div', so use the
                # Python-style handling of negative numbers and not
                # the C-style one
                vals = (ovfcheck(self.upper / other.upper),
                        ovfcheck(self.upper / other.lower),
                        ovfcheck(self.lower / other.upper),
                        ovfcheck(self.lower / other.lower))
                return IntBound(min4(vals), max4(vals))
            except OverflowError:
                pass
        return IntBound.unbounded()

    def mod_bound(self, other):
        """
        Calculates the mod of this abstract
        integer by the `other` abstract
        integer and returns the result.
        (Does not mutate `self`.)
        """
        r = IntBound.unbounded()
        if other.is_constant() and other.get_constant_int() == 0:
            return IntBound.unbounded()
        # with Python's modulo:  0 <= (x % pos) < pos
        #                        neg < (x % neg) <= 0
        # see test_prove_mod_bound_logic
        if other.upper > 0:
            upper = other.upper - 1
        else:
            upper = 0
        if other.lower < 0:
            lower = other.lower + 1
        else:
            lower = 0
        return IntBound(lower, upper)

    def lshift_bound(self, other):
        """
        Shifts this abstract integer `other`
        bits to the left, where `other` is
        another abstract integer.
        (Does not mutate `self`.)
        """

        tvalue, tmask = TNUM_UNKNOWN
        if other.is_constant():
            c_other = other.get_constant_int()
            if c_other >= LONG_BIT:
                 tvalue, tmask = TNUM_KNOWN_ZERO
            elif 0 <= c_other < LONG_BIT:
                tvalue, tmask = self._tnum_lshift(c_other)
            # else: bits are unknown because arguments invalid

        if other.known_nonnegative() and other.known_lt_const(LONG_BIT):
            try:
                vals = (ovfcheck(self.upper << other.upper),
                        ovfcheck(self.upper << other.lower),
                        ovfcheck(self.lower << other.upper),
                        ovfcheck(self.lower << other.lower))
                return IntBound(min4(vals), max4(vals), tvalue, tmask)
            except (OverflowError, ValueError):
                pass

        return IntBound.from_knownbits(tvalue, tmask)

    @always_inline
    def _tnum_lshift(self, c_other):
        # use signed integer sign extension logic
        tvalue = self.tvalue << c_other
        tmask = self.tmask << c_other
        return tvalue, tmask

    def rshift_bound(self, other):
        """
        Shifts this abstract integer `other` bits to the right, where `other`
        is another abstract integer, and extends its sign. This is the
        arithmetic shift on signed integers, ie the shifted in values are 0/1,
        depending on the sign.
        (Does not mutate `self`.)
        """

        tvalue, tmask = TNUM_UNKNOWN
        if other.is_constant():
            c_other = other.get_constant_int()
            if c_other >= LONG_BIT:
                # shift value out to the right, but do sign extend
                if msbonly(self.tmask): # sign-extend mask
                    tvalue, tmask = TNUM_UNKNOWN
                elif msbonly(self.tvalue): # sign-extend value
                    tvalue, tmask = TNUM_KNOWN_BITWISEONE
                else: # sign is 0 on both
                    tvalue, tmask = TNUM_KNOWN_ZERO
            elif c_other >= 0:
                tvalue, tmask = self._tnum_rshift(c_other)
            # else: bits are unknown because arguments invalid

        lower = MININT
        upper = MAXINT
        if other.known_nonnegative() and other.known_lt_const(LONG_BIT):
            vals = (self.upper >> other.upper,
                    self.upper >> other.lower,
                    self.lower >> other.upper,
                    self.lower >> other.lower)
            lower = min4(vals)
            upper = max4(vals)
        return IntBound(lower, upper, tvalue, tmask)

    @always_inline
    def _tnum_rshift(self, c_other):
        # use signed integer sign extension logic
        tvalue = self.r_uint(self.intmask(self.tvalue) >> c_other)
        tmask = self.r_uint(self.intmask(self.tmask) >> c_other)
        return tvalue, tmask

    def lshift_bound_cannot_overflow(self, other):
        """ returns True if self << other can never overflow """
        if other.known_nonnegative() and \
           other.known_lt_const(LONG_BIT):
            try:
                ovfcheck(self.upper << other.upper)
                ovfcheck(self.upper << other.lower)
                ovfcheck(self.lower << other.upper)
                ovfcheck(self.lower << other.lower)
                return True
            except (OverflowError, ValueError):
                pass
        return False

    def urshift_bound(self, other):
        """
        Shifts this abstract integer `other` bits to the right, where `other`
        is another abstract integer, *without* extending its sign. (Does not
        mutate `self`.)
        """

        # this seems to always be the signed variant..?
        lower = MININT
        upper = MAXINT
        tvalue, tmask = TNUM_UNKNOWN
        if other.is_constant():
            c_other = other.get_constant_int()
            if c_other >= LONG_BIT:
                # no sign to extend, we get constant 0
                tvalue, tmask = TNUM_KNOWN_ZERO
            elif c_other >= 0:
                tvalue, tmask = self._tnum_urshift(c_other)
                if self.lower >= 0:
                    upper = intmask(r_uint(self.upper) >> c_other)
                    lower = intmask(r_uint(self.lower) >> c_other)
            # else: bits are unknown because arguments invalid
        return IntBound(lower, upper, tvalue, tmask)

        # we don't do bounds on unsigned
        return IntBound.from_knownbits(tvalue, tmask)

    @always_inline
    def _tnum_urshift(self, c_other):
        tvalue = self._urshift(self.tvalue, c_other)
        tmask = self._urshift(self.tmask, c_other)
        return tvalue, tmask

    def and_bound(self, other):
        """
        Performs bit-wise AND of this abstract integer and the `other`,
        returning its result. (Does not mutate `self`.)
        """

        pos1 = self.known_nonnegative()
        pos2 = other.known_nonnegative()
        # the next three if-conditions are proven by test_prove_and_bound_logic
        lower = MININT
        upper = MAXINT
        if pos1 or pos2:
            lower = 0
        if pos1:
            upper = self.upper
        if pos2:
            upper = min(upper, other.upper)

        res_tvalue, res_tmask = self._tnum_and(other)
        return IntBound(lower, upper, res_tvalue, res_tmask)

    @always_inline
    def _tnum_and(self, other):
        self_pmask = self.tvalue | self.tmask
        other_pmask = other.tvalue | other.tmask
        and_vals = self.tvalue & other.tvalue
        return and_vals, self_pmask & other_pmask & ~and_vals

    def or_bound(self, other):
        """
        Performs bit-wise OR of this abstract integer and the `other`,
        returning its result. (Does not mutate `self`.)
        """

        tvalue, tmask = self._tnum_or(other)
        return self.from_knownbits(tvalue, tmask)

    @always_inline
    def _tnum_or(self, other):
        union_vals = self.tvalue | other.tvalue
        union_masks = self.tmask | other.tmask
        return union_vals, union_masks & ~union_vals

    def xor_bound(self, other):
        """
        Performs bit-wise XOR of this abstract integer and the `other`,
        returning its result.
        (Does not mutate `self`.)
        """
        tvalue, tmask = self._tnum_xor(other)
        return self.from_knownbits(tvalue, tmask)

    @always_inline
    def _tnum_xor(self, other):
        xor_vals = self.tvalue ^ other.tvalue
        union_masks = self.tmask | other.tmask
        return unmask_zero(xor_vals, union_masks), union_masks

    def neg_bound(self):
        """
        Arithmetically negates this abstract integer and returns the result.
        (Does not mutate `self`.)
        """
        res = self.invert_bound()
        res = res.add(1)
        return res

    def invert_bound(self):
        """
        Performs bit-wise NOT on this abstract integer returning its result.
        (Does not mutate `self`.)
        """
        upper = ~self.lower
        lower = ~self.upper
        tvalue = unmask_zero(~self.tvalue, self.tmask)
        tmask = self.tmask
        return self.new(lower, upper, tvalue, tmask)

    def contains(self, value):
        """
        Returns `True` iff this abstract integer contains the given `value`.
        """

        assert not isinstance(value, IntBound)

        if not we_are_translated():
            assert not isinstance(value, long)
        if not isinstance(value, int):
            if (self.lower == MININT and self.upper == MAXINT):
                return True # workaround for address as int
        if value < self.lower:
            return False
        if value > self.upper:
            return False

        u_vself = unmask_zero(self.tvalue, self.tmask)
        u_value = unmask_zero(r_uint(value), self.tmask)
        if u_vself != u_value:
            return False

        return True

    def is_within_range(self, lower, upper):
        """
        Check if all the numbers contained in this instance have are between
        lower and upper.
        """
        return lower <= self.lower and self.upper <= upper

    def clone(self):
        """
        Returns a copy of this abstract integer.
        """
        res = IntBound(self.lower, self.upper,
                       self.tvalue, self.tmask)
        return res

    def make_guards(self, box, guards, optimizer):
        """
        Generates guards from the information we have about the numbers this
        abstract integer contains.
        """
        if self.is_constant():
            guards.append(ResOperation(rop.GUARD_VALUE,
                                       [box, ConstInt(self.upper)]))
            return
        if self.lower > MININT:
            bound = self.lower
            op = ResOperation(rop.INT_GE, [box, ConstInt(bound)])
            guards.append(op)
            op = ResOperation(rop.GUARD_TRUE, [op])
            guards.append(op)
        if self.upper < MAXINT:
            bound = self.upper
            op = ResOperation(rop.INT_LE, [box, ConstInt(bound)])
            guards.append(op)
            op = ResOperation(rop.GUARD_TRUE, [op])
            guards.append(op)
        if not self._are_knownbits_implied():
            op = ResOperation(rop.INT_AND, [box, ConstInt(intmask(~self.tmask))])
            guards.append(op)
            op = ResOperation(rop.GUARD_VALUE, [op, ConstInt(intmask(self.tvalue))])
            guards.append(op)

    def is_bool(self):
        """
        Returns `True` iff self is exactly the set {0, 1}
        """
        return (self.known_nonnegative() and self.known_le_const(1))

    def is_unbounded(self):
        return (self.lower == MININT and self.upper == MAXINT and
                self.tvalue == r_uint(0) and self.tmask == r_uint(-1))


    def make_bool(self):
        """
        Mutates this abstract integer so that it does represent a conventional
        boolean value.
        (Mutates `self`.)
        """
        self.intersect_const(0, 1)

    def getconst(self):
        """
        Returns ConstInt with the only integer contained in this abstract
        integer. Caller needs to check that `.is_constant()` returns True,
        before calling.
        """
        return ConstInt(self.get_constant_int())

    def getnullness(self):
        """
        Returns information about whether this this abstract integer is known
        to be zero or not to be zero.
        """
        if self.known_gt_const(0) or \
           self.known_lt_const(0) or \
           self.tvalue != 0:
            return INFO_NONNULL
        if self.is_constant() and self.get_constant_int() == 0:
            return INFO_NULL
        return INFO_UNKNOWN

    def widen(self):
        info = self.clone()
        info.widen_update()
        return info

    def widen_update(self):
        if self.lower < MININT / 2:
            self.lower = MININT
        if self.upper > MAXINT / 2:
            self.upper = MAXINT
        self.tvalue, self.tmask = TNUM_UNKNOWN
        self.shrink()


    def and_bound_backwards(self, result):
        """
        result == int_and(self, other)
        We want to learn some bits about other, using the information from self
        and result_int.

        regular &:
                  other
         &  0   1   ?
         0  0   0   0
         1  0   1   ?
         ?  0   ?   ?   <- result
        self

        backwards & (this one):
                  self
            0   1   ?
         0  ?   0   ?
         1  X   1   1
         ?  ?   ?   ?   <- other
        result

        (X marks an inconsistent result).

        We can see that we only learn something about other at the places
        where a bit from self is 1. At those places, the corresponding bit in
        other has to be the corresponding bit in result.
        """

        tvalue, tmask, valid = self._tnum_and_backwards(result)
        if not valid:
            raise InvalidLoop("inconsistency in and_bound_backwards")
        return IntBound.from_knownbits(tvalue, tmask)

    @always_inline
    def _tnum_and_backwards(self, result):
        # in all the places where the result is 1 both arguments have to 1. in
        # the places where result is 0, other has to be 0 iff self is known 1.
        tvalue = result.tvalue
        tmask = ((~self.tvalue) | result.tmask) & ~tvalue
        # if we have a place where result is 1 but self is 0, then we are
        # inconsistent
        inconsistent = result.tvalue & ~self.tmask & ~self.tvalue
        return tvalue, tmask, inconsistent == 0

    def or_bound_backwards(self, result):
        """
        result_int == int_or(self, other)
        We want to refine our knowledge about other
        using this information

        regular |:
                  other
         &  0   1   ?
         0  0   1   ?
         1  1   1   1
         ?  ?   1   ?   <- result
        self

        backwards | (this one):
                  self
            0   1   ?
         0  0   X   0
         1  1   ?   ?
         ?  ?   ?   ?   <- other (where X=invalid)
        result

        """
        tvalue, tmask, valid = self._tnum_or_backwards(result)
        if not valid:
            raise InvalidLoop("inconsistency in or_bound_backwards")
        return IntBound.from_knownbits(tvalue, tmask)

    @always_inline
    def _tnum_or_backwards(self, result):
        # in all the places where the result is 0 both arguments have to be 0.
        zeros = (~result.tmask & ~result.tvalue)
        # apart from that, in the places where self is 0 and where result is 1
        # other must be 1
        tvalue = (result.tvalue & ~self.tvalue & ~self.tmask)
        tmask = ~(zeros | tvalue)
        # if we have a place where result is 0 but self is 1, then we are
        # inconsistent
        inconsistent = self.tvalue & zeros
        return tvalue, tmask, inconsistent == 0

    def rshift_bound_backwards(self, other):
        """
        Performs a `urshift`/`rshift` backwards on `self`. Basically
        left-shifts `self` by `other` binary digits, filling the lower part
        with ?, and returns the result.
        """
        if not other.is_constant():
            return IntBound.unbounded()
        c_other = other.get_constant_int()
        tvalue, tmask = TNUM_UNKNOWN
        if 0 <= c_other < LONG_BIT:
            tvalue = self.tvalue << r_uint(c_other)
            tmask = self.tmask << r_uint(c_other)
            # shift ? in from the right,
            tmask |= (r_uint(1) << r_uint(c_other)) - 1
        return IntBound.from_knownbits(tvalue, tmask)
    urshift_bound_backwards = rshift_bound_backwards

    def lshift_bound_backwards(self, other):
        """
        Performs a `lshift` backwards on `self`. Basically right-shifts `self`
        by `other` binary digits, filling the upper part with ?, and returns
        the result.
        """
        if not other.is_constant():
            return IntBound.unbounded()
        c_other = r_uint(other.get_constant_int())
        tvalue, tmask = TNUM_UNKNOWN
        if 0 <= c_other < LONG_BIT:
            tvalue = self.tvalue >> c_other
            tmask = self.tmask >> c_other
            # shift ? in from the left,
            s_tmask = ~(r_uint(-1) >> c_other)
            tmask |= s_tmask
            inconsistent = self.tvalue & ((1 << c_other) - 1)
            if inconsistent:
                raise InvalidLoop("lshift_bound_backwards inconsistent known bits")
        return IntBound.from_knownbits(tvalue, tmask)

    def shrink(self):
        """ Shrink the bounds and the knownbits to be more precise, but without
        changing the set of integers that is represented by self.

        Here's a diagram to show what is happening. This is the number line:
        MININT <---------0-----------------------------------------------> MAXINT

        We have a range in the number line
                           [lower     ...       upper]

        We also known bits, they represent a set of ints maybe looking like this:
                X X X X         X X X X         X X X X         X X X X
        (an X means the number matches the known bits, ' ' means it doesn't)

        Note that the lower and upper bounds could be more precise (ie bigger
        and smaller, respectively), because they don't match the known bits.
        Also, there are numbers that match the known bits to the left of lower
        and the right of upper, that are excluded by the range and thus
        unnecessary. We want to fix both of that.

        First we shrink the bounds so that they both match the known bits,
        then things look like this:
                                [lower   ...   upper]
                X X X X         X X X X         X X X X         X X X X
        This is achieved by moving lower to the right to the first number >=
        lower that matches the known bits (and mutatis mutandis for upper).

        Afterwards we use the information from the bounds to add more known
        bits. Having done that, things look maybe something like this:
                                [lower   ...   upper]
                                X X X X         X X X X
        Then we're done with shrinking.

        The set that is described by these two pieces of information together
        is neither expressible as purely a range, nor purely by known bits.
        It looks like this:
                                X X X X         X X X
        The set did not change through this process, but the bounds and the
        known bits becoming more precise makes it possible to compute more
        precise results when doing further operations with self.
        """
        # there's a proof in test_z3intbound that one pass of shrinking is
        # always enough. let's still assert that a second pass doesn't change
        # anything.
        changed = self._shrink_bounds_by_knownbits()
        changed |= self._shrink_knownbits_by_bounds()
        if not changed:
            return changed
        changed_again = self._shrink_bounds_by_knownbits()
        changed_again |= self._shrink_knownbits_by_bounds()
        assert not changed_again
        return changed

    def _shrink_bounds_by_knownbits(self):
        """
        Shrinks the bounds by the known bits.
        """
        # lower bound
        min_by_knownbits = self._get_minimum_signed_by_knownbits_atleast(self.lower)
        max_by_knownbits = self._get_maximum_signed_by_knownbits_atmost(self.upper)
        if min_by_knownbits > max_by_knownbits:
            raise InvalidLoop("range and knownbits contradict each other")
        changed = self.lower < min_by_knownbits or self.upper > max_by_knownbits
        if changed:
            self.lower = min_by_knownbits
            self.upper = max_by_knownbits
        return changed

    def _shrink_knownbits_by_bounds(self):
        """
        Infers known bits from the bounds. Basically fills a common prefix from
        lower and upper bound into the knownbits.
        """
        tvalue, tmask, valid = self._tnum_improve_knownbits_by_bounds()
        if not valid:
            raise InvalidLoop("knownbits and bounds don't agree")
        changed = self.tvalue != tvalue or self.tmask != tmask
        if changed:
            self.tmask = tmask
            self.tvalue = tvalue
        return changed

    @always_inline
    def _tnum_implied_by_bounds(self):
        # calculate higher bit mask by bounds
        hbm_bounds = leading_zeros_mask(
                self.r_uint(self.lower) ^ self.r_uint(self.upper))
        bounds_common = self.r_uint(self.lower) & hbm_bounds
        tmask = ~hbm_bounds
        return unmask_zero(bounds_common, tmask), tmask

    @always_inline
    def _tnum_improve_knownbits_by_bounds(self):
        # knownbits that are implied by the bounds
        tvalue, tmask = self._tnum_implied_by_bounds()
        # intersect them with the current knownbits
        return self._tnum_intersect(tvalue, tmask)

    def _debug_check(self):
        """
        Very simple debug check. Returns `True` iff the span of knownbits and
        the span of the bounds have a non-empty intersection. That does not
        guarantee for the actual concrete value set to contain any values!
        """
        assert self.lower <= self.upper
        min_knownbits = self._get_minimum_signed_by_knownbits()
        max_knownbits = self._get_maximum_signed_by_knownbits()
        if not min_knownbits <= self.upper:
            return False
        if not max_knownbits >= self.lower:
            return False
        # just to make sure
        if not min_knownbits <= max_knownbits:
            return False
        # make sure the set is not empty
        if self.is_constant():
            # does one constraint exclude the constant value?
            val = self.get_constant_int()
            if min_knownbits > val or max_knownbits < val \
               or self.lower > val or self.upper < val:
                return False
        else:
            # we have no constant, so keep checking
            u_lower = r_uint(self.lower)
            u_upper = r_uint(self.upper)
            # check if bounds common prefix agrees with known-bits
            hbm_bounds = leading_zeros_mask(u_lower ^ u_upper)
            bounds_common_prefix = u_lower & hbm_bounds
            if unmask_zero(bounds_common_prefix, self.tmask) != self.tvalue & hbm_bounds:
                return False
            # for the rest of the bunch, check by minima/maxima with threshold.
            #   (side note: the whole check can be reduced to this, but for the
            #    sake of robustness we want to keep the other checks above.)
            if self._get_minimum_signed_by_knownbits_atleast(self.lower) > self.upper \
               or self._get_maximum_signed_by_knownbits_atmost(self.upper) < self.lower:
                return False
        return True

    def knownbits_string(self, unk_sym='?'):
        """
        Returns a string representation about the knownbits part of this
        abstract integer. You can give any symbol or string for the "unknown
        bits" (default: '?'), the other digits are written as '1' and '0'.
        """
        results = []
        for bit in range(LONG_BIT):
            if self.tmask & (1 << bit):
                results.append(unk_sym)
            else:
                results.append(str((self.tvalue >> bit) & 1))
        results.reverse()
        return "".join(results)


def flip_msb(val_uint):
    return val_uint ^ r_uint(MININT)

def is_valid_tnum(tvalue, tmask):
    """
    Returns `True` iff `tvalue` and `tmask` would be valid tri-state number
    fields of an abstract integer, meeting all conventions and requirements.
    """
    if not isinstance(tvalue, r_uint):
        return False
    if not isinstance(tmask, r_uint):
        return False
    return 0 == (r_uint(tvalue) & r_uint(tmask))

def leading_zeros_mask(n):
    """
    calculates a bitmask in which only the leading zeros of `n` are set (1).
    """
    return ~next_pow2_m1(n)

def lowest_set_bit_only(val_uint):
    """
    Returns an val_int, but with all bits deleted but the lowest one that was
    set.
    """
    #assert isinstance(val_uint, r_uint)
    working_val = ~val_uint
    increased_val = working_val + 1
    result = (working_val^increased_val) & val_uint
    return result

def min4(t):
    """
    Returns the minimum of the values in the quadruplet t.
    """
    return min(min(t[0], t[1]), min(t[2], t[3]))

def max4(t):
    """
    Returns the maximum of the values in the quadruplet t.
    """
    return max(max(t[0], t[1]), max(t[2], t[3]))

def msbonly(v):
    """
    Returns `v` with all bits except the most significant bit set to 0 (zero).
    """
    return v & (1 << (LONG_BIT-1))

def next_pow2_m1(n):
    """Calculate next power of 2 minus one, greater than n"""
    n |= n >> 1
    n |= n >> 2
    n |= n >> 4
    n |= n >> 8
    n |= n >> 16
    if IS_64_BIT:
        n |= n >> 32
    return n

def unmask_one(value, mask):
    """
    Sets all unknowns determined by `mask` in `value` bit-wise to 1 (one) and
    returns the result.
    """
    return value | mask

def unmask_zero(value, mask):
    """
    Sets all unknowns determined by `mask` in `value` bit-wise to 0 (zero) and
    returns the result.
    """
    return value & ~mask