Checker.ml raises error for empty EBufCreateL in [infer'] but not in [check']

[Lin23299]

In Checker.ml, it raises an error for empty EBufCreateL in infer' :

  | EBufCreateL (_, es) ->
      begin match es with
      | [] ->
          checker_error env "%a, there is an empty buf create sequence" ploc env.location
      | first :: others ->
          let t = infer env first in
          List.iter (check env t) others;
          TArray (t, (K.UInt32, string_of_int (List.length es)))
      end

While it is allowed in check':

| EBufCreateL (_, es) ->
      let t, _ = assert_buffer env t in
      List.iter (check env t) es

I wonder whether there is a reason for this design? Twic, I am trying to translate [T;N] to arr{T data[N];} in eurydice and this checker fails the check on the argument:

&({ data = stack newbuf {  }; }: arr)

while

stack newbuf {  }

is allowed.

[msprotz]

Ok this is an implementation mistake. The intent is to prevent zero-sized stack allocations which are undefined behavior in C. Concretely, this is a GNU extension and not standard C:

void f() {
  int x[0];
}

The two frontends to krml are Low* (which now forbids zero-sized stack allocations by construction) and Rust (which does allow zero-sized stack allocations).

In that case, maybe Krml's checker should just ignore the problem, and Eurydice should feature a pass that eliminates zero-sized arrays in favor of something else? What do you think?

[Lin23299]

Thanks for the reply! I agree that eliminating zero-sized array in Eurydice is reasonable.

I'm not sure whether you want to keep this issue for the "implementation mistake". So please feel free to close it.

[msprotz]

Yes we should keep this issue open and I think you should disable the warning if you can, because you're going to trigger it from Eurydice, aren't you?

[Lin23299]

Yes, I think I will try to eliminate such case in Eurydice. Maybe after dealing with type-ploymorphic definition and possibly other issues.