Undefined behavior overlooked in a couple of array programs in PR #835

[divyeshunadkat]

The files array-cav19/array_tiling_poly6.c and array-cav19/array_tiling_tcpy.c added in the PR #835 have undefined behavior due to integer overflows.

Originally posted by @divyeshunadkat in #835 (comment)

[PhilippWendler]

Could you please provide a concrete test case (i.e., values for nondet variables) that shows the overflow and explain where it happens?

@avritichauhan Could you then please suggest fixes?

[hernanponcedeleon]

For array-cav19/array_tiling_poly6.c you can take S=2147483647.
In the last iteration of the first loop, i=2147483646 and thus ((i-1)*(i+1)) on line 18 overflows.

For array-cav19/array_tiling_tcpy.c, I assume (see below *) the result of 2*S in line 15 would be stored in a 32-bits variable resulting in an overflow for S=2147483647.

There has been some discussion in several issues/PRs (#1105, #1155) on how to fix such problems. One possibility is to do the following:

• do not use the current version of the benchmark for reachability category (since it contains UB), but use it for no-overflow
• use unsigned int for the variable that might overflow. Overflow of unsigned integers does not result in UB, but this will probably change the expected result for the reachability category as was initially intended.
• use long long variables (8 bytes) to avoid overflows. In most of the cases we should be able to keep the initial expected result for the reachability category (exceptions might be the cases where multiplications are involved since even then long long might not be enough).

(*) This is (part of) the llvm generated by clang

define i32 @main() #0 {
  %1 = alloca i32, align 4
  %2 = alloca i32, align 4
  %3 = alloca i32, align 4
  %4 = alloca i8*, align 8
  %5 = alloca i64, align 8
  %6 = alloca i64, align 8
  store i32 0, i32* %1, align 4
  %7 = call i32 (...) @__VERIFIER_nondet_int()
  store i32 %7, i32* %2, align 4
  %8 = load i32, i32* %2, align 4
  %9 = icmp sgt i32 %8, 1
  %10 = zext i1 %9 to i32
  call void @assume_abort_if_not(i32 %10)
  %11 = load i32, i32* %2, align 4
  %12 = mul nsw i32 2, %11

Memory %2 holds the value of S which is then loaded in %11. The multiplication is performed by the last instruction and the result is stored in the i32 variable %12. Since %11 can hold the value 2147483647, the overflow is possible.

[divyeshunadkat]

@hernanponcedeleon Thanks for quickly reverting with the test case :) 👍

@PhilippWendler @avritichauhan
In array-cav19/array_tiling_poly6.c basically for every value of S > ceil( sqrt(2147483647 + 1) ), the expressions ((i-1)*(i+1)) on line 18 and (i*i) on line 21 will cause an integer overflow after a certain number of iterations. I think the best way to go about this is to use the long long type for declaring the array variable a and the counter variable i.

In array-cav19/array_tiling_tcpy.c, the result of 2*S in lines 15, 16, 20 and 24 will cause an integer overflow for every value of S >= ceil(2147483647 / 2) Adding the statement assume_abort_if_not(S < 2147483647 / 2); after line 13 would solve the overflow.

[hernanponcedeleon]

In array-cav19/array_tiling_tcpy.c, the result of 2*S in lines 15, 16, 20 and 24 will cause an integer overflow for every value of S >= ceil(2147483647 / 2) Adding the statement assume_abort_if_not(2*S < 2147483647); after line 13 would solve the overflow.

I don't think this is the correct solution since the check can also result in an overflow (when computing 2*S). I think the correct check would actually be assume_abort_if_not(S < 1073741823)

[divyeshunadkat]

In array-cav19/array_tiling_tcpy.c, the result of 2*S in lines 15, 16, 20 and 24 will cause an integer overflow for every value of S >= ceil(2147483647 / 2) Adding the statement assume_abort_if_not(2*S < 2147483647); after line 13 would solve the overflow.

I don't think this is the correct solution since the check can also result in an overflow (when computing 2*S). I think the correct check would actually be assume_abort_if_not(S < 1073741823)

Oops. Changed it just before commenting from S < 2147483647 / 2! No wonder we need verification tools ;P
Corrected the original comment. Thanks @hernanponcedeleon

[divyeshunadkat]

Closing the issue as the PR with the fixes is merged. Thanks @avritichauhan @hernanponcedeleon @PhilippWendler