some accepted recursive values exhibit erroneous behavior with unexpected shallow copies #7768
Comments
|
Getting to this after being referred to it from #8956 and #9048;
Static vs. dynamic is well defined now thanks to @gasche's rec-check work. :) The above example is correctly rewritten by the solution we propose in #8956 ; aliasing of variables are detected for such cases: # let r = ref None
let rec x =
let s = { contents = 5 } in
r.contents <- Some s;
let _ = x in
s
let s = match !r with
| None -> "none"
| Some s -> Printf.sprintf "%b" (s != x)
;;
val r : int ref option ref = {contents = Some {contents = 5}}
val x : int ref = {contents = 5}
val s : string = "false"The definitions are rewritten to the following lambda: (let (r/80 = (makemutable 0 0a) s/82 = (makemutable 0 (int) 5))
(seq (setfield_ptr 0 r/80 (makeblock 0 s/82)) s/82
(makeblock 0 r/80 s/82))))Now, indeed, let-recs of values are already a niche, putting mutables inside is looking for trouble! |
|
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. |
|
I believe that this PR is still an issue (it is not completely clear whether it is a bug or a surprising effect of the specification). I think that it is logically waiting on #8956, which proposes a rewriting semantics for complex recursive-value definitions, and may clarify some aspects of the problem (make it easier to see what we can and should do here). |
|
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. |
Original bug ID: 7768
Reporter: @gasche
Assigned to: @lpw25
Status: assigned (set by @gasche on 2018-04-10T10:18:10Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.07.0+dev/beta2/rc1/rc2
Target version: 4.07.0+dev/beta2/rc1/rc2
Category: language features
Related to: #7706
Monitored by: @stedolan @yallop @hcarty
Bug description
Leo has an example in
#1565
which is
It is a bug that
(s != x)holds on this code: one would expect from the definition of x that s and x be equal, but the current compilation scheme pre-allocatesx, then computes its values (x) and copies it back into the pre-allocated space, so we get an implicit shallow copy ofs.Leo proposes to fix this issue by marking locally-bound values containing mutable data (whose shallow copy would be observable) as "Dynamic"-sized in the recursive-value analysis, the intuition being (I guess?) that Static means "can be preallocated" and thus implicitly "can be shallow-copied in non-observable ways".
On the other hand, mutable values that are bound to recursive identifiers but not locally-bound in the recursive definitions should remain Static because (1) otherwise reasonable code that is currently accepted would be rejected and (2) Leo claims that those mutable values are used linearily at value-construction time (no other initialization-time computation of the recursive declaration nest uses them), so they are undistinguishable from their shallow copies.
(This does not look obvious to me, and I am frustrated by the constant overloading of what those "Static" and "Dynamic" markers mean. It's past time for some proper design work.)
Additional information
I set the target 4.07+dev based on Leo's claim that this is easy to fix. I think the issue is non-critical (at worst, unexpected shallow copies happen; in particular, I don't think we can break type-soundness from this source of issues), so delaying to 4.08 would be fine.
The text was updated successfully, but these errors were encountered: