[BI] Replace panics with error messages, update Runt output

[ngernest]

Note: this PR should be reviewed before #287. #287 removes the monitor and integrates BI with the testing infrastructure, but CI currently fails on #287 due to BI panics on certain test cases. This PR (#289) fixes these issues, and once this branch is merged into #287's branch, CI should pass.

This PR replaces certain panics in the BI (e.g. encountered fork before a step) into dedicated error messages, per Kevin's comment here:

We should handle this in a different way. Probably instead of panicing we would like to exit more cleanly in the error case.

This involved adding a new FailureKind type to the BI diagnostics and updating the error message infrastructure -- Runt expect test outputs have also been updated.

Note that previously, when the BI panicked (e.g. an execution path reached the encountered fork before a step panic), the entire BI executable would terminate. Now though, this is represented as a Failure in the BI (it is still displayed), but if there are other execution paths that succeed, the BI displays the inferred transactions on those execution paths instead.

This is why certain expect test outputs (e.g. push_pop_loop_not_empty.bi.expect‎) now contain inferred transaction traces instead of just the panic error message. For example, for nested_busy_wait, this is the .tx file supplied to the interpreter:

trace {
    reset();
    push_n_times(7, 3);
    pop_n_times(7, 2);
    check_not_empty();          // FIFO is non-empty (has one element remaining)
}

The BI now infers the following:

// trace 0
trace {
    reset();
    push_n_times(7, 1);
    push_n_times(7, 2);
    pop_n_times(7, 2);
    check_not_empty();
}

// trace 1
trace {
    reset();
    push_n_times(7, 1);
    push_n_times(7, 2);
    pop_n_times(7, 1);
    pop_n_times(7, 1);
    check_not_empty();
}

...
// Different combinations of `push_n_times` & `pop_n_times` such that the no. of `repeat` loop iterations 
// adds up to 4 for each of them

This PR also changes the Only nano seconds are supported panic to an error message to make the expect test output more consistent, as the default output for panic error messages displays the OS thread ID of the running executable, which changes every time the executable is run.

Finally, for two test cases where the BI infers many traces (nested_busy_wait and push_pop_loop_empty), I have edited the Runt config to pass in the CLI argument --max-traces 20 for these two specific test cases (to avoid the .expect test file from being too long).

[ekiwi]

this is good

[ekiwi]

good

[ekiwi]

I would prefer for the error message to stay here and not to move it into a separate method.
The reason is that I would like to separate presentation and representation. I.e., proto_trace.rs should only care about conveying all the info, not how it gets presented to the user.

[ngernest]

Ah I see, that makes sense!

[ekiwi]

Let's keep the exact error messages local to where the get emitted.

[ekiwi]

great!

[ekiwi]

Unfortunately, this does not work.

There are two different kinds of “failures” here:

1. The protocol execution just does not match the given trace; that is what the bi uses the self.failures for. In this case, we keep on exploring other execution paths to see if we can find a matching one.
2. The protocol is malformed. That is what the bi currently handles with panics/assertion failures. In that case the whole execution should be stopped and no traces should be printed. In the short term, I would prefer to only test the bi on legal protocols and punt handling ill-formed protocols in a nicer way until later.

[ngernest]

Makes sense, thanks! For nested_busy_wait.prot specifically, I think the protocol (shown below) is malformed, because when outer_iters = 0 and inner_iters = 0, we skip both repeat loops, but then we have a fork() before any step()s have been called.

prot nested_busy_wait<DUT: Adder>(a: u32, b: u32, outer_iters: uint, inner_iters: uint, s: u32) {
  DUT.a := a;
  DUT.b := b;
  repeat outer_iters iterations {
    repeat inner_iters iterations {
      step();
      assert_eq(s, DUT.s);
    }
    step();
    assert_eq(s, DUT.s);
  }
  DUT.a := X;
  DUT.b := X;
  assert_eq(s, DUT.s);
  fork();
  step();
}

And in this case, following (2), we should have bi terminate (with an error message instead of a panic). If its okay, I can get rid of the FailureKind enum and just make the bi exit with an error message (e.g. using std::process::exit).

[ekiwi]

That would be a better solution, but - imho - the best solution is to just delete these .prot files. If you want to, you could open an issue as a reminder to revisit this problem of repeat loops that are taken zero times. But for now I would rather not have to think about dealing with broken protocols.

[ngernest]

Makes sense -- I looked at all the files where the bi (on main) emits the cannot fork at step zero panic and it looks like all of them suffer from the same "repeat loops taken zero times" issue ({push_pop_loop_empty, push_pop_loop_not_empty, busy_wait, nested_busy_wait, loop_with_assigns}.prot), so I'll just delete these files (& their associated .expect tests) for now.

[ekiwi]

Thanks!