Skip to content

The Pattern-Matching Bug: propagate mutability of argument positions#13138

Merged
gasche merged 1 commit intoocaml:trunkfrom
gasche:matching-bug-propagate-mut-2
May 13, 2024
Merged

The Pattern-Matching Bug: propagate mutability of argument positions#13138
gasche merged 1 commit intoocaml:trunkfrom
gasche:matching-bug-propagate-mut-2

Conversation

@gasche
Copy link
Copy Markdown
Member

@gasche gasche commented Apr 30, 2024

This is the next PR in the stack to fix #7241. To fix the bug, we need to pessimize the totality information coming from the type-checker when we switch on arguments/positions that may have been mutated. As suggested by the testcase match-side-effects/partiality.ml:deep, positions affected are not just those immediately below a mutable field, but also those that are transitively mutable -- there is a mutable field somewhere between the root of the value and the current position.

The present PR does not change the compilation behavior, it just adds a mut field to argument records to track whether the argument is in transitively-mutable position. (Currently this information is not tracked at all, unlike the information "immediately mutable" that can be reconstructed from the binding kind of the argument expression.)

(cc @ncik-roberts, @Octachron, @lthls )

{
arg;
binding_kind = StrictOpt;
mut = compose_mut mut Mutable;
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

I am not sure how I feel having constant multiplications by 0 or 1 in the source code, but why not.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

With this code organization I find it much easier to check how mutability information evolves during compilation. (Also: if I wanted to track both the "transitive mutability" and the "immediate mutability" of the argument position, this would be easy to do by changing mut here to be a pair, without changing much of the rest of the code. This would let us get rid of mut_of_binding_kind. I decided not to do it because there is bigger fish to fry, but it suggests that compose_mut is a nice abstraction to have.)

Copy link
Copy Markdown
Contributor

@ncik-roberts ncik-roberts left a comment

Choose a reason for hiding this comment

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

The code is correct, and it makes sense to me why this will be needed for your ensuing PRs.

@gasche gasche force-pushed the matching-bug-propagate-mut-2 branch 4 times, most recently from c56c967 to 50f6c2c Compare May 10, 2024 12:33
@gasche
Copy link
Copy Markdown
Member Author

gasche commented May 10, 2024

Thanks! I took the review comments into account.

@ncik-roberts
Copy link
Copy Markdown
Contributor

The diff looks to have picked up some unrelated changes in Changes and middle_end/flambda. Otherwise, it looks good to me.

@gasche gasche force-pushed the matching-bug-propagate-mut-2 branch from 50f6c2c to 32ba25f Compare May 10, 2024 13:03
@gasche
Copy link
Copy Markdown
Member Author

gasche commented May 13, 2024

Note: this needs a maintainer approval if we want to merge and rebase the follow-up PRs.

Copy link
Copy Markdown
Contributor

@lthls lthls left a comment

Choose a reason for hiding this comment

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

Approving on behalf of @ncik-roberts (after a quick look through the code)

@gasche gasche merged commit 4fc907d into ocaml:trunk May 13, 2024
@gasche
Copy link
Copy Markdown
Member Author

gasche commented May 13, 2024

Thanks! I merged, and rebased the follow-up PRs -- #13152, #13153, #13154.

ncik-roberts added a commit to oxcaml/oxcaml that referenced this pull request Jun 10, 2024
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.

Pattern matching with mutable and lazy patterns is unsound

4 participants