[CN] Double array access

[lwli11]

Is there an annotation to get this code to admit?

int main(){
    int graph[6][6] = {{0,1,1,0,0,0},
                     {1,0,1,0,0,0},
                     {1,1,0,1,1,0},
                     {0,0,1,0,0,0},
                     {0,0,1,0,0,1},
                     {0,0,0,0,1,0}};
   /*@ extract Owned<int>, 1; @*/
   /*@ extract Owned<int>, 1; @*/
   int i = graph[1][1];
}

Thanks!

[dc-mak]

Likely related to (#361, #357, #320), I think we may not just have good support for this yet sadly.

[septract]

Hm, yes. Here's a test-case:

// This verifies 
void array_1d() 
{
    int graph[6] = {1,0,1,0,0,0};
    /*@ extract Owned<int>, 1u64; @*/
    int i = graph[1];
    assert (i == 0); 
}

// This does not verify 
void array_2d() 
{
    int graph[6][6] = 
        { {0,1,1,0,0,0},
          {1,0,1,0,0,0},
          {1,1,0,1,1,0},
          {0,0,1,0,0,0},
          {0,0,1,0,0,1},
          {0,0,0,0,1,0} };
    /*@ extract Owned<int>, 1u64; @*/
    /*@ extract Owned<int>, 1u64; @*/
    int i = graph[1][1];
    assert (i == 0); 
}

[peterohanley]

This works fine:

void array_2d()
{
    int graph[6][6] =
        { {0,1,1,0,0,0},
          {1,0,1,0,0,0},
          {1,1,0,1,1,0},
          {0,0,1,0,0,0},
          {0,0,1,0,0,1},
          {0,0,0,0,1,0} };
    /*@ extract Owned<int[6]>, 1u64; @*/
    /*@ extract Owned<int>, 1u64; @*/
    int i = graph[1][1];
    assert (i == 0);
}

It is tough if you're receiving this array as an argument though.

void array_2d_arg(int graph[6][6])
{
    /*@ extract Owned<int[6]>, 1u64; @*/
    /*@ extract Owned<int>, 1u64; @*/
    int i = graph[1][1];
    assert (i == 0);
}

% cn verify array2.c
[1/2]: array_2d_arg
array2.c:27:9: warning: extract: index added, no resources (yet) extracted.
    /*@ extract Owned<int[6]>, 1u64; @*/
        ^~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
array2.c:28:9: warning: extract: index added, no resources (yet) extracted.
    /*@ extract Owned<int>, 1u64; @*/
        ^~~~~~~~~~~~~~~~~~~~~~~~~ 
array2.c:29:13: error: Missing resource for reading
    int i = graph[1][1];
            ^~~~~~~~~~~ 
Resource needed: Owned<signed int>(array_shift<signed int>(array_shift<signed int>(array_shift<signed int[6]>(graph
        , (u64)1i32), (u64)0i32), (u64)1i32))

For comparison here's the error with the incorrect spec on the local array:

% cn verify array2.c    
[1/1]: array_2d
array2.c:11:9: warning: extract: index added, no resources (yet) extracted.
    /*@ extract Owned<int>, 1u64; @*/
        ^~~~~~~~~~~~~~~~~~~~~~~~~ 
array2.c:12:9: warning: extract: index added, no resources (yet) extracted.
    /*@ extract Owned<int>, 1u64; @*/
        ^~~~~~~~~~~~~~~~~~~~~~~~~ 
array2.c:13:13: error: Missing resource for reading
    int i = graph[1][1];
            ^~~~~~~~~~~ 
Resource needed: Owned<signed int>(array_shift<signed int>(array_shift<signed int>(array_shift<signed int[6]>(array_shift<signed int[6]>(&graph
          , (u64)0i32), (u64)1i32), (u64)0i32), (u64)1i32))

There is an extra array_shift<signed int[6]> and then an extra &. The latter is because it's now an argument but I don't understand why the extra array level has appeared.

[septract]

Oh neat, so this specific example does actually work. Thanks @peterohanley !

[dc-mak]

Does it work when the function is called main? I recall trying what Peter did but having it not work.

[dc-mak]

For the argument vs local, it's likely because array arguments are a bit of a lie in C and that's just actually a int** and something's getting confused as a result (it shouldn't be, but that's likely related to the source of the discrepancy).

[septract]

@dc-mak this verifies:

int main()
{
  int graph[6][6] =
      { {0,1,1,0,0,0},
        {1,0,1,0,0,0},
        {1,1,0,1,1,0},
        {0,0,1,0,0,0},
        {0,0,1,0,0,1},
        {0,0,0,0,1,0} };
  /*@ extract Owned<int[6]>, 1u64; @*/
  /*@ extract Owned<int>, 1u64; @*/
  int i = graph[1][1];
  assert (i == 0);
  return 1; 
}

CN version: git-c5c1da0b3 [2024-08-12 11:23:50 -0700]