CN: Declare n-ary tuple on demand rather than encoding a fixed limit

[lwli11]

This code causes a crash:

typedef struct {
        int id;
} x_t;
typedef struct {
   x_t* a;
   x_t* b;
   x_t* c;
   x_t* d;
  x_t* e;
   x_t* f;
   x_t* g;
   x_t* h;
   x_t* i;
   x_t* j;
   x_t* k;
   x_t* l;
   x_t* m;
   x_t* v;
} st_t;

extern st_t* init_st();
/*@
        spec init_st();
        requires true;
        ensures take x = Owned<st_t>(return);
      take a0 = Owned<x_t>(x.a);
        take b0 = Owned<x_t>(x.b);
        take c0 = Owned<x_t>(x.c);
        take d0 = Owned<x_t>(x.d);
        take e0 = Owned<x_t>(x.e);
        take f0 = Owned<x_t>(x.f);
        take g0 = Owned<x_t>(x.g);
       take h0 = Owned<x_t>(x.h);
        take i0 = Owned<x_t>(x.i);
        take j0 = Owned<x_t>(x.j);
        take k0 = Owned<x_t>(x.k);
        take l0 = Owned<x_t>(x.l);
        take m0=Owned<x_t>(x.m);
        take v0=Owned<x_t>(x.v);
@*/

st_t* test()
/*@
        ensures take x = Owned<st_t>(return);
@*/
{
        st_t* s = init_st();
        return s;
}

cn: internal error, uncaught exception:
    File "backend/cn/lib/solver.ml", line 235, characters 4-10: Assertion failed
    Raised at Cn__Solver.CN_Tuple.name in file "backend/cn/lib/solver.ml", line 235, characters 4-31
    Called from Cn__Solver.CN_Tuple.t in file "backend/cn/lib/solver.ml", line 247, characters 13-25
    Called from Cn__Solver.translate_var in file "backend/cn/lib/solver.ml", line 684, characters 37-61
    Called from Cn__Solver.translate_term in file "backend/cn/lib/solver.ml", line 919, characters 41-62
    Called from Cn__Solver.translate_term in file "backend/cn/lib/solver.ml", line 961, characters 63-85
    Called from Cn__Solver.add_assumption in file "backend/cn/lib/solver.ml", line 1105, characters 46-68
    Called from Cn__Typing.add_c_internal in file "backend/cn/lib/typing.ml", line 410, characters 11-51
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.sandbox in file "backend/cn/lib/typing.ml", line 86, characters 10-13
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.run_from_pause in file "backend/cn/lib/typing.ml", line 68, characters 50-55
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 163, characters 6-454
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 182, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

while this does not:

typedef struct {
        int id;
} x_t;
typedef struct {
   x_t* a;
   x_t* b;
   x_t* c;
   x_t* d;
  x_t* e;
   x_t* f;
   x_t* g;
   x_t* h;
   x_t* i;
   x_t* j;
   x_t* k;
   x_t* l;
   x_t* m;
   x_t* v;
} st_t;

extern st_t* init_st();
/*@
        spec init_st();
        requires true;
        ensures take x = Owned<st_t>(return);
      take a0 = Owned<x_t>(x.a);
        take b0 = Owned<x_t>(x.b);
        take c0 = Owned<x_t>(x.c);
        take d0 = Owned<x_t>(x.d);
        take e0 = Owned<x_t>(x.e);
        take f0 = Owned<x_t>(x.f);
        take g0 = Owned<x_t>(x.g);
       take h0 = Owned<x_t>(x.h);
        take i0 = Owned<x_t>(x.i);
        take j0 = Owned<x_t>(x.j);
        take k0 = Owned<x_t>(x.k);
        take l0 = Owned<x_t>(x.l);
        take m0=Owned<x_t>(x.m);
//      take v0=Owned<x_t>(x.v);
@*/

st_t* test()
/*@
        ensures take x = Owned<st_t>(return);
@*/
{
        st_t* s = init_st();
        return s;
}

The only change I can see is one less take statement, and changing from v to n doesn't make a difference so it's not the variable name itself.

[septract]

This is caused by the following code in backend/cn/lib/solver.ml (line 235):

module CN_Tuple = struct
  let max_arity = 15

  let name arity =
    assert (arity <= max_arity);
    "cn_tuple_" ^ string_of_int arity
  ... 

The origin commit is 0ab06e0 by @dc-mak.

@dc-mak @yav is there a reason for this to be hard-coded to 15?

[yav]

There are no arbitrary sized tuples in SMT-LIB, so we pre-define a bunch of tuples up to a size. The size is arbitrary, so we can easily make it bigger, but that might have some performance implications, as we define these every time we start a solver.

Another option would be to keep track in the type checker of what sized tuples actually appear in the code and only declare those. I think @cp526 said that this shouldn't be too hard to do.

EDIT: we could do this either before calling into the solver, or we could modify the solver to declare things on demand as it encounters them. Doing it ahead of time might be better because then we could declare the tuples once at the start. If we do it on demand in the solver, we may have to declare them multiple types, depending on which scope they end up being declared in. This is because the solver is encremental, and we push/pop scopes of assertions. So if we enter a scope, declare a tuple, then exit it, we'd need to re-declare it again when we leave the scope. The solver already has stuff to keep track of these sorts of changes, so it shouldn't be too hard to do there either.

[septract]

It seems cleaner to declare on-demand since this doesn't require some arbitrary limit, and also doesn't require any fancy inference to figure out what sizes to declare. Or declare 8 by default, and then on-demand.