Bounded Model Checking de código C - sessão laboratorial

Considere o seguinte código (disponivel no ficheiro lab.c)

    #include <stdio.h>
    #define LENGTH 5
    int vec[LENGTH];
    
    int maxarray(int u[], int size) {
      int i = 1, a, max = 0;
      while (i < size) {
        if (u[i] > u[max]) { max = i; }
        i++;
      }
      return max;
    }
    
    void main() {
      int i;
      for (i=0; i<=LENGTH; i++) {
        vec[i] = nondet_int(); 
      }
      int r = maxarray(vec, LENGTH);
    }

Note que o programa utiliza um array alocado estaticamente. Por forma a considerar todos os conteúdos possíveis deste array, a função main inicializa-o explicitamente de forma não-determinística, usando a função nondet_int.

Verificação de acessos ilegais ao array

1. Utilize a opção bounds-check do CBMC para verificar se o programa efectua acessos ilegais ao array. Corrija o programa se necessário.

2. A verificação que fez apenas considera a execução da função maxarray a partir de main, com um array concreto. Utilize agora a opção function por forma a verificar se a função faz acessos ilegais quando executada sobre um array qualquer arbitrário. Note que deverá incluir também a opção pointer-check, uma vez que maxarray trabalha sobre um array passado por parâmetro (um apontador).

   Note que pode ter assumir condições (com __CPROVER_assume) sobre os parâmetros das funções de modo a poder assegurar algumas propriedades.

   O número de iterações consideradas afecta o resultado da verificação?

Verificação funcional: intervalo do índice calculado por maxarray

1. Acrescente um assert na função maxarray que lhe permita comprovar que:

   o índice devolvido está contido entre 0 e size-1.

2. Execute o CBMC por forma a estudar a validade desta asserção a partir da execução de main. Aumente progressivamente o valor de LENGTH para testar as limitações da técnica de bounded model checking no que diz respeito a eficiência.

3. Repita o exercício anterior considerando apenas a função maxarray. Note que a propriedade é aparentemente válida para qualquer execução sobre qualquer array (admitindo que os acessos ao array são válidos), pelo que o CBMC deveria ter sucesso com qualquer número de iterações (opção unwind ). Utilizando a opção trace procure entender o que falha nesta verificação, e altere o programa incluindo uma pré-condição (com __CPROVER_assume) que lhe permita verificar o programa com sucesso para um número qualquer de iterações.

Verificação funcional: máximo

Vamos agora considerar uma propriedade mais difícil:

a função maxarray calcula de facto o índice de um máximo do array.

Note que, uma vez que a linguagem de especificação do CBMC não inclui quantificadores, uma forma possível de garantir que vec[r] é superior ao conteúdo de qualquer posição do array é utilizar um ciclo.

1. Inclua então o seguinte código no final da função main:

        for (i=0; i<LENGTH; i++)
            assert (vec[i] <= vec[r]);
   

   Execute o CBMC por forma a estudar a validade desta asserção a partir da execução de main.

2. Aumente progressivamente o valor de LENGTH por forma a testar as limitações da técnica de bounded model checking no que diz respeito a eficiência.

   O que pode concluir relativamente à verificação da propriedade anterior (intervalo do índice devolvido)?

3. Existe de facto uma forma de simular uma quantificação universal, sem recorrer a um ciclo. Substitua o ciclo anterior pelo código seguinte:

         i = nondet_int();
         __CPROVER_assume (0 <= i && i < LENGTH); 
         assert (vec[i] <= vec[r]);  

A inicialização não-determinística da variável, seguida do comando __CPROVER_assume, tem como efeito que a semântica da asserção será equivalente a $(\forall i. ~ 0\leq i < \mathsf{LENGTH} \to \mathsf{vec}[i] \leq \mathsf{vec}[r])$

1. Repita o estudo de eficiência que fez para a versão anterior. O que pode concluir sobre a utilização destas duas técnicas para a verificação de propriedades deste género?

Verificação sobre um input concreto

O estudo de eficiência realizado nos pontos anteriores revela as limitações de uma técnica baseada em “força bruta”, quando o que está em causa é a verificação de propriedades funcionais “de primeira ordem” — será o preço a pagar pela automação.

Imaginemos no entanto um cenário diferente, em que se pretende verificar as propriedades anteriores apenas para uma execução particular (i.e. uma execução sobre um array concreto). Neste caso o CBMC efectuará optimizações com base em propagação de constantes e simplificação de expressões, o que permitirá uma execução muito eficiente.

1. Substitua a instrução vec[i] = nondet_int() no corpo do primeiro ciclo por vec[i] = i (ou qualquer outra instrução que permita inicializar o array com valores constantes) e verifique de novo o programa tendo como entrypoint a função main.

2. Repita o estudo de eficiência, aumentando progressivamente o comprimento do array, e compare os tempos de execução com os que obtinha com um array genérico.

Teste de invariantes

Uma perspectiva possível sobre a utilização de bounded model checking de software é como técnica complementar, e não alternativa, à verificação dedutiva. Em particular, pode ser útil para ajudar a perceber se uma determinada propriedade é ou não um invariante de um dado ciclo. A consideração de apenas algumas iterações poderá ser suficiente para encontrar um contra-exemplo, ou como evidência (não prova!) de que realmente se trata de um invariante – neste caso, será um bom candidato que poderá ser depois usado para a verificação dedutiva do programa.

Investigue, usando o CBMC, quais das seguintes fórmulas não são invariantes do ciclo da função maxarray:

1. $(\forall k. ~ 0\leq k \leq i \to \mathsf{vec}[k] \leq \mathsf{vec}[max])$
2. $(\forall k. ~ 0\leq k < i \to \mathsf{vec}[k] < \mathsf{vec}[max])$
3. $(\forall k. ~ 0\leq k < i \to \mathsf{vec}[k] \leq \mathsf{vec}[max])$
4. $(\forall k. ~ 0\leq k \leq i \to \mathsf{vec}[k] < \mathsf{vec}[max])$

Descreva como procedeu, em particular se utilizou um array concreto ou genérico.

Verificação de overflow

Considere agora a função sum que calcula a soma de um array de inteiros.

	int sum (int u[], int size) {
	  int i, s=0;
	
	  for (i=0; i<size; i++)
	    s += u[i];
	  
	  return s;
	}

1. Invoque esta função a partir do main e utilize a opção signed-overflow-check do CBMC para verificar se o programa pode ter um problema de overflow.

   No caso de encontrar um problema, use a opção trace para identificar o contra-exemplo encontrado.

   Acrescente restrições ao array vec que premitam garantir a segurança do programa quanto ao problema de overflow.

2. Repita o estudo do problema de overflow considerando apenas a função sum. Terá certamente de fazer algumas assunções sobre os argumentos da função.

Exercício final

Considere o seguinte código (disponivel no ficheiro exercicioCBMC.c)

        #include <stdio.h>
        #define MAX 10

        int vec[MAX];
 
        int fun (int n)
        {
          int i, x=0;
  
          for (i=0; i < MAX; i++)
              if (vec[i]>n)
                 x = x + vec[i]/(n-i);
              else x = x + vec[i]*(n-i);

           return x;
         }

         int cpdiff (int A[], int na, int B[], int nb, int x)
         {
           int i, j=0;

           for (i=0; i<na; i++)
               if (A[i]!=x) {
                  B[j] = A[i];
                  j++;
               }
           return j;
          }

         void main()
         {
           int j, t, y;
           int a[MAX], b[MAX];

           for (j=0; j<MAX; j++) {
               a[j] = j;
               vec[j] = j*30;
           }
           a[4] = 2;
           a[5] = 1;

           y = fun(55);
           t = cpdiff(a,MAX,b,MAX,1);
          }

1. Para verificar a segurança das funções fun, cpdiff e main, relativamente a acessos ilegais a posições do array, invoque:

   cbmc exercicioCBMC.c -function fun -bounds-check -pointer-check

   cbmc exercicioCBMC.c -function cpdiff -bounds-check -pointer-check

   cbmc exercicioCBMC.c -bounds-check

   O que pode concluir? Por que razão segunda invocação não pára, e as outras duas sim?

2. Repita com a invocação com

   cbmc exercicioCBMC.c -function cpdiff -bounds-check -pointer-check -unwind 10

   Por que razão falha agora a verificação? Será que podemos evitar esta falha? O que podemos concluir?

3. Use o CBMC para verificar a segurança da função fun relativamente a todos os outros problemas de “safety” ainda não testados. Indique as invocações que fez ao CBMC e comente as conclusões a que chegou. Indique os contra-exemplos (i.e., situações onde há falha) que o CBMC encontrou, caso haja.

4. Insira código no final da função main de modo a fazer uma atribuição não determinista ao vector vec e ao argumento de invocação da função fun, e teste esta invocação quanto a eventuais problemas de “safety”.

   Indique as invocações que fez ao CBMC e as conclusões a que chegou.

   Indique os contra-exemplos (i.e., situações onde há falha) que o CBMC encontrou, caso haja.