Skip to content

Commit f42a427

Browse files
anfeloranfelor
committed
Overwriting tests (ocaml-flambda#3123)
* Tests for overwriting * Remove old tests for unique overwrites and fix typos * Add overwriting tests back * Add tests for lifting out constants * Update tests * Use extension universe alpha * Test all cases for gc soundness bug * Review feedback: add more CRs and clarify overwriting_map.ml * Review feedback: Add allocation counter to rbtree * Review feedback: also test mixed blocks and unboxed float blocks in the lift constants test * Review feedback: as discussed in meeting * Review feedback
1 parent 1198f8e commit f42a427

13 files changed

+945
-112
lines changed

‎testsuite/tests/typing-unique/overwriting.ml

+143
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
(* TEST
2+
flags += "-extension-universe alpha";
3+
expect;
4+
*)
5+
6+
(* CR uniqueness: More tests to consider adding here:
7+
- overwriting tuples
8+
- overwriting labeled tuples
9+
- overwriting labeled tuples where only some labels are given
10+
- overwriting tuples (and labeled ones) with the new .. syntax
11+
- overwriting inline records (binding a variable to the whole constructor application,
12+
like | (K { ... }) as v -> ...)
13+
- overwriting inline records (binding a variable just to the inline record,
14+
like | K r -> ...)
15+
- overwriting constructor fields
16+
- overwriting mutable fields (yes, this is a bit silly, but we should test it)
17+
- overwriting immutable fields of records with mutable fields
18+
- local variants of (some of) the above
19+
- overwriting into a local record with a freshly-constructed bit of memory
20+
(to make sure that inference does not locally allocate the new memory)
21+
*)
22+
23+
type record_update = { x : string; y : string }
24+
[%%expect{|
25+
type record_update = { x : string; y : string; }
26+
|}]
27+
28+
29+
let update (unique_ r : record_update) =
30+
let x = overwrite_ r with { x = "foo" }
31+
in x.x
32+
[%%expect{|
33+
Line 2, characters 10-41:
34+
2 | let x = overwrite_ r with { x = "foo" }
35+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
36+
Alert : Overwrite not implemented.
37+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
38+
39+
|}]
40+
41+
let update2 = update { x = "bar" }
42+
[%%expect{|
43+
Line 1, characters 14-20:
44+
1 | let update2 = update { x = "bar" }
45+
^^^^^^
46+
Error: Unbound value "update"
47+
|}]
48+
49+
(* Only global values may be written during overwrites,
50+
since the GC does not allow heap-to-stack pointers.
51+
However, it is fine if there are local values (like y here)
52+
that are not overwritten. We test 2^3 configurations:
53+
- the overwritten value can be local/global
54+
- the resulting value can be local/global
55+
- the value written in the record can be local/global *)
56+
57+
let gc_soundness_bug (local_ unique_ r) (local_ x) =
58+
exclave_ overwrite_ r with { x }
59+
[%%expect{|
60+
Line 2, characters 11-34:
61+
2 | exclave_ overwrite_ r with { x }
62+
^^^^^^^^^^^^^^^^^^^^^^^
63+
Alert : Overwrite not implemented.
64+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
65+
66+
|}]
67+
68+
let disallowed_by_locality (local_ unique_ r) (local_ x) =
69+
overwrite_ r with { x }
70+
[%%expect{|
71+
Line 2, characters 2-25:
72+
2 | overwrite_ r with { x }
73+
^^^^^^^^^^^^^^^^^^^^^^^
74+
Alert : Overwrite not implemented.
75+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
76+
77+
|}]
78+
79+
let gc_soundness_bug (unique_ r) (local_ x) =
80+
exclave_ overwrite_ r with { x }
81+
[%%expect{|
82+
Line 2, characters 11-34:
83+
2 | exclave_ overwrite_ r with { x }
84+
^^^^^^^^^^^^^^^^^^^^^^^
85+
Alert : Overwrite not implemented.
86+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
87+
88+
|}]
89+
90+
let disallowed_by_locality (unique_ r) (local_ x) =
91+
overwrite_ r with { x }
92+
[%%expect{|
93+
Line 2, characters 2-25:
94+
2 | overwrite_ r with { x }
95+
^^^^^^^^^^^^^^^^^^^^^^^
96+
Alert : Overwrite not implemented.
97+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
98+
99+
|}]
100+
101+
let gc_soundness_no_bug (local_ unique_ r) x =
102+
exclave_ overwrite_ r with { x }
103+
[%%expect{|
104+
Line 2, characters 11-34:
105+
2 | exclave_ overwrite_ r with { x }
106+
^^^^^^^^^^^^^^^^^^^^^^^
107+
Alert : Overwrite not implemented.
108+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
109+
110+
|}]
111+
112+
let disallowed_by_locality (local_ unique_ r) x =
113+
overwrite_ r with { x }
114+
[%%expect{|
115+
Line 2, characters 2-25:
116+
2 | overwrite_ r with { x }
117+
^^^^^^^^^^^^^^^^^^^^^^^
118+
Alert : Overwrite not implemented.
119+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
120+
121+
|}]
122+
123+
let gc_soundness_no_bug (unique_ r) x =
124+
exclave_ overwrite_ r with { x }
125+
[%%expect{|
126+
Line 2, characters 11-34:
127+
2 | exclave_ overwrite_ r with { x }
128+
^^^^^^^^^^^^^^^^^^^^^^^
129+
Alert : Overwrite not implemented.
130+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
131+
132+
|}]
133+
134+
let gc_soundness_no_bug (unique_ r) x =
135+
overwrite_ r with { x }
136+
[%%expect{|
137+
Line 2, characters 2-25:
138+
2 | overwrite_ r with { x }
139+
^^^^^^^^^^^^^^^^^^^^^^^
140+
Alert : Overwrite not implemented.
141+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
142+
143+
|}]

‎testsuite/tests/typing-unique/overwriting_lift_constants.ml

+83
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
(* TEST
2+
flags += "-extension-universe alpha";
3+
expect;
4+
reference = "${test_source_directory}/overwriting_lift_constants.reference";
5+
*)
6+
7+
(* CR uniqueness: To run this test replace 'expect' above by 'native'
8+
and delete the expect block. *)
9+
10+
type point = { mutable dim : int; x : float; y : float; z : float }
11+
12+
(* First: check that overwriting happens at all *)
13+
let unsafe_dup : 'a @ unique -> 'a * 'a @ unique =
14+
Obj.magic (fun x -> (x, x))
15+
16+
let check_overwriting_enabled () =
17+
let (p, q) = unsafe_dup { dim = 3; x = 1.0; y = 2.0; z = 3.0 } in
18+
let p = overwrite_ p with { dim = 4; x = 1.0; y = 2.0; z = 3.0 } in
19+
p == q
20+
21+
(* This file tests how constants are lifted out.
22+
Unique constants can not be lifted out since they
23+
might be overwritten but all other constants should still
24+
be lifted out.
25+
Since this pass is not yet implemented, I have added the
26+
expected result from the prototype in a comment to each test.
27+
*)
28+
29+
(* Same test for float blocks *)
30+
type fpoint = { x : float; y : float; z : float }
31+
32+
let fupdate_with_constant (p : fpoint) =
33+
let q = overwrite_ p with { x = 2.0; y = 3.0; z = 4.0 } in
34+
q
35+
36+
let test2 () =
37+
let p = { x = 1.0; y = 2.0; z = 3.0 } in
38+
let q = { x = 1.0; y = 2.0; z = 3.0 } in
39+
fupdate_with_constant p == fupdate_with_constant q
40+
41+
(* The tail of the list should be lifted out *)
42+
let constant_list x =
43+
x :: 2 :: []
44+
45+
(* While the head is different, the tails are the same *)
46+
let test3 () =
47+
List.hd (constant_list 1) == List.hd (constant_list 2),
48+
List.tl (constant_list 1) == List.tl (constant_list 2)
49+
50+
(* Since the tail was marked unique, it can not be lifted out *)
51+
let constant_list_unique x =
52+
let unique_ y = 2 :: [] in x :: y
53+
54+
let test4 () =
55+
List.hd (constant_list_unique 1) == List.hd (constant_list_unique 2),
56+
List.tl (constant_list_unique 1) == List.tl (constant_list_unique 2)
57+
58+
(* Since the tail was marked unique, it can not be lifted out *)
59+
let constant_list_unique2 x =
60+
let unique_ z = [] in
61+
let unique_ y = 2 :: z in x :: y
62+
63+
let test5 () =
64+
List.hd (constant_list_unique2 1) == List.hd (constant_list_unique2 2),
65+
List.tl (constant_list_unique2 1) == List.tl (constant_list_unique2 2)
66+
67+
let () =
68+
Printf.printf "%B\n" (check_overwriting_enabled ());
69+
Printf.printf "%B\n" (test2 ());
70+
Printf.printf "(%B, %B)\n" (test3 ());
71+
Printf.printf "(%B, %B)\n" (test4 ());
72+
Printf.printf "(%B, %B)\n" (test5 ());
73+
74+
[%%expect{|
75+
type point = { mutable dim : int; x : float; y : float; z : float; }
76+
val unsafe_dup : '_a @ unique -> '_a * '_a @ unique @@ global many = <fun>
77+
Line 9, characters 10-66:
78+
9 | let p = overwrite_ p with { dim = 4; x = 1.0; y = 2.0; z = 3.0 } in
79+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
80+
Alert : Overwrite not implemented.
81+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
82+
83+
|}]

‎testsuite/tests/typing-unique/overwriting_lift_constants.reference

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
true
2+
true
3+
(false, true)
4+
(false, false)
5+
(false, false)

‎testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml

+70
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
(* TEST
2+
flags += "-extension-universe alpha";
3+
expect;
4+
reference = "${test_source_directory}/overwriting_lift_constants_bug.reference";
5+
*)
6+
7+
(* CR uniqueness: To run this test replace 'expect' above by 'native'
8+
and delete the expect block. *)
9+
10+
type point = { dim : int; x : float; y : float; z : float }
11+
12+
let constant_lift b =
13+
let unique_ p = { dim = 3; x = 1.0; y = 2.0; z = 3.0 } in
14+
if b then p else overwrite_ p with { x = 2.0 }
15+
16+
type fpoint = { x : float; y : float; z : float }
17+
18+
let fconstant_lift b =
19+
let unique_ p = { x = 1.0; y = 2.0; z = 3.0 } in
20+
if b then p else overwrite_ p with { x = 2.0 }
21+
22+
type mpoint = { dim : int option; x : float#; y : float#; z : float# }
23+
24+
let mconstant_lift b =
25+
let unique_ p = { dim = Some 3; x = #1.0; y = #2.0; z = #3.0 } in
26+
if b then p else overwrite_ p with { x = #2.0 }
27+
28+
type ufpoint = { x : float#; y : float#; z : float# }
29+
30+
let ufconstant_lift b =
31+
let unique_ p = { x = #1.0; y = #2.0; z = #3.0 } in
32+
if b then p else overwrite_ p with { x = #2.0 }
33+
34+
type utpoint = { xy : #(float * float); z : float }
35+
36+
let ufconstant_lift b =
37+
let unique_ p = { xy = #(1.0, 2.0); z = 3.0 } in
38+
if b then p else overwrite_ p with { xy = #(2.0, 2.0) }
39+
40+
let () =
41+
let x = (constant_lift true).x in
42+
let y = (constant_lift false).x in
43+
let z = (constant_lift true).x in
44+
Printf.printf "%f %f %f\n" x y z;
45+
let x = (fconstant_lift true).x in
46+
let y = (fconstant_lift false).x in
47+
let z = (fconstant_lift true).x in
48+
Printf.printf "%f %f %f\n" x y z;
49+
let x = Float_u.to_float (mconstant_lift true).x in
50+
let y = Float_u.to_float (mconstant_lift false).x in
51+
let z = Float_u.to_float (mconstant_lift true).x in
52+
Printf.printf "%f %f %f\n" x y z;
53+
let x = Float_u.to_float (ufconstant_lift true).x in
54+
let y = Float_u.to_float (ufconstant_lift false).x in
55+
let z = Float_u.to_float (ufconstant_lift true).x in
56+
Printf.printf "%f %f %f\n" x y z;
57+
let x = Float_u.to_float (fst (ufconstant_lift true).xy) in
58+
let y = Float_u.to_float (fst (ufconstant_lift false).xy) in
59+
let z = Float_u.to_float (fst (ufconstant_lift true).xy) in
60+
Printf.printf "%f %f %f\n" x y z
61+
62+
[%%expect{|
63+
type point = { dim : int; x : float; y : float; z : float; }
64+
Line 5, characters 19-48:
65+
5 | if b then p else overwrite_ p with { x = 2.0 }
66+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
67+
Alert : Overwrite not implemented.
68+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
69+
70+
|}]

‎testsuite/tests/typing-unique/overwriting_lift_constants_bug.reference

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
1.000000 2.000000 1.000000
2+
1.000000 2.000000 1.000000
3+
1.000000 2.000000 1.000000
4+
1.000000 2.000000 1.000000
5+
1.000000 2.000000 1.000000

‎testsuite/tests/typing-unique/overwriting_map.ml

+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
(* TEST
2+
flags += "-extension-universe alpha";
3+
expect;
4+
reference = "${test_source_directory}/overwriting_map.reference";
5+
*)
6+
7+
(* CR uniqueness: To run this test replace 'expect' above by 'native'
8+
and delete the expect block. *)
9+
10+
let rec map f xs =
11+
match xs with
12+
| hd :: tl as xs -> overwrite_ xs with f hd :: map f tl
13+
| [] -> []
14+
15+
let () =
16+
let xs = [1;2;3] in
17+
18+
let baseline_allocation = Gc.allocated_bytes() -. Gc.allocated_bytes() in
19+
let before = Gc.allocated_bytes () in
20+
let _ = Sys.opaque_identity (map (fun x -> x + 1) xs) in
21+
let after = Gc.allocated_bytes () in
22+
let bytes_per_word = Sys.word_size / 8 in
23+
let delta =
24+
int_of_float ((after -. before) -. baseline_allocation) / bytes_per_word
25+
in
26+
let msg =
27+
match delta with
28+
| 0 -> "No Allocation"
29+
| n -> "Allocated " ^ string_of_int n ^ " words"
30+
in
31+
Printf.printf "%15s: %s\n" "List.map" msg
32+
33+
[%%expect{|
34+
Line 3, characters 22-57:
35+
3 | | hd :: tl as xs -> overwrite_ xs with f hd :: map f tl
36+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
37+
Alert : Overwrite not implemented.
38+
Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
39+
40+
|}]

‎testsuite/tests/typing-unique/overwriting_map.reference

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
List.map: No Allocation

0 commit comments

Comments
 (0)