Incorrect SMT encoding produced (related to print statements containing arrays) #7623
Description
CBMC version: 5.79.0 (cbmc-5.79.0-47-g98bba8e6b5)
Operating system: Mac OS (M1)
Exact command line resulting in the issue: cbmc --cvc4 test.c
What behaviour did you expect: This is a simple C file which initialises a 3 dimensional array and then prints it, with an assert(0) at the end of the file. I expected a correct SMT encoding to be generated
What happened instead: CBMC produces an SMT encoding that contains (_ bv256 8), a bitvector value too big to fit in the bitvector of size 8.
SMT2 solver returned error message:
"Parse Error: /var/folders/ww/73cqk_1x2n1cryjs5gspl5sc0000gn/T/smt2_dec_problem_57743.mCKO4t:7094.59: Overflow in bitvector construction (specified bitvector size 8 too small to hold value 256)
...lect array.90 (_ bv0 64)) (concat (_ bv256 8) (_ bv0 56))))
^
"
I printed the smt file, using cbmc --cvc4 --outfile test.smt2 test.c, and the incorrect SMT encoding is generated by the substitute for an array constructor
(declare-fun |printf::va_arg$84!0| () (_ BitVec 32))
; the following is a substitute for an array constructor
(declare-fun array.91 () (Array (_ BitVec 64) (_ BitVec 64)))
(assert (= (select array.91 (_ bv0 64)) (concat (_ bv259 8) (_ bv0 56))))
; set_to true (equal)
(define-fun |printf::va_args$169!0#1| () (Array (_ BitVec 64) (_ BitVec 64)) array.91)
It seems to be dependent on the number of print statements. The bug does not appear if:
- the array is only 2 dimensional
- the array size is less than 5
- only one print statement appears in the print loop
- the array elements are initialised to a constant value rather than a nondet value
file test.c:
#define SIZE 5 // the error occurs only when size is 5 or more
int alloc_0[SIZE][SIZE][SIZE];
int main() {
for (int i = 0; i < SIZE; i++) {
for (int j = 0; j < SIZE; j++) {
for (int k = 0; k < SIZE; k++) {
alloc_0[i][j][k] = nondet(); // error only occurs when alloc_0 is set to nondets, not constants.
}
}
}
// --------------------------------
for (int i = 0; i < SIZE; i++) {
for (int j = 0; j < SIZE; j++) {
for (int k = 0; k < SIZE; k++) {
// the error occurs only when BOTH these print statements are present
printf("%d ", alloc_0[i][j][k]);
printf("\n");
}
}
}
__CPROVER_assert(0, "reached the end");
}