summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoopsJoinCtxs.mli
blob: bb9f14edee01d0607597ef2a872035d51be06da5 (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
open Values
open Contexts
open InterpreterUtils
open InterpreterLoopsCore

(** Merge an abstraction into another abstraction in a context.

    This function is similar to {!InterpreterBorrows.merge_into_abstraction}.
    
    Parameters:
    - [loop_id]
    - [abs_kind]
    - [can_end]
    - [ctx]
    - [aid0]
    - [aid1]
 *)
val merge_into_abstraction :
  loop_id ->
  abs_kind ->
  bool ->
  eval_ctx ->
  abstraction_id ->
  abstraction_id ->
  eval_ctx * abstraction_id

(** Join two contexts.

    We use this to join the environments at loop (re-)entry to progressively
    compute a fixed point.

    We make the hypothesis (and check it) that the environments have the same
    prefixes (same variable ids, same abstractions, etc.). The prefix of
    variable and abstraction ids is given by the [fixed_ids] identifier sets. We
    check that those prefixes are the same (the dummy variables are the same,
    the abstractions are the same), match the values mapped to by the variables
    which are not dummy, then group the additional dummy variables/abstractions
    together. In a sense, the [fixed_ids] define a frame (in a separation logic
    sense).

    Note that when joining the values mapped to by the non-dummy variables, we
    may introduce duplicated borrows. Also, we don't match the abstractions
    which are not in the prefix, and this can also lead to borrow
    duplications. For this reason, the environment needs to be collapsed
    afterwards to get rid of those duplicated loans/borrows.

    For instance, if we have:
    {[
      fixed = { abs0 }

      env0 = {
        abs0 { ML l0 }
        l -> MB l0 s0
      }

      env1 = {
        abs0 { ML l0 }
        l -> MB l1 s1
        abs1 { MB l0, ML l1 }
      }
    ]}

    We get:
    {[
      join env0 env1 = {
        abs0 { ML l0 } (* abs0 is fixed: we simply check it is equal in env0 and env1 *)
        l -> MB l2 s2
        abs1 { MB l0, ML l1 } (* abs1 is new: we keep it unchanged *)
        abs2 { MB l0, MB l1, ML l2 } (* Introduced when joining on the "l" variable *)
      }
    ]}

    Rem.: in practice, this join works because we take care of pushing new values
    and abstractions *at the end* of the environments, meaning the environment
    prefixes keep the same structure.

    Rem.: assuming that the environment has some structure poses *no soundness
    issue*. It can only make the join fail if the environments actually don't have
    this structure: this is a *completeness issue*.
    
    Parameters:
    - [loop_id]
    - [fixed_ids]
    - [ctx0]
    - [ctx1]
  *)
val join_ctxs : loop_id -> ids_sets -> eval_ctx -> eval_ctx -> ctx_or_update

(** Join the context at the entry of the loop with the contexts upon reentry
    (upon reaching the [Continue] statement - the goal is to compute a fixed
    point for the loop entry).

    As we may have to end loans in the environments before doing the join,
    we return those updated environments, and the joined environment.
    
    This function is mostly built on top of {!join_ctxs}.
    
    Parameters:
    - [config]
    - [loop_id]
    - [fixed_ids]
    - [old_ctx]
    - [ctxl]
 *)
val loop_join_origin_with_continue_ctxs :
  config ->
  loop_id ->
  ids_sets ->
  eval_ctx ->
  eval_ctx list ->
  (eval_ctx * eval_ctx list) * eval_ctx