blob: 250cd2230704b45687f523e4b4ec5700aca6a4b0 (
plain)
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
|
open Identifiers
open Types
open Values
open Expressions
module FunDefId = 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 fun_sig = {
region_params : region_var list;
num_early_bound_regions : int;
type_params : type_var list;
inputs : sty list;
output : sty;
}
[@@deriving show]
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. *)
|
