[Re-opening] Improve error recoverability in `ToIrListener` #1228

bugarela · 2023-10-20T18:36:31Z

new PR for #1223 (which I messed up with a local merge that ruined it forever) - please see that PR's description to understand the changes on this PR.

Also added some further improvements on diagnostics and error reporting, as I experienced some crashing behavior on manual tests last week.

…ing-error-recovery-2

shonfeder

I have a few questions and minor suggestions.

The only blocking change request in my mind is the exception handling I noted.

shonfeder · 2023-11-01T13:37:51Z

quint/src/parsing/ToIrListener.ts

+      // another, so it's better not to hide this completely. We should turn this
+      // back into `assert`s after we feel more confident about it.
+      console.log(
+        'ATTENTION: There is some component(s) left on the stack(s) after parsing a module, please report a bug'


If we are asking for a bug report, I think this should just be an error-level message? WDYT?

shonfeder · 2023-11-01T13:44:33Z

quint/src/parsing/ToIrListener.ts

+    if (def.kind !== 'def') {
+      // only `QuintDef` is allowed in `nondet` expressions
+      return
+    }


Given the comment, should this be an error?

This is already ensured by the parser, so we must already have gathered an error for this that will be reported later.

Sorry if I'm being a bit dense, but if this is ensured by the parser, then should this not be just an assert? Or are you saying that this is not ensured by the parser, but an erroneous node here will already have an error report from the parser?

In general, the latter. So, if we have an assert, the assertion will throw and omit the properly described error.

For this particular case, I'm not sure if/how this case could be reached, since the grammar requires 'nondet' for this rule. But, if somehow this is possible, the reported error still is much better than an assertion - and there must be a reported error.

But, iiuc, if we get here and this is not a def them something must be broken with the parser? So assert or exceptions seems justified. Otherwise, e.g., what is something changes upstream that removes generation of an error when this is not a def? Then we would proceed silently and without marking any errer, no?

Yes, you are right. We talked about this at the meeting yesterday and @konnov suggested spitting some log lines when these branches are hit. It's not ideal, as it might generate noise on top of the proper error messages for the users, but it would help us spot problems while debugging.

Since we don't have a proper logging facility, I'm just prefixing the logs with [DEBUG] for now.

Do you think this is a reasonable solution?

Yep, that sounds good. Thanks.

shonfeder · 2023-11-01T13:48:27Z

quint/src/parsing/ToIrListener.ts

-      // if the definition has parameters, introduce a lambda
-      let body = expr ?? this.undefinedDef(ctx)
-      const id = this.getId(ctx)
+    let body = expr ?? this.undefinedExpr(ctx)()


Perhaps best to put the default where expr is bound, so that any future changes to this handle that refers to expr will also get the default value. This is also more consistent with the preceding code.

shonfeder · 2023-11-01T15:24:23Z

quint/src/parsing/ToIrListener.ts

+  private undefinedExpr(ctx: any): () => QuintEx {
+    return () => {
+      const id = this.getId(ctx)
+      return { id, kind: 'bool', value: true }
+    }
+  }


Should we introduce an UndefinedExpr node in the IR so we can be very clear about where holes are showing up? I'm worried we could end up with weird bugs where parts of the AST are replaced with true and it will be hard for maintainers to find out why that would be happening.

Hmm that might be a good idea for the next step. For now, the IR with undefined components should only be manipulated in name resolution. After that, we halt the process and report all errors gathered so far. This is not something guaranteed, but I'm pretty confident that we are ensuring that this is the case.

For the next steps, I want the type checker and effect checker to run over this IR as well, and my original plan was to have a check like: if there is an error for the id of this component, don't try to infer type/effect for the component.

Perhaps introducing undefined components to the IR, as you suggest, is a better alternative than relying on the errors. This would be a bigger change tho, as it requires another case in many IR-related functions and tests.

I see. Maybe something to consider for a followup, then. But I'm worried this will be confusing and can lead to lost time debugging. Could this be marked by making it named value or something? Like

val __undefinedExprGenerated = true; true

I like that idea!

shonfeder · 2023-11-01T15:25:22Z

quint/src/parsing/ToIrListener.ts

+  private undefinedDeclaration(ctx: any): () => QuintDeclaration {
+    return () => {
+      const id = this.getId(ctx)
+      return { id, kind: 'assume', name: '_', assumption: this.undefinedExpr(ctx)() }


Can we name it something like

Suggested change

return { id, kind: 'assume', name: '_', assumption: this.undefinedExpr(ctx)() }

return { id, kind: 'assume', name: `_undefinedDecl${id}`, assumption: this.undefinedExpr(ctx)() }

shonfeder · 2023-11-01T15:26:05Z

quint/src/parsing/ToIrListener.ts

+  private undefinedType(ctx: any): () => QuintType {
+    return () => {
+      const id = this.getId(ctx)
+      return { id, kind: 'bool' }
+    }
+  }
+
+  private undefinedVariant(ctx: any): () => RowField {
+    return () => ({ fieldName: '_', fieldType: this.undefinedType(ctx)() })
  }


Same question about making undefined forms clearer applies here.

shonfeder · 2023-11-01T15:31:48Z

quint/src/parsing/quintParserFrontend.ts

+    if (errors.length === 0) {
+      throw e
+    }
+    // ignore the exception, we already have errors to report


But what if the exception is not obviously explained by the recorded errors? Then we would end up swallowing unknown exceptions, potentially hiding errors.

Instead, I suggest this catch only apply to errors which are from a known family of errors that we are sure will be reflected in the errors, and anything else is left to bubble up. In my experience, a catch-all that recovers without a record of the exception inevitably comes back to bite you :D

But what if the exception is not obviously explained by the recorded errors?

It is not, what is happening is that the generated code breaks internally when the AST is malformed (because of parser errors). The idea is: there is something being reported, you should fix that problem first and then try again. If an exception is thrown after that (which should be impossible), then you can worry about the exception.

It should always be the case that the exception is a direct consequence of one of the errors, and that fixing the errors will make the exception go away.

Instead, I suggest this catch only apply to errors which are from a known family of errors that we are sure will be reflected in the errors

That I cannot do, because I'm introducing this try catch to handle unpredictable (or hard to predict) errors that are internal to the generated code from antlr4ts. Took me some manual testing to find the first case where some error is thrown, and I don't think I could ever find all possible errors that can be thrown.

I'm not following, maybe we can talk about this a bit tomorrow.

Thanks for talking thru the reasoning here. I am still a bit worried this may hide problems at some point, but less so and not enough to block here.

Perhaps the comment could be expanded to explain the reasoning?

…in builtin.qnt)

bugarela added 5 commits October 20, 2023 15:33

Improve error recoverability in ToIrListener

6cc44b4

Add integration test

2cf9513

Add CHANGELOG entry for fixed bug

aaf9686

Re-arrange conditionals and add explanatory comments

fcc772d

Fix CHANGELOG mistake

f5c931f

bugarela requested a review from konnov October 20, 2023 18:36

bugarela added 3 commits November 1, 2023 08:39

Improve diagnostics handling

a6ea326

Wrap AST walking into try catch

2d42066

Merge remote-tracking branch 'origin/main' into gabriela/improve-pars…

c8770f0

…ing-error-recovery-2

bugarela self-assigned this Nov 1, 2023

bugarela requested a review from shonfeder November 1, 2023 12:42

shonfeder suggested changes Nov 1, 2023

View reviewed changes

Merge branch 'main' into gabriela/improve-parsing-error-recovery-2

f426a7b

bugarela mentioned this pull request Nov 7, 2023

Refactoring parser tests #1237

Merged

shonfeder self-requested a review November 7, 2023 16:08

shonfeder approved these changes Nov 7, 2023

View reviewed changes

bugarela added 3 commits November 7, 2023 16:12

Add log messages and make undefined components easier to spot

232fe61

Use a different default value for definitions with a reader only (as …

9f4912e

…in builtin.qnt)

Update fixtures again

6a40d27

bugarela enabled auto-merge November 7, 2023 19:50

bugarela merged commit 6f63808 into main Nov 7, 2023
15 checks passed

bugarela deleted the gabriela/improve-parsing-error-recovery-2 branch November 7, 2023 19:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Re-opening] Improve error recoverability in `ToIrListener` #1228

[Re-opening] Improve error recoverability in `ToIrListener` #1228

bugarela commented Oct 20, 2023 •

edited

Loading

shonfeder left a comment

shonfeder Nov 1, 2023

shonfeder Nov 1, 2023

bugarela Nov 1, 2023

shonfeder Nov 2, 2023

bugarela Nov 6, 2023

shonfeder Nov 7, 2023

bugarela Nov 7, 2023

shonfeder Nov 7, 2023

shonfeder Nov 1, 2023

shonfeder Nov 1, 2023

bugarela Nov 1, 2023

shonfeder Nov 7, 2023 •

edited

Loading

bugarela Nov 7, 2023

shonfeder Nov 1, 2023

shonfeder Nov 1, 2023

shonfeder Nov 1, 2023

bugarela Nov 1, 2023

shonfeder Nov 2, 2023

shonfeder Nov 7, 2023

	return { id, kind: 'assume', name: '_', assumption: this.undefinedExpr(ctx)() }
	return { id, kind: 'assume', name: `_undefinedDecl${id}`, assumption: this.undefinedExpr(ctx)() }

[Re-opening] Improve error recoverability in ToIrListener #1228

[Re-opening] Improve error recoverability in ToIrListener #1228

Conversation

bugarela commented Oct 20, 2023 • edited Loading

shonfeder left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder Nov 7, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

[Re-opening] Improve error recoverability in `ToIrListener` #1228

[Re-opening] Improve error recoverability in `ToIrListener` #1228

bugarela commented Oct 20, 2023 •

edited

Loading

shonfeder Nov 7, 2023 •

edited

Loading