Inefficient bitvector codegen when used in option & compiler bug?

[Timmmm]

If you have the type option(bits(32)) you might expect something like this:

enum kind_zoptionzIbzK { Kind_zNonezIbzK, Kind_zSomezIbzK };

struct zoptionzIbzK {
  enum kind_zoptionzIbzK kind;
  union {
    struct { unit zNonezIbzK; };
    struct { fbits zSomezIbzK; };
  };
};

but I actually found it uses lbits instead of fbits. Presumably it is choosing to merge all the option(bits(N)) rather than monomorphise them?

Additionally, I was going to investigate with this incomplete test program:

default Order dec

$include <prelude.sail>
$include <string.sail>
$include <mapping.sail>

overload operator ^ = {concat_str}

let x : option(bits(32)) = None()
let y : option(bits(128)) = None()

function main() -> unit = {
    match x {
      Some(x) => print_endline("x is " ^ bits_str(x)),
      _ => (),
    };
}

but it seems to generate invalid C? I get these errors:

/home/codasip.com/timothy.hutt/workspace/sail/_build/default/lib/sail.h:107:22: warning: implicit declaration of function ‘create_zoption’; did you mean ‘create_zexception’? [-Wimplicit-function-declaration]
 #define CREATE(type) create_ ## type
                      ^~~~~~~
model.c:151:41: note: in expansion of macro ‘CREATE’
 static void create_letbind_0(void) {    CREATE(zoption)(&zx);
                                         ^~~~~~
model.c:157:22: warning: passing argument 1 of ‘copy_zoptionzIbzK’ from incompatible pointer type [-Wincompatible-pointer-types]
   COPY(zoptionzIbzK)(&zx, zgsz30);
                      ^~~
model.c:36:53: note: expected ‘struct zoptionzIbzK *’ but argument is of type ‘struct zoption *’
 static void COPY(zoptionzIbzK)(struct zoptionzIbzK *rop, struct zoptionzIbzK op)
                                ~~~~~~~~~~~~~~~~~~~~~^~~
In file included from model.c:1:
model.c: In function ‘kill_letbind_0’:
/home/codasip.com/timothy.hutt/workspace/sail/_build/default/lib/sail.h:113:20: warning: implicit declaration of function ‘kill_zoption’; did you mean ‘kill_zexception’? [-Wimplicit-function-declaration]
 #define KILL(type) kill_ ## type
                    ^~~~~
model.c:161:39: note: in expansion of macro ‘KILL’
 static void kill_letbind_0(void) {    KILL(zoption)(&zx);
                                       ^~~~
model.c: In function ‘create_letbind_1’:
model.c:171:22: warning: passing argument 1 of ‘copy_zoptionzIbzK’ from incompatible pointer type [-Wincompatible-pointer-types]
   COPY(zoptionzIbzK)(&zy, zgsz31);
                      ^~~
model.c:36:53: note: expected ‘struct zoptionzIbzK *’ but argument is of type ‘struct zoption *’
 static void COPY(zoptionzIbzK)(struct zoptionzIbzK *rop, struct zoptionzIbzK op)
                                ~~~~~~~~~~~~~~~~~~~~~^~~
model.c: In function ‘zmain’:
model.c:188:11: error: invalid use of undefined type ‘struct zoption’
     if (zx.kind != Kind_zSomezIbzK) goto case_4;
           ^
model.c:190:46: error: invalid use of undefined type ‘struct zoption’
     zxshadowz30 = CONVERT_OF(fbits, lbits)(zx.zSomezIbzK, true);
                                              ^
model.c: At top level:
model.c:150:16: error: storage size of ‘zx’ isn’t known
 struct zoption zx;
                ^~
model.c:164:16: error: storage size of ‘zy’ isn’t known
 struct zoption zy;

[Alasdair]

Bug should be fixed now.

When it comes to polymorphic types, we always represent them in their most general form. This is because (for example) a function could create an option(bits(32)), then pass it to a function forall 'n, 'n > 0. option(bits('n)) -> unit, which could store it into a register and so on. So in order to make sure the types always line up in these various places, we have to choose a representation that works in all these places.

[Timmmm]

Ah that makes sense. I guess you could fully monomorphise everything but I think the "small bitvector optimisation" is probably a more reasonable solution. Thanks for the bug fix!