Bypassing an unsigned addition overflow detected by CBMC

Question

CBMC detects a possible unsigned addition overflow in the following lines:

l = (t + *b)&(0xffffffffL);
c += (l < t);

I agree that there is a possibility of an overflow in the first line, but I am taking care of the carry in the next line which CBMC is not able to look at. If in case there is an overflow I am setting the carry 1. So since I am aware of this and this and this is how I want my code to work I would like to move on with the verification process. So, how is it that I tell the CBMC to overlook this bug and move on?

godfatherofpolka · Accepted Answer

TL;DR It depends on what the actual types of the variables are. In all cases, CBMC detects an actual bug that could cause undefined behaviour. This means, you should fix your code rather than disable the message in CBMC.

Full answer:

Generally: To the best of my knowledge, CBMC does not allow the exclusion of specific properties (on the other hand, you can check only one single specific property using the --property flag). If you would like a official answer/opinion or make a feature request, I would recommend posting in the CProver Support group.

_{(Of course, one could use __CPROVER_assume in order to make CBMC exclude the traces leading to the error, but this would be a very, very, very bad idea, as this might make other problems unreachable.)}

Variant 1: I assume your code looks something like (related to this: please, please post self-contained examples and explain precisely what the issue is, it's hard to guess these things)

long nondet_long(void);

void main(void) {
  long l = 0;
  int c = 0;
  long t = nondet_long();
  long s = nondet_long();
  long *b = &s;

  l = (t + *b) & (0xffffffffL); 
  c += (l < t);
}

and you are running

    cbmc --signed-overflow-check test.c

giving an output similar to the following one?

    CBMC version 5.1 64-bit x86_64 macos
    Parsing test.c
    Converting
    Type-checking test
    Generating GOTO Program
    Adding CPROVER library
    Function Pointer Removal
    Partial Inlining
    Generic Property Instrumentation
    Starting Bounded Model Checking
    size of program expression: 41 steps
    simple slicing removed 3 assignments
    Generated 2 VCC(s), 2 remaining after simplification
    Passing problem to propositional reduction
    converting SSA
    Running propositional reduction
    Post-processing
    Solving with MiniSAT 2.2.0 with simplifier
    792 variables, 2302 clauses
    SAT checker: negated claim is SATISFIABLE, i.e., does not hold
    Runtime decision procedure: 0.006s
    Building error trace

    Counterexample:

    State 17 file test.c line 4 function main thread 0
    ----------------------------------------------------
      l=0 (0000000000000000000000000000000000000000000000000000000000000000)

    State 18 file test.c line 4 function main thread 0
    ----------------------------------------------------
      l=0 (0000000000000000000000000000000000000000000000000000000000000000)

    State 19 file test.c line 5 function main thread 0
    ----------------------------------------------------
      c=0 (00000000000000000000000000000000)

    State 20 file test.c line 5 function main thread 0
    ----------------------------------------------------
      c=0 (00000000000000000000000000000000)

    State 21 file test.c line 6 function main thread 0
    ----------------------------------------------------
      t=0 (0000000000000000000000000000000000000000000000000000000000000000)

    State 22 file test.c line 6 function main thread 0
    ----------------------------------------------------
      t=-9223372036854775808 (1000000000000000000000000000000000000000000000000000000000000000)

    State 23 file test.c line 7 function main thread 0
    ----------------------------------------------------
      s=0 (0000000000000000000000000000000000000000000000000000000000000000)

    State 24 file test.c line 7 function main thread 0
    ----------------------------------------------------
      s=-9223372036854775807 (1000000000000000000000000000000000000000000000000000000000000001)

    State 25 file test.c line 8 function main thread 0
    ----------------------------------------------------
      b=((long int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

    State 26 file test.c line 8 function main thread 0
    ----------------------------------------------------
      b=&s!0@1 (0000001000000000000000000000000000000000000000000000000000000000)

    Violated property:
      file test.c line 10 function main
      arithmetic overflow on signed + in t + *b
      !overflow("+", signed long int, t, *b)

    VERIFICATION FAILED

I do not think you should disable this property check, even if you could. The reason for this is, as you say, that this addition can overflow, and, integer overflow is undefined behaviour in C, or, as this answer to the question How to check integer overflow in C? nicely puts it:

[O]nce you've executed x + y, if it overflowed, you're already hosed. It's too late to do any checking - your program could have crashed already. Think of it like checking for division by zero - if you wait until after the division has been executed to check, it's already too late.

See also Integer overflow and undefined behavior and How disastrous is integer overflow in C++?.

Thus, this is an actual bug and CBMC has a good reason for telling you about it. What you actually should do is adapt your code so that there are no potential overflows! The answer mentioned above suggests something like (remember to include limits.h):

if ((*b > 0 && t > LONG_MAX - *b) 
    || (*b < 0 && LONG_MIN < *b && t < LONG_MIN - *b) 
    || (*b==LONG_MIN && t < 0))
{
    /* Overflow will occur, need to do maths in a more elaborate, but safe way! */
    /* ... */
}
else
{
    /* No overflow, addition is safe! */
    l = (t + *b) & (0xffffffffL);
    /* ... */
}

Variant 2: Here, I assume, your code looks something like:

unsigned int nondet_uint(void);

void main(void) {
  unsigned int l = 0;
  unsigned int c = 0;
  unsigned int t = nondet_uint();
  unsigned int s = nondet_uint();
  unsigned int *b = &s;

  l = (t + *b) & (0xffffffffL);
  c += (l < t);
}

and you are running

    cbmc --unsigned-overflow-check  test.c

giving an output similar to the following one?

CBMC version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 42 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
519 variables, 1306 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.01s
Building error trace

Counterexample:

State 17 file test.c line 4 function main thread 0
----------------------------------------------------
  l=0 (00000000000000000000000000000000)

State 18 file test.c line 4 function main thread 0
----------------------------------------------------
  l=0 (00000000000000000000000000000000)

State 19 file test.c line 5 function main thread 0
----------------------------------------------------
  c=0 (00000000000000000000000000000000)

State 20 file test.c line 5 function main thread 0
----------------------------------------------------
  c=0 (00000000000000000000000000000000)

State 21 file test.c line 6 function main thread 0
----------------------------------------------------
  t=0 (00000000000000000000000000000000)

State 22 file test.c line 6 function main thread 0
----------------------------------------------------
  t=4187126263 (11111001100100100111100111110111)

State 23 file test.c line 7 function main thread 0
----------------------------------------------------
  s=0 (00000000000000000000000000000000)

State 24 file test.c line 7 function main thread 0
----------------------------------------------------
  s=3329066504 (11000110011011011000011000001000)

State 25 file test.c line 8 function main thread 0
----------------------------------------------------
  b=((unsigned int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 26 file test.c line 8 function main thread 0
----------------------------------------------------
  b=&s!0@1 (0000001000000000000000000000000000000000000000000000000000000000)

Violated property:
  file test.c line 10 function main
  arithmetic overflow on unsigned + in t + *b
  !overflow("+", unsigned int, t, *b)

VERIFICATION FAILED

Again, this is an actual bug and CBMC has a good reason for telling you about it. This one could be fixed by

l = ((unsigned long)t + (unsigned long)*b) & (0xffffffffL);
c += (l < t);

which gives

CBMC version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 42 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
542 variables, 1561 clauses
SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.002s
VERIFICATION SUCCESSFUL

Variant 3: If things are as the previous one, but you have signed int instead of unsigned int, things get a bit more complicated. Here, assuming you use (written in a slightly more elaborate way to better see what is going on)

int nondet_int(void);

void main(void) {
  int l = 0;
  int c = 0;
  int t = nondet_int();
  int s = nondet_int();

  long longt = (long)t;
  long longs = (long)s;
  long temp1 = longt + longs;
  long temp2 = temp1 & (0xffffffffL);

  l = temp2;
  c += (l < t);
}

and run

    cbmc --signed-overflow-check test.c

you will get

CBMC version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 48 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
872 variables, 2430 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.008s
Building error trace

Counterexample:

State 17 file test.c line 4 function main thread 0
----------------------------------------------------
  l=0 (00000000000000000000000000000000)

State 18 file test.c line 4 function main thread 0
----------------------------------------------------
  l=0 (00000000000000000000000000000000)

State 19 file test.c line 5 function main thread 0
----------------------------------------------------
  c=0 (00000000000000000000000000000000)

State 20 file test.c line 5 function main thread 0
----------------------------------------------------
  c=0 (00000000000000000000000000000000)

State 21 file test.c line 6 function main thread 0
----------------------------------------------------
  t=0 (00000000000000000000000000000000)

State 22 file test.c line 6 function main thread 0
----------------------------------------------------
  t=-2147483648 (10000000000000000000000000000000)

State 23 file test.c line 7 function main thread 0
----------------------------------------------------
  s=0 (00000000000000000000000000000000)

State 24 file test.c line 7 function main thread 0
----------------------------------------------------
  s=1 (00000000000000000000000000000001)

State 25 file test.c line 9 function main thread 0
----------------------------------------------------
  longt=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 26 file test.c line 9 function main thread 0
----------------------------------------------------
  longt=-2147483648 (1111111111111111111111111111111110000000000000000000000000000000)

State 27 file test.c line 10 function main thread 0
----------------------------------------------------
  longs=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 28 file test.c line 10 function main thread 0
----------------------------------------------------
  longs=1 (0000000000000000000000000000000000000000000000000000000000000001)

State 29 file test.c line 11 function main thread 0
----------------------------------------------------
  temp1=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 31 file test.c line 11 function main thread 0
----------------------------------------------------
  temp1=-2147483647 (1111111111111111111111111111111110000000000000000000000000000001)

State 32 file test.c line 12 function main thread 0
----------------------------------------------------
  temp2=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 33 file test.c line 12 function main thread 0
----------------------------------------------------
  temp2=2147483649 (0000000000000000000000000000000010000000000000000000000000000001)

Violated property:
  file test.c line 14 function main
  arithmetic overflow on signed type conversion in (signed int)temp2
  temp2 = -2147483648l

VERIFICATION FAILED

Or, written more concisely, if you have

t == -2147483648 (0b10000000000000000000000000000000)
s == 1           (0b00000000000000000000000000000001)

then

temp2 == 2147483649 (0b0000000000000000000000000000000010000000000000000000000000000001)

and an attempt to convert this into a signed int is trouble, because it is out of range (see also Does cast between signed and unsigned int maintain exact bit pattern of variable in memory? ).

As you can see, this counterexample also is an actual bug, and again, CBMC is right in telling you about it. This means in particular, your masking/maths does not work as expected (your masking turns a negative number into a positive number that is out of bounds) and you need to fix your code, so that the result is within the necessary range. (It's probably worthwhile to carefully think about what you actually want to do in order to make sure you get the right results.)

Bypassing an unsigned addition overflow detected by CBMC

Tags:

c

integer

integer-overflow

model-checking

cbmc

AcidBurn

1 Answers

godfatherofpolka

Recent Activity

Donate For Us

Bypassing an unsigned addition overflow detected by CBMC

Tags:

c

integer

integer-overflow

model-checking

cbmc

AcidBurn

1 Answers

godfatherofpolka

Related questions

Recent Activity

Donate For Us