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
184
185
186
187
|
open Identifiers
open Types
open Values
open Expressions
module FunDeclId = IdGen ()
type var = {
index : VarId.id; (** Unique variable identifier *)
name : string option;
var_ty : ety;
(** The variable type - erased type, because variables are not used
** in function signatures: they are only used to declare the list of
** variables manipulated by a function body *)
}
[@@deriving show]
(** A variable, as used in a function definition *)
type assumed_fun_id =
| Replace (** `core::mem::replace` *)
| BoxNew
| BoxDeref (** `core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref` *)
| BoxDerefMut
(** `core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut` *)
| BoxFree
| VecNew
| VecPush
| VecInsert
| VecLen
| VecIndex (** `core::ops::index::Index::index<alloc::vec::Vec<T>, usize>` *)
| VecIndexMut
(** `core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>` *)
[@@deriving show, ord]
type fun_id = Local of FunDeclId.id | Assumed of assumed_fun_id
[@@deriving show, ord]
type assertion = { cond : operand; expected : bool } [@@deriving show]
type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
[@@deriving show]
type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups
[@@deriving show]
type fun_sig = {
region_params : region_var list;
num_early_bound_regions : int;
regions_hierarchy : region_var_groups;
type_params : type_var list;
inputs : sty list;
output : sty;
}
[@@deriving show]
(** A function signature, as used when declaring functions *)
type inst_fun_sig = {
regions_hierarchy : abs_region_groups;
inputs : rty list;
output : rty;
}
[@@deriving show]
(** A function signature, after instantiation *)
type call = {
func : fun_id;
region_params : erased_region list;
type_params : ety list;
args : operand list;
dest : place;
}
[@@deriving show]
(** Ancestor for [typed_value] iter visitor *)
class ['self] iter_statement_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
method visit_place : 'env -> place -> unit = fun _ _ -> ()
method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
method visit_call : 'env -> call -> unit = fun _ _ -> ()
method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
end
(** Ancestor for [typed_value] map visitor *)
class ['self] map_statement_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
method visit_place : 'env -> place -> place = fun _ x -> x
method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
method visit_operand : 'env -> operand -> operand = fun _ x -> x
method visit_call : 'env -> call -> call = fun _ x -> x
method visit_integer_type : 'env -> integer_type -> integer_type =
fun _ x -> x
method visit_scalar_value : 'env -> scalar_value -> scalar_value =
fun _ x -> x
end
type statement =
| Assign of place * rvalue
| FakeRead of place
| SetDiscriminant of place * VariantId.id
| Drop of place
| Assert of assertion
| Call of call
| Panic
| Return
| Break of int
(** Break to (outer) loop. The [int] identifies the loop to break to:
* 0: break to the first outer loop (the current loop)
* 1: break to the second outer loop
* ...
*)
| Continue of int
(** Continue to (outer) loop. The loop identifier works
the same way as for [Break] *)
| Nop
| Sequence of statement * statement
| Switch of operand * switch_targets
| Loop of statement
and switch_targets =
| If of statement * statement (** Gives the "if" and "else" blocks *)
| SwitchInt of integer_type * (scalar_value list * statement) list * statement
(** The targets for a switch over an integer are:
- the list `(matched values, statement to execute)`
We need a list for the matched values in case we do something like this:
`switch n { 0 | 1 => ..., _ => ... }
- the "otherwise" statement
Also note that we precise the type of the integer (uint32, int64, etc.)
which we switch on. *)
[@@deriving
show,
visitors
{
name = "iter_statement";
variety = "iter";
ancestors = [ "iter_statement_base" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
concrete = true;
},
visitors
{
name = "map_statement";
variety = "map";
ancestors = [ "map_statement_base" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
concrete = true;
}]
type fun_decl = {
def_id : FunDeclId.id;
name : fun_name;
signature : fun_sig;
arg_count : int;
locals : var list;
body : statement;
}
[@@deriving show]
(** TODO: function definitions (and maybe type definitions in the future)
* contain information like `divergent`. I wonder if this information should
* be stored directly inside the definitions or inside separate maps/sets.
* Of course, if everything is stored in separate maps/sets, nothing
* prevents us from computing this info in Charon (and thus exporting directly
* it with the type/function defs), in which case we just have to implement special
* treatment when deserializing, to move the info to a separate map. *)
|
