Skip to content

Commit c01fc3f

Browse files
noahvanesnoahvanes
committed
add allocated store to match formalisation
1 parent 5349a0d commit c01fc3f

4 files changed

Lines changed: 50 additions & 46 deletions

File tree

‎code/shared/src/main/scala/maf/core/Store.scala‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -283,15 +283,15 @@ case class LocalStore[A <: Address, V](content: SmartMap[A, (V, AbstractCount)])
283283
acc + (adr -> (lat.join(vlu1, vlu2), cnt1.join(cnt2)))
284284
))
285285
// replaying a delta that was computed w.r.t. a GC'd store
286-
def replay(delta: Delta[A,V], updated: Set[A]): Delta[A,V] =
286+
def replay(delta: Delta[A,V], allocated: Set[A]): Delta[A,V] =
287287
Delta(delta.delta.map { case bnd @ (adr, (v, c)) =>
288-
if updated.contains(adr) then
289-
bnd
290-
else
288+
if allocated.contains(adr) then
291289
get(adr) match {
292290
case None => bnd
293291
case Some((v2, c2)) => (adr, (lat.join(v2, v), CountInf))
294292
}
293+
else
294+
bnd
295295
})
296296

297297
case class LocalStoreGC[A <: Address,V]()(using lat: LatticeWithAddrs[V, A], shouldCount: A=>Boolean) extends AbstractGC[LocalStore[A,V], A]:

‎code/shared/src/main/scala/maf/modular/scheme/modflocal/SchemeModFLocal.scala‎

Lines changed: 22 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ abstract class SchemeModFLocal(prg: SchemeExp) extends ModAnalysis[SchemeExp](pr
6969
// RESULTS
7070
//
7171

72-
var results: Map[Component, Set[(Val, Dlt, Set[Adr])]] = Map.empty
72+
var results: Map[Component, Set[(Val, Dlt, Set[Adr], Set[Adr])]] = Map.empty
7373

7474
case class ResultDependency(cmp: Component) extends Dependency
7575

@@ -91,9 +91,11 @@ abstract class SchemeModFLocal(prg: SchemeExp) extends ModAnalysis[SchemeExp](pr
9191
def withRestrictedStore(rs: Set[Adr])(blk: A[Val]): A[Val] =
9292
(anl, env, sto, ctx) =>
9393
val gcs = LocalStoreGC().collect(sto, rs)
94-
blk(anl, env, gcs, ctx).map { (v, d, u) =>
95-
val gcd = DeltaGC(gcs).collect(d, lattice.refs(v) ++ u)
96-
(v, gcd, u)
94+
blk(anl, env, gcs, ctx).map { (v, d, u, a) =>
95+
val gcu = u.filter(gcs.contains)
96+
val gca = a.filter(d.delta.contains)
97+
val gcd = DeltaGC(gcs).collect(d, lattice.refs(v) ++ gcu)
98+
(v, gcd, gcu, gca)
9799
}
98100

99101
import analysisM_._
@@ -118,27 +120,27 @@ abstract class SchemeModFLocal(prg: SchemeExp) extends ModAnalysis[SchemeExp](pr
118120

119121
override protected def nontail[X](blk: => A[X]) =
120122
(anl, env, sto, ctx) =>
121-
blk(anl, env, sto, ctx).map { (v, d, u) =>
122-
(v, sto.replay(d, u), u)
123+
blk(anl, env, sto, ctx).map { (v, d, u, a) =>
124+
(v, sto.replay(d, a), u, a)
123125
}
124126
//
125127
// ANALYSISM MONAD
126128
//
127129

128-
type A[X] = (anl: Anl, env: Env, sto: Sto, ctx: Ctx) => Set[(X, Dlt, Set[Adr])]
130+
type A[X] = (anl: Anl, env: Env, sto: Sto, ctx: Ctx) => Set[(X, Dlt, Set[Adr], Set[Adr])]
129131

130132
protected def analysisM: AnalysisM[A] = new AnalysisM[A]:
131133
// MONAD
132134
def unit[X](x: X) =
133-
(_, _, sto, _) => Set((x, Delta.emptyDelta[Adr,Val], Set.empty))
135+
(_, _, sto, _) => Set((x, Delta.emptyDelta[Adr,Val], Set.empty, Set.empty))
134136
def map[X, Y](m: A[X])(f: X => Y) =
135-
(anl, env, sto, ctx) => m(anl, env, sto, ctx).map((x, d, u) => (f(x), d, u))
137+
(anl, env, sto, ctx) => m(anl, env, sto, ctx).map((x, d, u, a) => (f(x), d, u, a))
136138
def flatMap[X, Y](m: A[X])(f: X => A[Y]) =
137139
(anl, env, sto, ctx) =>
138140
for
139-
(x0, d0, u0) <- m(anl, env, sto, ctx)
140-
(x1, d1, u1) <- f(x0)(anl, env, sto.integrate(d0), ctx)
141-
yield (x1, Delta.compose(d1, d0), u0 ++ u1.filter(sto.contains)) //TODO: is this one necessary?
141+
(x0, d0, u0, a0) <- m(anl, env, sto, ctx)
142+
(x1, d1, u1, a1) <- f(x0)(anl, env, sto.integrate(d0), ctx)
143+
yield (x1, Delta.compose(d1, d0), u0 ++ u1, a0 ++ a1)
142144
// MONADJOIN
143145
def mbottom[X] =
144146
(_, _, _, _) => Set.empty
@@ -149,21 +151,21 @@ abstract class SchemeModFLocal(prg: SchemeExp) extends ModAnalysis[SchemeExp](pr
149151
mbottom // we are not interested in errors here (at least, not yet ...)
150152
// STOREM
151153
def addrEq =
152-
(anl, _, sto, _) => Set((eqA(sto), Delta.emptyDelta, Set.empty))
154+
(anl, _, sto, _) => Set((eqA(sto), Delta.emptyDelta, Set.empty, Set.empty))
153155
def extendSto(adr: Adr, vlu: Val) =
154-
(anl, _, sto, _) => Set(((), extendV(sto, adr, vlu), Set.empty))
156+
(anl, _, sto, _) => Set(((), extendV(sto, adr, vlu), Set.empty, Set(adr)))
155157
def updateSto(adr: Adr, vlu: Val) =
156-
(anl, _, sto, _) => Set(((), updateV(sto, adr, vlu), Set(adr)))
158+
(anl, _, sto, _) => Set(((), updateV(sto, adr, vlu), Set(adr), Set.empty))
157159
def lookupSto(adr: Adr) =
158-
flatMap((anl, _, sto, _) => Set((sto.lookupValue(adr), Delta.emptyDelta, Set.empty)))(inject)
160+
flatMap((anl, _, sto, _) => Set((sto.lookupValue(adr), Delta.emptyDelta, Set.empty, Set.empty)))(inject)
159161
// CTX STUFF
160162
def getCtx =
161-
(_, _, sto, ctx) => Set((ctx, Delta.emptyDelta, Set.empty))
163+
(_, _, sto, ctx) => Set((ctx, Delta.emptyDelta, Set.empty, Set.empty))
162164
def withCtx[X](f: Ctx => Ctx)(blk: A[X]): A[X] =
163165
(anl, env, sto, ctx) => blk(anl, env, sto, f(ctx))
164166
// ENV STUFF
165167
def getEnv =
166-
(_, env, sto, _) => Set((env, Delta.emptyDelta, Set.empty))
168+
(_, env, sto, _) => Set((env, Delta.emptyDelta, Set.empty, Set.empty))
167169
def withEnv[X](f: Env => Env)(blk: A[X]): A[X] =
168170
(anl, env, sto, ctx) => blk(anl, f(env), sto, ctx)
169171
// CALL STUFF
@@ -181,15 +183,15 @@ abstract class SchemeModFLocal(prg: SchemeExp) extends ModAnalysis[SchemeExp](pr
181183
// local state
182184
var results = inter.results
183185

184-
def call(lam: Lam, env: Env, sto: Sto, ctx: Ctx): Set[(Val, Dlt, Set[Adr])] =
186+
def call(lam: Lam, env: Env, sto: Sto, ctx: Ctx): Set[(Val, Dlt, Set[Adr], Set[Adr])] =
185187
val cmp = CallComponent(lam, env, sto, ctx)
186188
spawn(cmp)
187189
register(ResultDependency(cmp))
188190
results.getOrElse(cmp, Set.empty)
189191

190192
def analyzeWithTimeout(timeout: Timeout.T): Unit =
191193
val res = eval(cmp.exp)(this, cmp.env, cmp.sto, cmp.ctx)
192-
val rgc = res.map((v, d, u) => (v, DeltaGC(cmp.sto).collect(d, lattice.refs(v) ++ u), u))
194+
val rgc = res.map((v, d, u, a) => (v, DeltaGC(cmp.sto).collect(d, lattice.refs(v) ++ u), u, a))
193195
val old = results.getOrElse(cmp, Set.empty)
194196
if rgc != old then
195197
intra.results += cmp -> rgc

‎code/shared/src/main/scala/maf/modular/scheme/modflocal/SchemeModFLocalFS.scala‎

Lines changed: 23 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](
2121
type Sto = LocalStore[Adr, Val]
2222
type Dlt = Delta[Adr, Val]
2323
type Cnt = AbstractCount
24-
type Res = Map[Cmp, (Val, Dlt, Set[Adr])]
24+
type Res = Map[Cmp, (Val, Dlt, Set[Adr], Set[Adr])]
2525
type Sts = Map[Cmp, Sto]
2626
type Anl = SchemeModFLocalFSIntraAnalysis
2727

@@ -91,9 +91,11 @@ abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](
9191
def withRestrictedStore(rs: Set[Adr])(blk: A[Val]): A[Val] =
9292
(anl, env, sto, ctx) =>
9393
val gcs = LocalStoreGC().collect(sto, rs)
94-
blk(anl, env, sto, ctx).map { (vlu, dlt, upd) =>
95-
val gcd = DeltaGC(gcs).collect(dlt, lattice.refs(vlu) ++ upd)
96-
(vlu, gcd, upd)
94+
blk(anl, env, sto, ctx).map { (vlu, dlt, upd, all) =>
95+
val gcu = upd.filter(gcs.contains)
96+
val gca = all.filter(dlt.delta.contains)
97+
val gcd = DeltaGC(gcs).collect(dlt, lattice.refs(vlu) ++ gcu)
98+
(vlu, gcd, gcu, gca)
9799
}
98100

99101
override protected def applyClosure(app: App, lam: Lam, ags: List[Val], fvs: Iterable[(Adr, Val)]): A[Val] =
@@ -109,20 +111,20 @@ abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](
109111
// ANALYSISM MONAD
110112
//
111113

112-
type A[X] = (Anl, Env, Sto, Ctx) => Option[(X, Dlt, Set[Adr])]
114+
type A[X] = (Anl, Env, Sto, Ctx) => Option[(X, Dlt, Set[Adr], Set[Adr])]
113115

114116
given analysisM: AnalysisM[A] with
115117
// MONAD
116118
def unit[X](x: X) =
117-
(_, _, _, _) => Some((x, Delta.emptyDelta, Set.empty))
119+
(_, _, _, _) => Some((x, Delta.emptyDelta, Set.empty, Set.empty))
118120
def map[X, Y](m: A[X])(f: X => Y) =
119-
(anl, env, sto, ctx) => m(anl, env, sto, ctx).map((x, d, u) => (f(x), d, u))
121+
(anl, env, sto, ctx) => m(anl, env, sto, ctx).map((x, d, u, a) => (f(x), d, u, a))
120122
def flatMap[X, Y](m: A[X])(f: X => A[Y]) =
121123
(anl, env, sto, ctx) =>
122124
for
123-
(x0, d0, u0) <- m(anl, env, sto, ctx)
124-
(x1, d1, u1) <- f(x0)(anl, env, sto.integrate(d0), ctx)
125-
yield (x1, Delta.compose(d1, d0), u0 ++ u1.filter(sto.contains))
125+
(x0, d0, u0, a0) <- m(anl, env, sto, ctx)
126+
(x1, d1, u1, a1) <- f(x0)(anl, env, sto.integrate(d0), ctx)
127+
yield (x1, Delta.compose(d1, d0), u0 ++ u1, a0 ++ a1)
126128
// MONADJOIN
127129
def mbottom[X] =
128130
(_, _, _, _) => None
@@ -131,27 +133,27 @@ abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](
131133
(x(anl, env, sto, ctx), y(anl, env, sto, ctx)) match
132134
case (None, yres) => yres
133135
case (xres, None) => xres
134-
case (Some((xv, xs, xu)), Some(yv, ys, yu)) => Some((Lattice[X].join(xv, yv), sto.join(xs, ys), xu ++ yu))
136+
case (Some((xv, xs, xu, xa)), Some(yv, ys, yu, ya)) => Some((Lattice[X].join(xv, yv), sto.join(xs, ys), xu ++ yu, xa ++ ya))
135137
// MONADERROR
136138
def fail[X](err: Error) =
137139
mbottom // we are not interested in errors here (at least, not yet ...)
138140
// STOREM
139141
def addrEq =
140-
(_, _, sto, _) => Some((eqA(sto), Delta.emptyDelta, Set.empty))
142+
(_, _, sto, _) => Some((eqA(sto), Delta.emptyDelta, Set.empty, Set.empty))
141143
def extendSto(adr: Adr, vlu: Val) =
142-
(_, _, sto, _) => Some((), extendV(sto, adr, vlu), Set.empty)
144+
(_, _, sto, _) => Some((), extendV(sto, adr, vlu), Set.empty, Set(adr))
143145
def updateSto(adr: Adr, vlu: Val) =
144-
(_, _, sto, _) => Some((), updateV(sto, adr, vlu), Set(adr))
146+
(_, _, sto, _) => Some((), updateV(sto, adr, vlu), Set(adr), Set.empty)
145147
def lookupSto(adr: Adr) =
146-
(_, _, sto, _) => sto.getValue(adr).map((_, Delta.emptyDelta, Set.empty))
148+
(_, _, sto, _) => sto.getValue(adr).map((_, Delta.emptyDelta, Set.empty, Set.empty))
147149
// CTX STUFF
148150
def getCtx =
149-
(_, _, _, ctx) => Some((ctx, Delta.emptyDelta, Set.empty))
151+
(_, _, _, ctx) => Some((ctx, Delta.emptyDelta, Set.empty, Set.empty))
150152
def withCtx[X](f: Ctx => Ctx)(blk: A[X]) =
151153
(anl, env, sto, ctx) => blk(anl, env, sto, f(ctx))
152154
// ENV STUFF
153155
def getEnv =
154-
(_, env, _, _) => Some((env, Delta.emptyDelta, Set.empty))
156+
(_, env, _, _) => Some((env, Delta.emptyDelta, Set.empty, Set.empty))
155157
def withEnv[X](f: Env => Env)(blk: A[X]) =
156158
(anl, env, sto, ctx) => blk(anl, f(env), sto, ctx)
157159
// CALL STUFF
@@ -176,16 +178,16 @@ abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](
176178
// register dependencies on all addresses
177179
sto.content.keys.foreach(adr => register(AddrDependencyFS(cmp, adr)))
178180
// GC the result
179-
val rgc = eval(cmp.exp)(this, cmp.env, sto, cmp.ctx).map { (v, d, u) =>
180-
(v, DeltaGC(sto).collect(d, lattice.refs(v) ++ u), u)
181+
val rgc = eval(cmp.exp)(this, cmp.env, sto, cmp.ctx).map { (v, d, u, a) =>
182+
(v, DeltaGC(sto).collect(d, lattice.refs(v) ++ u), u, a)
181183
}
182184
// update the result of this component
183185
val old = results.get(cmp)
184186
if (rgc != old) then
185187
results += cmp -> rgc.get
186188
trigger(ResultDependency(cmp))
187189

188-
def call(cll: Cll, sto: Sto): Option[(Val, Dlt, Set[Adr])] =
190+
def call(cll: Cll, sto: Sto): Option[(Val, Dlt, Set[Adr], Set[Adr])] =
189191
// spawn the component
190192
spawn(cll)
191193
// add bindings to its store
@@ -204,7 +206,7 @@ abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](
204206

205207
override def doWrite(dep: Dependency): Boolean = dep match
206208
case ResultDependency(cmp) =>
207-
val old = inter.results.getOrElse(cmp, (lattice.bottom, Delta.emptyDelta, Set.empty))
209+
val old = inter.results.getOrElse(cmp, (lattice.bottom, Delta.emptyDelta, Set.empty, Set.empty))
208210
val cur = intra.results(cmp) // we are certain to have a result here!
209211
if old != cur then
210212
inter.results += cmp -> cur

‎code/shared/src/main/scala/maf/modular/scheme/modflocal/SchemeSemantics.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ trait SchemeSemantics:
149149
protected def evalCall(app: App): A[Val] =
150150
for
151151
fun <- nontail { eval(app.f) }
152-
ags <- app.args.mapM(arg => nontail {eval(arg) })
152+
ags <- app.args.mapM(arg => nontail { eval(arg) })
153153
res <- applyFun(app, fun, ags)
154154
yield res
155155

0 commit comments

Comments
 (0)