vstd_extra/
ptr_extra.rs

1use vstd::prelude::*;
2
3use vstd::simple_pptr::*;
4
5verus! {
6
7#[macro_export]
8macro_rules! borrow_field {
9    ($ptr:expr) => { $ptr };
10    ($ptr:expr => $field:tt, $perm:expr) => {
11        verus_exec_expr!(
12            $ptr.borrow(Tracked($perm)).$field
13    )};
14    ($ptr:expr => $field1:tt . $field2:tt, $perm:expr) => {
15        verus_exec_expr!(
16            $ptr.borrow(Tracked($perm)).$field1.$field2
17    )};
18}
19
20#[macro_export]
21macro_rules! update_field {
22    ($ptr:expr => $field:tt <- $val:expr; $set:expr , $idx:expr) => {
23        verus_exec_expr!(
24        {
25            let tracked mut __own = $set.tracked_remove($idx);
26            let mut __tmp = $ptr.take(Tracked(&mut __own));
27            __tmp.$field = $val;
28            $ptr.put(Tracked(&mut __own), __tmp);
29            proof { $set.tracked_insert($idx, __own); }
30        })
31    };
32    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $set:expr , $idx:expr) => {
33        verus_exec_expr!(
34        {
35            let tracked mut __own = $set.tracked_remove($idx);
36            let mut __tmp = $ptr.take(Tracked(&mut __own));
37            __tmp.$field1.$field2 = $val;
38            $ptr.put(Tracked(&mut __own), __tmp);
39            proof { $set.tracked_insert($idx, __own); }
40        })
41    };
42    ($ptr:expr => $field:tt <- $val:expr; $set:expr , $idx:expr, inner) => {
43        verus_exec_expr!(
44        {
45            let tracked mut __own = $set.tracked_remove($idx);
46            let mut __tmp = $ptr.take(Tracked(&mut __own));
47            __tmp.$field = $val;
48            $ptr.put(Tracked(&mut __own.points_to), __tmp);
49            proof { $set.tracked_insert($idx, __own); }
50        })
51    };
52    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $set:expr , $idx:expr, inner) => {
53        verus_exec_expr!(
54        {
55            let tracked mut __own = $set.tracked_remove($idx);
56            let mut __tmp = $ptr.take(Tracked(&mut __own));
57            __tmp.$field1.$field2 = $val;
58            $ptr.put(Tracked(&mut __own.points_to), __tmp);
59            proof { $set.tracked_insert($idx, __own); }
60        })
61    };
62    ($ptr:expr => $field:tt <- $val:expr; $perm:expr) => {
63        verus_exec_expr!(
64        {
65            let mut __tmp = $ptr.take(Tracked(&mut $perm));
66            __tmp.$field = $val;
67            $ptr.put(Tracked(&mut $perm), __tmp);
68        })
69    };
70    ($ptr:expr => $field1:tt . $field2:tt <- $val:expr; $perm:expr) => {
71        verus_exec_expr!(
72        {
73            let mut __tmp = $ptr.take(Tracked(&mut $perm));
74            __tmp.$field1.$field2 = $val;
75            $ptr.put(Tracked(&mut $perm), __tmp);
76        })
77    };
78    ($ptr:expr => $field:tt += $val:expr; $perm:expr) => {
79        verus_exec_expr!(
80        {
81            let mut __tmp = $ptr.take(Tracked(&mut $perm));
82            __tmp.$field = __tmp.$field + $val;
83            $ptr.put(Tracked(&mut $perm), __tmp);
84        })
85    };
86    ($ptr:expr => $field:tt -= $val:expr; $perm:expr) => {
87        verus_exec_expr!(
88        {
89            let mut __tmp = $ptr.take(Tracked(&mut $perm));
90            __tmp.$field = __tmp.$field - $val;
91            $ptr.put(Tracked(&mut $perm), __tmp);
92        })
93    }
94}
95
96} // verus!
97pub use {borrow_field, update_field};
vstd_extra/ptr_extra.rs

vstd_extra/
ptr_extra.rs
