summaryrefslogtreecommitdiff
path: root/compiler/ValuesUtils.ml
blob: 9c4b8b45f242f6f6e47ad461616f9386929bc0f5 (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
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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
open Utils
open TypesUtils
open Types
open Values
open Errors
include Charon.ValuesUtils

(** Utility exception *)
exception FoundSymbolicValue of symbolic_value

let mk_unit_value : typed_value =
  { value = VAdt { variant_id = None; field_values = [] }; ty = mk_unit_ty }

let mk_typed_value (meta : Meta.meta) (ty : ty) (value : value) : typed_value =
  sanity_check (ty_is_ety ty) meta;
  { value; ty }

let mk_typed_avalue (meta : Meta.meta) (ty : ty) (value : avalue) : typed_avalue =
  sanity_check (ty_is_rty ty) meta;
  { value; ty }

let mk_bottom (meta : Meta.meta) (ty : ty) : typed_value =
  sanity_check (ty_is_ety ty) meta;
  { value = VBottom; ty }

let mk_abottom (meta : Meta.meta) (ty : ty) : typed_avalue =
  sanity_check (ty_is_rty ty) meta;
  { value = ABottom; ty }

let mk_aignored (meta : Meta.meta) (ty : ty) : typed_avalue =
  sanity_check (ty_is_rty ty) meta;
  { value = AIgnored; ty }

let value_as_symbolic (meta : Meta.meta) (v : value) : symbolic_value =
  match v with VSymbolic v -> v | _ -> craise meta "Unexpected"

(** Box a value *)
let mk_box_value (meta : Meta.meta) (v : typed_value) : typed_value =
  let box_ty = mk_box_ty v.ty in
  let box_v = VAdt { variant_id = None; field_values = [ v ] } in
  mk_typed_value meta box_ty box_v

let is_bottom (v : value) : bool = match v with VBottom -> true | _ -> false

let is_aignored (v : avalue) : bool =
  match v with AIgnored -> true | _ -> false

let is_symbolic (v : value) : bool =
  match v with VSymbolic _ -> true | _ -> false

let as_symbolic (meta : Meta.meta) (v : value) : symbolic_value =
  match v with VSymbolic s -> s | _ -> craise meta "Unexpected"

let as_mut_borrow (meta : Meta.meta) (v : typed_value) : BorrowId.id * typed_value =
  match v.value with
  | VBorrow (VMutBorrow (bid, bv)) -> (bid, bv)
  | _ -> craise meta "Unexpected"

let is_unit (v : typed_value) : bool =
  ty_is_unit v.ty
  &&
  match v.value with
  | VAdt av -> av.variant_id = None && av.field_values = []
  | _ -> false

(** Check if a value contains a *concrete* borrow (i.e., a [Borrow] value -
    we don't check if there are borrows hidden in symbolic values).
 *)
let borrows_in_value (v : typed_value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_borrow_content _env _ = raise Found
    end
  in
  (* We use exceptions *)
  try
    obj#visit_typed_value () v;
    false
  with Found -> true

(** Check if a value contains reserved mutable borrows (which are necessarily
    *concrete*: a symbolic value can't "hide" reserved borrows).
 *)
let reserved_in_value (v : typed_value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_VReservedMutBorrow _env _ = raise Found
    end
  in
  (* We use exceptions *)
  try
    obj#visit_typed_value () v;
    false
  with Found -> true

(** Check if a value contains a loan (which is necessarily *concrete*: symbolic
    values can't "hide" loans).
 *)
let loans_in_value (v : typed_value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_loan_content _env _ = raise Found
    end
  in
  (* We use exceptions *)
  try
    obj#visit_typed_value () v;
    false
  with Found -> true

(** Check if a value contains concrete borrows or loans *)
let concrete_borrows_loans_in_value (v : typed_value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_borrow_content _env _ = raise Found
      method! visit_loan_content _env _ = raise Found
    end
  in
  (* We use exceptions *)
  try
    obj#visit_typed_value () v;
    false
  with Found -> true

(** Check if a value contains outer loans (i.e., loans which are not in borrwed
    values. *)
let outer_loans_in_value (v : typed_value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_loan_content _env _ = raise Found

      method! visit_borrow_content _ _ =
        (* Do nothing so as *not to dive* in borrowed values *) ()
    end
  in
  (* We use exceptions *)
  try
    obj#visit_typed_value () v;
    false
  with Found -> true

let find_first_primitively_copyable_sv_with_borrows
    (type_infos : TypesAnalysis.type_infos) (v : typed_value) :
    symbolic_value option =
  (* The visitor *)
  let obj =
    object
      inherit [_] iter_typed_value

      method! visit_VSymbolic _ sv =
        let ty = sv.sv_ty in
        if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
          raise (FoundSymbolicValue sv)
        else ()
    end
  in
  (* Small helper *)
  try
    obj#visit_typed_value () v;
    None
  with FoundSymbolicValue sv -> Some sv

(** Strip the outer shared loans in a value.
    Ex.:
    [shared_loan {l0, l1} (3 : u32, shared_loan {l2} (4 : u32))] ~~>
    [(3 : u32, shared_loan {l2} (4 : u32))]
 *)
let rec value_strip_shared_loans (v : typed_value) : typed_value =
  match v.value with
  | VLoan (VSharedLoan (_, v')) -> value_strip_shared_loans v'
  | _ -> v

(** Check if a symbolic value has borrows *)
let symbolic_value_has_borrows (infos : TypesAnalysis.type_infos)
    (sv : symbolic_value) : bool =
  ty_has_borrows infos sv.sv_ty

(** Check if a value has borrows in **a general sense**.

    It checks if:
    - there are concrete borrows
    - there are symbolic values which may contain borrows
 *)
let value_has_borrows (infos : TypesAnalysis.type_infos) (v : value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_borrow_content _env _ = raise Found

      method! visit_symbolic_value _ sv =
        if symbolic_value_has_borrows infos sv then raise Found else ()
    end
  in
  (* We use exceptions *)
  try
    obj#visit_value () v;
    false
  with Found -> true

(** Check if a value has loans.

    Note that loans are necessarily concrete (there can't be loans hidden
    inside symbolic values).
 *)
let value_has_loans (v : value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_loan_content _env _ = raise Found
    end
  in
  (* We use exceptions *)
  try
    obj#visit_value () v;
    false
  with Found -> true

(** Check if a value has loans or borrows in **a general sense**.

    It checks if:
    - there are concrete loans or concrete borrows
    - there are symbolic values which may contain borrows (symbolic values
      can't contain loans).
 *)
let value_has_loans_or_borrows (infos : TypesAnalysis.type_infos) (v : value) :
    bool =
  let obj =
    object
      inherit [_] iter_typed_value
      method! visit_borrow_content _env _ = raise Found
      method! visit_loan_content _env _ = raise Found

      method! visit_symbolic_value _ sv =
        if ty_has_borrow_under_mut infos sv.sv_ty then raise Found else ()
    end
  in
  (* We use exceptions *)
  try
    obj#visit_value () v;
    false
  with Found -> true

(** Remove the shared loans in a value *)
let value_remove_shared_loans (v : typed_value) : typed_value =
  let visitor =
    object (self : 'self)
      inherit [_] map_typed_value as super

      method! visit_typed_value env v =
        match v.value with
        | VLoan (VSharedLoan (_, sv)) -> self#visit_typed_value env sv
        | _ -> super#visit_typed_value env v
    end
  in
  visitor#visit_typed_value () v