@@ -8,6 +8,51 @@ import Contexts.*
8
8
import ast .tpd
9
9
import tpd .Tree
10
10
11
+ /** The co-inductive cache used for analysis
12
+ *
13
+ * The cache contains two maps from `(Config, Tree)` to `Res`:
14
+ *
15
+ * - input cache (`this.last`)
16
+ * - output cache (`this.current`)
17
+ *
18
+ * The two caches are required because we want to make sure in a new iteration,
19
+ * an expression is evaluated exactly once. The monotonicity of the analysis
20
+ * ensures that the cache state goes up the lattice of the abstract domain,
21
+ * consequently the algorithm terminates.
22
+ *
23
+ * The general skeleton for usage of the cache is as follows
24
+ *
25
+ * def analysis() = {
26
+ * def iterate(entryExp: Expr)(using Cache) =
27
+ * eval(entryExp, initConfig)
28
+ * if cache.hasChanged && noErrors then
29
+ * cache.last = cache.current
30
+ * cache.current = Empty
31
+ * cache.changed = false
32
+ * iterate(outputCache, emptyCache)
33
+ * else
34
+ * reportErrors
35
+ *
36
+ *
37
+ * def eval(exp: Exp, config: Config)(using Cache) =
38
+ * cache.cachedEval(config, expr) {
39
+ * // Actual recursive evaluation of expression.
40
+ * //
41
+ * // Only executed if the entry `(exp, config)` is not in the output cache.
42
+ * }
43
+ *
44
+ * iterate(entryExp)(using new Cache)
45
+ * }
46
+ *
47
+ * See the documentation for the method `Cache.cachedEval` for more information.
48
+ *
49
+ * What goes to the configuration (`Config`) and what goes to the result (`Res`)
50
+ * need to be decided by the specific analysis and justified by reasoning about
51
+ * soundness.
52
+ *
53
+ * @param Config The analysis state that matters for evaluating an expression.
54
+ * @param Res The result from the evaluation the given expression.
55
+ */
11
56
class Cache [Config , Res ]:
12
57
import Cache .*
13
58
@@ -36,28 +81,36 @@ class Cache[Config, Res]:
36
81
def get (config : Config , expr : Tree ): Option [Res ] =
37
82
current.get(config, expr)
38
83
39
- /** Copy the value (config, expr)` from the last cache to the current cache
84
+ /** Evaluate an expression with cache
40
85
*
41
- * It assumes `default` if it doesn't exist in the last cache.
86
+ * The algorithmic skeleton is as follows:
42
87
*
43
- * It updates the current caches if the values change.
88
+ * if this.current.contains(config, expr) then
89
+ * return cached value
90
+ * else
91
+ * val assumed = this.last(config, expr) or bottom value if absent
92
+ * this.current(config, expr) = assumed
93
+ * val actual = eval(exp)
94
+ *
95
+ * if assumed != actual then
96
+ * this.changed = true
97
+ * this.current(config, expr) = actual
44
98
*
45
- * The two caches are required because we want to make sure in a new iteration, an expression is evaluated once.
46
99
*/
47
- def cachedEval (config : Config , expr : Tree , cacheResult : Boolean , default : Res )(eval : => Res ): Res =
100
+ def cachedEval (config : Config , expr : Tree , cacheResult : Boolean , default : Res )(eval : Tree => Res ): Res =
48
101
this .get(config, expr) match
49
102
case Some (value) => value
50
103
case None =>
51
104
val assumeValue : Res =
52
- last.get(config, expr) match
105
+ this . last.get(config, expr) match
53
106
case Some (value) => value
54
107
case None =>
55
- this .last = last.updatedNested(config, expr, default)
108
+ this .last = this . last.updatedNested(config, expr, default)
56
109
default
57
110
58
- this .current = current.updatedNested(config, expr, assumeValue)
111
+ this .current = this . current.updatedNested(config, expr, assumeValue)
59
112
60
- val actual = eval
113
+ val actual = eval(expr)
61
114
if actual != assumeValue then
62
115
// println("Changed! from = " + assumeValue + ", to = " + actual)
63
116
this .changed = true
0 commit comments