11package maf .cli .experiments .precision
22
3- import maf .modular .scheme .aam ._
43import maf .cli .experiments ._
54import maf .language .scheme ._
65import maf .lattice ._
@@ -9,21 +8,26 @@ import maf.util.benchmarks._
98import maf .util .{Reader , Writer }
109import maf .language .scheme .primitives .SchemePrelude
1110import maf .bench .scheme .*
12-
1311import scala .concurrent .duration ._
12+ import maf .modular .scheme .modflocal ._
13+
1414
15+ // compares analyses by counting number of over-approximations w.r.t. a concrete interpreter
16+ // (lower is better)
1517abstract class AnalysisComparisonAlt [Num : IntLattice , Rea : RealLattice , Bln : BoolLattice , Chr : CharLattice , Str : StringLattice , Smb : SymbolLattice ]
1618 extends PrecisionBenchmarks [Num , Rea , Bln , Chr , Str , Smb ]:
1719
1820 // the precision comparison is parameterized by:
1921 // - the analyses to compare in terms of precision
22+ // - the benchmarks to compare the analyses on
2023 // - the number of runs for the concrete interpreter
2124 def analyses : List [(SchemeExp => Analysis , String )]
22-
23- // and can, optionally, be configured in its timeouts (default: 30min.) and the number of concrete runs
24- def timeout () = Timeout .start(Duration (5 , MINUTES )) // timeout for the analyses
25+ def benchmarks : List [Benchmark ]
2526 def runs = 3 // number of runs for the concrete interpreter
2627
28+ // and can, optionally, be configured in its timeouts (default: 10min.) and the number of concrete runs
29+ def timeout () = Timeout .start(Duration (10 , MINUTES )) // timeout for the analyses
30+
2731 // keep the results of the benchmarks in a table
2832 enum Result :
2933 case Success (abs : Int )
@@ -33,7 +37,9 @@ abstract class AnalysisComparisonAlt[Num: IntLattice, Rea: RealLattice, Bln: Boo
3337 case Result .Success (abs) => s " $abs"
3438 case Result .Timeout (abs) => s " TIMEOUT (>= $abs) "
3539 case Result .Errored => " ERROR"
36- var results : Table [Result ] = Table .empty
40+
41+ var precisionResults : Table [Result ] = Table .empty
42+ var performanceResults : Table [Option [Double ]] = Table .empty
3743
3844 protected def additionalCounts (analysisName : String , path : Benchmark , r1 : ResultMap , r2 : ResultMap ): Unit = ()
3945
@@ -54,7 +60,7 @@ abstract class AnalysisComparisonAlt[Num: IntLattice, Rea: RealLattice, Bln: Boo
5460 val t0 = System .nanoTime
5561 val otherResult = runAnalysis(analysis, name, program, path, timeout())
5662 val t1 = System .nanoTime
57- val duration = (System .nanoTime - t0) / 1e9d
63+ val duration = (System .nanoTime - t0) / 1e9d // duration is reported in seconds
5864 println(s " duration: $duration" )
5965 val (lessPrecise, size) = otherResult match
6066 case Terminated (analysisResult) =>
@@ -64,11 +70,39 @@ abstract class AnalysisComparisonAlt[Num: IntLattice, Rea: RealLattice, Bln: Boo
6470 additionalCounts(name, path, partialResult, concreteResult)
6571 (Result .Timeout (compareOrdered(partialResult, concreteResult, check = false ).size), Result .Timeout (partialResult.keys.size))
6672 case Errored (_) => (Result .Errored , Result .Errored )
67- results = results .add(path, name, lessPrecise)
68- results = results .add(path, s " $name-total " , size)
73+ precisionResults = precisionResults .add(path, name, lessPrecise)
74+ // precisionResults = precisionResults .add(path, s"$name-total", size)
6975 }
7076
71- object AnalysisComparisonAlt1
77+ private def runBenchmarks (benchmarks : List [Benchmark ], outputFolder : Option [String ] = None ) =
78+ assert(benchmarks.size == benchmarks.toSet.size) // sanity check to make sure we don't have duplicates
79+ benchmarks.foreach(runBenchmark)
80+ showResults(outputFolder)
81+
82+ protected def showResults (outputFolder : Option [String ]) =
83+ println(" PRECISION RESULTS" )
84+ println(" =================" )
85+ println()
86+ println(precisionResults.prettyString())
87+ println()
88+ println(" PERFORMANCE RESULTS" )
89+ println(" ===================" )
90+ println()
91+ println(performanceResults.prettyString())
92+ outputFolder.foreach { dir =>
93+ writeToFile(precisionResults, s " $dir/precision-benchmarks.csv " )
94+ writeToFile(performanceResults, s " $dir/performance-benchmarks.csv " )
95+ }
96+
97+ protected def writeToFile [X ](results : Table [X ], path : String ) =
98+ val writer = Writer .open(path)
99+ Writer .write(writer, results.toCSVString(rowName = " benchmark" ))
100+ Writer .close(writer)
101+
102+ def main (args : Array [String ]) = runBenchmarks(benchmarks, args.headOption)
103+
104+
105+ abstract class SASBenchmarks
72106 extends AnalysisComparisonAlt [
73107 ConstantPropagation .I ,
74108 ConstantPropagation .R ,
@@ -77,101 +111,98 @@ object AnalysisComparisonAlt1
77111 ConstantPropagation .S ,
78112 ConstantPropagation .Sym
79113 ]:
80- def k = 0
81- lazy val aam0 : (SchemeExp => Analysis , String ) = (aamAnalysis(_, 0 ), s " 0-CFA AAM " )
82- lazy val aam1 : (SchemeExp => Analysis , String ) = (aamAnalysis(_, 1 ), s " 1-CFA AAM " )
83- lazy val aam2 : (SchemeExp => Analysis , String ) = (aamAnalysis(_, 2 ), s " 2-CFA AAM " )
84- lazy val dss0 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalAnalysis(_, 0 ), " 0-CFA DSS" )
85- lazy val dss1 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalAnalysis(_, 1 ), " 1-CFA DSS" )
86- lazy val dss2 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalAnalysis(_, 2 ), " 2-CFA DSS" )
87- lazy val dssFS0 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 0 ), " 0-CFA FS-DSS" )
88- lazy val dssFS1 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 1 ), " 1-CFA FS-DSS" )
89- lazy val dssFS2 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 2 ), " 2-CFA FS-DSS" )
90- // lazy val wdss: (SchemeExp => Analysis, String) = (SchemeAnalyses.modFlocalAnalysisWidened(_, k), s"$k-CFA WDSS")
91- // lazy val dssFS: (SchemeExp => Analysis, String) = (SchemeAnalyses.modflocalFSAnalysis(_, k), s"$k-CFA DSS-FS")
92- // lazy val adaptive: List[(SchemeExp => Analysis, String)] = ls.map { l =>
93- // (SchemeAnalyses.modflocalAnalysisAdaptiveA(_, k, l), s"$k-CFA DSS w/ ASW (l = $l)")
94- // }
95-
96- def aamAnalysis (prg : SchemeExp , k : Int ) = new SchemeAAMGCAnalysis (prg, k)
97-
98- def analyses = List (
99- aam0, aam1, aam2,
100- dss0, dss1, dss2,
101- dssFS0, dssFS1, dssFS2
102- )
103-
104- def gambit = List (" array1.scm" ,
105- " deriv.scm" ,
106- // "graphs.scm",
107- " nqueens.scm" ,
108- " puzzle.scm" ,
109- " sum.scm" ,
110- " triangl.scm" ,
111- " browse.scm" ,
112- " destruc.scm" ,
113- " lattice.scm" ,
114- " paraffins.scm" ,
115- " sboyer.scm" ,
116- " sumloop.scm" ,
117- // "wc.scm",
118- // "cat.scm",
119- " diviter.scm" ,
120- " matrix.scm" ,
121- " perm9.scm" ,
122- " scheme.scm" ,
123- // "tail.scm",
124- " compiler.scm" ,
125- " earley.scm" ,
126- " mazefun.scm" ,
127- " peval.scm" ,
128- " slatex.scm" ,
129- " tak.scm" ,
130-
131- // "ctak.scm",
132- // "fibc.scm",
133- " nboyer.scm" ,
134- " primes.scm" ,
135- " string.scm" ,
136- " trav1.scm"
137- ).map(file => s " test/R5RS/various/ $file" )
138-
139- def sas2025 =
114+
115+ lazy val aam0 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .aamGCAnalysis(_, 0 ), " 0-CFA AAM" )
116+ lazy val aam1 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .aamGCAnalysis(_, 1 ), " 1-CFA AAM" )
117+ lazy val aam2 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .aamGCAnalysis(_, 2 ), " 2-CFA AAM" )
118+ lazy val dss0 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalAnalysis(_, 0 ), " 0-CFA DSS" )
119+ lazy val dss1 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalAnalysis(_, 1 ), " 1-CFA DSS" )
120+ lazy val dss2 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalAnalysis(_, 2 ), " 2-CFA DSS" )
121+ lazy val dssFS0 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 0 , true ), " 0-CFA DSS-FS" )
122+ lazy val dssFS1 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 1 , true ), " 1-CFA DSS-FS" )
123+ lazy val dssFS2 : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 2 , true ), " 2-CFA DSS-FS" )
124+ lazy val dssFS0NoGC : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 0 , false ), " 0-CFA DSS-FS (without GC)" )
125+ lazy val dssFS1NoGC : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 1 , false ), " 1-CFA DSS-FS (without GC)" )
126+ lazy val dssFS2NoGC : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalFSAnalysis(_, 2 , false ), " 2-CFA DSS-FS (without GC)" )
127+
128+ def gabrielBenchmarks =
129+ List (
130+ " boyer" ,
131+ " browse" ,
132+ " cpstak" ,
133+ " dderiv" ,
134+ " deriv" ,
135+ " destruc" ,
136+ " diviter" ,
137+ " divrec" ,
138+ " takl" ,
139+ // "triangl" <- times out in concrete interpreter
140+ ).map(name => s " test/R5RS/gabriel/ $name.scm " )
141+
142+ def extraBenchmarks =
140143 List (
141- // "test/R5RS/gambit/deriv.scm",
142- // "test/R5RS/gambit/tak.scm",
143- // "test/R5RS/various/grid.scm",
144- // "test/R5RS/various/regex.scm",
145- // "test/R5RS/WeiChenRompf2019/rsa.scm"
144+ " test/R5RS/various/grid.scm" ,
145+ " test/R5RS/gambit/matrix.scm" ,
146+ " test/R5RS/various/mceval.scm" ,
147+ " test/R5RS/various/regex.scm" ,
148+ " test/R5RS/WeiChenRompf2019/rsa.scm" ,
149+ " test/R5RS/gambit/tak.scm" ,
146150 )
147151
148- def gabriel = List (
149- " boyer" ,
150- " browse" ,
151- " cpstak" ,
152- " dderiv" ,
153- " deriv" ,
154- " destruc" ,
155- " diviter" ,
156- " divrec" ,
157- " puzzle" ,
158- " takl" ,
159- // "triangl"
160- ).map(name => s " test/R5RS/gabriel/ $name.scm " )
161-
162- def main (args : Array [String ]) = runBenchmarks(gabriel)
152+ def benchmarks = gabrielBenchmarks ++ extraBenchmarks
163153
164154 override def parseProgram (txt : String ): SchemeExp =
165155 val parsed = SchemeParser .parse(txt)
166156 val prelud = SchemePrelude .addPrelude(parsed, incl = Set (" __toplevel_cons" , " __toplevel_cdr" , " __toplevel_set-cdr!" ))
167157 val transf = SchemeMutableVarBoxer .transform(prelud)
168158 SchemeParser .undefine(transf)
169159
170- def runBenchmarks (benchmarks : List [Benchmark ]) =
171- assert(benchmarks.size == benchmarks.toSet.size)
172- benchmarks.foreach(runBenchmark)
173- val cols = analyses.map(_._2)
174- println(results.prettyString(columns = cols))
175- val writer = Writer .open(" benchOutput/precision/precision-benchmarks.csv" )
176- Writer .write(writer, results.toCSVString(rowName = " benchmark" , columns = cols))
177- Writer .close(writer)
160+ object AllSASBenchmarks extends SASBenchmarks :
161+ def analyses = List (
162+ aam0, aam1, aam2,
163+ dss0, dss1, dss2,
164+ dssFS0, dssFS1, dssFS2,
165+ dssFS0NoGC, dssFS1NoGC, dssFS2NoGC
166+ )
167+
168+ object Table2Benchmarks extends SASBenchmarks :
169+ def analyses = List (
170+ aam0, aam1, aam2,
171+ dss0, dss1, dss2,
172+ )
173+
174+ object Table3Benchmarks extends SASBenchmarks :
175+ def analyses = List (
176+ dss0, dss1, dss2,
177+ dssFS0, dssFS1, dssFS2,
178+ )
179+
180+ object Table4Benchmarks extends SASBenchmarks :
181+ def analyses = List (
182+ dssFS0, dssFS1, dssFS2,
183+ dssFS0NoGC, dssFS1NoGC, dssFS2NoGC
184+ )
185+
186+ object CountIterationBenchmark extends SASBenchmarks :
187+
188+ def analyses = List (
189+ dssFS0, dssFS0NoGC
190+ )
191+
192+ var results : Table [Int ] = Table .empty
193+
194+ override protected def forBenchmark (path : Benchmark , program : SchemeExp ): Unit =
195+ println(s " ANALYZING $path" )
196+ analyses.foreach { case (analysis, name) =>
197+ val anl = analysis(program)
198+ anl.analyzeWithTimeout(Timeout .start(Duration (15 , MINUTES )))
199+ results = results.add(path, name, anl.asInstanceOf [SchemeModFLocalFS ].iterations)
200+ }
201+
202+ override def timeout () = Timeout .none
203+
204+ override protected def showResults (outputFolder : Option [String ]) =
205+ println(results.prettyString())
206+ outputFolder.foreach { dir =>
207+ writeToFile(results, s " $dir/iteration-benchmarks.csv " )
208+ }
0 commit comments