11package maf .cli .experiments .precision
22
3+ import maf .modular .scheme .aam ._
34import maf .cli .experiments ._
45import maf .language .scheme ._
56import maf .lattice ._
67import maf .lattice .interfaces .{BoolLattice , CharLattice , IntLattice , RealLattice , StringLattice , SymbolLattice }
78import maf .util ._
89import maf .util .benchmarks ._
10+ import maf .language .scheme .primitives .SchemePrelude
911
1012import scala .concurrent .duration ._
1113
@@ -19,10 +21,10 @@ abstract class AnalysisComparison[Num: IntLattice, Rea: RealLattice, Bln: BoolLa
1921 def otherAnalyses (): List [(SchemeExp => Analysis , String )]
2022
2123 // 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
24+ def analysisTimeout (): Timeout .T = Timeout .start(Duration (30 , SECONDS )) // timeout for (non-base) analyses
25+ def concreteTimeout (): Timeout .T = Timeout .start( Duration ( 30 , SECONDS )) // timeout for concrete interpreter
2426
25- def concreteRuns () = 5
27+ def concreteRuns () = 3
2628
2729 // keep the results of the benchmarks in a table
2830 var results : Table [Option [Int ]] = Table .empty[Option [Int ]]
@@ -63,38 +65,86 @@ object AnalysisComparison1
6365 ConstantPropagation .S ,
6466 ConstantPropagation .Sym
6567 ]:
68+
6669 val k = 0
67- val l = 1000
70+
71+ lazy val aam : (SchemeExp => Analysis , String ) = (new SchemeAAMGCAnalysis (_, k), s " $k-CFA AAM " )
72+ lazy val dss : (SchemeExp => Analysis , String ) = (SchemeAnalyses .modflocalAnalysis(_, k), s " $k-CFA DSS " )
73+
6874 def baseAnalysis (prg : SchemeExp ): Analysis =
69- SchemeAnalyses .kCFAAnalysis(prg, k)
70- def otherAnalyses () =
71- // run some regular k-cfa analyses
75+ SchemeAnalyses .contextInsensitiveAnalysis(prg) // context-insensitive analysis
76+ def otherAnalyses () = aam :: dss :: Nil
77+
78+ def gambit = List (" array1.scm" ,
79+ " deriv.scm" ,
80+ // "graphs.scm",
81+ " nqueens.scm" ,
82+ " puzzle.scm" ,
83+ " sum.scm" ,
84+ " triangl.scm" ,
85+ " browse.scm" ,
86+ " destruc.scm" ,
87+ " lattice.scm" ,
88+ " paraffins.scm" ,
89+ " sboyer.scm" ,
90+ " sumloop.scm" ,
91+ " wc.scm" ,
92+ " cat.scm" ,
93+ " diviter.scm" ,
94+ " matrix.scm" ,
95+ " perm9.scm" ,
96+ " scheme.scm" ,
97+ " tail.scm" ,
98+ " compiler.scm" ,
99+ " earley.scm" ,
100+ " mazefun.scm" ,
101+ " peval.scm" ,
102+ " slatex.scm" ,
103+ " tak.scm" ,
104+ " ctak.scm" ,
105+ " fibc.scm" ,
106+ " nboyer.scm" ,
107+ " primes.scm" ,
108+ " string.scm" ,
109+ " trav1.scm"
110+ ).map(file => s " test/R5RS/various/ $file" )
111+
112+ def gabriel = List (
113+ " boyer" ,
114+ " browse" ,
115+ " cpstak" ,
116+ " dderiv" ,
117+ " deriv" ,
118+ " destruc" ,
119+ " diviter" ,
120+ " divrec" ,
121+ " puzzle" ,
122+ " takl" ,
123+ " triangl"
124+ ).map(name => s " test/R5RS/gabriel/ $name.scm " )
125+
126+ def sas2025 =
72127 List (
73- // (SchemeAnalyses.modflocalAnalysis(_, 0), "0-CFA DSS"),
74- // (SchemeAnalyses.modflocalAnalysisAdaptiveA(_, k, l), s"$k-CFA DSS w/ ASW (l = $l)")
128+ " test/R5RS/gambit/deriv.scm" ,
129+ " test/R5RS/gambit/tak.scm" ,
130+ " test/R5RS/various/grid.scm" ,
131+ " test/R5RS/various/regex.scm" ,
132+ " test/R5RS/various/rsa.scm"
75133 )
76134
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- }
94135
95- def runBenchmarks (benchmarks : Set [Benchmark ]) =
136+ def main (args : Array [String ]) = runBenchmarks(sas2025)
137+
138+ override def parseProgram (txt : String ): SchemeExp =
139+ val parsed = SchemeParser .parse(txt)
140+ val prelud = SchemePrelude .addPrelude(parsed, incl = Set (" __toplevel_cons" , " __toplevel_cdr" , " __toplevel_set-cdr!" ))
141+ val transf = SchemeMutableVarBoxer .transform(prelud)
142+ SchemeParser .undefine(transf)
143+
144+ def runBenchmarks (benchmarks : List [Benchmark ]) =
145+ assert(benchmarks.size == benchmarks.toSet.size)
96146 benchmarks.foreach(runBenchmark)
97147 println(results.prettyString(format = _.map(_.toString()).getOrElse(" TIMEOUT" )))
98- val writer = Writer .open(" benchOutput/precision/adaptive- precision-benchmarks.csv" )
148+ val writer = Writer .open(" benchOutput/precision/precision-benchmarks.csv" )
99149 Writer .write(writer, results.toCSVString(format = _.map(_.toString()).getOrElse(" TIMEOUT" ), rowName = " benchmark" ))
100150 Writer .close(writer)
0 commit comments