Skip to content

Commit a3a47ba

Browse files
authored
Update analysis/ownership/README.md to add syntax highlighting to code snippets. (#1156)
2 parents 0872f48 + ddd0b63 commit a3a47ba

File tree

1 file changed

+99
-78
lines changed
  • c2rust-refactor/src/analysis/ownership

1 file changed

+99
-78
lines changed

c2rust-refactor/src/analysis/ownership/README.md

Lines changed: 99 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -20,37 +20,37 @@ permission also includes the ability to free the pointed-to data, which amounts
2020
to "moving to nowhere".
2121

2222
Here is a simple example to illustrate the major features of the analysis:
23-
24-
struct Array {
25-
data: *mut i32,
26-
}
27-
28-
unsafe fn new_array(len: usize) -> *mut Array {
29-
let data = malloc(size_of::<i32>() * len);
30-
let arr = malloc(size_of::<Array>());
31-
(*arr).data = data;
32-
arr
33-
}
34-
35-
unsafe fn delete_array(arr: *mut Array) {
36-
free((*arr).data);
37-
free(arr);
38-
}
39-
40-
unsafe fn element_ptr(arr: *mut Array, idx: usize) -> *mut i32 {
41-
(*arr).data.offset(idx)
42-
}
43-
44-
unsafe fn get(arr: *mut Array, idx: usize) -> i32 {
45-
let elt: *mut i32 = element_ptr(arr, idx);
46-
*elt
47-
}
48-
49-
unsafe fn set(arr: *mut Array, idx: usize, val: i32) {
50-
let elt: *mut i32 = element_ptr(arr, idx);
51-
*elt = val;
52-
}
53-
23+
```rust
24+
struct Array {
25+
data: *mut i32,
26+
}
27+
28+
unsafe fn new_array(len: usize) -> *mut Array {
29+
let data = malloc(size_of::<i32>() * len);
30+
let arr = malloc(size_of::<Array>());
31+
(*arr).data = data;
32+
arr
33+
}
34+
35+
unsafe fn delete_array(arr: *mut Array) {
36+
free((*arr).data);
37+
free(arr);
38+
}
39+
40+
unsafe fn element_ptr(arr: *mut Array, idx: usize) -> *mut i32 {
41+
(*arr).data.offset(idx)
42+
}
43+
44+
unsafe fn get(arr: *mut Array, idx: usize) -> i32 {
45+
let elt: *mut i32 = element_ptr(arr, idx);
46+
*elt
47+
}
48+
49+
unsafe fn set(arr: *mut Array, idx: usize, val: i32) {
50+
let elt: *mut i32 = element_ptr(arr, idx);
51+
*elt = val;
52+
}
53+
```
5454

5555
The analysis infers pointer permissions by observing how pointers are used, and
5656
applying the rules of the Rust reference model. For instance, the `set`
@@ -78,10 +78,12 @@ subject to a set of constraints. For example, here is the inferred polymorphic
7878
signature of `element_ptr`, with permission annotations written in comments
7979
(since there is no Rust syntax for them):
8080

81-
fn element_ptr /* <s0, s1> */ (arr: /* s0 */ *mut Array,
82-
idx: usize)
83-
-> /* s1 */ *mut i32
84-
/* where s1 <= s0 */;
81+
```rust
82+
fn element_ptr /* <s0, s1> */ (arr: /* s0 */ *mut Array,
83+
idx: usize)
84+
-> /* s1 */ *mut i32
85+
/* where s1 <= s0 */;
86+
```
8587

8688
The function has two permission parameters, `s0` and `s1`, which are the
8789
permissions of the argument and return pointers respectively. The signature
@@ -216,10 +218,12 @@ combination of outputs, it finds the least-restrictive valid assignment of
216218
permissions to the remaining (input) variables. For example, given this
217219
function:
218220

219-
fn element_ptr /* <s0, s1> */ (arr: /* s0 */ *mut Array,
220-
idx: usize)
221-
-> /* s1 */ *mut i32
222-
/* where s1 <= s0 */;
221+
```rust
222+
fn element_ptr /* <s0, s1> */ (arr: /* s0 */ *mut Array,
223+
idx: usize)
224+
-> /* s1 */ *mut i32
225+
/* where s1 <= s0 */;
226+
```
223227

224228
The only output variable is `s1`, which appears in the return type. The
225229
monomorphization step will try each assignment to `s1` that is allowed by the
@@ -237,15 +241,17 @@ and by similar logic records `READ, READ` as the final one.
237241
The next step of monomorphization is to select a monomorphic variant to call at
238242
each callsite of each monomorphized function. Given a pair of functions:
239243

240-
fn f /* <s0, s1> */ (arr: /* s0 */ *mut Array) -> /* s1 */ *mut i32
241-
/* where s1 <= s0 */ {
242-
g(arr)
243-
}
244+
```rust
245+
fn f /* <s0, s1> */ (arr: /* s0 */ *mut Array) -> /* s1 */ *mut i32
246+
/* where s1 <= s0 */ {
247+
g(arr)
248+
}
244249

245-
fn g /* <s0, s1> */ (arr: /* s0 */ *mut Array) -> /* s1 */ *mut i32
246-
/* where s1 <= s0 */ {
247-
...
248-
}
250+
fn g /* <s0, s1> */ (arr: /* s0 */ *mut Array) -> /* s1 */ *mut i32
251+
/* where s1 <= s0 */ {
252+
...
253+
}
254+
```
249255

250256
For pointer permissions to line up properly, a monomorphic variant of `f`
251257
specialized to `READ, READ` will need to call a variant of `g` also specialized
@@ -284,11 +290,12 @@ There are four annotation types currently supported by the ownership system.
284290
`MOVE`). The given permission values will be applied to the pointers in the
285291
static or field type, following a preorder traversal of the type. For
286292
example:
287-
288-
struct S {
289-
#[ownership_static(READ, WRITE, MOVE)]
290-
f: *mut (*mut u8, *mut u16)
291-
}
293+
```rust
294+
struct S {
295+
#[ownership_static(READ, WRITE, MOVE)]
296+
f: *mut (*mut u8, *mut u16)
297+
}
298+
```
292299

293300
Here the outermost pointer will be given permission `READ`, the pointer to
294301
`u8` will be given permission WRITE, and the pointer to `u16` will be given
@@ -310,10 +317,11 @@ There are four annotation types currently supported by the ownership system.
310317
numbered according to a preorder traversal of each node in the argument and
311318
return types of the function. This example shows location of each variable
312319
in a simple signature:
313-
314-
fn get_err(arr: /* _0 */ *mut Array,
315-
element_out: /* _1 */ *mut /* _2 */ *mut i32)
316-
-> /* _3 */ *const c_char;
320+
```rust
321+
fn get_err(arr: /* _0 */ *mut Array,
322+
element_out: /* _1 */ *mut /* _2 */ *mut i32)
323+
-> /* _3 */ *const c_char;
324+
```
317325

318326
* `#[ownership_mono(<suffix>, <perms>)]` supplies a monomorphic signature to be
319327
used for the annotated function. The `suffix` argument is a quoted string,
@@ -330,10 +338,11 @@ There are four annotation types currently supported by the ownership system.
330338
argument inference and later transformations.
331339

332340
Example:
333-
334-
#[ownership_mono("mut", WRITE, WRITE)]
335-
#[ownership_mono("", READ, READ)]
336-
fn first(arr: *mut Array) -> *mut i32;
341+
```rust
342+
#[ownership_mono("mut", WRITE, WRITE)]
343+
#[ownership_mono("", READ, READ)]
344+
fn first(arr: *mut Array) -> *mut i32;
345+
```
337346

338347
This function will have two monomorphic variants, one where both pointers'
339348
permission values are `WRITE` and one where both are `READ`. When the
@@ -357,18 +366,22 @@ another.
357366
358367
As a concrete example of the purpose of this feature, consider the following
359368
code:
369+
370+
```rust
371+
fn f(arr: *mut Array) -> *mut i32 { ... g(arr) ... }
360372
361-
fn f(arr: *mut Array) -> *mut i32 { ... g(arr) ... }
362-
363-
fn g(arr: *mut Array) -> *mut i32 { ... }
373+
fn g(arr: *mut Array) -> *mut i32 { ... }
374+
```
364375
365376
The user works first on (the module containing) `g`, resulting in splitting `g`
366377
into two variants:
367378
368-
fn f(arr: *mut Array) -> *mut i32 { ... g_mut(arr) ... }
379+
```rust
380+
fn f(arr: *mut Array) -> *mut i32 { ... g_mut(arr) ... }
369381
370-
fn g(arr: *mut Array) -> *mut i32 { ... }
371-
fn g_mut(arr: *mut Array) -> *mut i32 { ... }
382+
fn g(arr: *mut Array) -> *mut i32 { ... }
383+
fn g_mut(arr: *mut Array) -> *mut i32 { ... }
384+
```
372385
373386
Note that, because there is still only one variant of `f`, the transformation
374387
must choose a single `g` variant for `f` to call. In this case, it chose the
@@ -385,11 +398,13 @@ Treating `g` and `g_mut` as two variants of a single function allows the
385398
analysis to switch between `g` variants in the different variants of `f`,
386399
resulting in correct code like the following:
387400
388-
fn f(arr: *mut Array) -> *mut i32 { ... g(arr) ... }
389-
fn f_mut(arr: *mut Array) -> *mut i32 { ... g_mut(arr) ... }
401+
```rust
402+
fn f(arr: *mut Array) -> *mut i32 { ... g(arr) ... }
403+
fn f_mut(arr: *mut Array) -> *mut i32 { ... g_mut(arr) ... }
390404
391-
fn g(arr: *mut Array) -> *mut i32 { ... }
392-
fn g_mut(arr: *mut Array) -> *mut i32 { ... }
405+
fn g(arr: *mut Array) -> *mut i32 { ... }
406+
fn g_mut(arr: *mut Array) -> *mut i32 { ... }
407+
```
393408
394409
The `ownership_split_variants` automatically annotates the split functions so
395410
they will be combined into a variant group during further analysis. Variant
@@ -413,17 +428,21 @@ The analysis as described so far tries to mimic the Rust ownership model as
413428
implemented in the Rust compiler. However, collection data structures in Rust
414429
often use unsafe code to bypass parts of the ownership model. A particularly
415430
common case is in removal methods, such as `Vec::pop`:
416-
417-
impl<T> Vec<T> {
418-
fn pop(&mut self) -> Option<T> { ... }
419-
}
431+
432+
```rust
433+
impl<T> Vec<T> {
434+
fn pop(&mut self) -> Option<T> { ... }
435+
}
436+
```
420437
421438
This method moves a `T` out of `self`'s internal storage, but only takes `self`
422439
by mutable reference. Under the "normal" rules, this is impossible, and the
423440
analysis described above will infer a stricter signature for the raw pointer
424441
equivalent:
425-
426-
fn pop(this: /* MOVE */ *mut Vec) -> /* MOVE */ *mut c_void { ... }
442+
443+
```rust
444+
fn pop(this: /* MOVE */ *mut Vec) -> /* MOVE */ *mut c_void { ... }
445+
```
427446

428447
The analysis as implemented includes a small adjustment (the "collection hack")
429448
to let it infer the correct signature for such methods.
@@ -434,5 +453,7 @@ the LHS, we constraint it to be at least `min(lhs_perm, WRITE)`. The result is
434453
that it becomes possible to move a `MOVE` pointer out of a struct when only
435454
`WRITE` permission is available for the pointer to that struct. Then the
436455
analysis will infer the correct type for `pop`:
437-
438-
fn pop(this: /* WRITE */ *mut Vec) -> /* MOVE */ *mut c_void { ... }
456+
457+
```rust
458+
fn pop(this: /* WRITE */ *mut Vec) -> /* MOVE */ *mut c_void { ... }
459+
```

0 commit comments

Comments
 (0)