CBMC 5.86 crashes

[tihanyin]

CBMC 5.86 crashes with the following small C program.

Details:

CBMC version: 5.86.0 (cbmc-5.86.0) 64-bit x86_64 linux
Operating system: Ubuntu 22.04.2 LTS
Command line: cbmc FormAI_59971.c

C program:

//FormAI DATASET v1.0 Category: Space Invaders Game Clone ; Style: realistic
#include <stdio.h>
#include <stdlib.h>
#include <time.h>

#define ROWS 5
#define COLS 10

/* Function prototypes */
void print_gameboard(int rows, int cols, char gameboard[rows][cols]);
void clear_gameboard(int rows, int cols, char gameboard[rows][cols]);
void spawn_enemy_ships(int rows, int cols, char gameboard[rows][cols]);
void move_enemy_ships(int rows, int cols, char gameboard[rows][cols]);
void player_shot(int rows, int cols, char gameboard[rows][cols], int player_row);
void enemy_shot(int rows, int cols, char gameboard[rows][cols], int* score);

/* Main function */
int main()
{
    char gameboard[ROWS][COLS];
    int player_row = ROWS - 1;
    int score = 0;
    int quit = 0;
    char input;
    
    /* Set seed for random number generator */
    srand(time(NULL));
    
    /* Clear gameboard and spawn enemy ships */
    clear_gameboard(ROWS, COLS, gameboard);
    spawn_enemy_ships(ROWS, COLS, gameboard);
    
    /* Main game loop */
    while(!quit)
    {
        /* Print gameboard and score */
        printf("Score: %d\n", score);
        print_gameboard(ROWS, COLS, gameboard);
        
        /* Get player input */
        printf("Move left (a) / right (d) / shoot (s) / quit (q): ");
        scanf(" %c", &input);
        
        /* Process player input */
        switch(input)
        {
            case 'a':
                if(player_row > 0)
                {
                    player_row--;
                }
                break;
                
            case 'd':
                if(player_row < COLS - 1)
                {
                    player_row++;
                }
                break;
                
            case 's':
                player_shot(ROWS, COLS, gameboard, player_row);
                enemy_shot(ROWS, COLS, gameboard, &score);
                break;
                
            case 'q':
                quit = 1;
                break;
                
            default:
                printf("Invalid input\n");
        }
        
        /* Move enemy ships */
        move_enemy_ships(ROWS, COLS, gameboard);
        
        /* Check for game over */
        for(int i = 0; i < COLS; i++)
        {
            if(gameboard[0][i] == 'E')
            {
                printf("Game over\n");
                quit = 1;
                break;
            }
        }
    }
    
    return 0;
}

/* Function definitions */

void print_gameboard(int rows, int cols, char gameboard[rows][cols])
{
    printf("\n");
    for(int i = 0; i < rows; i++)
    {
        for(int j = 0; j < cols; j++)
        {
            printf("%c ", gameboard[i][j]);
        }
        printf("\n");
    }
    printf("\n");
}

void clear_gameboard(int rows, int cols, char gameboard[rows][cols])
{
    for(int i = 0; i < rows; i++)
    {
        for(int j = 0; j < cols; j++)
        {
            gameboard[i][j] = '.';
        }
    }
}

void spawn_enemy_ships(int rows, int cols, char gameboard[rows][cols])
{
    for(int i = 0; i < cols; i++)
    {
        gameboard[0][i] = 'E';
    }
}

void move_enemy_ships(int rows, int cols, char gameboard[rows][cols])
{
    /* Check if any enemy ships are at the bottom */
    for(int i = 0; i < cols; i++)
    {
        if(gameboard[ROWS - 1][i] == 'E')
        {
            printf("Game over\n");
            exit(0);
        }
    }
    
    /* Move enemy ships down by one row */
    for(int i = ROWS - 1; i > 0; i--)
    {
        for(int j = 0; j < cols; j++)
        {
            gameboard[i][j] = gameboard[i - 1][j];
        }
    }
    
    /* Spawn new row of enemy ships at top */
    spawn_enemy_ships(1, cols, gameboard);
}

void player_shot(int rows, int cols, char gameboard[rows][cols], int player_row)
{
    gameboard[ROWS - 1][player_row] = 'P';
    for(int i = ROWS - 2; i >= 0; i--)
    {
        if(gameboard[i][player_row] == 'E')
        {
            gameboard[i][player_row] = '.';
            return;
        }
        else if(gameboard[i][player_row] == 'P')
        {
            gameboard[i][player_row] = '.';
        }
    }
}

void enemy_shot(int rows, int cols, char gameboard[rows][cols], int* score)
{
    int random_col = rand() % cols; /* Choose random column for enemy shot */
    
    for(int i = 0; i < ROWS; i++)
    {
        if(gameboard[i][random_col] == 'P')
        {
            gameboard[i][random_col] = '.';
            (*score)++;
            return;
        }
    }
}

OUTPUT:

cbmc FormAI_59971.c
CBMC version 5.86.0 (cbmc-5.86.0) 64-bit x86_64 linux
Parsing FormAI_59971.c
Converting
Type-checking FormAI_59971
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
**** WARNING: no body for function srand
--- begin invariant violation report ---
Invariant check failed
File: ../src/util/simplify_expr.cpp:3069 function: simplify_rec
Condition: Postcondition
Reason: (as_const(tmp).type().id() == ID_array && expr.type().id() == ID_array) || as_const(tmp).type() == expr.type()
Backtrace:
cbmc(+0xa89f20) [0x56454a9fdf20]
cbmc(+0xa8abf9) [0x56454a9febf9]
cbmc(+0x1e9604) [0x56454a15d604]
cbmc(+0xaeb7da) [0x56454aa5f7da]
cbmc(+0xaec648) [0x56454aa60648]
cbmc(+0x4c378c) [0x56454a43778c]
cbmc(+0x4c3671) [0x56454a437671]
cbmc(+0x4c6285) [0x56454a43a285]
cbmc(+0x4ba392) [0x56454a42e392]
cbmc(+0x457f5d) [0x56454a3cbf5d]
cbmc(+0x4dfa96) [0x56454a453a96]
cbmc(+0x4e1a18) [0x56454a455a18]
cbmc(+0x328648) [0x56454a29c648]
cbmc(+0x4e1b08) [0x56454a455b08]
cbmc(+0x4e1bd7) [0x56454a455bd7]
cbmc(+0x4e126b) [0x56454a45526b]
cbmc(+0x3064f1) [0x56454a27a4f1]
cbmc(+0x305061) [0x56454a279061]
cbmc(+0x1c8b92) [0x56454a13cb92]
cbmc(+0x1c445b) [0x56454a13845b]
cbmc(+0x1bb4af) [0x56454a12f4af]
cbmc(+0x1a7fc9) [0x56454a11bfc9]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f47ac629d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f47ac629e40]
cbmc(+0x1bce15) [0x56454a130e15]

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
typecast
  * type: pointer
      * #source_location: 
        * file: FormAI_59971.c
        * line: 108
        * function: clear_gameboard
        * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
      * width: 64
      * #failed_symbol: clear_gameboard::gameboard$object
      0: array
          * #source_location: 
            * file: FormAI_59971.c
            * line: 108
            * function: clear_gameboard
            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
          * #index_type: signedbv
              * width: 64
              * #c_type: signed_long_int
          * size: symbol
              * type: unsignedbv
                  * width: 64
                  * #constant: 1
                  * #c_type: unsigned_long_int
              * identifier: clear_gameboard$array_size::clear_gameboard$array_size$1!0#0
              * expression: symbol
                  * type: unsignedbv
                      * width: 64
                      * #constant: 1
                      * #c_type: unsigned_long_int
                  * identifier: clear_gameboard$array_size::clear_gameboard$array_size$1
              * #SSA_symbol: 1
              * L0: 0
              * L2: 0
              * L1_object_identifier: clear_gameboard$array_size::clear_gameboard$array_size$1!0
          0: signedbv
              * width: 8
              * #c_type: char
  0: address_of
      * type: pointer
          * width: 64
          0: signedbv
              * width: 8
              * #c_type: char
      0: index
          * type: signedbv
              * width: 8
              * #c_type: char
          0: index
              * type: array
                  * #source_location: 
                    * file: FormAI_59971.c
                    * line: 20
                    * function: main
                    * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                  * #index_type: signedbv
                      * width: 64
                      * #c_type: signed_long_int
                  * size: constant
                      * type: signedbv
                          * width: 64
                          * #c_type: signed_long_int
                      * value: A
                  0: signedbv
                      * width: 8
                      * #c_type: char
              0: symbol
                  * type: array
                      * #source_location: 
                        * file: FormAI_59971.c
                        * line: 20
                        * function: main
                        * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                      * #index_type: signedbv
                          * width: 64
                          * #c_type: signed_long_int
                      * size: constant
                          * type: signedbv
                              * width: 64
                              * #c_type: signed_long_int
                          * value: 5
                      0: array
                          * #source_location: 
                            * file: FormAI_59971.c
                            * line: 20
                            * function: main
                            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                          * #index_type: signedbv
                              * width: 64
                              * #c_type: signed_long_int
                          * size: constant
                              * type: signedbv
                                  * width: 64
                                  * #c_type: signed_long_int
                              * value: A
                          0: signedbv
                              * width: 8
                              * #c_type: char
                  * identifier: main::1::gameboard!0@1
                  * expression: symbol
                      * type: array
                          * #source_location: 
                            * file: FormAI_59971.c
                            * line: 20
                            * function: main
                            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                          * #index_type: signedbv
                              * width: 64
                              * #c_type: signed_long_int
                          * size: constant
                              * type: signedbv
                                  * width: 64
                                  * #c_type: signed_long_int
                              * value: 5
                          0: array
                              * #source_location: 
                                * file: FormAI_59971.c
                                * line: 20
                                * function: main
                                * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                              * #index_type: signedbv
                                  * width: 64
                                  * #c_type: signed_long_int
                              * size: constant
                                  * type: signedbv
                                      * width: 64
                                      * #c_type: signed_long_int
                                  * value: A
                              0: signedbv
                                  * width: 8
                                  * #c_type: char
                      * #source_location: 
                        * file: FormAI_59971.c
                        * line: 30
                        * function: main
                        * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                      * identifier: main::1::gameboard
                      * #lvalue: 1
                  * #SSA_symbol: 1
                  * L0: 0
                  * L1: 1
                  * L1_object_identifier: main::1::gameboard!0@1
              1: constant
                  * type: signedbv
                      * width: 64
                      * #c_type: signed_long_int
                  * value: 0
          1: constant
              * type: signedbv
                  * width: 64
                  * #c_type: signed_long_int
              * value: 0
+
  * type: pointer
      * #source_location: 
        * file: FormAI_59971.c
        * line: 108
        * function: clear_gameboard
        * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
      * width: 64
      0: array
          * #source_location: 
            * file: FormAI_59971.c
            * line: 108
            * function: clear_gameboard
            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
          * #index_type: signedbv
              * width: 64
              * #c_type: signed_long_int
          * size: symbol
              * type: unsignedbv
                  * width: 64
                  * #constant: 1
                  * #c_type: unsigned_long_int
              * identifier: clear_gameboard$array_size::clear_gameboard$array_size$1!0
              * expression: symbol
                  * type: unsignedbv
                      * width: 64
                      * #constant: 1
                      * #c_type: unsigned_long_int
                  * identifier: clear_gameboard$array_size::clear_gameboard$array_size$1
              * #SSA_symbol: 1
              * L0: 0
              * L1_object_identifier: clear_gameboard$array_size::clear_gameboard$array_size$1!0
          0: signedbv
              * width: 8
              * #c_type: char
  0: typecast
      * type: pointer
          * #source_location: 
            * file: FormAI_59971.c
            * line: 108
            * function: clear_gameboard
            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
          * width: 64
          * #failed_symbol: clear_gameboard::gameboard$object
          0: array
              * #source_location: 
                * file: FormAI_59971.c
                * line: 108
                * function: clear_gameboard
                * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
              * #index_type: signedbv
                  * width: 64
                  * #c_type: signed_long_int
              * size: symbol
                  * type: unsignedbv
                      * width: 64
                      * #constant: 1
                      * #c_type: unsigned_long_int
                  * identifier: clear_gameboard$array_size::clear_gameboard$array_size$1!0#0
                  * expression: symbol
                      * type: unsignedbv
                          * width: 64
                          * #constant: 1
                          * #c_type: unsigned_long_int
                      * identifier: clear_gameboard$array_size::clear_gameboard$array_size$1
                  * #SSA_symbol: 1
                  * L0: 0
                  * L2: 0
                  * L1_object_identifier: clear_gameboard$array_size::clear_gameboard$array_size$1!0
              0: signedbv
                  * width: 8
                  * #c_type: char
      0: address_of
          * type: pointer
              * width: 64
              0: signedbv
                  * width: 8
                  * #c_type: char
          0: index
              * type: signedbv
                  * width: 8
                  * #c_type: char
              0: index
                  * type: array
                      * #source_location: 
                        * file: FormAI_59971.c
                        * line: 20
                        * function: main
                        * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                      * #index_type: signedbv
                          * width: 64
                          * #c_type: signed_long_int
                      * size: constant
                          * type: signedbv
                              * width: 64
                              * #c_type: signed_long_int
                          * value: A
                      0: signedbv
                          * width: 8
                          * #c_type: char
                  0: symbol
                      * type: array
                          * #source_location: 
                            * file: FormAI_59971.c
                            * line: 20
                            * function: main
                            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                          * #index_type: signedbv
                              * width: 64
                              * #c_type: signed_long_int
                          * size: constant
                              * type: signedbv
                                  * width: 64
                                  * #c_type: signed_long_int
                              * value: 5
                          0: array
                              * #source_location: 
                                * file: FormAI_59971.c
                                * line: 20
                                * function: main
                                * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                              * #index_type: signedbv
                                  * width: 64
                                  * #c_type: signed_long_int
                              * size: constant
                                  * type: signedbv
                                      * width: 64
                                      * #c_type: signed_long_int
                                  * value: A
                              0: signedbv
                                  * width: 8
                                  * #c_type: char
                      * identifier: main::1::gameboard!0@1
                      * expression: symbol
                          * type: array
                              * #source_location: 
                                * file: FormAI_59971.c
                                * line: 20
                                * function: main
                                * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                              * #index_type: signedbv
                                  * width: 64
                                  * #c_type: signed_long_int
                              * size: constant
                                  * type: signedbv
                                      * width: 64
                                      * #c_type: signed_long_int
                                  * value: 5
                              0: array
                                  * #source_location: 
                                    * file: FormAI_59971.c
                                    * line: 20
                                    * function: main
                                    * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                                  * #index_type: signedbv
                                      * width: 64
                                      * #c_type: signed_long_int
                                  * size: constant
                                      * type: signedbv
                                          * width: 64
                                          * #c_type: signed_long_int
                                      * value: A
                                  0: signedbv
                                      * width: 8
                                      * #c_type: char
                          * #source_location: 
                            * file: FormAI_59971.c
                            * line: 30
                            * function: main
                            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
                          * identifier: main::1::gameboard
                          * #lvalue: 1
                      * #SSA_symbol: 1
                      * L0: 0
                      * L1: 1
                      * L1_object_identifier: main::1::gameboard!0@1
                  1: constant
                      * type: signedbv
                          * width: 64
                          * #c_type: signed_long_int
                      * value: 0
              1: constant
                  * type: signedbv
                      * width: 64
                      * #c_type: signed_long_int
                  * value: 0
  1: typecast
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      0: constant
          * type: signedbv
              * width: 32
              * #c_type: signed_int
          * #source_location: 
            * file: FormAI_59971.c
            * line: 110
            * function: clear_gameboard
            * working_directory: /home/tihanyin/Desktop/research/FormAI_dataset/CBMC_crash
          * value: 0
          * #base: 10
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
Aborted (core dumped)

[thomasspriggs]

I think this particular error may be down to the INVARIANT being overly restrictive. But this needs more investigation to confirm and fix.

The INVARIANT basically says that the type before simplification and after simplification should be the same. This makes intuitive sense until you realise that the type of an array can contain an expression for the size and it could be valid to apply simplification to the size expression. There is already an exception on array types, but it only checks the root of the type. In this case the condition misses that the difference is in an array type, because the type is a pointer to an array.

The types are different and fail the check as the input has an array of size clear_gameboard$array_size::clear_gameboard$array_size$1!0 and the output has size clear_gameboard$array_size::clear_gameboard$array_size$1!0#0. I think this could be a valid transform or it could be due to inconsistent types in the input expression.

Sorry not to have a complete answer, but I wanted to share what I have worked out so far.

[tautschnig]

Thank you for the bug report and the analysis! It seems we need to fix state.rename<L1_WITH_CONSTANT_PROPAGATION>, or the way it is to be used: it may replace SSA L1 symbols with expressions that have types L2 renamed. This causes trouble when the containing expression (in this case: a pointer addition) does not have that type L2 renamed. I still need to do more debugging to figure out where to fix this.