Wasm-DSL / spectec

Wasm SpecTec specification tools
https://wasm-dsl.github.io/spectec/
Other
25 stars 8 forks source link

[backend-prose/interpreter] Error messages from backends #73

Open rossberg opened 4 months ago

rossberg commented 4 months ago

When recently changing some of the AST syntax in the specs, I ran into various errors from the backends. They mostly just consisted of uncaught exceptions.

A dual problem was that some restrictions/assumptions were not checked, but simply lead to less than useful output, with no indication of why.

Since the backends are naturally more specialised and hence more restrictive than the frontend or IL validation, this is a user-facing issue. Consequently, backends need to

  1. check all assumptions they make about the input, and fail visibly for cases they cannot handle correctly,

  2. produce useful error messages for cases they cannot handle, including line information, ideally using the Source.error infrastructure.

presenthee commented 3 months ago

86 made changes to error messages in backend-interpreter and backend-prose. Should we close the issue or is further improvement needed?

rossberg commented 3 months ago

I suspect there are still some left. For example, last week I changed the names of some context and store elements, and all I got from the interpreter were plenty of Not_found exceptions. I had to print stack traces to figure out what's going on and where they were coming from. I eventually tracked it down to Ds.lookup_env, which just side-prints a message to stderr, without position information, and that output is swallowed by the test runner.

Unfortunately, OCaml does not yet have an effect system to track down all the functions that could throw, but would it be possible to somehow go through the code and vet all uses of try, throw, and print, and thus find at least all exceptions and messages originating from the backends themselves?

presenthee commented 3 months ago

Understood. It seems that an error thrown by the interpreter is caught by the runner again. I'll fix it first. Besides, as you mentioned, we need manual inspection. I could list all exceptions and messages in backend-interpreter and il2al (because they seem to be the most problematic part) in a document as we did for prose diff. Does it sound ok?

rossberg commented 3 months ago

Thanks!

At first I thought a doc would be overkill, but thinking again, it could actually be useful, because from that we could also derive documentation about the constraints/assumptions imposed by backends (plus instructions about what needs changing when such an assumption needs to be modified).

Essentially, every error detected by a backend ought to be in one of two possible categories:

  1. It can arise for user input that is valid according to the frontend. Then this should raise a Source.Error exception with position information and a message comprehensible to end users.

  2. It should never occur on valid input. Then it probably should be an assertion.

As a result, there should not be any other way in which errors are reported to the end user than through raising Source.Error.

I think we only need to collect those from the first category in the doc (or ones for which it is not obvious).