Skip to content

Commit 7d12746

Browse files
committed
fix ModFLocalFS
1 parent 26813c4 commit 7d12746

4 files changed

Lines changed: 77 additions & 62 deletions

File tree

code/jvm/src/main/scala/maf/cli/experiments/SchemeAnalyses.scala

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,13 @@ object SchemeAnalyses:
148148
with FIFOWorklistAlgorithm[SchemeExp]
149149
with SchemeModFLocalAnalysisResults
150150

151+
def modflocalFSAnalysis(prg: SchemeExp, k: Int) =
152+
new SchemeModFLocalFS(prg)
153+
with SchemeConstantPropagationDomain
154+
with SchemeModFLocalCallSiteSensitivity(k)
155+
with FIFOWorklistAlgorithm[SchemeExp]
156+
with SchemeModFLocalFSAnalysisResults
157+
151158
// Flow sensitive analysis
152159
def modFFlowSensitive(prg: SchemeExp) =
153160
new SimpleFlowSensitiveAnalysis(prg)

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

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import maf.lattice._
77
import maf.lattice.interfaces.{BoolLattice, CharLattice, IntLattice, RealLattice, StringLattice, SymbolLattice}
88
import maf.util._
99
import maf.util.benchmarks._
10+
import maf.language.scheme.primitives.SchemePrelude
1011

1112
import scala.concurrent.duration._
1213

@@ -21,9 +22,9 @@ abstract class AnalysisComparison[Num: IntLattice, Rea: RealLattice, Bln: BoolLa
2122

2223
// and can, optionally, be configured in its timeouts (default: 5min.)
2324
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
25+
def concreteTimeout(): Timeout.T = Timeout.start(Duration(30, SECONDS)) //timeout for concrete interpreter
2526

26-
def concreteRuns() = 5
27+
def concreteRuns() = 3
2728

2829
// keep the results of the benchmarks in a table
2930
var results: Table[Option[Int]] = Table.empty[Option[Int]]
@@ -114,15 +115,25 @@ object AnalysisComparison1
114115
"cpstak",
115116
"dderiv",
116117
"deriv",
117-
"destruct",
118+
"destruc",
118119
"diviter",
119120
"divrec",
120121
"puzzle",
121122
"takl",
122123
"triangl"
123124
).map(name => s"test/R5RS/gabriel/$name.scm")
124125

125-
def main(args: Array[String]) = runBenchmarks(gabriel)
126+
def sas2025 =
127+
List(
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"
133+
)
134+
135+
136+
def main(args: Array[String]) = runBenchmarks(sas2025)
126137

127138
override def parseProgram(txt: String): SchemeExp =
128139
val parsed = SchemeParser.parse(txt)

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

Lines changed: 33 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import maf.lattice.interfaces.{BoolLattice, CharLattice, IntLattice, RealLattice
88
import maf.util.benchmarks._
99
import maf.util.{Reader, Writer}
1010
import maf.language.scheme.primitives.SchemePrelude
11+
import maf.bench.scheme.*
1112

1213
import scala.concurrent.duration._
1314

@@ -20,7 +21,7 @@ abstract class AnalysisComparisonAlt[Num: IntLattice, Rea: RealLattice, Bln: Boo
2021
def analyses: List[(SchemeExp => Analysis, String)]
2122

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

2627
// keep the results of the benchmarks in a table
@@ -77,8 +78,15 @@ object AnalysisComparisonAlt1
7778
ConstantPropagation.Sym
7879
]:
7980
def k = 0
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")
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")
8290
//lazy val wdss: (SchemeExp => Analysis, String) = (SchemeAnalyses.modFlocalAnalysisWidened(_, k), s"$k-CFA WDSS")
8391
//lazy val dssFS: (SchemeExp => Analysis, String) = (SchemeAnalyses.modflocalFSAnalysis(_, k), s"$k-CFA DSS-FS")
8492
//lazy val adaptive: List[(SchemeExp => Analysis, String)] = ls.map { l =>
@@ -87,7 +95,11 @@ object AnalysisComparisonAlt1
8795

8896
def aamAnalysis(prg: SchemeExp, k: Int) = new SchemeAAMGCAnalysis(prg, k)
8997

90-
def analyses = aam :: dss :: Nil
98+
def analyses = List(
99+
aam0, aam1, aam2,
100+
dss0, dss1, dss2,
101+
dssFS0, dssFS1, dssFS2
102+
)
91103

92104
def gambit = List("array1.scm",
93105
"deriv.scm",
@@ -102,89 +114,52 @@ object AnalysisComparisonAlt1
102114
"paraffins.scm",
103115
"sboyer.scm",
104116
"sumloop.scm",
105-
"wc.scm",
106-
"cat.scm",
117+
//"wc.scm",
118+
//"cat.scm",
107119
"diviter.scm",
108120
"matrix.scm",
109121
"perm9.scm",
110122
"scheme.scm",
111-
"tail.scm",
123+
//"tail.scm",
112124
"compiler.scm",
113125
"earley.scm",
114126
"mazefun.scm",
115127
"peval.scm",
116128
"slatex.scm",
117129
"tak.scm",
118-
"ctak.scm",
119-
"fibc.scm",
130+
131+
//"ctak.scm",
132+
//"fibc.scm",
120133
"nboyer.scm",
121134
"primes.scm",
122135
"string.scm",
123136
"trav1.scm"
124137
).map(file => s"test/R5RS/various/$file")
125138

139+
def sas2025 =
140+
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"
146+
)
147+
126148
def gabriel = List(
127149
"boyer",
128150
"browse",
129151
"cpstak",
130152
"dderiv",
131153
"deriv",
132-
"destruct",
154+
"destruc",
133155
"diviter",
134156
"divrec",
135157
"puzzle",
136158
"takl",
137-
"triangl"
159+
//"triangl"
138160
).map(name => s"test/R5RS/gabriel/$name.scm")
139161

140162
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",
169-
//"test/R5RS/gambit/earley.scm",
170-
//"test/R5RS/gambit/matrix.scm",
171-
//"test/R5RS/gambit/mazefun.scm",
172-
//"test/R5RS/gambit/nqueens.scm",
173-
//"test/R5RS/gambit/peval.scm",
174-
//"test/R5RS/scp1/flatten.scm",
175-
//"test/R5RS/icp/icp_1c_multiple-dwelling.scm",
176-
//"test/R5RS/icp/icp_1c_ontleed.scm",
177-
//"test/R5RS/icp/icp_1c_prime-sum-pair.scm",
178-
//"test/R5RS/icp/icp_2_aeval.scm",
179-
//"test/R5RS/icp/icp_3_leval.scm",
180-
//"test/R5RS/icp/icp_5_regsim.scm",
181-
//"test/R5RS/icp/icp_7_eceval.scm",
182-
//"test/R5RS/icp/icp_8_compiler.scm",
183-
//"test/R5RS/various/lambda-update.scm",
184-
"test/R5RS/various/strong-update.scm"
185-
)
186-
)
187-
*/
188163

189164
override def parseProgram(txt: String): SchemeExp =
190165
val parsed = SchemeParser.parse(txt)

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

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import maf.language.CScheme._
1010
import maf.lattice.interfaces.BoolLattice
1111
import maf.lattice.interfaces.LatticeWithAddrs
1212
import maf.util.datastructures.SmartMap
13+
import maf.core.Monad.MonadSyntaxOps
1314

1415
abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](prg) with SchemeSemantics:
1516
inter: SchemeDomain with SchemeModFLocalSensitivity =>
@@ -98,11 +99,32 @@ abstract class SchemeModFLocalFS(prg: SchemeExp) extends ModAnalysis[SchemeExp](
9899
(vlu, gcd, gcu, gca)
99100
}
100101

102+
import analysisM_._
103+
override def eval(exp: Exp): A[Val] =
104+
withEnv(_.restrictTo(exp.fv)) {
105+
getEnv >>= { env =>
106+
withRestrictedStore(env.addrs) {
107+
super.eval(exp)
108+
}
109+
}
110+
}
111+
112+
override protected def applyPrimitive(app: App, prm: Prim, ags: List[Val]): A[Val] =
113+
withRestrictedStore(ags.flatMap(lattice.refs).toSet) {
114+
super.applyPrimitive(app, prm, ags)
115+
}
116+
101117
override protected def applyClosure(app: App, lam: Lam, ags: List[Val], fvs: Iterable[(Adr, Val)]): A[Val] =
102118
withRestrictedStore(ags.flatMap(lattice.refs).toSet ++ fvs.flatMap((_, vlu) => lattice.refs(vlu))) {
103119
super.applyClosure(app, lam, ags, fvs)
104120
}
105121

122+
override protected def nontail[X](blk: => A[X]) =
123+
(anl, env, sto, ctx) =>
124+
blk(anl, env, sto, ctx).map { (v, d, u, a) =>
125+
(v, sto.replay(d, a), u, a)
126+
}
127+
106128
override def init() =
107129
super.init()
108130
stores += MainComponent -> initialSto

0 commit comments

Comments
 (0)