summaryrefslogtreecommitdiff
path: root/compiler/Assumed.ml
blob: aa0cfccf31ba517c87fd8eb14bee9cae48cb1b03 (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
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
(** This module contains various utilities for the assumed functions.

    Note that [Box::free] is peculiar: we don't really handle it as a function,
    because it is legal to free a box whose boxed value is [⊥] (it often
    happens that we move a value out of a box before freeing this box).
    Semantically speaking, we thus handle [Box::free] as a value drop and
    not as a function call, and thus never need its signature.
    
    TODO: implementing the concrete evaluation functions for the
    assumed functions is really annoying (see
    [InterpreterStatements.eval_non_local_function_call_concrete]),
    I think it should be possible, in most situations, to write bodies which
    model the behaviour of those unsafe functions. For instance, [Box::deref_mut]
    should simply be:
    {[
      fn deref_mut<'a, T>(x : &'a mut Box<T>) -> &'a mut T {
        &mut ( *x ) // box dereferencement is a primitive operation
      }
    ]}
    
    For vectors, we could "cheat" by using the index as a field index (vectors
    would be encoded as ADTs with a variable number of fields). Of course, it
    would require a bit of engineering, but it would probably be quite lightweight
    in the end.
    {[
      Vec::get_mut<'a,T>(v : &'a mut Vec<T>, i : usize) -> &'a mut T {
        &mut ( ( *x ).i )
      }
    ]}
 *)

open Names
open TypesUtils
module T = Types
module A = LlbcAst

module Sig = struct
  (** A few utilities *)

  let rvar_id_0 = T.RegionId.of_int 0
  let rvar_0 : T.region = T.RVar rvar_id_0
  let rg_id_0 = T.RegionGroupId.of_int 0
  let tvar_id_0 = T.TypeVarId.of_int 0
  let tvar_0 : T.ty = T.TVar tvar_id_0
  let cgvar_id_0 = T.ConstGenericVarId.of_int 0
  let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0

  (** Region 'a of id 0 *)
  let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" }

  (** Region group: [{ parent={}; regions:{'a of id 0} }] *)
  let region_group_0 : T.region_group =
    { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] }

  (** Type parameter [T] of id 0 *)
  let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" }

  let usize_ty : T.ty = T.TLiteral (TInteger Usize)

  (** Const generic parameter [const N : usize] of id 0 *)
  let cg_param_0 : T.const_generic_var =
    { T.index = cgvar_id_0; name = "N"; ty = TInteger Usize }

  let empty_const_generic_params : T.const_generic_var list = []

  let mk_generic_args regions types const_generics : T.generic_args =
    { regions; types; const_generics; trait_refs = [] }

  let mk_generic_params regions types const_generics : T.generic_params =
    { regions; types; const_generics; trait_clauses = [] }

  let mk_ref_ty (r : T.region) (ty : T.ty) (is_mut : bool) : T.ty =
    let ref_kind = if is_mut then T.Mut else T.Shared in
    mk_ref_ty r ty ref_kind

  let mk_array_ty (ty : T.ty) (cg : T.const_generic) : T.ty =
    TAdt (TAssumed TArray, mk_generic_args [] [ ty ] [ cg ])

  let mk_slice_ty (ty : T.ty) : T.ty =
    TAdt (TAssumed TSlice, mk_generic_args [] [ ty ] [])

  let mk_sig generics inputs output : A.fun_sig =
    let preds : T.predicates =
      { regions_outlive = []; types_outlive = []; trait_type_constraints = [] }
    in
    {
      is_unsafe = false;
      generics;
      preds;
      parent_params_info = None;
      inputs;
      output;
    }

  (** [fn<T>(T) -> Box<T>] *)
  let box_new_sig : A.fun_sig =
    let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
    let inputs = [ tvar_0 (* T *) ] in
    let output = mk_box_ty tvar_0 (* Box<T> *) in
    mk_sig generics inputs output

  (** [fn<T>(Box<T>) -> ()] *)
  let box_free_sig : A.fun_sig =
    let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
    let inputs = [ mk_box_ty tvar_0 (* Box<T> *) ] in
    let output = mk_unit_ty (* () *) in
    mk_sig generics inputs output

  (** Array/slice functions *)

  (** Small helper.

      Return the type:
      {[
        fn<'a, T>(&'a input_ty, index_ty) -> &'a output_ty
      ]}

      Remarks:
      The [input_ty] and [output_ty] are parameterized by a type variable id.
      The [mut_borrow] boolean controls whether we use a shared or a mutable
      borrow.
   *)
  let mk_array_slice_borrow_sig (cgs : T.const_generic_var list)
      (input_ty : T.TypeVarId.id -> T.ty) (index_ty : T.ty option)
      (output_ty : T.TypeVarId.id -> T.ty) (is_mut : bool) : A.fun_sig =
    let generics =
      mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *)
    in
    let inputs =
      [
        mk_ref_ty rvar_0
          (input_ty type_param_0.index)
          is_mut (* &'a (mut) input_ty<T> *);
      ]
    in
    let inputs =
      List.append inputs (match index_ty with None -> [] | Some ty -> [ ty ])
    in
    let output =
      mk_ref_ty rvar_0
        (output_ty type_param_0.index)
        is_mut (* &'a (mut) output_ty<T> *)
    in
    mk_sig generics inputs output

  let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig =
    (* Array<T, N> *)
    let input_ty id =
      if is_array then mk_array_ty (T.TVar id) cgvar_0
      else mk_slice_ty (T.TVar id)
    in
    (* usize *)
    let index_ty = usize_ty in
    (* T *)
    let output_ty id = T.TVar id in
    let cgs = if is_array then [ cg_param_0 ] else [] in
    mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut

  let array_index_sig (is_mut : bool) = mk_array_slice_index_sig true is_mut
  let slice_index_sig (is_mut : bool) = mk_array_slice_index_sig false is_mut

  let array_to_slice_sig (is_mut : bool) : A.fun_sig =
    (* Array<T, N> *)
    let input_ty id = mk_array_ty (T.TVar id) cgvar_0 in
    (* Slice<T> *)
    let output_ty id = mk_slice_ty (T.TVar id) in
    let cgs = [ cg_param_0 ] in
    mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut

  let array_repeat_sig =
    let generics =
      (* <T, N> *)
      mk_generic_params [] [ type_param_0 ] [ cg_param_0 ]
    in
    let inputs = [ tvar_0 (* T *) ] in
    let output =
      (* [T; N] *)
      mk_array_ty tvar_0 cgvar_0
    in
    mk_sig generics inputs output

  (** Helper:
      [fn<T>(&'a [T]) -> usize]
   *)
  let slice_len_sig : A.fun_sig =
    let generics =
      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
    in
    let inputs =
      [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ]
    in
    let output = mk_usize_ty (* usize *) in
    mk_sig generics inputs output
end

type raw_assumed_fun_info =
  A.assumed_fun_id * A.fun_sig * bool * name * bool list option

type assumed_fun_info = {
  fun_id : A.assumed_fun_id;
  fun_sig : A.fun_sig;
  can_fail : bool;
  name : name;
  keep_types : bool list option;
      (** We may want to filter some type arguments.

          For instance, all the `Vec` functions (and the `Vec` type itself) take
          an `Allocator` type as argument, that we ignore.
       *)
}

let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info =
  let fun_id, fun_sig, can_fail, name, keep_types = raw in
  { fun_id; fun_sig; can_fail; name; keep_types }

(** The list of assumed functions and all their information:
    - their signature
    - a boolean indicating whether the function can fail or not (if true: can fail)
    - their name

    Rk.: following what is written above, we don't include [Box::free].

    Remark about the vector functions: for [Vec::len] to be correct and return
    a [usize], we have to make sure that vectors are bounded by the max usize.
    As a consequence, [Vec::push] is monadic.
 *)
let raw_assumed_fun_infos : raw_assumed_fun_info list =
  [
    ( BoxNew,
      Sig.box_new_sig,
      false,
      to_name [ "alloc"; "boxed"; "Box"; "new" ],
      Some [ true; false ] );
    (* BoxFree shouldn't be used *)
    ( BoxFree,
      Sig.box_free_sig,
      false,
      to_name [ "alloc"; "boxed"; "Box"; "free" ],
      Some [ true; false ] );
    (* Array Index *)
    ( ArrayIndexShared,
      Sig.array_index_sig false,
      true,
      to_name [ "@ArrayIndexShared" ],
      None );
    ( ArrayIndexMut,
      Sig.array_index_sig true,
      true,
      to_name [ "@ArrayIndexMut" ],
      None );
    (* Array to slice*)
    ( ArrayToSliceShared,
      Sig.array_to_slice_sig false,
      true,
      to_name [ "@ArrayToSliceShared" ],
      None );
    ( ArrayToSliceMut,
      Sig.array_to_slice_sig true,
      true,
      to_name [ "@ArrayToSliceMut" ],
      None );
    (* Array Repeat *)
    (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ], None);
    (* Slice Index *)
    ( SliceIndexShared,
      Sig.slice_index_sig false,
      true,
      to_name [ "@SliceIndexShared" ],
      None );
    ( SliceIndexMut,
      Sig.slice_index_sig true,
      true,
      to_name [ "@SliceIndexMut" ],
      None );
    (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ], None);
  ]

let assumed_fun_infos : assumed_fun_info list =
  List.map mk_assumed_fun_info raw_assumed_fun_infos

let get_assumed_fun_info (id : A.assumed_fun_id) : assumed_fun_info =
  match List.find_opt (fun x -> id = x.fun_id) assumed_fun_infos with
  | Some info -> info
  | None ->
      raise
        (Failure ("get_assumed_fun_info: not found: " ^ A.show_assumed_fun_id id))

let get_assumed_fun_sig (id : A.assumed_fun_id) : A.fun_sig =
  (get_assumed_fun_info id).fun_sig

let get_assumed_fun_name (id : A.assumed_fun_id) : fun_name =
  (get_assumed_fun_info id).name

let assumed_fun_can_fail (id : A.assumed_fun_id) : bool =
  (get_assumed_fun_info id).can_fail