@@ -8,6 +8,51 @@ import Contexts.*
88import ast .tpd
99import tpd .Tree
1010
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+ */
1156class Cache [Config , Res ]:
1257 import Cache .*
1358
@@ -36,28 +81,36 @@ class Cache[Config, Res]:
3681 def get (config : Config , expr : Tree ): Option [Res ] =
3782 current.get(config, expr)
3883
39- /** Copy the value (config, expr)` from the last cache to the current cache
84+ /** Evaluate an expression with cache
4085 *
41- * It assumes `default` if it doesn't exist in the last cache.
86+ * The algorithmic skeleton is as follows:
4287 *
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
4498 *
45- * The two caches are required because we want to make sure in a new iteration, an expression is evaluated once.
4699 */
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 =
48101 this .get(config, expr) match
49102 case Some (value) => value
50103 case None =>
51104 val assumeValue : Res =
52- last.get(config, expr) match
105+ this . last.get(config, expr) match
53106 case Some (value) => value
54107 case None =>
55- this .last = last.updatedNested(config, expr, default)
108+ this .last = this . last.updatedNested(config, expr, default)
56109 default
57110
58- this .current = current.updatedNested(config, expr, assumeValue)
111+ this .current = this . current.updatedNested(config, expr, assumeValue)
59112
60- val actual = eval
113+ val actual = eval(expr)
61114 if actual != assumeValue then
62115 // println("Changed! from = " + assumeValue + ", to = " + actual)
63116 this .changed = true
0 commit comments