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
206
|
open Names
open Types
open Values
open Expressions
open Identifiers
module FunDeclId = IdGen ()
module GlobalDeclId = IdGen ()
(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
type global_id_converter = { fun_count : int }
[@@deriving show]
(** Converts a global id to its corresponding function id.
To do so, it adds the global id to the number of function declarations :
We have the bijection `global_id <=> fun_id + fun_id_count`.
*)
let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id =
FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count)
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 = Regular of FunDeclId.id | Assumed of assumed_fun_id
[@@deriving show, ord]
type assign_global = {
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]
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_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_assign_global : 'env -> assign_global -> 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_assign_global : 'env -> assign_global -> assign_global = 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 =
| Assign of place * rvalue
| AssignGlobal of assign_global
| 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 = { arg_count : int; locals : var list; body : statement }
[@@deriving show]
type fun_decl = {
def_id : FunDeclId.id;
name : fun_name;
signature : fun_sig;
body : fun_body option;
is_global : bool;
}
[@@deriving show]
|
