Skip to content

Commit 26813c4

Browse files
noahvanesnoahvanes
committed
fix bugs + setup experiment 1
1 parent c01fc3f commit 26813c4

4 files changed

Lines changed: 184 additions & 70 deletions

File tree

‎code/jvm/src/main/scala/maf/cli/experiments/precision/AnalysisComparison.scala‎

Lines changed: 69 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package maf.cli.experiments.precision
22

3+
import maf.modular.scheme.aam._
34
import maf.cli.experiments._
45
import maf.language.scheme._
56
import maf.lattice._
@@ -19,8 +20,8 @@ abstract class AnalysisComparison[Num: IntLattice, Rea: RealLattice, Bln: BoolLa
1920
def otherAnalyses(): List[(SchemeExp => Analysis, String)]
2021

2122
// and can, optionally, be configured in its timeouts (default: 5min.)
22-
def analysisTimeout(): Timeout.T = Timeout.start(Duration(45, MINUTES)) //timeout for (non-base) analyses
23-
def concreteTimeout(): Timeout.T = Timeout.none //timeout for concrete interpreter
23+
def analysisTimeout(): Timeout.T = Timeout.start(Duration(30, SECONDS)) //timeout for (non-base) analyses
24+
def concreteTimeout(): Timeout.T = Timeout.start(Duration(1, MINUTES)) //timeout for concrete interpreter
2425

2526
def concreteRuns() = 5
2627

@@ -63,38 +64,76 @@ object AnalysisComparison1
6364
ConstantPropagation.S,
6465
ConstantPropagation.Sym
6566
]:
67+
6668
val k = 0
67-
val l = 1000
69+
70+
lazy val aam: (SchemeExp => Analysis, String) = (new SchemeAAMGCAnalysis(_, k), s"$k-CFA AAM")
71+
lazy val dss: (SchemeExp => Analysis, String) = (SchemeAnalyses.modflocalAnalysis(_, k), s"$k-CFA DSS")
72+
6873
def baseAnalysis(prg: SchemeExp): Analysis =
69-
SchemeAnalyses.kCFAAnalysis(prg, k)
70-
def otherAnalyses() =
71-
// run some regular k-cfa analyses
72-
List(
73-
//(SchemeAnalyses.modflocalAnalysis(_, 0), "0-CFA DSS"),
74-
//(SchemeAnalyses.modflocalAnalysisAdaptiveA(_, k, l), s"$k-CFA DSS w/ ASW (l = $l)")
75-
)
76-
77-
def main(args: Array[String]) = runBenchmarks(
78-
Set(
79-
"test/R5RS/various/mceval.scm"
80-
)
81-
)
82-
83-
def check(path: Benchmark) =
84-
val txt = Reader.loadFile(path)
85-
val prg = SchemeParser.parseProgram(txt)
86-
val con = runInterpreter(prg, path).get
87-
val Terminated(abs) = runAnalysis(SchemeAnalyses.fullArgContextSensitiveAnalysis(_), "analysis", prg, path)
88-
val allKeys = con.keys ++ abs.keys
89-
allKeys.foreach { k =>
90-
val absVal = abs.getOrElse(k, "⊥")
91-
val concVal = con.getOrElse(k, "⊥")
92-
if absVal != concVal then println(s"$k -> $absVal ; $concVal ")
93-
}
74+
SchemeAnalyses.contextInsensitiveAnalysis(prg) //context-insensitive analysis
75+
def otherAnalyses() = aam :: dss :: Nil
76+
77+
def gambit = List("array1.scm",
78+
"deriv.scm",
79+
// "graphs.scm",
80+
"nqueens.scm",
81+
"puzzle.scm",
82+
"sum.scm",
83+
"triangl.scm",
84+
"browse.scm",
85+
"destruc.scm",
86+
"lattice.scm",
87+
"paraffins.scm",
88+
"sboyer.scm",
89+
"sumloop.scm",
90+
"wc.scm",
91+
"cat.scm",
92+
"diviter.scm",
93+
"matrix.scm",
94+
"perm9.scm",
95+
"scheme.scm",
96+
"tail.scm",
97+
"compiler.scm",
98+
"earley.scm",
99+
"mazefun.scm",
100+
"peval.scm",
101+
"slatex.scm",
102+
"tak.scm",
103+
"ctak.scm",
104+
"fibc.scm",
105+
"nboyer.scm",
106+
"primes.scm",
107+
"string.scm",
108+
"trav1.scm"
109+
).map(file => s"test/R5RS/various/$file")
110+
111+
def gabriel = List(
112+
"boyer",
113+
"browse",
114+
"cpstak",
115+
"dderiv",
116+
"deriv",
117+
"destruct",
118+
"diviter",
119+
"divrec",
120+
"puzzle",
121+
"takl",
122+
"triangl"
123+
).map(name => s"test/R5RS/gabriel/$name.scm")
124+
125+
def main(args: Array[String]) = runBenchmarks(gabriel)
126+
127+
override def parseProgram(txt: String): SchemeExp =
128+
val parsed = SchemeParser.parse(txt)
129+
val prelud = SchemePrelude.addPrelude(parsed, incl = Set("__toplevel_cons", "__toplevel_cdr", "__toplevel_set-cdr!"))
130+
val transf = SchemeMutableVarBoxer.transform(prelud)
131+
SchemeParser.undefine(transf)
94132

95-
def runBenchmarks(benchmarks: Set[Benchmark]) =
133+
def runBenchmarks(benchmarks: List[Benchmark]) =
134+
assert(benchmarks.size == benchmarks.toSet.size)
96135
benchmarks.foreach(runBenchmark)
97136
println(results.prettyString(format = _.map(_.toString()).getOrElse("TIMEOUT")))
98-
val writer = Writer.open("benchOutput/precision/adaptive-precision-benchmarks.csv")
137+
val writer = Writer.open("benchOutput/precision/precision-benchmarks.csv")
99138
Writer.write(writer, results.toCSVString(format = _.map(_.toString()).getOrElse("TIMEOUT"), rowName = "benchmark"))
100139
Writer.close(writer)

‎code/jvm/src/main/scala/maf/cli/experiments/precision/AnalysisComparisonAlt.scala‎

Lines changed: 89 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package maf.cli.experiments.precision
22

3+
import maf.modular.scheme.aam._
34
import maf.cli.experiments._
45
import maf.language.scheme._
56
import maf.lattice._
@@ -19,7 +20,7 @@ abstract class AnalysisComparisonAlt[Num: IntLattice, Rea: RealLattice, Bln: Boo
1920
def analyses: List[(SchemeExp => Analysis, String)]
2021

2122
// and can, optionally, be configured in its timeouts (default: 30min.) and the number of concrete runs
22-
def timeout() = Timeout.start(Duration(30, MINUTES)) // timeout for the analyses
23+
def timeout() = Timeout.start(Duration(30, SECONDS)) // timeout for the analyses
2324
def runs = 3 // number of runs for the concrete interpreter
2425

2526
// keep the results of the benchmarks in a table
@@ -76,33 +77,95 @@ object AnalysisComparisonAlt1
7677
ConstantPropagation.Sym
7778
]:
7879
def k = 0
79-
def ls = List(100)
80-
lazy val modf: (SchemeExp => Analysis, String) = (SchemeAnalyses.kCFAAnalysis(_, k), s"$k-CFA MODF")
81-
lazy val dss: (SchemeExp => Analysis, String) = (SchemeAnalyses.modflocalAnalysis(_, k), s"$k-CFA DSS")
80+
lazy val aam: (SchemeExp => Analysis, String) = (aamAnalysis(_, k), s"$k-CFA AAM")
81+
lazy val dss: (SchemeExp => Analysis, String) = (SchemeAnalyses.modflocalAnalysis(_, k), s"$k-CFA DSS")
8282
//lazy val wdss: (SchemeExp => Analysis, String) = (SchemeAnalyses.modFlocalAnalysisWidened(_, k), s"$k-CFA WDSS")
8383
//lazy val dssFS: (SchemeExp => Analysis, String) = (SchemeAnalyses.modflocalFSAnalysis(_, k), s"$k-CFA DSS-FS")
8484
//lazy val adaptive: List[(SchemeExp => Analysis, String)] = ls.map { l =>
8585
// (SchemeAnalyses.modflocalAnalysisAdaptiveA(_, k, l), s"$k-CFA DSS w/ ASW (l = $l)")
8686
//}
87-
def analyses = modf :: dss :: Nil
88-
def main(args: Array[String]) = runBenchmarks(
89-
Set(
90-
//"test/R5RS/various/collatz.scm",
91-
//"test/R5RS/various/mceval.scm",
92-
//"test/R5RS/various/church.scm",
93-
//"test/R5RS/various/regex.scm",
94-
//"test/R5RS/various/blur.scm",
95-
//"test/R5RS/various/bound-precision.scm",
96-
//"test/R5RS/various/eta.scm",
97-
//"test/R5RS/various/gcipd.scm",
98-
//"test/R5RS/various/four-in-a-row.scm",
99-
//"test/R5RS/various/grid.scm",
100-
//"test/R5RS/various/mj09.scm",
101-
//"test/R5RS/various/primtest.scm",
102-
//"test/R5RS/various/rsa.scm",
103-
//"test/R5RS/gambit/deriv.scm",
104-
//"test/R5RS/gambit/tak.scm",
105-
//"test/R5RS/gambit/browse.scm",
87+
88+
def aamAnalysis(prg: SchemeExp, k: Int) = new SchemeAAMGCAnalysis(prg, k)
89+
90+
def analyses = aam :: dss :: Nil
91+
92+
def gambit = List("array1.scm",
93+
"deriv.scm",
94+
// "graphs.scm",
95+
"nqueens.scm",
96+
"puzzle.scm",
97+
"sum.scm",
98+
"triangl.scm",
99+
"browse.scm",
100+
"destruc.scm",
101+
"lattice.scm",
102+
"paraffins.scm",
103+
"sboyer.scm",
104+
"sumloop.scm",
105+
"wc.scm",
106+
"cat.scm",
107+
"diviter.scm",
108+
"matrix.scm",
109+
"perm9.scm",
110+
"scheme.scm",
111+
"tail.scm",
112+
"compiler.scm",
113+
"earley.scm",
114+
"mazefun.scm",
115+
"peval.scm",
116+
"slatex.scm",
117+
"tak.scm",
118+
"ctak.scm",
119+
"fibc.scm",
120+
"nboyer.scm",
121+
"primes.scm",
122+
"string.scm",
123+
"trav1.scm"
124+
).map(file => s"test/R5RS/various/$file")
125+
126+
def gabriel = List(
127+
"boyer",
128+
"browse",
129+
"cpstak",
130+
"dderiv",
131+
"deriv",
132+
"destruct",
133+
"diviter",
134+
"divrec",
135+
"puzzle",
136+
"takl",
137+
"triangl"
138+
).map(name => s"test/R5RS/gabriel/$name.scm")
139+
140+
def main(args: Array[String]) = runBenchmarks(gabriel)
141+
/*
142+
List(
143+
//VARIOUS
144+
"test/R5RS/various/collatz.scm",
145+
"test/R5RS/various/mceval.scm",
146+
"test/R5RS/various/church.scm",
147+
"test/R5RS/various/regex.scm",
148+
"test/R5RS/various/blur.scm",
149+
"test/R5RS/various/bound-precision.scm",
150+
"test/R5RS/various/eta.scm",
151+
"test/R5RS/various/gcipd.scm",
152+
"test/R5RS/various/four-in-a-row.scm",
153+
"test/R5RS/various/grid.scm",
154+
"test/R5RS/various/mj09.scm",
155+
"test/R5RS/various/primtest.scm",
156+
"test/R5RS/various/rsa.scm",
157+
//GAMBIT
158+
"test/R5RS/gambit/array1.scm",
159+
"test/R5RS/gambit/deriv.scm",
160+
"test/R5RS/gambit/tak.scm",
161+
"test/R5RS/gambit/array1.scm",
162+
"test/R5RS/gambit/destruc.scm",
163+
"test/R5RS/gambit/diviter.scm",
164+
"test/R5RS/gambit/lattice.scm",
165+
"test/R5RS/gambit/nboyer.scm",
166+
"test/R5RS/gambit/paraffins.scm",
167+
"test/R5RS/gambit/perm9.scm",
168+
"test/R5RS/gambit/perm.scm",
106169
//"test/R5RS/gambit/earley.scm",
107170
//"test/R5RS/gambit/matrix.scm",
108171
//"test/R5RS/gambit/mazefun.scm",
@@ -121,14 +184,16 @@ object AnalysisComparisonAlt1
121184
"test/R5RS/various/strong-update.scm"
122185
)
123186
)
187+
*/
124188

125189
override def parseProgram(txt: String): SchemeExp =
126190
val parsed = SchemeParser.parse(txt)
127191
val prelud = SchemePrelude.addPrelude(parsed, incl = Set("__toplevel_cons", "__toplevel_cdr", "__toplevel_set-cdr!"))
128192
val transf = SchemeMutableVarBoxer.transform(prelud)
129193
SchemeParser.undefine(transf)
130194

131-
def runBenchmarks(benchmarks: Set[Benchmark]) =
195+
def runBenchmarks(benchmarks: List[Benchmark]) =
196+
assert(benchmarks.size == benchmarks.toSet.size)
132197
benchmarks.foreach(runBenchmark)
133198
val cols = analyses.map(_._2)
134199
println(results.prettyString(columns = cols))

‎code/jvm/src/main/scala/maf/cli/experiments/precision/PrecisionBenchmarks.scala‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,11 @@ import maf.util._
1212
import maf.util.benchmarks.Timeout
1313
import maf.language.scheme.interpreter.EmptyIO
1414

15+
sealed trait BaseAddr extends Address { def printable = true; def idn: Identity }
16+
case class VarAddr(vrb: Identifier) extends BaseAddr { def idn: Identity = vrb.idn; override def toString = s"<variable $vrb>" }
17+
case class PtrAddr(exp: Expression) extends BaseAddr { def idn = exp.idn; override def toString = s"<pointer $exp>" }
18+
case class PrmAddr(nam: String) extends BaseAddr { def idn: Identity = Identity.none; override def toString = s"<primitive $nam>" }
19+
1520
abstract class PrecisionBenchmarks[Num: IntLattice, Rea: RealLattice, Bln: BoolLattice, Chr: CharLattice, Str: StringLattice, Smb: SymbolLattice]:
1621

1722
type Benchmark = String
@@ -23,15 +28,11 @@ abstract class PrecisionBenchmarks[Num: IntLattice, Rea: RealLattice, Bln: BoolL
2328

2429
implicit def cpAnalysis(anl: ModularSchemeDomain): Analysis = anl.asInstanceOf[Analysis]
2530

26-
sealed trait BaseAddr extends Address { def printable = true; def idn: Identity }
27-
case class VarAddr(vrb: Identifier) extends BaseAddr { def idn: Identity = vrb.idn; override def toString = s"<variable $vrb>" }
28-
case class PtrAddr(exp: Expression) extends BaseAddr { def idn = exp.idn; override def toString = s"<pointer $exp>" }
29-
case class PrmAddr(nam: String) extends BaseAddr { def idn: Identity = Identity.none; override def toString = s"<primitive $nam>" }
30-
3131
private def convertAddr(addr: Address): BaseAddr = addr match
3232
case maf.modular.scheme.VarAddr(vrb, _) => VarAddr(vrb)
3333
case maf.modular.scheme.PtrAddr(exp, _) => PtrAddr(exp)
3434
case maf.modular.scheme.PrmAddr(nam) => PrmAddr(nam)
35+
case a: maf.modular.scheme.aam.AAMScheme#SchemeAddress => a.toBaseAddr
3536

3637
val baseDomain = new ModularSchemeLattice[BaseAddr, Str, Bln, Num, Rea, Chr, Smb]
3738
val baseLattice = baseDomain.schemeLattice
@@ -125,10 +126,12 @@ abstract class PrecisionBenchmarks[Num: IntLattice, Rea: RealLattice, Bln: BoolL
125126
val value1 = b1.getOrElse(pos, baseLattice.bottom)
126127
val value2 = b2.getOrElse(pos, baseLattice.bottom)
127128
if value1 == value2 then (acc._1 + pos, acc._2, acc._3, acc._4)
128-
else if baseLattice.subsumes(value1, value2) then (acc._1, acc._2 + pos, acc._3, acc._4)
129-
else if baseLattice.subsumes(value2, value1) then (acc._1, acc._2, acc._3 + pos, acc._4)
129+
else if baseLattice.subsumes(value1, value2) then
130+
(acc._1, acc._2 + pos, acc._3, acc._4)
131+
else if baseLattice.subsumes(value2, value1) then
132+
(acc._1, acc._2, acc._3 + pos, acc._4)
130133
else // neither value is more precise than the other
131-
(acc._1, acc._2, acc._3, acc._4 + pos)
134+
(acc._1, acc._2, acc._3, acc._4 + pos)
132135
}
133136

134137
/**
@@ -204,6 +207,7 @@ abstract class PrecisionBenchmarks[Num: IntLattice, Rea: RealLattice, Bln: BoolL
204207
else TimedOut(res)
205208
catch
206209
case e: Exception =>
210+
e.printStackTrace()
207211
println(s"Analyzer failed with exception $e")
208212
Errored(e)
209213
case e: VirtualMachineError =>

‎code/shared/src/main/scala/maf/modular/scheme/aam/AAMScheme.scala‎

Lines changed: 14 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -51,23 +51,29 @@ abstract class AAMScheme(prg: SchemeExp) extends ModAnalysis[SchemeExp](prg):
5151

5252
// addresses
5353

54-
case class NAdr(nat: String) extends Address:
54+
sealed trait SchemeAddress extends Address:
55+
def toBaseAddr: maf.cli.experiments.precision.BaseAddr
56+
57+
case class NAdr(nat: String) extends SchemeAddress:
5558
def idn = Identity.none
5659
def printable = false
57-
case class VAdr(vrb: Var, ctx: Ctx) extends Address:
60+
def toBaseAddr = maf.cli.experiments.precision.PrmAddr(nat)
61+
case class VAdr(vrb: Var, ctx: Ctx) extends SchemeAddress:
5862
def idn = vrb.idn
5963
def printable = true
60-
case class PAdr(exp: Exp, ctx: Ctx) extends Address:
64+
def toBaseAddr = maf.cli.experiments.precision.VarAddr(vrb)
65+
case class PAdr(exp: Exp, ctx: Ctx) extends SchemeAddress:
6166
def idn = exp.idn
6267
def printable = true
68+
def toBaseAddr = maf.cli.experiments.precision.PtrAddr(exp)
6369
trait KAdr extends Address:
6470
def printable = false
65-
case class KA(e: Exp, ctx: Ctx) extends KAdr:
66-
def idn = e.idn
71+
case class KA(ev: Ev, sto: Sto) extends KAdr:
72+
def idn = ev.e.idn
6773
case object HaltAddr extends KAdr:
6874
def idn = Identity.none
6975

70-
def kalloc(e: Exp, ctx: Ctx) = KA(e, ctx)
76+
def kalloc(ev: Ev, sto: Sto) = KA(ev, sto)
7177
def alloc(v: Var, ctx: Ctx) = VAdr(v, ctx)
7278
def alloc(e: Exp, ctx: Ctx) = PAdr(e, ctx)
7379

@@ -244,7 +250,7 @@ abstract class AAMScheme(prg: SchemeExp) extends ModAnalysis[SchemeExp](prg):
244250
push(LtrK(rst, adr, bdy, ρ, t, aₖ), exp, ρ, t, σ, σₖ)
245251

246252
protected def push(frm: Frame, e: Exp, ρ: Env, t: Ctx, σ: Sto, σₖ: KSto) =
247-
val ak2 = kalloc(e, t)
253+
val ak2 = kalloc(Ev(e, ρ, t), σ)
248254
Set(State(Ev(e, ρ, t), σ, σₖ.extend(ak2, Set(frm)), ak2))
249255

250256
private def result(v: Val, σ: Sto, σₖ: KSto, aₖ: KAdr) =
@@ -270,7 +276,7 @@ abstract class AAMScheme(prg: SchemeExp) extends ModAnalysis[SchemeExp](prg):
270276
given SchemePrimM[AAM, Adr, Val] with
271277
def lookupSto(a: Adr): AAM[Val] = (_, σ) => Set((σ(a), σ))
272278
def extendSto(a: Adr, v: Val) = (_, σ) => Set(((), σ.extend(a, v)))
273-
def updateSto(a: Adr, v: Val) = (_, σ) => Set(((), σ.extend(a, v)))
279+
def updateSto(a: Adr, v: Val) = (_, σ) => Set(((), σ.update(a, v)))
274280
def allocVar(v: Var): AAM[Adr] = (c, σ) => Set((alloc(v, c), σ))
275281
def allocPtr(e: Exp): AAM[Adr] = (c, σ) => Set((alloc(e, c), σ))
276282
def mbottom[X]: AAM[X] = (_, _) => Set.empty

0 commit comments

Comments
 (0)