Fixed bug in textinput::adjust_vertical concerning selection_origin #22458
Conversation
|
Thanks for the pull request, and welcome! The Servo team is excited to review your changes, and you should hear from @jdm (or someone else) soon. |
|
Heads up! This PR modifies the following files:
|
|
Nice work! I only have some code syntax comments below. |
|
Neat that you used formal methods to prove properties about the code! Thanks for fixing this! |
|
@bors-servo r+ |
|
|
|
@bors-servo r- Sorry, do you mind squashing your commits into one? |
…pdate This bug was discovered using the F* formal verification framework. Style changes (match -> if let) Replace if let Some(_) by .is_some()
|
The commits are squashed :) |
|
@bors-servo r+ |
|
|
bors-servo
added a commit
that referenced
this pull request
Dec 22, 2018
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 retry |
bors-servo
added a commit
that referenced
this pull request
Dec 23, 2018
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 retry |
bors-servo
added a commit
that referenced
this pull request
Dec 23, 2018
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 -->
|
|
|
LGTM. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
The
adjust_verticalfunction of theTextInputmodule was forgetting to update theselection_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* program that was functionally equivalent. Then I used the
assert_ok_selectionas a post-condition on the following functions :select_allclear_selectionadjust_selection_for_horizontal_changeclear_selection_to_limitadjust_verticalperform_horizontal_adjustmentadjust_horizontaladjust_horizontal_to_line_endI 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../mach build -ddoes not report any errors./mach test-tidydoes not report any errorsThis change is