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
|
open Identifiers
open Types
open Values
open Expressions
module FunDefId = IdGen ()
module RegionGroupId = 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 = BoxNew | BoxDeref | BoxDerefMut | BoxFree
[@@deriving show]
type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
[@@deriving show]
type assertion = { cond : operand; expected : bool } [@@deriving show]
type ('id, 'r) g_region_group = {
id : 'id;
regions : 'r list;
parents : 'id list;
}
[@@deriving show]
(** A group of regions.
Results from a lifetime analysis: we group the regions with the same
lifetime together, and compute the hierarchy between the regions.
This is necessary to introduce the proper abstraction with the
proper constraints, when evaluating a function call in symbolic mode.
*)
type ('r, 'id) g_region_groups = ('r, 'id) g_region_group list [@@deriving show]
type region_var_group = (RegionGroupId.id, RegionVarId.id) g_region_group
[@@deriving show]
type region_var_groups = (RegionGroupId.id, RegionVarId.id) g_region_groups
[@@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]
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
[@@deriving show]
and switch_targets =
| If of statement * statement (** Gives the "if" and "else" blocks *)
| SwitchInt of integer_type * (scalar_value * statement) list * statement
(** The targets for a switch over an integer are:
- the list `(matched value, statement to execute)`
- the "otherwise" statement.
Also note that we precise the type of the integer (uint32, int64, etc.)
which we switch on. *)
[@@deriving show]
type fun_def = {
def_id : FunDefId.id;
name : name;
signature : fun_sig;
divergent : bool;
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. *)
|
