summaryrefslogtreecommitdiff
path: root/src/ValuesUtils.ml
blob: 2814615cf93ebfbc975b9f07d44be3ec87cdc676 (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
open Utils
open TypesUtils
open Types
open Values
module TA = TypesAnalysis

exception FoundSymbolicValue of symbolic_value
(** Utility exception *)

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

let mk_typed_value (ty : ety) (value : value) : typed_value = { value; ty }

let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }

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

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

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

let as_symbolic (v : value) : symbolic_value =
  match v with Symbolic s -> s | _ -> failwith "Unexpected"

let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value =
  match v.value with
  | Borrow (MutBorrow (bid, bv)) -> (bid, bv)
  | _ -> failwith "Unexpected"

(** Check if a value contains a borrow *)
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 inactivated mutable borrows *)
let inactivated_in_value (v : typed_value) : bool =
  let obj =
    object
      inherit [_] iter_typed_value

      method! visit_InactivatedMutBorrow _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 *)
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 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 _ _ = ()
    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 : TA.type_infos)
    (v : typed_value) : symbolic_value option =
  (* The visitor *)
  let obj =
    object
      inherit [_] iter_typed_value

      method! visit_Symbolic _ 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
  | Loan (SharedLoan (_, v')) -> value_strip_shared_loans v'
  | _ -> v