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
Crash when pattern-matching lazy values modifies the scrutinee #5992
Comments
Comment author: meyer I can't reproduce crash on 4.00.1 32 bits Linux. Could you provide a gdb backtrace? thanks |
Comment author: @yallop It appears to crash with ocamlc, but raise Match_failure with ocamlopt.
|
Comment author: @garrigue Interesting.
Lazy patterns are not supposed to have side-effects, but what should we do when they have? |
Comment author: @lefessan It is a known bug, lazy evaluation in pattern matching introduces the possibility to have side-effects that modify the values being pattern matched (it was actually discussed last Monday during the "bug meeting" that the local core team had). We should probably change the way the pattern-matching is compiled in the presence of a combination of lazy values and mutable values, to have a less efficient but safer execution. |
Comment author: @alainfrisch When-guards can already change parts of the scrutinee. This is less powerful than lazy patterns, since this cannot be done within a single branch, but I guess there are some provisions to avoid bad surprises in that case (or not?). Could we use the same technique for lazy patterns? |
Comment author: @lpw25
This is done by always assuming that patterns containing when-guards are non-exhaustive, so that they raise a match failure exception instead of seg fault. As in the following example:
The same thing could probably be done for lazy patterns. |
Comment author: @lpw25
I've attached a patch that does this. It certainly fixes Jeremy's example: ./ocaml ~/lazypatterns.ml |
Comment author: @lefessan I have two concerns with this solution:
For me, this is already a bug : the semantics should be that clauses are tested one line after the other one, and so, line "| { contents = 1 } -> 2" should be triggered, which is not the case. Using the same solution means increasing the problem instead of solving it... (2) I think that, since pattern-matching is compiled on the typed tree, we should use the information that the matched value is immutable to enable optimal compilation only when it preserves the semantics, i.e. in the absence of either mutable values, OR in the absence of when/lazy constructs. |
Comment author: @lpw25
A relaxed semantics: the ordering between effects and matches is unspecified and any program relying on it is essentially incorrect. Of course a more well-specified semantics could be implemented, but only at the expense of efficiency.
These are really separate problems. One is a soundness bug due to using "incorrect" exhaustiveness information to guide an optimisation. The other is about whether matching in the presence of side-effects should have a well-specified semantics.
I certainly agree that the patterns only need to be marked as non-exhaustive if they access mutable values. |
Comment author: @yallop I agree with Leo that there are two distinct issues here: the optimization based on the mistaken assumption of exhaustiveness, and the question of the order of evaluation for pattern matching. It's clear that we need to be more careful about assuming exhaustiveness when the match includes both lazy patterns and mutable data. I agree with Fabrice that the current behaviour of both lazy patterns and guards is unsatisfactory with respect to ordering. People writing OCaml programs will generally assume that the semantics of matching is to consider the pattern cases top-to-bottom, left-to-right. Although the manual is careful to avoid actually saying anything about the order of matching, several OCaml books say that matching is sequential: "When a match expression is evaluated, the expression expression to be matched is first evaluated, and its value is compared with the patterns in order." "The expression expr is matched sequentially to the various patterns p1, ..., pn." "Cases are explored in a top-down fashion: when a branch fails, the analysis resumes with the next possible branch. However, the analysis stops as soon as the branch is successful; then, its right hand side is evaluated and returned as result." |
Comment author: @alainfrisch In addition to changing the compilation scheme in presence of both mutable fields in the pattern and the possibility of side-effects (when-guard or lazy patterns), it would be good to report this as a warning. |
Comment author: @maranget The bug is now fixed, in the sense that the proposed example Luc |
Comment author: @xavierleroy
It is entirely unspecified when those side effects occur w.r.t. the matching operation itself.
I disagree. Pattern-matching is such an essential operation of the language that we want full liberty to compile in whatever testing order is efficient. And code such as your example should never be written in the first place.
They are all wrong. |
Comment author: @yallop Thanks, Luc! |
Original bug ID: 5992
Reporter: @yallop
Assigned to: @maranget
Status: closed (set by @xavierleroy on 2015-12-11T18:18:47Z)
Resolution: fixed
Priority: normal
Severity: major
Category: back end (clambda to assembly)
Related to: #7241
Monitored by: @gasche
Bug description
File attachments
The text was updated successfully, but these errors were encountered: