Cannot assign static-length array to VLA

[mlbrooks]

Intro case:

void f( int rows, int cols, float x[rows][cols] );

void g() {
    float m[4][5];
    f( 4, 5, m );
}

GCC, Actual and Authority: compiles successfully
CFA Actual:

No reasonable alternatives for expression Applying untyped:
  Name: f
...to:
  constant expression (4 4: signed int)
  constant expression (5 5: signed int)
  Name: m

CFA Expected: as GCC

The following cases show where the problem does or does not occur.

In summary, with all cases in discussion being assignment/initialization of a pointer or reference (to an array), C allows these assignments to disregard statically known stride information, in favour of "trust me" runtime stride information, but CFA is finding the types incompatible. The requested assignment is no less sound than any use of C-style "trust me" runtime stride information. CFA's rejection of these cases is not differentiating safer C programs from unsafer C programs.

#ifndef VER
#define VER 1
#endif

#if   VER==1
                            #define RECEIVER_OBJ(x)    float x[rows][cols]
#elif VER==2
                            #define RECEIVER_OBJ(x)    float x[][cols]
#elif VER==3
                            #define RECEIVER_OBJ(x)    float (*x)[cols]
#elif VER==4 && \
      defined(__cforall)
                            #define RECEIVER_OBJ(x)    float (&x)[rows][cols]
#elif VER==5 && \
      defined(__cforall)
                            #define RECEIVER_OBJ(x)    float (&x)[rows][5]
#elif VER==11
                            #define RECEIVER_OBJ(x)    float x[*][*] 
#elif VER==12
                            #define RECEIVER_OBJ(x)    float x[][*]
#elif VER==13
                            #define RECEIVER_OBJ(x)    float (*x)[*]
#elif VER==14 && \
      defined(__cforall)
                            #define RECEIVER_OBJ(x)    float (&x)[*][*]
#elif VER==15 && \
      defined(__cforall)
                            #define RECEIVER_OBJ(x)    float (&x)[*][5]
#elif VER==901
                            #define RECEIVER_OBJ(x)    float x[rows][5] 
#elif VER==991
                            #define RECEIVER_OBJ(x)    float x[*][5] 
#elif VER==902
                            #define RECEIVER_OBJ(x)    float x[][5]
#elif VER==903
                            #define RECEIVER_OBJ(x)    float (*x)[5]
#elif VER==9045 && \
      defined(__cforall)
                            #define RECEIVER_OBJ(x)    float (&x)[4][5] 
#elif VER==9945 && \
      defined(__cforall)
                            #define RECEIVER_OBJ(x)    float (&x)[*][5] 
#else
#error Bad Version
#endif

void f( int rows, int cols, RECEIVER_OBJ() );

void help( int rows, int cols ) {

    float m[4][5];

    f( 4, 5, m );

  #if VER==3 || VER==903 || VER==4 || VER==5 || VER==9045
    RECEIVER_OBJ(x) = m;
    RECEIVER_OBJ(y);
  #endif

  #if VER==3 || VER==903
    y = m;
  #elif VER==4 || VER==5 || VER==9045
    &y = &m;
  #endif
}

Behaviour:

gcc -x c x.cfa -c -DVER=1
gcc -x c x.cfa -c -DVER=2
gcc -x c x.cfa -c -DVER=3
gcc -x c x.cfa -c -DVER=11
gcc -x c x.cfa -c -DVER=12
gcc -x c x.cfa -c -DVER=13
gcc -x c x.cfa -c -DVER=901
gcc -x c x.cfa -c -DVER=991
gcc -x c x.cfa -c -DVER=902
gcc -x c x.cfa -c -DVER=903

Actual and Authority: All succeed

cfa x.cfa -c -DVER=1
cfa x.cfa -c -DVER=2
cfa x.cfa -c -DVER=3
cfa x.cfa -c -DVER=4
cfa x.cfa -c -DVER=5
cfa x.cfa -c -DVER=11
cfa x.cfa -c -DVER=12
cfa x.cfa -c -DVER=13
cfa x.cfa -c -DVER=14
cfa x.cfa -c -DVER=15
}}
Actual: All fail, each with at least one no reasonable alternatives error similar to intro case CFA actual.
Expected: All succeed, as for GCC

{{{
cfa x.cfa -c -DVER=901
cfa x.cfa -c -DVER=991
cfa x.cfa -c -DVER=902
cfa x.cfa -c -DVER=903
cfa x.cfa -c -DVER=9045
cfa x.cfa -c -DVER=9945
}}}
Actual and Expected: All succeed

White-box investigation has found:

Within AlternativeFinder's makeFunctionAlternatives, the unify call is rejecting the assignment.

Unify_old::postvisit(ArrayType *) is making that judgment, requiring "array types must both be VLA or both not VLA."

Yet in this case, C allows a pointer to non-VLA argument to be passed for a pointer to a VLA parameter.

Note the judgment at issue is the same as is troubling ticket #175:
 - GenPoly::typesCompatible ... case for ArrayType
 - Unify_old::postvisit(ArrayType *)