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

Assertion failed when pressing directional keys inside a textarea #22457

Closed
denismerigoux opened this issue Dec 14, 2018 · 0 comments

Comments

Projects
None yet
1 participant
@denismerigoux
Copy link
Contributor

commented Dec 14, 2018

When running ./mach run "https://www.w3schools.com/tags/tryit.asp?filename=tryhtml_textarea" after a --dev build, and playing around with the selection inside the text area, I usually get this error :

assertion failed: self.edit_point <= begin

It seems that the function adjust_vertical of file components/script/textinput.rs is breaking the debug assertions in assert_ok_selection.

bors-servo added a commit that referenced this issue Dec 22, 2018

Auto merge of #22458 - denismerigoux:master, r=jdm
Fixed bug in textinput::adjust_vertical concerning selection_origin

<!-- Please describe your changes on the following line: -->
The `adjust_vertical` function of the `TextInput` module was forgetting to update the `selection_origin`.

I discovered the bug and figured out how it fix it using formal verification. More precisely, I manually translated the Rust code in a [F*](https://www.fstar-lang.org/) program that was functionally equivalent. Then I used the `assert_ok_selection` as a post-condition on the following functions :

* `select_all`
* `clear_selection`
* `adjust_selection_for_horizontal_change`
* `clear_selection_to_limit`
* `adjust_vertical`
* `perform_horizontal_adjustment`
* `adjust_horizontal`
* `adjust_horizontal_to_line_end`

I managed to prove automatically (using the Z3 backend of F*) that the post-condition held for all the functions except for `adjust_vertical`. I used the error messages from F* to infer the missing code so that the postcondition could hold and manually translated it to this PR diff.

I also added a simple unit test that would fail without this patch, and observed that the assertion failures noted in #22457 disappeared with this patch.

This verification work also allows me to say that the code of all the functions is now functionally correct in the sense that they all yield a valid selection in the sense of `asssert_ok_selection`, in all cases.

---
<!-- Thank you for contributing to Servo! Please replace each `[ ]` by `[X]` when the step is complete, and replace `___` with appropriate data: -->
- [x] `./mach build -d` does not report any errors
- [x] `./mach test-tidy` does not report any errors
- [x] These changes fix #22457 (GitHub issue number if applicable)

<!-- Either: -->
- [x] There are tests for these changes

<!-- Also, please make sure that "Allow edits from maintainers" checkbox is checked, so that we can help you if you get stuck somewhere along the way.-->

<!-- Pull requests that do not address these steps are welcome, but they will require additional verification as part of the review process. -->

<!-- Reviewable:start -->
---
This change is [<img src="https://reviewable.io/review_button.svg" height="34" align="absmiddle" alt="Reviewable"/>](https://reviewable.io/reviews/servo/servo/22458)
<!-- Reviewable:end -->

bors-servo added a commit that referenced this issue Dec 23, 2018

Auto merge of #22458 - denismerigoux:master, r=jdm
Fixed bug in textinput::adjust_vertical concerning selection_origin

<!-- Please describe your changes on the following line: -->
The `adjust_vertical` function of the `TextInput` module was forgetting to update the `selection_origin`.

I discovered the bug and figured out how it fix it using formal verification. More precisely, I manually translated the Rust code in a [F*](https://www.fstar-lang.org/) program that was functionally equivalent. Then I used the `assert_ok_selection` as a post-condition on the following functions :

* `select_all`
* `clear_selection`
* `adjust_selection_for_horizontal_change`
* `clear_selection_to_limit`
* `adjust_vertical`
* `perform_horizontal_adjustment`
* `adjust_horizontal`
* `adjust_horizontal_to_line_end`

I managed to prove automatically (using the Z3 backend of F*) that the post-condition held for all the functions except for `adjust_vertical`. I used the error messages from F* to infer the missing code so that the postcondition could hold and manually translated it to this PR diff.

I also added a simple unit test that would fail without this patch, and observed that the assertion failures noted in #22457 disappeared with this patch.

This verification work also allows me to say that the code of all the functions is now functionally correct in the sense that they all yield a valid selection in the sense of `asssert_ok_selection`, in all cases.

---
<!-- Thank you for contributing to Servo! Please replace each `[ ]` by `[X]` when the step is complete, and replace `___` with appropriate data: -->
- [x] `./mach build -d` does not report any errors
- [x] `./mach test-tidy` does not report any errors
- [x] These changes fix #22457 (GitHub issue number if applicable)

<!-- Either: -->
- [x] There are tests for these changes

<!-- Also, please make sure that "Allow edits from maintainers" checkbox is checked, so that we can help you if you get stuck somewhere along the way.-->

<!-- Pull requests that do not address these steps are welcome, but they will require additional verification as part of the review process. -->

<!-- Reviewable:start -->
---
This change is [<img src="https://reviewable.io/review_button.svg" height="34" align="absmiddle" alt="Reviewable"/>](https://reviewable.io/reviews/servo/servo/22458)
<!-- Reviewable:end -->

bors-servo added a commit that referenced this issue Dec 23, 2018

Auto merge of #22458 - denismerigoux:master, r=jdm
Fixed bug in textinput::adjust_vertical concerning selection_origin

<!-- Please describe your changes on the following line: -->
The `adjust_vertical` function of the `TextInput` module was forgetting to update the `selection_origin`.

I discovered the bug and figured out how it fix it using formal verification. More precisely, I manually translated the Rust code in a [F*](https://www.fstar-lang.org/) program that was functionally equivalent. Then I used the `assert_ok_selection` as a post-condition on the following functions :

* `select_all`
* `clear_selection`
* `adjust_selection_for_horizontal_change`
* `clear_selection_to_limit`
* `adjust_vertical`
* `perform_horizontal_adjustment`
* `adjust_horizontal`
* `adjust_horizontal_to_line_end`

I managed to prove automatically (using the Z3 backend of F*) that the post-condition held for all the functions except for `adjust_vertical`. I used the error messages from F* to infer the missing code so that the postcondition could hold and manually translated it to this PR diff.

I also added a simple unit test that would fail without this patch, and observed that the assertion failures noted in #22457 disappeared with this patch.

This verification work also allows me to say that the code of all the functions is now functionally correct in the sense that they all yield a valid selection in the sense of `asssert_ok_selection`, in all cases.

---
<!-- Thank you for contributing to Servo! Please replace each `[ ]` by `[X]` when the step is complete, and replace `___` with appropriate data: -->
- [x] `./mach build -d` does not report any errors
- [x] `./mach test-tidy` does not report any errors
- [x] These changes fix #22457 (GitHub issue number if applicable)

<!-- Either: -->
- [x] There are tests for these changes

<!-- Also, please make sure that "Allow edits from maintainers" checkbox is checked, so that we can help you if you get stuck somewhere along the way.-->

<!-- Pull requests that do not address these steps are welcome, but they will require additional verification as part of the review process. -->

<!-- Reviewable:start -->
---
This change is [<img src="https://reviewable.io/review_button.svg" height="34" align="absmiddle" alt="Reviewable"/>](https://reviewable.io/reviews/servo/servo/22458)
<!-- Reviewable:end -->
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.