summaryrefslogtreecommitdiff
path: root/compiler/Contexts.ml
blob: a30ed0f17f6a0486f0b22e37af630dfc5b529884 (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
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
open Types
open Expressions
open Values
open LlbcAst
open LlbcAstUtils
open ValuesUtils
open Identifiers
module L = Logging

(** The [Id] module for dummy variables.

    Dummy variables are used to store values that we don't want to forget
    in the environment, because they contain borrows for instance, typically
    because they might be overwritten during an assignment.
  *)
module DummyVarId =
IdGen ()

type dummy_var_id = DummyVarId.id [@@deriving show, ord]

(** The local logger *)
let log = L.contexts_log

(** Some global counters.

  Note that those counters were initially stored in {!eval_ctx} values,
  but it proved better to make them global and stateful:
  - when branching (and thus executing on several paths with different
    contexts) it is better to really have unique ids everywhere (and
    not have fresh ids shared by several contexts even though introduced
    after the branching) because at some point we might need to merge the
    different contexts
  - also, it is a lot more convenient to not store those counters in contexts
    objects

  =============
  **WARNING**:
  =============
  Pay attention when playing with closures, as you may not always generate
  fresh identifiers without noticing it, especially when using type abbreviations.
  For instance, consider the following:
  {[
    type fun_type = unit -> ...
    fn f x : fun_type =
      let id = fresh_id () in
      ...
      fun () -> ...
   
    let g = f x in   // <-- the fresh identifier gets generated here
    let x1 = g () in // <-- no fresh generation here
    let x2 = g () in
    ...
  ]}

  This is why, in such cases, we often introduce all the inputs, even
  when they are not used (which happens!).
  {[
    fn f x : fun_type =
     fun .. ->
      let id = fresh_id () in
      ...
  ]}

  Note that in practice, we never reuse closures, except when evaluating
  a branching in the execution (which is fine, because the branches evaluate
  independentely of each other). Still, it is always a good idea to be
  defensive.

  However, the same problem arises with logging. 

  Also, a more defensive way would be to not use global references, and
  store the counters in the evaluation context. This is actually what was
  originally done, before we updated the code to use global counters because
  it proved more convenient (and even before updating the code of the
  interpreter to use CPS).
 *)

let symbolic_value_id_counter, fresh_symbolic_value_id =
  SymbolicValueId.fresh_stateful_generator ()

let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator ()
let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()

let abstraction_id_counter, fresh_abstraction_id =
  AbstractionId.fresh_stateful_generator ()

let loop_id_counter, fresh_loop_id = LoopId.fresh_stateful_generator ()

let fun_call_id_counter, fresh_fun_call_id =
  FunCallId.fresh_stateful_generator ()

let dummy_var_id_counter, fresh_dummy_var_id =
  DummyVarId.fresh_stateful_generator ()

(** We shouldn't need to reset the global counters, but it might be good to
    do it from time to time, for instance every time we start evaluating/
    synthesizing a function.
    
    The reasons are manifold:
    - it might prevent the counters from overflowing (although this seems
      extremely unlikely - as a side node: we have overflow checks to make
      sure the synthesis doesn't get impacted by potential overflows)
    - most importantly, it allows to always manipulate low values, which
      is always a lot more readable when debugging
 *)
let reset_global_counters () =
  symbolic_value_id_counter := SymbolicValueId.generator_zero;
  borrow_id_counter := BorrowId.generator_zero;
  region_id_counter := RegionId.generator_zero;
  abstraction_id_counter := AbstractionId.generator_zero;
  loop_id_counter := LoopId.generator_zero;
  fun_call_id_counter := FunCallId.generator_zero;
  dummy_var_id_counter := DummyVarId.generator_zero

(** Ancestor for {!type:env} iter visitor *)
class ['self] iter_env_base =
  object (_self : 'self)
    inherit [_] iter_abs
    method visit_var_id : 'env -> var_id -> unit = fun _ _ -> ()
    method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
  end

(** Ancestor for {!type:env} map visitor *)
class ['self] map_env_base =
  object (_self : 'self)
    inherit [_] map_abs
    method visit_var_id : 'env -> var_id -> var_id = fun _ x -> x

    method visit_dummy_var_id : 'env -> dummy_var_id -> dummy_var_id =
      fun _ x -> x
  end

(** A binder used in an environment, to map a variable to a value *)
type var_binder = {
  index : var_id;  (** Unique variable identifier *)
  name : string option;  (** Possible name *)
}

(** A binder, for a "real" variable or a dummy variable *)
and binder = BVar of var_binder | BDummy of dummy_var_id

(** Environment value: mapping from variable to value, abstraction (only
    used in symbolic mode) or stack frame delimiter.
 *)
and env_elem =
  | EBinding of binder * typed_value
      (** Variable binding - the binder is None if the variable is a dummy variable
          (we use dummy variables to store temporaries while doing bookkeeping such
           as ending borrows for instance). *)
  | EAbs of abs
  | EFrame

and env = env_elem list
[@@deriving
  show,
    visitors
      {
        name = "iter_env";
        variety = "iter";
        ancestors = [ "iter_env_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      },
    visitors
      {
        name = "map_env";
        variety = "map";
        ancestors = [ "map_env_base" ];
        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
        concrete = true;
      }]

type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show]

type config = {
  mode : interpreter_mode;
      (** Concrete mode (interpreter) or symbolic mode (for synthesis) **)
}
[@@deriving show]

let mk_config (mode : interpreter_mode) : config = { mode }

type type_context = {
  type_decls_groups : type_declaration_group TypeDeclId.Map.t;
  type_decls : type_decl TypeDeclId.Map.t;
  type_infos : TypesAnalysis.type_infos;
}
[@@deriving show]

type fun_context = {
  fun_decls : fun_decl FunDeclId.Map.t;
  fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
  regions_hierarchies : region_var_groups FunIdMap.t;
}
[@@deriving show]

type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
[@@deriving show]

type trait_decls_context = { trait_decls : trait_decl TraitDeclId.Map.t }
[@@deriving show]

type trait_impls_context = { trait_impls : trait_impl TraitImplId.Map.t }
[@@deriving show]

type decls_ctx = {
  type_ctx : type_context;
  fun_ctx : fun_context;
  global_ctx : global_context;
  trait_decls_ctx : trait_decls_context;
  trait_impls_ctx : trait_impls_context;
}
[@@deriving show]

(** A reference to a trait associated type *)
type trait_type_ref = { trait_ref : trait_ref; type_name : string }
[@@deriving show, ord]

(* TODO: correctly use the functors so as not to have a duplication below *)
module TraitTypeRefOrd = struct
  type t = trait_type_ref

  let compare = compare_trait_type_ref
  let to_string = show_trait_type_ref
  let pp_t = pp_trait_type_ref
  let show_t = show_trait_type_ref
end

module TraitTypeRefMap = Collections.MakeMap (TraitTypeRefOrd)

(** Evaluation context *)
type eval_ctx = {
  type_context : type_context;
  fun_context : fun_context;
  global_context : global_context;
  trait_decls_context : trait_decls_context;
  trait_impls_context : trait_impls_context;
  region_groups : RegionGroupId.id list;
  type_vars : type_var list;
  const_generic_vars : const_generic_var list;
  const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
      (** The map from const generic vars to their values. Those values
          can be symbolic values or concrete values (in the latter case:
          if we run in interpreter mode).

          TODO: this is actually not used in symbolic mode, where we
          directly introduce fresh symbolic values.
       *)
  norm_trait_types : ty TraitTypeRefMap.t;
      (** The normalized trait types (a map from trait types to their representatives).
          Note that this doesn't take into account higher-order type constraints
          (of the shape `for<'a> ...`). *)
  env : env;
  ended_regions : RegionId.Set.t;
}
[@@deriving show]

let lookup_type_var_opt (ctx : eval_ctx) (vid : TypeVarId.id) : type_var option
    =
  TypeVarId.nth_opt ctx.type_vars vid

let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
  TypeVarId.nth ctx.type_vars vid

let lookup_const_generic_var_opt (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
    const_generic_var option =
  ConstGenericVarId.nth_opt ctx.const_generic_vars vid

let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
    const_generic_var =
  ConstGenericVarId.nth ctx.const_generic_vars vid

(** Lookup a variable in the current frame *)
let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
  (* We take care to stop at the end of current frame: different variables
     in different frames can have the same id!
  *)
  let rec lookup env =
    match env with
    | [] ->
        raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid))
    | EBinding (BVar var, v) :: env' ->
        if var.index = vid then (var, v) else lookup env'
    | (EBinding (BDummy _, _) | EAbs _) :: env' -> lookup env'
    | EFrame :: _ -> raise (Failure "End of frame")
  in
  lookup env

let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder =
  fst (env_lookup_var ctx.env vid)

let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
  TypeDeclId.Map.find tid ctx.type_context.type_decls

let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
  FunDeclId.Map.find fid ctx.fun_context.fun_decls

let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
    global_decl =
  GlobalDeclId.Map.find gid ctx.global_context.global_decls

let ctx_lookup_trait_decl (ctx : eval_ctx) (id : TraitDeclId.id) : trait_decl =
  TraitDeclId.Map.find id ctx.trait_decls_context.trait_decls

let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
  TraitImplId.Map.find id ctx.trait_impls_context.trait_impls

(** Retrieve a variable's value in the current frame *)
let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
  snd (env_lookup_var env vid)

(** Retrieve a variable's value in an evaluation context *)
let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
  env_lookup_var_value ctx.env vid

(** Retrieve a const generic value in an evaluation context *)
let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
    : typed_value =
  Types.ConstGenericVarId.Map.find vid ctx.const_generic_vars_map

(** Update a variable's value in the current frame.

    This is a helper function: it can break invariants and doesn't perform
    any check.
*)
let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
  (* We take care to stop at the end of current frame: different variables
     in different frames can have the same id!
  *)
  let rec update env =
    match env with
    | [] -> raise (Failure "Unexpected")
    | EBinding ((BVar b as var), v) :: env' ->
        if b.index = vid then EBinding (var, nv) :: env'
        else EBinding (var, v) :: update env'
    | ((EBinding (BDummy _, _) | EAbs _) as ee) :: env' -> ee :: update env'
    | EFrame :: _ -> raise (Failure "End of frame")
  in
  update env

let var_to_binder (var : var) : var_binder =
  { index = var.index; name = var.name }

(** Update a variable's value in an evaluation context.

    This is a helper function: it can break invariants and doesn't perform
    any check.
*)
let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
    eval_ctx =
  { ctx with env = env_update_var_value ctx.env vid nv }

(** Push a variable in the context's environment.

    Checks that the pushed variable and its value have the same type (this
    is important).
*)
let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
  assert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty);
  let bv = var_to_binder var in
  { ctx with env = EBinding (BVar bv, v) :: ctx.env }

(** Push a list of variables.

    Checks that the pushed variables and their values have the same type (this
    is important).
*)
let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
    =
  log#ldebug
    (lazy
      ("push_vars:\n"
      ^ String.concat "\n"
          (List.map
             (fun (var, value) ->
               (* We can unfortunately not use Print because it depends on Contexts... *)
               show_var var ^ " -> " ^ show_typed_value value)
             vars)));
  assert (
    List.for_all
      (fun (var, (value : typed_value)) ->
        TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
      vars);
  let vars =
    List.map
      (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
      vars
  in
  let vars = List.rev vars in
  { ctx with env = List.append vars ctx.env }

(** Push a dummy variable in the context's environment. *)
let ctx_push_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) (v : typed_value)
    : eval_ctx =
  { ctx with env = EBinding (BDummy vid, v) :: ctx.env }

(** Remove a dummy variable from a context's environment. *)
let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
    eval_ctx * typed_value =
  let rec remove_var (env : env) : env * typed_value =
    match env with
    | [] -> raise (Failure "Could not lookup a dummy variable")
    | EBinding (BDummy vid', v) :: env when vid' = vid -> (env, v)
    | ee :: env ->
        let env, v = remove_var env in
        (ee :: env, v)
  in
  let env, v = remove_var ctx.env in
  ({ ctx with env }, v)

(** Lookup a dummy variable in a context's environment. *)
let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
  let rec lookup_var (env : env) : typed_value =
    match env with
    | [] -> raise (Failure "Could not lookup a dummy variable")
    | EBinding (BDummy vid', v) :: _env when vid' = vid -> v
    | _ :: env -> lookup_var env
  in
  lookup_var ctx.env

let erase_regions (ty : ty) : ty =
  let v =
    object
      inherit [_] map_ty
      method! visit_region _ _ = RErased
    end
  in
  v#visit_ty () ty

(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
  ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))

(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
  let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
  ctx_push_vars ctx vars

let env_find_abs (env : env) (pred : abs -> bool) : abs option =
  let rec lookup env =
    match env with
    | [] -> None
    | EBinding (_, _) :: env' -> lookup env'
    | EAbs abs :: env' -> if pred abs then Some abs else lookup env'
    | EFrame :: env' -> lookup env'
  in
  lookup env

let env_lookup_abs (env : env) (abs_id : AbstractionId.id) : abs =
  Option.get (env_find_abs env (fun abs -> abs.abs_id = abs_id))

(** Remove an abstraction from the context, as well as all the references to
    this abstraction (for instance, remove the abs id from all the parent sets
    of all the other abstractions).
 *)
let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
  let rec remove (env : env) : env * abs option =
    match env with
    | [] -> raise (Failure "Unreachable")
    | EFrame :: _ -> (env, None)
    | EBinding (bv, v) :: env ->
        let env, abs_opt = remove env in
        (EBinding (bv, v) :: env, abs_opt)
    | EAbs abs :: env ->
        if abs.abs_id = abs_id then (env, Some abs)
        else
          let env, abs_opt = remove env in
          (* Update the parents set *)
          let parents = AbstractionId.Set.remove abs_id abs.parents in
          (EAbs { abs with parents } :: env, abs_opt)
  in
  remove env

(** Substitue an abstraction in an environment.

    Note that we substitute an abstraction (identified by its id) with a different
    abstraction which **doesn't necessarily have the same id**. Because of this,
    we also substitute the abstraction id wherever it is used (i.e., in the
    parent sets of the other abstractions).
 *)
let env_subst_abs (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
    env * abs option =
  let rec update (env : env) : env * abs option =
    match env with
    | [] -> raise (Failure "Unreachable")
    | EFrame :: _ -> (* We're done *) (env, None)
    | EBinding (bv, v) :: env ->
        let env, opt_abs = update env in
        (EBinding (bv, v) :: env, opt_abs)
    | EAbs abs :: env ->
        if abs.abs_id = abs_id then (EAbs nabs :: env, Some abs)
        else
          let env, opt_abs = update env in
          (* Update the parents set *)
          let parents = abs.parents in
          let parents =
            if AbstractionId.Set.mem abs_id parents then
              let parents = AbstractionId.Set.remove abs_id parents in
              AbstractionId.Set.add nabs.abs_id parents
            else parents
          in
          (EAbs { abs with parents } :: env, opt_abs)
  in
  update env

let ctx_lookup_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) : abs =
  env_lookup_abs ctx.env abs_id

let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
  env_find_abs ctx.env p

(** See the comments for {!env_remove_abs} *)
let ctx_remove_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) :
    eval_ctx * abs option =
  let env, abs = env_remove_abs ctx.env abs_id in
  ({ ctx with env }, abs)

(** See the comments for {!env_subst_abs} *)
let ctx_subst_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
    eval_ctx * abs option =
  let env, abs_opt = env_subst_abs ctx.env abs_id nabs in
  ({ ctx with env }, abs_opt)

let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
    (can_end : bool) : eval_ctx =
  let abs = ctx_lookup_abs ctx abs_id in
  let abs = { abs with can_end } in
  fst (ctx_subst_abs ctx abs_id abs)

let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
  let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
  match decl_group with RecGroup _ -> true | NonRecGroup _ -> false

(** Visitor to iterate over the values in the *current* frame *)
class ['self] iter_frame =
  object (self : 'self)
    inherit [_] iter_env

    method! visit_env : 'acc -> env -> unit =
      fun acc env ->
        match env with
        | [] -> ()
        | EFrame :: _ -> (* We stop here *) ()
        | em :: env ->
            self#visit_env_elem acc em;
            self#visit_env acc env
  end

(** Visitor to map over the values in the *current* frame *)
class ['self] map_frame_concrete =
  object (self : 'self)
    inherit [_] map_env

    method! visit_env : 'acc -> env -> env =
      fun acc env ->
        match env with
        | [] -> []
        | EFrame :: env -> (* We stop here *) EFrame :: env
        | em :: env ->
            let em = self#visit_env_elem acc em in
            let env = self#visit_env acc env in
            em :: env
  end

(** Visitor to iterate over the values in a context *)
class ['self] iter_eval_ctx =
  object (_self : 'self)
    inherit [_] iter_env as super

    method visit_eval_ctx : 'acc -> eval_ctx -> unit =
      fun acc ctx -> super#visit_env acc ctx.env
  end

(** Visitor to map the values in a context *)
class ['self] map_eval_ctx =
  object (_self : 'self)
    inherit [_] map_env as super

    method visit_eval_ctx : 'acc -> eval_ctx -> eval_ctx =
      fun acc ctx ->
        let env = super#visit_env acc ctx.env in
        { ctx with env }
  end

let env_iter_abs (f : abs -> unit) (env : env) : unit =
  List.iter
    (fun (ee : env_elem) ->
      match ee with EBinding _ | EFrame -> () | EAbs abs -> f abs)
    env

let env_map_abs (f : abs -> abs) (env : env) : env =
  List.map
    (fun (ee : env_elem) ->
      match ee with EBinding _ | EFrame -> ee | EAbs abs -> EAbs (f abs))
    env

let env_filter_abs (f : abs -> bool) (env : env) : env =
  List.filter
    (fun (ee : env_elem) ->
      match ee with EBinding _ | EFrame -> true | EAbs abs -> f abs)
    env