Frama-C slice: parallelizable loop

Question

I am trying to perform a backward slicing of an array element at specific position. I tried two different source codes. The first one is (first.c):

const int in_array[5][5]={
                          1,2,3,4,5,
                          6,7,8,9,10,
                          11,12,13,14,15,
                          16,17,18,19,20,
                          21,22,23,24,25
};

int out_array[5][5];
int main(unsigned int x, unsigned int y)
{
  int res;
  int i;
  int j;
  for(i=0; i<5; i++){
    for(j=0; j<5; j++){
      out_array[i][j]=i*j*in_array[i][j];
    }
  }
  res = out_array[x][y];
  return res;
}

I run the command:

frama-c-gui -slevel 10 -val -slice-return main file.c

and get the following generated code:

int main(unsigned int x, unsigned int y)
{
  int res;
  int i;
  int j;
  i = 0;
  while (i < 5) {
    j = 0;
    while (j < 5){
      out_array[i][j] = (i * j) * in_array[i][i];
      j ++;
    }
    i ++;
  }
  res = out_array[x][y];
  return res;
}

This seems to be ok, since the x and y are not defined, so the "res" can be at any position in the out_array. I tried then with the following code:

const int in_array[5][5]={
                          1,2,3,4,5,
                          6,7,8,9,10,
                          11,12,13,14,15,
                          16,17,18,19,20,
                          21,22,23,24,25
};

int out_array[5][5];
int main(void)
{
  int res;
  int i;
  int j;
  for(i=0; i<5; i++){
    for(j=0; j<5; j++){
      out_array[i][j]=i*j*in_array[i][j];
    }
  }
  res = out_array[3][3];
  return res;
}

The result given was exactly the same. However, since I am explicitly looking for a specific position inside the array, and the loops are independent (parallelizable), I would expect the output to be something like this:

int main(void)
{
  int res;
  int i;
  int j;
  i = 3;
  j = 3;
  out_array[i][j]=(i * j) * in_array[i][j];
  res = out_array[3][3];
}

I am not sure if is it clear from the examples. What I want to do is to identify, for a given array position, which statements impact its final result. Thanks in advance for any support.

score 2 · Accepted Answer · answered Feb 18 '15 at 17:17

You obtain "the statements which impact the final result". The issue is that not all loop iterations are useful, but there is no way for the slicing to remove a statement to the code in its current form. If you perform syntactic loop unrolling, with -ulevel 5, then you will each loop iteration is individualized, and slicing can decide for each of them whether it is to be included in the slice or not. In the end, frama-c-gui -ulevel 5 -slice-return main loop.c gives you the following code

int main(void)
{
  int res;
  int i;
  int j;
  i = 0;
  i ++;
  i ++;
  i ++;
  j = 0;
  j ++;
  j ++;
  j ++;
  out_array[i][j] = (i * j) * in_array[i][j];
  res = out_array[3][3];
  return res;
}

which is indeed the minimal set of instructions needed to compute the value of out_array[3][3].

Of course whether -ulevel n scales up to very high values of n is another question.

Frama-C slice: parallelizable loop

1 Answers1