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
|
open Errors
module T = Types
module V = Values
module E = Expressions
module A = CfimAst
open SymbolicAst
open ValuesUtils
open InterpreterUtils
type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's
type ended_loan = (V.mvalue, V.mvalue list) ended
type ended_borrow = (V.mvalue, V.mvalue) ended
type ended_loan_or_borrow =
| EndedLoan of ended_loan
| EndedBorrow of ended_borrow
(** Return the list of the meta-values given to the top owned ended mutable
loans/borrows of an abstraction
We expect an abstraction where all the loans/borrows have ended.
*)
let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list
=
(* The accumulator *)
let acc = ref [] in
let add x = acc := x :: !acc in
let add_loan x = add (EndedLoan x) in
let add_borrow x = add (EndedBorrow x) in
let add_sloan x = add_loan (EndedSymbolic x) in
let add_cloan x = add_loan (EndedConcrete x) in
let add_sborrow x = add_borrow (EndedSymbolic x) in
let add_cborrow x = add_borrow (EndedConcrete x) in
(* The visitor *)
let obj =
object
inherit [_] V.iter_abs as super
method! visit_aproj env aproj =
match aproj with
| AEndedProjLoans (msv, []) ->
(* The symbolic value was left unchanged *)
add_sloan [ mk_typed_value_from_symbolic_value msv ]
| AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl)
| AEndedProjBorrows mv -> add_sborrow mv
| AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
failwith "Unreachable"
method! visit_aloan_content env lc =
match lc with
| AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable"
| AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
(* Add the meta-value and stop the exploration *)
add_cloan given_back_meta
| AEndedSharedLoan (_, _) ->
(* We don't dive into shared loans: there is nothing to give back
* inside (note that there could be a mutable borrow in the shared
* value, pointing to a mutable loan in the child avalue, but this
* borrow is in practice immutable *)
()
| AIgnoredMutLoan (_, _) ->
(* There can be *inner* mutable loans, but not outer ones *)
failwith "Unreachable"
| AEndedIgnoredMutLoan _ ->
(* Dive in *)
super#visit_aloan_content env lc
| AIgnoredSharedLoan _ ->
(* Ignore *)
()
method! visit_aborrow_content env bc =
match bc with
| AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
failwith "Unreachable"
| AEndedMutBorrow (mv, _) ->
(* Add the meta-value and stop the exploration *)
add_cborrow mv
| AEndedIgnoredMutBorrow _ ->
(* Dive in *)
super#visit_aborrow_content env bc
| AProjSharedBorrow _ ->
(* Ignore *)
()
end
in
(* Apply *)
obj#visit_abs () abs;
(* Return the accumulated values *)
List.rev !acc
|
