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
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
|
open Names
open Types
open Values
open Expressions
open Identifiers
module FunDeclId = IdGen ()
module GlobalDeclId = IdGen ()
open Meta
(** A variable, as used in a function definition *)
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]
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 = Regular of FunDeclId.id | Assumed of assumed_fun_id
[@@deriving show, ord]
type global_assignment = { dst : VarId.id; global : GlobalDeclId.id }
[@@deriving show]
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]
(** A function signature, as used when declaring functions *)
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, after instantiation *)
type inst_fun_sig = {
regions_hierarchy : abs_region_groups;
inputs : rty list;
output : rty;
}
[@@deriving show]
type call = {
func : fun_id;
region_args : erased_region list;
type_args : 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_global_assignment : 'env -> global_assignment -> unit =
fun _ _ -> ()
method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
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_global_assignment
: 'env -> global_assignment -> global_assignment =
fun _ x -> x
method visit_meta : 'env -> meta -> meta = fun _ x -> x
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 = {
meta : meta; (** The statement meta-data *)
content : raw_statement; (** The statement itself *)
}
and raw_statement =
| Assign of place * rvalue
| AssignGlobal of global_assignment
| 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_body = {
meta : meta;
arg_count : int;
locals : var list;
body : statement;
}
[@@deriving show]
type fun_decl = {
def_id : FunDeclId.id;
meta : meta;
name : fun_name;
signature : fun_sig;
body : fun_body option;
is_global_decl_body : bool;
}
[@@deriving show]
type global_decl = {
def_id : GlobalDeclId.id;
meta : meta;
body_id : FunDeclId.id;
name : global_name;
ty : ety;
}
[@@deriving show]
|
