Pattern matching with mutable and lazy patterns is unsound #7241
Comments
|
Comment author: @stedolan Playing with it a bit more, the example can be simplified to the following, which does not use laziness: The issue is not the type-equality behaviour of GADTs, but the existential quantification. In this example, mutation causes the optimised pattern-matching to confuse the values bound under two different existential quantifiers. Either lazy patterns (as in the original example) or when guards (above) are enough to cause mutation during matching. |
|
Comment author: bvaugon Remarks, the "when" is also broken. For example, the following code crash in the similar way: type (_, _) eq = Refl : ('a, 'a) eq
type (_, _) deq = Deq : ('a, 'x) eq option * ('x, 'b) eq option -> ('a, 'b) deq
let deq1 = Deq (Some Refl, None)
let deq2 = Deq (None, Some Refl)
type ('a, 'b) t = {
a : bool;
mutable b : ('a, 'b) deq;
}
let r = { a = true; b = deq1 }
let g (type a) (type b) : (a, b) t -> (a, b) eq = function
| { a = true; b = Deq (Some _, _) } when (r.b <- deq2; false) ->
assert false
| { a = true; b = Deq (None, _) }
| { a = false }
| { b = Deq (_, None) } ->
assert false
| { b = Deq (Some Refl, Some Refl) } ->
Refl
let bad = g r
let castint (type a) (Refl : (int, a) eq) (x : int) : a = x
let _ = print_string (castint bad 42) |
|
Comment author: @alainfrisch I did not try to produce an example, and this would be more tricky, but even without lazy or when guards, it is impossible to guarantee that arbitrary code won't be executed during pattern matching as soon as patterns need to allocate (e.g. to read from a float from unboxed records or arrays). These allocations can trigger the GC and thus finalizer which could modify mutable parts of the matched value. It might be possible to delay these allocations (at least until the "when" guard), but this would probably require some refactoring of the PM compiler. (Of course, the pattern can "traverse" the unboxed floats.) |
|
Comment author: @alainfrisch Setting Target version to "later", since there is no clear resolution plan. |
|
Comment author: @garrigue I don't even think that one needs existentials to do that. type u = {a: bool; mutable b: int option}
let f x =
match x with
{a=false} -> 0
| {b=None} -> 1
| _ when (x.b <- None; false) -> 2
| {a=true; b=Some y} -> y
let _ = f {a=true; b=Some 5}The (insufficient) fix in matching.ml is let check_partial is_mutable is_lazy pat_act_list = function
| Partial -> Partial
| Total ->
if
pat_act_list = [] || (* allow empty case list *)
List.exists (fun (pats, _) -> is_mutable pats) pat_act_list &&
List.exists (fun (pats, lam) -> is_guarded lam || is_lazy pats)
pat_act_list
then Partial
else Total |
|
Comment author: @alainfrisch Frightening. Jacques: do you agree with my guess that this could even occur without when guards (with patterns that allocates and GC alarms/finalizers)? |
|
Comment author: @xavierleroy Currenty worked on at #717 |
|
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
|
The program in the original report still causes a segmentation fault, which seems reason enough to leave this open. There's also been recent activity on this issue elsewhere. Under #717, @trefis wrote in October 2019:
|
|
I wonder how other languages with pattern matching and mutation deal with this issue (F#, Scala...). Do they all suffer from the same unsoundness? |
|
Whether one is unsound or not is a question of assumptions and optimizations made during matching. Very naive implementations would typically be correct, and slightly more elaborate implementations may very well be buggy just as ours. Handling multicore is not a difficulty. What we need is to reason about the points during pattern-matching where side-effects may be performed. Currently this happens during evaluation of guards, float unboxing and |
|
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
|
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
|
Regarding finalizers, etc., it might be helpful to consider a version of |
|
I have a proposal to "fix this issue for good", but it requires more work and some research. I am writing a summary of the proposal below for future reference. Background on pattern-matching contextsThe current pattern-matching compilation algorithm maintains some "context" information to optimize its generated code. During pattern-matching compilation we match on a row of inputs; we maintain a context that encodes statically-known information about this row of inputs. For example if you write match x1, x2 with
| Some y, foo...
| bar...then the compilation of the The bugThe problem we are discussing is that this "context" information, that is used to generate optimized matching code, can become invalid if the pattern-matching inputs are mutated in the middle of the matching logic. Consider the simplest example of unsoundness due to Jacques Garrigue above: type u = {a: bool; mutable b: int option}
let f x =
match x with
| {a = false; b = _} -> 0
| {a = _; b = None} -> 1
| {a = _; b = _} when (x.b <- None; false) -> 2
| {a = true; b = Some y} -> y
let _ = f {a=true; b=Some 5}One way to think of what is going on here is as follows:
Generated codeThis "optimization based on static contexts" logic is apparent in the code generated for this example, obtained with (let
(f/393 =
(function x : int
(let (xa =a (field_int 0 x))
(catch
(catch
(if xa (exit 7) 0)
with (7)
(let (xb/1 =o (field_mut 1 x))
(catch (if xb/1 (exit 8) 1)
with (8)
(if (seq (setfield_ptr 1 x 0) 0) 2 (exit 6)))))
with (6)
(let
(xb/2 =o (field_mut 1 x)
y =a (field_imm 0 xb/2))
y)))))The first-clause check for The second-clause check for In the compilation of the fourth clause (the The backtracking nature of pattern-matching compilationNotice that the code contains two distinct accesses to the second field of In this particular example, this seems wasteful: we could have placed the "fourth clause logic", the The presence of such redundant reads would be avoidable in this example but is unavoidable in general: this "backtracking" aspect of the pattern-matching compiler is essential to avoid code-explosion issues. Backtracking allows distinct paths through the matching control flow to merge by jumping to the same exit, avoiding exponential code explosion. These code-explosion issues are not theoretical, they show up very quickly in practice when using or-patterns (or range patterns, etc.). Note that the cost of this "backtracking" is greatly reduced by those static optimization contexts: we "backtrack" to the toplevel and have to match the whole input again, but in fact we know that Conversely, if we were not "backtracking" during compilation, we would not need these static optimization contexts. Existing fix proposal: removing mutable subtrees from the contextThe obvious fix for this issue is to remove from the static optimization context any knowledge that may be invalidated by mutation, that is, any sub-value whose path from the root (the scrutinee) contains a mutable read. This is the approach proposed by Luc Maranget in #717 At the time where this fix was proposed, people were worried that systematically erasing mutable information from contexts would degrade pattern-matching performance too much -- there are indeed example in the wild where this pessimized code generation. Luc refined his approach to try to reason about when a mutation may occur (in a lazy pattern or on a One problem with this approach is that this approximation of which pattern-matching may suffer from side-effects is incorrect. Reading a floating-point value may also generate side-effects (the allocation can switch control to another piece of code), and with OCaml 5.x we have to consider the case of arbitrary races from other domain -- so we would be back to pessimizing all the time. Alternative proposal (sketch): changing the compilation strategyMy alternative proposal is to change the compilation strategy so that the arguments that we are matching over (the input row) coincides with the leaves of the static context. In other words, we carry extra inputs in intermediate steps of the pattern-matching compilation that corresponds to our static knowledge. Consider our running example: let f x =
match x with
| {a = false; b = _} -> 0
| {a = _; b = None} -> 1
| {a = _; b = _} when (x.b <- None; false) -> 2
| {a = true; b = Some y} -> yAfter matching the second clause and Then when we reach the fourth row, we still have On our example this would correspond to the following generated code: (let
(f/393 =
(function x : int
(let (xa =a (field_int 0 x))
(catch
(catch
(if xa (exit 7) 0)
with (7)
(let (xb =o (field_mut 1 x))
(catch
(if xb
(let y =a (field_imm 0 xb)
(exit 8 y))
1)
with (8 y)
(if (seq (setfield_ptr 1 x 0) 0) 2 (exit 6 y)))))
with (6 y) y)))))In this modified version, the branch in the second clause that adds In summary: whenever we decide to gain some static knowledge of some part of the matched value, we also take a "snapshot" of this part that we carry around as long as we make this static assuption. "Using' this static knowledge is done by using this snapshot directly, instead of re-doing some reads of the inputs that could have been invalidated by a state update. This gives a sensible semantics, that is clearly safe in presence of mutation, without pessimizing compilation by adding new branches for safety. (Note that this approach does not guarantee the absence of redundant reads: some control flow path may merge with other control flow paths with less static context information, and their shared code at this point may perform reads that are redundant for inputs coming from the more-informed exit point. Those reads are safe in presence of mutation.) This is only a sketch, and I am not completely clear of the details. Do we want to systematically keep all the "leaves" of the static context as extra inputs? Maybe this is too many arguments in practice. Do we want to only keep the results of mutable reads, as we know that we can reconstruct immutable reads safely? Or maybe we could have some analysis of which of those leaves are going to be useful later, and only keep those. (Say we could have I'm not familiar enough with this part of the pattern-matching compilation strategy to tell which choices in this design space are feasible / not too invasive -- if any. My impression is that doing this nicely is more work than the code-pessimizing fix, but also more satisfying. This is, basically, research. (Note: another approach to implement this would be to treat it as a post-pattern-matching optimization pass that removes redundant reads after some data-flow analysis. This is probably easier to implement as it can be kept independent from the pattern-matching machinery, but it is more heavy-weight -- we would need to compare code fragments for syntactic equality, etc. More importantly, it is less clear that the result is correct -- fixes the bug -- because there is no clear relation between the post-processing analysis and the potentially-unsafe decisions relying on static optimization contexts.) Current planBoth of these possible roads to a fix are delayed/blocked by the fact that no one knows this part of the pattern-matching compiler codebase well enough to implement or review them with confidence. The first step for me would be to read and document the current implementation of static optimization contexts, to ensure that at least Luc, myself and other welcome volunteers understand the current codebase well enough to assess proposed changes to the implementation. |
|
Today I worked on this again with @trefis, and we:
Why the bug can happenOne aspect of Luc's bugfix that has left us bewildered for seven years now is that there is already code in the compiler to handle this problem: the Contexts and jump summariesWhen turning a pattern matrix into code, the pattern-matching compiler takes as input some static information on the match arguments called the "context". Along with the generated code, it returns a "jump summary", which gives a more precise version of this context for each raise to an exit point in the generated code -- that context has been refined by further splits occurring within the generated code. Combining jump summariesThe pattern-matching compiler generates code that is formed of "switch" nodes that look somewhat like this: We start from the current context, and refine it in each branch: the branch context remembers the constructor that was matched, and has a different arity based on the number of arguments. We then produce the generated code of the branch under this context, and receive a jump summary with the same branch-specific arity. At this point we must "combine" the jump summaries of all branches, re-applying the matched constructor to obtain a common arity corresponding to the input arguments. When re-applying the head constructor, the pattern-matching compiler is careful to call the Why the bug then?type u = {a: bool; mutable b: int option}
let f x =
match x with
| {a = false; b = _} -> 0
| {a = _; b = None} -> 1
| {a = _; b = _} when (x.b <- None; false) -> 2
| {a = true; b = Some y} -> y
let _ = f {a=true; b=Some 5}In our example, the problem comes from using static context on the At this point, the |
The problem with the proposal aboveThe idea of my proposal above is to generate different code on exits depending on the context of its exit handler -- if the exit handler makes assumptions on certain mutable reads, include them as extra data in the exit. The difficulty we encountered is that the context of the exit handler is only fully known once all exit points have been generated. We would have to backpatch the generated exit code at this point (eww!), or change the data structure / control flow of this part of the pattern-matching compiler to go through an intermediate representation where exit points are not yet fully known. One possible way to do this is to change the return type of functions as follows: (* before *)
.... -> Jumps.t * lambda
(* after *)
.... -> Jumps.t * (Final_jumps_info.t -> lambda)but this sounds like a fairly invasive change. An alternative proposalRemember our example: type u = {a: bool; mutable b: int option}
let f x =
match x with
| {a = false; b = _} -> 0
| {a = _; b = None} -> 1
| {a = _; b = _} when (x.b <- None; false) -> 2
| {a = true; b = Some y} -> y
let _ = f {a=true; b=Some 5}And its currently-generated code: My proposal was to amend the However, we could have generated the code differently such that To do this the pattern-matching compiler should genrate the binding for the record fields at the point where it decomposes the record in the matrix, instead of generating the binding for each field at the point where the corresponding column is split. This goes counter to the current implementation which is careful to delay those let-bindings as late as possible in the generation process. We are not sure how to implement it well and what would be the downsides (in general we could deduplicate some code but also add some unnecessary memory reads in some branches).
We believe that this idea suffices to fix the problem in general. Consider the
|
The infamous matching bug ocaml#7241 corresponds to two distinct issues that arise when side-effects mutate the value being matched on: 1. Incorrect contexts: context information from the pre-mutation switches is retained. 2. Incorrect partiality information: type-checker-provided partiality information becomes incorrect. This commit fixes the first problem: incorrect contexts.
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired.
|
Since last week I have a working fix for this issue, but there are several pieces which I am sending as separate PRs for easier review. (Each piece is faster to review, can be reviewed more carefully, and can be reviewed by different people.) Here is a map of the current group of merged PRs, submitted PRs and upcoming branches. Merged
Submitted
Upcoming branchesNone! |
|
@goldfirere mentioned to me that you were looking for a reviewer for some pieces of this. Let me know how I can be helpful here — what pieces are you seeking review on? |
|
Thanks! #12534 is waiting for a review, and also #12555. The two PRs are independent. (There was a decision to make between #12555 and #12556 which are competing approaches to solve the same problem, but I decided to go for #12555 and closed #12556. Feel free to have a look at both if you are interested in the nitty gritty details.) |
|
(Apologies for the silence. I haven't forgotten about this — I hope to get started sometime in the next two weeks.) |
|
Great news, thanks! (I was thinking of pinging again, but turns out this was also on your mind.) |
The infamous matching bug ocaml#7241 corresponds to two distinct issues that arise when side-effects mutate the value being matched on: 1. Incorrect contexts: context information from the pre-mutation switches is retained. 2. Incorrect partiality information: type-checker-provided partiality information becomes incorrect. This commit fixes the first problem: incorrect contexts.
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired.
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired.
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired.
|
Yep, it's not fixed yet. (I wish!) But the PRs still in flight should be enough to fix it. |
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired.
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired.
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired. Note: the [check_partial] function also contained hidden logic to deal with the pattern-matching programs with no cases at all (more precisely, those that have only refutation cases, like `function _ -> .`), we retain this logic and move it to `toplevel_handler`.
|
@Octachron, @lthls, @trefis: at the current point in time, all standing PRs for this issue have been reviewed and approved by @ncik-roberts, they are all rebased on the current trunk, so the next thing they need to move forward is approval from a maintainer. I have kept the tracking comment #7241 (comment) up-to-date with a list of all remaining PRs, stacked on top of each other. |
|
All PRs working on this issue have now been reviewed, merged, and will be part of the 5.3 release. We can now close the bug :-) |
|
Ah, also: we wrote an extended abstract to explain (from a high-level) this bug for the ML Workshop 2024, which some people might find useful as a condensed summary of the bug, the necessary background on the OCaml pattern-matching compiler, and the fixes we implemented:
|
Original bug ID: 7241
Reporter: @stedolan
Assigned to: @maranget
Status: assigned (set by @mshinwell on 2017-03-09T12:39:53Z)
Resolution: open
Priority: normal
Severity: crash
Category: typing
Related to: #5992
Monitored by: junsli braibant @gasche @hcarty
Bug description
Optimised pattern matching skips checking conditions that seem redundant. However, since OCaml supports pattern-matching mutable fields, and code execution during matching via "lazy" patterns, the truth of some conditions can vary during matching.
This can cause seemingly-impossible cases to be taken, if forcing lazy values causes mutations that confuse the optimised matching logic. Due to the presence of GADTs, taking an impossible case is a soundness issue.
For example, this program segfaults:
This program uses mutation to change a field from "deq1" to "deq2" during matching, making it seem like the impossible "Deq (Some Refl, Some Refl)". (The behaviour is very dependent on the exact sequence of cases in "g", and seemingly-equivalent programs will often give different behaviour).
The text was updated successfully, but these errors were encountered: