Big compile time regression with new bitfield syntax

[Timmmm]

Using the new [foo with a=b] bitfield syntax instead of update_a(foo, b) seems to cause a crazy regression in compile time,

This is possibly the cause of https://github.com/riscv/sail-riscv/issues/323 though I haven't checked the vector code to see if it actually does this yet.

Old syntax, Sail:
real    0m0.097s
user    0m0.076s
sys     0m0.012s

Old syntax, GCC:
real    0m0.371s
user    0m0.317s
sys     0m0.043s

New syntax, Sail:
real    0m40.968s
user    0m40.473s
sys     0m0.270s

New syntax: GCC:
real    0m0.427s
user    0m0.347s
sys     0m0.049s

Actually it didn't seem to affect the C compilation time much which is a bit different to the vector issue. Anyway something is up!

Here's my test case:

default Order dec

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

overload operator ^ = {concat_str}

val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
val zero_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)

function sign_extend(m, v) = sail_sign_extend(v, m)
function zero_extend(m, v) = sail_zero_extend(v, m)

val zeros : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
function zeros (n) = sail_zeros (n)

val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
function ones (n) = sail_ones (n)

bitfield Dcsr : bits(32) = {
  DEBUGVER : 31 .. 28,
  EBREAKVS : 17,
  EBREAKVU : 16,
  EBREAKM : 15,
  EBREAKS : 13,
  EBREAKU : 12,
  STEPIE : 11,
  STOPCOUNT : 10,
  STOPTIME : 9,
  CAUSE : 8 .. 6,
  V : 5,
  MPRVEN : 4,
  NMIP : 3,
  STEP : 2,
  PRV : 1 .. 0
}

function legalize_dcsr(o : Dcsr, v : bits(32)) -> Dcsr = {
  let v = Mk_Dcsr([v with 27 .. 18 = zeros()]);
  [
    v with
    DEBUGVER = (zeros()),
    EBREAKVS = (if true then v[EBREAKVS] else 0b0),
    EBREAKVU = (if true then v[EBREAKVU] else 0b0),
    EBREAKS = (if true  then v[EBREAKS] else 0b0),
    EBREAKU = (if true  then v[EBREAKU] else 0b0),
    STEPIE = (if true then v[STEPIE] else 0b0),
    STOPCOUNT = (if true then v[STOPCOUNT] else zeros()),
    STOPTIME = (if true then v[STOPTIME] else zeros()),
    CAUSE = (v[CAUSE]),
    V = (if true then v[V] else 0b0),
    MPRVEN = (if true then v[MPRVEN] else zeros()),
    NMIP = (v[NMIP])
  ]
}

// function legalize_dcsr(o : Dcsr, v : bits(32)) -> Dcsr = {
//   let v  = [v with 27 .. 18 = zeros()];
//   let v : Dcsr = Mk_Dcsr(v);
//   let v = update_DEBUGVER(v, zeros());
//   let v = update_EBREAKVS(v, if true then v[EBREAKVS] else 0b0);
//   let v = update_EBREAKVU(v, if true then v[EBREAKVU] else 0b0);
//   let v = update_EBREAKS(v, if true  then v[EBREAKS] else 0b0);
//   let v = update_EBREAKU(v, if true  then v[EBREAKU] else 0b0);
//   let v = update_STEPIE(v, if true then v[STEPIE] else 0b0);
//   let v = update_STOPCOUNT(v, if true then v[STOPCOUNT] else zeros());
//   let v = update_STOPTIME(v, if true then v[STOPTIME] else zeros());
//   let v = update_CAUSE(v, v[CAUSE]);
//   let v = update_V(v, if true then v[V] else 0b0);
//   let v = update_MPRVEN(v, if true then v[MPRVEN] else zeros());
//   let v = update_NMIP(v, v[NMIP]);
//   v
// }

function main() -> unit = ()

Comment out one of the function versions as appropriate, then compile with:

SAIL_LIB=$(sail -dir)
time sail test.sail -c -o model --c-preserve legalize_dcsr
time cc model.c -o model -O -I "$SAIL_LIB/lib" $SAIL_LIB/lib/*.c -lgmp -lz

I had a look at the generated C. The new syntax seems to get a load of nested structs:

Another thing I noticed is that if you make a mistake, like:

 let v = update_DEBUGVER(v, sdkljghdfkjgh());

Then the old syntax gives this immediately:

Type error:
test.sail:60.10-45:
60 |  let v = update_DEBUGVER(v, sdkljghdfkjgh());
   |          ^---------------------------------^
   | No overloading for update_DEBUGVER, tried:
   | * _update_Dcsr_DEBUGVER
   |    No function type found for sdkljghdfkjgh

real    0m0.076s
user    0m0.067s
sys     0m0.008s

With the new syntax it takes 46s and the error message is 165 MB! I think that might be a personal record. It starts like this:

Type error:
test.sail:40.2-54.3:
40 |  [
   |  ^
54 |  ]
   |--^
   | No overloading for vector_update, tried:
   | * bitvector_update
   |    No overloading for vector_update, tried:
   |    * bitvector_update
   |       No overloading for vector_update, tried:
   |       * bitvector_update
   |          No overloading for vector_update, tried:
   |          * bitvector_update
   |             No overloading for vector_update, tried:
   |             * bitvector_update
   |                No overloading for vector_update, tried:
   |                * bitvector_update
   |                   No overloading for vector_update, tried:
   |                   * bitvector_update
   |                      No overloading for vector_update, tried:
   |                      * bitvector_update
   |                         No overloading for vector_update, tried:
   |                         * bitvector_update
   |                            No overloading for vector_update, tried:
   |                            * bitvector_update
   |                               No overloading for vector_update, tried:
   |                               * bitvector_update
   |                                  No overloading for vector_update, tried:
   |                                  * bitvector_update
   |                                     Could not unify bitvector('n) and Dcsr
   |                                  * plain_vector_update
   |                                     Could not unify vector('n, 'a) and Dcsr
   |                                  
   |                                  Caused by test.sail:42.16-29:
   |                                  42 |    DEBUGVER = (sdkljghdfkjgh()),
   |                                     |                ^-----------^
   |    | No function type found for sdkljghdfkjgh
   |                               * plain_vector_update
   |                                  No overloading for vector_update, tried:
   |                                  * bitvector_update
   |                                     Could not unify bitvector('n) and Dcsr
   |                                  * plain_vector_update
   |                                     Could not unify vector('n, 'a) and Dcsr
   |                                  
   |                                  Caused by test.sail:42.16-29:
   |                                  42 |    DEBUGVER = (sdkljghdfkjgh()),
   |                                     |                ^-----------^

[Alasdair]

If you write it in the same way with the intermediate variables, i.e:

function legalize_dcsr(o : Dcsr, v : bits(32)) -> Dcsr = {
    let v  = [v with 27 .. 18 = zeros()];
    let v : Dcsr = Mk_Dcsr(v);
    let v = [v with DEBUGVER = zeros()];
    ...
}

that should work around the issue.

[v with X = a, Y = b, Z = c] is being de-sugared into [[v with X = a] with Y = b] with Z = c], which is causing the nesting you see in the output (but it should be harmless in the C output it's just extra braces). When the error occurs it starts backtracking trying to find an alternate interpretation of the syntax that could work (by treating v as a bitvector variable and X, Y, Z as expressions with integer values, and it'll go through all possible combinations).

You could get a similar issue if you nested update_Z(update_Y(update_X(v, a), b), c), although it would be a little harder to trigger as it would require multiple bitfields with the same field names.

[Timmmm]

by treating v as a bitvector variable

Doesn't it already know the type of v at this point though? Or is it just trying to say "btw this would work if v was a bitvector"?

Also that explains the slow compilation when there's an error, but what about when it compiles successfully?

Do you think this will be easy to fix or should I just go ahead and rewrite all the code?

[Alasdair]

I think this should fix it: https://github.com/rems-project/sail/commit/5929b9b958a2a2c614782e5d211556fef383cfa5

[Timmmm]

That was fast! And it works perfectly. Compile time back to normal :tada:

It didn't affect my Vector compile time issue unfortunately but I guess that's not surprising since that's a C issue, and after looking briefly it doesn't seem like Vector used this syntax anyway. I'm still working on narrowing that down.

Thank you!!