# Meaning of Using BitVectors to Model Integers to account for Overflow

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.

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.

• So we should model them as fixed-sized bitvectors so we can show that there will be overflows and to take that into account (seems like you're saying). That's good to know, I would've thought the reverse. Commented Jul 22, 2018 at 17:45
• Yes, exactly. Just a couple of lines down from the sentence you quoted, the paper gives a nice example of where that behavior might be different: with mathematical integers, `a * b` can only be `0` if either `a` or `b` are `0`. However, if you model integers as bitvectors, the theorem prover is actually able to find a counter-example to the assumption that `a * b` can never be `0` if neither `a` nor `b` are `0`. For example, for a C♯ `byte`, the following is true: `byte b = 2 * 128; b == 0 //=> true` Commented Jul 22, 2018 at 21:56

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.

• So wondering what it means to model your integers using bitvectors then. That is, what you would be checking for during modeling/verification. It seems like you would then see if the bitvector grew past a certain point, which you can't do if it's a fixed count. Commented Jul 22, 2018 at 2:11
• The existing number system already models integers as fixed sized arrays of bits. Bitvectors are just variable sized arrays of bits so they grow instead of overflowing Commented Jul 22, 2018 at 2:33
• The paper is saying to model integers as used in programming languages as fixed-size bitvectors in the correctness proof precisely because they model overflow correctly, as opposed to the mathematically ideal integers of the specification language which never overflow. Commented Jul 22, 2018 at 8:37
• I may have misunderstood your question. Overflow is an error condition (though not all languages always treat it that way). It means the mathematically correct answer cannot be represented in the fixed size box you have chosen to store your result. There can be no 'correct ' way to model the wrong answer besides somehow marking it and the surround code as wrong. Commented Jul 22, 2018 at 20:22
• I since looked at the second paper you linked. I think that author was just saying that in the context of using SAT theorem provers, representing arithmetic logic as logic on an array of bits was easier than defining it in terms of math. I'm not completely familiar with this reading but it does make sense. The behavior of computer logic does not follow that if math first atithmatic. Instead the numerical functions (like plus) are defined as bit operations . The bit operations and math have the same results. EXCEPT when you overflow Commented Jul 22, 2018 at 20:41