Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Throw a graceful error when type checking for ctpop fails #2504

Merged
merged 4 commits into from
Jun 28, 2023

Conversation

JustusAdam
Copy link
Contributor

@JustusAdam JustusAdam commented Jun 2, 2023

Description of changes:

This PR addresses one of the issue raised in #2121 where a typecheck for ctpop in the backend makes kani crash.

With these changes it now reports a clean compiler error with the usual span information, e.g.

error: Type check failed for intrinsic `ctpop`: Expected integer type, found ()
   |
12 |     let n = ctpop(());
   |             ^^^^^^^^^

error: aborting due to previous error

Resolved issues:

Relates to #2121

Concrete coverage of the subissues

Call-outs / outstanding questions

  • At the moment I essentially perform the same type check that cprover_bindings does but earlier, when we have access to the rustc session and can gracefully emit errors. The clean thing to do here is to only perform this type check in one place. Probably cleanest to have functions that perform type checks (such as Expr::popcont) return Result so that it propagates the error gracefully and then turn it into a rustc error. That's a bigger change though that I think needs feedback.
  • I used the Debug printing of the internal Type struct here, since that's what's available at that point and because it does not implement Display, but this won't mean much to the user so I'll have to revisit this to make it more meaningful.
  • Emitting errors via tcx.sess does not immediately abort the compilation (unlike assert!). This means I need to emit a no-op Stmt to make codegen_intrinsic's type happy. Depending on the statement used and when exactly the compiler aborts this could (possibly) cause weird error downstream. I'm using Stmt::skip but that may not be the right choice.

Testing:

TODO

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@JustusAdam
Copy link
Contributor Author

Thank you for your comments @celinval. I opened this PR so we have the diff available.

At the moment I added this logic analogous with the example you posted. I can keep doing that for the other subissues, but my concern is that this both has a chance to miss other cases in which such type checks are necessary and also means that all checks are performed twice (in code gen and binding library) which means they can start to diverge at some point.

Wrt types, I can make sure to use Ty instead.

Thanks for clarifying on the abort. I'm not quite sure where the nearest abort_if_errors call is to the intrinsics lowering. Are you saying that I should add one?

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Awesome! That's about it. Can you also please add a test?

@JustusAdam
Copy link
Contributor Author

I can do that. What I feel like I haven't quite gotten an answer to yet is what I am supposed to do with the similar issues. #2121 contains a few concrete examples, but presumably this whole thing is bigger, as in there are many intrinsics that have type requirements that are checked via assert in cprover_bindings and could cause similar crashes to the ones reported in #2121. Do you want me to just fix the examples from the issue or generally propagate all potential type check errors that may arise from the typer checking in cprover_bindings? It feels like this may be the right time to nip these in the bud?

@JustusAdam JustusAdam force-pushed the fix-2121 branch 2 times, most recently from 3285620 to 70699f4 Compare June 6, 2023 19:47
@JustusAdam JustusAdam marked this pull request as ready for review June 6, 2023 20:39
@JustusAdam JustusAdam requested a review from a team as a code owner June 6, 2023 20:39
@JustusAdam
Copy link
Contributor Author

I force pushed an update with the requested changes to this branch but for some reason I don't see it reflected here. I'll have to investigate that. Sorry for the confusion

@JustusAdam JustusAdam force-pushed the fix-2121 branch 2 times, most recently from a2c8c51 to f924cee Compare June 7, 2023 23:20
@JustusAdam
Copy link
Contributor Author

Okay now it's reflected.

Throws a graceful type error for `ctpop` in the code gen.
Adds the expectation to the test case.
Marks the test case as no longer `fixme`
@adpaco-aws
Copy link
Contributor

Looks like only a few rustdoc errors are blocking this PR... @JustusAdam can you please take a look?

@celinval
Copy link
Contributor

BTW, can you please update the title of this PR and description to something more meaningful? Thanks!

@JustusAdam JustusAdam changed the title Fix for #2121 Throw a graceful error when type checking for ctpop fails Jun 26, 2023
@JustusAdam
Copy link
Contributor Author

I'm not sure what the perf regression error is supposed to tell me there. Can anyone shed a light?

@karkhaz
Copy link
Contributor

karkhaz commented Jun 26, 2023

I'm not sure what the perf regression error is supposed to tell me there. Can anyone shed a light?

That actually looks like it's broken in CI. Don't worry about it, this check isn't blocking the PR.

@adpaco-aws adpaco-aws merged commit a6e516e into model-checking:main Jun 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants