1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
//@ skip
//@ charon-args=--no-code-duplication
//! This module contains functions with nested borrows in their signatures.
pub fn id_mut_mut<'a, 'b, T>(x: &'a mut &'b mut T) -> &'a mut &'b mut T {
x
}
pub fn id_mut_pair<'a, T>(x: &'a mut (&'a mut T, u32)) -> &'a mut (&'a mut T, u32) {
x
}
pub fn id_mut_pair_test1() {
let mut x: u32 = 0;
let px = &mut x;
let mut p = (px, 1);
let pp0 = &mut p;
let pp1 = id_mut_pair(pp0);
let mut y = 2;
*pp1 = (&mut y, 3);
}
pub fn id_mut_mut_pair<'a, T>(
x: &'a mut &'a mut (&'a mut T, u32),
) -> &'a mut &'a mut (&'a mut T, u32) {
x
}
pub fn id_mut_mut_mut_same<'a, T>(x: &'a mut &'a mut &'a mut u32) -> &'a mut &'a mut &'a mut u32 {
x
}
pub fn id_borrow1<'a, 'b, 'c>(_x: &'a mut &'b u32, _y: &'a &'a mut u32) {
()
}
/// For symbolic execution: testing what happens with several abstractions.
pub fn id_mut_mut_test1() {
let mut x = 0;
let mut px = &mut x;
let ppx = &mut px;
let ppy = id_mut_mut(ppx);
**ppy = 1;
// Ending one abstraction
assert!(*px == 1);
// Ending the other abstraction
assert!(x == 1);
}
/*
/// For symbolic execution: testing what happens with several abstractions.
/// This case is a bit trickier, because we modify the borrow graph through
/// a value returned by a function call.
/// TODO: not supported! We overwrite a borrow in a returned value.
pub fn id_mut_mut_test2() {
let mut x = 0;
let mut px = &mut x;
let ppx = &mut px;
let ppy = id_mut_mut(ppx);
**ppy = 1;
// This time, we replace one of the borrows
let mut y = 2;
let py = &mut y;
*ppy = py;
// Ending one abstraction
assert!(*px == 2);
*px = 3;
// Ending the other abstraction
assert!(x == 1);
assert!(y == 3);
}
*/
/*
/// For symbolic execution: testing what happens with several abstractions.
/// See what happens when chaining function calls.
/// TODO: not supported! We overwrite a borrow in a returned value.
pub fn id_mut_mut_test3() {
let mut x = 0;
let mut px = &mut x;
let ppx = &mut px;
let ppy = id_mut_mut(ppx); // &'a mut &'b mut i32
**ppy = 1;
let ppz = id_mut_mut(ppy); // &'c mut &'b mut i32
**ppz = 2;
// End 'a and 'c
assert!(*px == 2);
// End 'b (2 abstractions at once)
assert!(x == 2);
}*/
/*
/// For symbolic execution: testing what happens with several abstractions.
/// See what happens when chaining function calls.
/// This one is slightly more complex than the previous one.
pub fn id_mut_mut_test4() {
let mut x = 0;
let mut px = &mut x;
let ppx = &mut px;
let ppy = id_mut_mut(ppx); // &'a mut &'b mut i32
**ppy = 1;
let ppz = id_mut_mut(ppy); // &'c mut &'b mut i32
**ppz = 2;
// End 'c
assert!(**ppy == 2);
// End 'a
assert!(*px == 2);
// End 'b (2 abstractions at once)
assert!(x == 2);
}
*/
fn id<'a, T>(x: &'a mut T) -> &'a mut T {
x
}
/// Checking projectors over symbolic values
pub fn test_borrows1() {
let mut x = 3;
let y = id(&mut x);
let z = id(y);
// We do not write a statement which would expand `z` on purpose:
// we want to test that the handling of non-expanded symbolic values
// is correct
assert!(x == 3);
}
fn id_pair<'a, 'b, T>(x: &'a mut T, y: &'b mut T) -> (&'a mut T, &'b mut T) {
(x, y)
}
/// Similar to the previous one
pub fn test_borrows2() {
let mut x = 3;
let mut y = 4;
let z = id_pair(&mut x, &mut y);
// We do not write a statement which would expand `z` on purpose:
// we want to test that the handling of non-expanded symbolic values
// is correct
assert!(x == 3);
assert!(y == 4);
}
/// input type: 'b must last longer than 'a
/// output type: 'a must last longer than 'b
/// So: 'a = 'b, and the function is legal.
pub fn nested_mut_borrows1<'a, 'b>(x: &'a mut &'b mut u32) -> &'b mut &'a mut u32 {
x
}
pub fn nested_shared_borrows1<'a, 'b>(x: &'a &'b u32) -> &'a &'b u32 {
x
}
pub fn nested_borrows1<'a, 'b>(x: &'a mut &'b u32) -> &'a mut &'b u32 {
x
}
pub fn nested_borrows2<'a, 'b>(x: &'a &'b mut u32) -> &'a &'b mut u32 {
x
}
fn nested_borrows1_test1() {
let x = 0;
let mut px = &x;
let ppx = &mut px;
let ppy = nested_borrows1(ppx);
assert!(**ppy == 0);
assert!(x == 0);
}
fn nested_borrows1_test2<'a, 'b>(x: &'a mut &'b u32) -> &'a mut &'b u32 {
nested_borrows1(x)
}
fn nested_borrows2_test1() {
let mut x = 0;
let px = &mut x;
let ppx = &px;
let ppy = nested_borrows2(ppx);
assert!(**ppy == 0);
assert!(x == 0);
}
|
