Meaning of Using BitVectors to Model Integers to account for Overflow

Question

I have just encountered this sentence:

Depending on the context, we may prefer to model integers as bitvectors rather than mathematical integers, since the Int type does not model overflow.

I am wondering what this means. I am new to learning about integer overflow. Wondering what it means to model integers as bitvectors and how you would do that. And then how that would allow you to account for overflow (wondering if you would then write tests for it of some sort, or it is somehow implicit in the model). It is intriguing the idea of modeling integers so that they take into account real-world problems like integer overflows. Maybe if it could be outlined using JavaScript as an example which I am familiar with that would be helpful.

Another paper says something similar:

Overflows are a common source of programming errors, which makes it crucial to model them accordingly. In the theory of fixed-size bitvectors, overflow effects are directly modeled by the semantics of its function symbols and require no extra encoding constraints. These properties make bitvector logic a perfect fit for many verification purposes, especially in the field of low-level programming.

Answer 1

The thing that many programming languages call "integers" are not actually integers, they are fixed-size bitvectors interpreted as integers … but because they are fixed-size, they can "overflow", meaning the result of a computation can be larger than what fits into the fixed-size bitvector.

All that sentence is saying is that since (programming language) integers are fixed-size bitvectors in a real-world programming language, we should also model them as fixed-size bitvectors in our specification language and proof instead of modeling them as (mathematically ideal) integers which behave differently.

In particular, integer overflow can be a common source of bugs, so modeling the safety properties of a system but ignoring a common source of bugs makes no sense.

Answer 2

This is easiest to understand with unsigned integers and the answer is essentially the same.

Also, unsigned integers come in different sizes but to simplify the presentation I'll assume 32 bit integers.

You may recall in elementary school learning about place value notion and numbers in different bases. In elementary school we were taught 213 was 2 x 100 + 1x10 + 3x1. You represent a number as the sum of a series of factors times powers of ten.

You may have also seen that generalized to different bases (like base 8 or base 5 or base 16).

Well, the way numbers are typically represented in modern digital computers is base 2 (aka binary).

So 1001 means 1x2x2x2 + 0x2x2 + 0x2 +1×1 (sorry cannot type exponents on this keyboard).

So any number nonnegative integer can be represented as a series of ones or zeros (often called bits), where the value of the number is the sum like above (base 2 place value notation).

Now if u choose to represent your numbers with a fixed count of digits (32 and 64 are common choices) then when you perform arithmatic you may end up with a number that won't fit (>= 2 pow (32) in our case). This is an overflow.

Typically the word vector in computerese refers to an array whose size is determined at runtime to be large enough.

If instead of representing numbers with a fixed number of bits you do so with a dynamically allocated array of bits (vector) you have no overflow. Btw these dynamicly allocated representations of numbers are usually referred to as bignums.