Allow vla in cil result

[michael-schwarz]

Resolves #5.
Needs to be merged at the same time as https://github.com/goblint/analyzer/tree/allow_vla_in_cil_result is merged into Goblint master.

[michael-schwarz]

Printing CILs internal representation into C again requires some more work

int main(void) {
    int n = 20;
    int d[n][n];

    if(n<20) {
        d[0][0] = 7;
    }

    return 0;
}

is turned into

int main(void) 
{ 
  int n;
 
  {
    {
#line 2
    n = 20;
#line 3
    int d[n][n];
    }

#line 5
    if (n < 20) {
        {
#line 6
        d[0][0] = 7;
        }
    }
#line 8
    return (0);
  }
}

which won't compile because d is out of scope in line 6 where it is used. 😞

[michael-schwarz]

Turns out this is not a CIL problem (it works in CIL) but a result of the allBBVisitor https://github.com/goblint/analyzer/blob/c74ebb1577c58ad70f4863fe431c53a6a934533a/src/util/cilfacade.ml#L38
that runs before dumping CIL if Goblint is run with --enable justcil

[vogler]

Printing CILs internal representation into C again requires some more work

int main(void) {
    int n = 20;
    int d[n][n];

    if(n<20) {
        d[0][0] = 7;
    }

    return 0;
}

is turned into

int main(void) 
{ 
  int n;
 
  {
    {
#line 2
    n = 20;
#line 3
    int d[n][n];
    }

#line 5
    if (n < 20) {
        {
#line 6
        d[0][0] = 7;
        }
    }
#line 8
    return (0);
  }
}

which won't compile because d is out of scope in line 6 where it is used. 😞

It assumes that instructions can't be declarations.
// In stmtkind, only Instr is guaranteed to have no control flow, Block might.

[vogler]

vla-multi.c:

#include <stdlib.h>

int f(int i, int n, int m, int a[n][m]) {
  return a[i][2*i];
}

// how to encode multi-dimensional VLAs with alloca?
int main(int argc, char** argv) {
  int l = argc;
  int x;
  if (l==1) {
    // normal two-dimensional array, VLA: 5 and 6 might be variables
    // -> solution: add a constructor to Cil.instr for (VLA-)declarations?
    int a[5][6];
    a[1][2] = 42;
    x = a[1][2];
    x = f(1, 5, 6, a);
    return x;
  } else if (l==2) {
    // pointer to 2nd arrays, problem is that 6 might still be a variable
    // -> not a solution for VLAs
    int (*a)[6];
    a = alloca(sizeof(int [6]) * 5);
    a[1][2] = 42;
    x = a[1][2];
    x = f(1, 5, 6, a);
    return x;
  } else {
    // pointer to int
    // -> works but needs a lot of instrumentation
    int* a;
    // sizes we need to move the pointer by where size_1 is for the first index, _2 for the second. need to save them into temp. variables because the value of the original expression can change (and also to trigger possible side-effects at the location of the declaration).
    size_t a_size_2 = sizeof(int);
    size_t a_size_1 = 6 * a_size_2;
    a = alloca(5 * a_size_1);
    // a[1][2] = 42; // this needs to go to a + 1*6 + 2
    *(a + 1*a_size_1 + 2*a_size_2) = 42;
    x = *(a + 1*a_size_1 + 2*a_size_2);
    // x = f(1, 5, 6, a); // incompatible pointer types passing 'int **' to parameter of type 'int (*)[*]' [-Wincompatible-pointer-types]
    // we can only cast to a pointer to an array
    x = f(1, 5, 6, (int (*)[6]) a);
    return x;
  }
}

[vogler]

Summary (cf. #7 (comment)):

• Cil.instr += VarDecl
• Goblint:
  • MyCFG.edge += VDecl
  • Analyses.Spec.vdecl only overwritten in Base

Currently only used for VLAs, but could be used for any declaration, which has the advantage that the state would only contain variables that have already been declared so far. OTOH one should then introduce a dual transfer function for when a variable goes out of scope. Cil's renaming would probably have to be kept in case of shadowing.

[vogler]

File "src/ext/ccl/ccl.ml", line 1366, characters 11-9715:
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- VarDecl (_, _)
File "src/ext/llvm/llvmgen.ml", line 897, characters 48-589:
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- VarDecl (_, _)
File "src/ext/pta/ptranal.ml", line 271, characters 2-1266:
- Warning 8: this pattern-matching is not exhaustive.
- Here is an example of a case that is not matched:
- VarDecl (_, _)

[vogler]

Also, all osx builds are failing (probably unrelated): https://travis-ci.com/goblint/cil/builds/134384476