Major regression in compile time due to improved error messages

[Timmmm]

For some reason this commit makes compile time for the RISC-V Sail model much much worse, but annoyingly only for our fork. I couldn't reproduce the issue in the open source one.

On the previous commit:

        User time (seconds): 8.36
        System time (seconds): 0.44
        Percent of CPU this job got: 99%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 0:08.84
        Maximum resident set size (kbytes): 460992

On that commit:

        User time (seconds): 2133.44
        System time (seconds): 0.15
        Percent of CPU this job got: 99%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 35:36.99
        Maximum resident set size (kbytes): 126832

Actually I killed it after 35 minutes.

Kind of annoying I don't have a public reproducer but maybe you have some clue? Or a suggestion for how to debug it? Does an OCaml profiler exist?

[Timmmm]

Oh also, it compiles without errors, so it seems a little weird that changing error message handling would affect anything. Unless the changes in that commit also affect warnings somehow?

[Timmmm]

Ah I found opt_tc_debug which gave me the culprit (I think) straight away! And also explained why we don't see it in the open source one. A lot of the CHERI functions seem to trigger huge explosions in the opt_tc_debug output trees.

One in particular is really bad - capToString():

function capToString(cap : Capability) -> string = {
  let len = getCapLength(cap);
  let len_str = BitStr(to_bits(cap_len_width + 3, len));
  let perms = arch_perms_decode(cap.arch_perms);
  "t:" ^ (if cap.tag then "1" else "0") ^
  " perms:" ^
    (if perms[R] == 0b1 then "R" else "") ^
    (if perms[W] == 0b1 then "W" else "") ^
    (if perms[C] == 0b1 then "C" else "") ^
    (if perms[X] == 0b1 then "X" else "") ^
    (if perms[ASR] == 0b1 then "Asr" else "") ^
  " sealed:" ^ (if cap.sealed then "1" else "0") ^
  " address:" ^ BitStr(cap.address) ^
  " base:" ^ BitStr(getCapBaseBits(cap)) ^
  " top:" ^ BitStr(getCapTopBits(cap)) ^
  " length:" ^ len_str
}

I guess maybe it's the worst because it calls all the other complicated capability functions (e.g. getCapTopBits())?

Anyway the output looks like this:

I killed it after 500k lines of output without finishing that function.

Also if I change this line in type_check.ml

  | exception Unification_error (l, m) -> Error (l, 1, Err_function_arg (exp_loc arg, typ, Err_other m))

Back to

  | exception Unification_error (l, m) -> typ_error l m

then it's fine again. I guess this is an early exit from the explosion...

[Alasdair]

Yes, I see why. I made it continue checking for what I thought would only be a little bit after the first error on a function application to see how many subsequent errors that causes, but the nested ^ applications there are a worst-case scenario for that kind of exploration

[Alasdair]

Might be fixed by #526

It's trying to tackle the root cause of why overloaded definitions are slow to typecheck, rather than specifically this error, but it should mean the string literals in this example immediately collapse the state space of what the type-checker can try.

[Alasdair]

The above PR brings make -B csim (which includes all the C compilation) from 55s to 37s for me, so it seems like a fairly significant improvement.

[Timmmm]

I tried on the latest sail2 and it's fast again, thanks! Not any faster than before, but it's pretty fast anyway (9s for the Sail compilation).