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

fix: return-statement reachability analysis #302

Merged
merged 2 commits into from
Apr 26, 2024

Conversation

anton-trunov
Copy link
Member

@anton-trunov anton-trunov commented Apr 26, 2024

Closes #268

  • I have updated CHANGELOG.md
  • I have added unit tests to demonstrate the contribution is correctly implemented
  • I have run all the tests locally and no test failure was reported
  • I did not do unrelated and/or undiscussed refactorings

@anton-trunov anton-trunov added this to the v1.3.0 milestone Apr 26, 2024
Copy link
Member

@novusnota novusnota left a comment

Choose a reason for hiding this comment

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

How could we fix the stmts-failed/case-41.tact in the future? Recursive descent of sorts?

Other than that, splendid work!

@anton-trunov
Copy link
Member Author

anton-trunov commented Apr 26, 2024

Thanks @novusnota!

How could we fix the stmts-failed/case-41.tact in the future? Recursive descent of sorts?

It can be done for the simple case of Booleans, but not in general.

Consider the following example:

if belongs(x, aSetOfIntegers) {
    return 1;
}
if belongs(x, anotherSetOfIntegers) {
    return 2;
}

if aSetOfIntegers \union anotherSetOfIntegers == Int then we have covered all the paths, but it's too expensive to try and solve it (or even undecidable). Btw, Rust solves this issue in the same way essentially, but it has if-expressions so it's a typechecking error.

You can try using SMT solvers (or your own custom solver) to do this, but it's not worth it in practice.

@anton-trunov anton-trunov merged commit 040e648 into main Apr 26, 2024
3 checks passed
@anton-trunov anton-trunov deleted the return-statement-reachability branch April 26, 2024 18:25
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.

Missing return statement not caught by Tact compiler
3 participants