risc-v/boot: verbosely log boot errors

[axel-h]

Log an explicit error message for everything that can fail during boot. This is helpful for debugging, e.g. when porting the kernel to a new platform or changing the system configuration.

[axel-h]

The preprocess test fail because of the printf call that this patch adds.

[lsf37]

These look good from my side.

Should not affect the proofs since it's all boot code, but let me start a testboard just to make sure.

[lsf37]

@ssrg-bamboo proof

[nomadeel]

@ssrg-bamboo proof

[ssrg-bamboo]

Hello, I'm a bot! I've set up a proof testboard for this PR here, and results should show up as pending in status checks in a few minutes.

[nomadeel]

I guess the bot didn't receive the first message as a notification.

[axel-h]

Can I merge this now or is there another manual step needed to update the preprocess templates?

[mbrcknl]

Can I merge this now or is there another manual step needed to update the preprocess templates?

A preprocess test failure just compares this pull request with the current head to determine whether this PR potentially impacts the proofs. Once you merge this, it's the new head, so it will be the basis for future preprocess tests.

TL;DR: no need to do anything to update the preprocess check. We just need a reasonable level of confidence this won't break the proofs. And I'm reasonably confident of that.

Not sure what's going on with the simulation tests, though. I guess most are timeouts? Except maybe clang armv6a, which seems unrelated to this PR.

[lsf37]

Let me re-run the simulations. Only armv6a seems to have actually failed, the others were cancelled because of that failure. There is one test in the test set that is dodgy on GH (see #seL4/ci-actions#112).

[lsf37]

To add on to Matt's explanation: it's Ok to merge it, i.e. no other prework or preconditions, but there is an extra step afterwards (which we can do, but you also have sufficient access to run the script if you want -- usually a verification person should be involved in that, but Matt already gave his Ok).

Basically, the preprocess-base is the last known-good version that has a proof, and that only bumps automatically to other preprocess-equal versions or if we explicitly tell it to.

That latter part is the "preprocess bump" script that people might have mentioned before. It lives in https://github.com/seL4/l4v/tree/master/misc/bump together with a bit more explanation.

[lsf37]

Ok, all simulation runs successful now. It does look like that failure is not that rare and we should do something about it.

[lsf37]

(preprocess bump done as well)