Skip to content

Commit 2a53c11

Browse files
amoelleramoeller
committed
Cumulative updates
1 parent e8b4245 commit 2a53c11

File tree

8 files changed

+106
-79
lines changed

8 files changed

+106
-79
lines changed

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,7 @@ where `<source>` can be a file or a directory containing `.tip` files and
8888
`[out]` is an output directory (default: ./out).
8989

9090
To see the possible options, run `tip` without options.
91+
Option `-verbose` is recommended when developing and testing analyses.
9192

9293
## Help to Scala novices
9394

‎examples/interval0.tip‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
main() {
2+
var x,y;
3+
y = 0;
4+
x = 7;
5+
x = x + 1;
6+
while (input) {
7+
x = 7;
8+
x = x+1;
9+
y = y+1;
10+
}
11+
return 0;
12+
}

‎src/tip/Tip.scala‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -123,14 +123,14 @@ object Tip extends App {
123123
| immediately after the analysis name (default: use the simple fixpoint solver):
124124
|
125125
| wl use the worklist solver
126-
| wli use the worklist solver with init
127-
| wliw use the worklist solver with init and widening
128-
| wliwn use the worklist solver with init, widening, and narrowing
129-
| wlip use the worklist solver with init and propagation
130-
| iwli use the worklist solver with init, interprocedural version
131-
| iwlip use the worklist solver with init and propagation, interprocedural version
132-
| csiwlip use the worklist solver with init and propagation, context-sensitive (with call string) interprocedural version
133-
| cfiwlip use the worklist solver with init and propagation, context-sensitive (with functional approach) interprocedural version
126+
| wlr use the worklist solver with reachability
127+
| wlrw use the worklist solver with reachability and widening
128+
| wlrwn use the worklist solver with reachability, widening, and narrowing
129+
| wlrp use the worklist solver with reachability and propagation
130+
| iwlr use the worklist solver with reachability, interprocedural version
131+
| iwlrp use the worklist solver with reachability and propagation, interprocedural version
132+
| csiwlrp use the worklist solver with reachability and propagation, context-sensitive (with call string) interprocedural version
133+
| cfiwlrp use the worklist solver with reachability and propagation, context-sensitive (with functional approach) interprocedural version
134134
| ide use the IDE solver
135135
|
136136
| e.g. -sign wl will run the sign analysis using the basic worklist solver

‎src/tip/analysis/FlowSensitiveAnalysis.scala‎

Lines changed: 31 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ object FlowSensitiveAnalysis {
3333
def select(kind: Analysis.Value, options: AnalysisOption.Value, cfg: FragmentCfg)(implicit declData: DeclarationData): Option[FlowSensitiveAnalysis[_]] = {
3434

3535
val typedCfg = options match {
36-
case AnalysisOption.iwli | AnalysisOption.iwlip | AnalysisOption.`csiwlip` | AnalysisOption.`cfiwlip` | AnalysisOption.`ide` =>
36+
case AnalysisOption.`iwlr` | AnalysisOption.`iwlrp` | AnalysisOption.`csiwlrp` | AnalysisOption.`cfiwlrp` | AnalysisOption.`ide` =>
3737
cfg match {
3838
case w: InterproceduralProgramCfg => Right(w)
3939
case _ => throw new RuntimeException(s"Whole CFG needed")
@@ -67,43 +67,43 @@ object FlowSensitiveAnalysis {
6767
case Analysis.constprop => new ConstantPropagationAnalysisWorklistSolver(typedCfg.left.get)
6868
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
6969
})
70-
case AnalysisOption.`wli` =>
70+
case AnalysisOption.`wlr` =>
7171
Some(kind match {
72-
case Analysis.sign => new IntraprocSignAnalysisWorklistSolverWithInit(typedCfg.left.get)
73-
case Analysis.interval => new IntervalAnalysisWorklistSolverWithInit(typedCfg.left.get)
72+
case Analysis.sign => new IntraprocSignAnalysisWorklistSolverWithReachability(typedCfg.left.get)
73+
case Analysis.interval => new IntervalAnalysisWorklistSolverWithReachability(typedCfg.left.get)
7474
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
7575
})
76-
case AnalysisOption.`wliw` =>
76+
case AnalysisOption.`wlrw` =>
7777
Some(kind match {
7878
case Analysis.interval => new IntervalAnalysisWorklistSolverWithWidening(typedCfg.left.get)
7979
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
8080
})
81-
case AnalysisOption.`wliwn` =>
81+
case AnalysisOption.`wlrwn` =>
8282
Some(kind match {
8383
case Analysis.interval => new IntervalAnalysisWorklistSolverWithWideningAndNarrowing(typedCfg.left.get)
8484
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
8585
})
86-
case AnalysisOption.`wlip` =>
86+
case AnalysisOption.`wlrp` =>
8787
Some(kind match {
88-
case Analysis.sign => new IntraprocSignAnalysisWorklistSolverWithInitAndPropagation(typedCfg.left.get)
88+
case Analysis.sign => new IntraprocSignAnalysisWorklistSolverWithReachabilityAndPropagation(typedCfg.left.get)
8989
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
9090
})
91-
case AnalysisOption.`iwli` =>
91+
case AnalysisOption.`iwlr` =>
9292
Some(kind match {
93-
case Analysis.sign => new InterprocSignAnalysisWorklistSolverWithInit(typedCfg.right.get)
93+
case Analysis.sign => new InterprocSignAnalysisWorklistSolverWithReachability(typedCfg.right.get)
9494
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
9595
})
96-
case AnalysisOption.`iwlip` =>
96+
case AnalysisOption.`iwlrp` =>
9797
Some(kind match {
98-
case Analysis.sign => new InterprocSignAnalysisWorklistSolverWithInitAndPropagation(typedCfg.right.get)
98+
case Analysis.sign => new InterprocSignAnalysisWorklistSolverWithReachabilityAndPropagation(typedCfg.right.get)
9999
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
100100
})
101-
case AnalysisOption.`csiwlip` =>
101+
case AnalysisOption.`csiwlrp` =>
102102
Some(kind match {
103103
case Analysis.sign => new CallStringSignAnalysis(typedCfg.right.get)
104104
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
105105
})
106-
case AnalysisOption.`cfiwlip` =>
106+
case AnalysisOption.`cfiwlrp` =>
107107
Some(kind match {
108108
case Analysis.sign => new FunctionalSignAnalysis(typedCfg.right.get)
109109
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
@@ -121,40 +121,40 @@ object FlowSensitiveAnalysis {
121121
*
122122
* - Enabled: use the simple fixpoint solver
123123
* - wl: use the worklist solver
124-
* - wli: use the worklist solver with init
125-
* - wliw: use the worklist solver with init and widening
126-
* - wliwn: use the worklist solver with init, widening, and narrowing
127-
* - wlip: use the worklist solver with init and propagation
128-
* - iwli: use the worklist solver with init, interprocedural version
129-
* - iwlip: use the worklist solver with init and propagation, interprocedural version
130-
* - csiwlip: use the worklist solver with init and propagation, context-sensitive (with call string) interprocedural version
131-
* - cfiwlip: use the worklist solver with init and propagation, context-sensitive (with functional approach) interprocedural version
124+
* - wlr: use the worklist solver with reachability
125+
* - wlrw: use the worklist solver with reachability and widening
126+
* - wlrwn: use the worklist solver with reachability, widening, and narrowing
127+
* - wlrp: use the worklist solver with reachability and propagation
128+
* - iwlr: use the worklist solver with reachability, interprocedural version
129+
* - iwlrp: use the worklist solver with reachability and propagation, interprocedural version
130+
* - csiwlrp: use the worklist solver with reachability and propagation, context-sensitive (with call string) interprocedural version
131+
* - cfiwlrp: use the worklist solver with reachability and propagation, context-sensitive (with functional approach) interprocedural version
132132
* - ide: use the IDE solver
133133
*/
134134
object AnalysisOption extends Enumeration {
135-
val simple, Disabled, wl, wli, wliw, wliwn, wlip, iwli, iwlip, csiwlip, cfiwlip, ide = Value
135+
val simple, Disabled, wl, wlr, wlrw, wlrwn, wlrp, iwlr, iwlrp, csiwlrp, cfiwlrp, ide = Value
136136

137137
def interprocedural(v: Value): Boolean =
138138
v match {
139-
case `iwli` => true
140-
case `iwlip` => true
141-
case `csiwlip` => true
142-
case `cfiwlip` => true
139+
case `iwlr` => true
140+
case `iwlrp` => true
141+
case `csiwlrp` => true
142+
case `cfiwlrp` => true
143143
case `ide` => true
144144
case _ => false
145145
}
146146

147147
def contextsensitive(v: Value): Boolean =
148148
v match {
149-
case `csiwlip` => true
150-
case `cfiwlip` => true
149+
case `csiwlrp` => true
150+
case `cfiwlrp` => true
151151
case _ => false
152152
}
153153

154154
def withWidening(v: Value): Boolean =
155155
v match {
156-
case `wliw` => true
157-
case `wliwn` => true
156+
case `wlrw` => true
157+
case `wlrwn` => true
158158
case _ => false
159159
}
160160
}

‎src/tip/analysis/IntervalAnalysis.scala‎

Lines changed: 22 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -79,9 +79,9 @@ abstract class IntervalAnalysis(cfg: FragmentCfg)(implicit declData: Declaration
7979
/**
8080
* Interval analysis, using the worklist solver with init and widening.
8181
*/
82-
class IntervalAnalysisWorklistSolverWithInit(cfg: ProgramCfg)(implicit declData: DeclarationData)
82+
class IntervalAnalysisWorklistSolverWithReachability(cfg: ProgramCfg)(implicit declData: DeclarationData)
8383
extends IntervalAnalysis(cfg)
84-
with WorklistFixpointSolverWithInit[CfgNode]
84+
with WorklistFixpointSolverWithReachability[CfgNode]
8585
with ForwardDependencies {
8686

8787
val first = cfg.funEntries.values.toSet[CfgNode]
@@ -92,7 +92,7 @@ class IntervalAnalysisWorklistSolverWithInit(cfg: ProgramCfg)(implicit declData:
9292
*/
9393
class IntervalAnalysisWorklistSolverWithWidening(cfg: ProgramCfg)(implicit declData: DeclarationData)
9494
extends IntervalAnalysis(cfg)
95-
with WorklistFixpointSolverWithInitAndSimpleWidening[CfgNode]
95+
with WorklistFixpointSolverWithReachabilityAndWidening[CfgNode]
9696
with ForwardDependencies {
9797

9898
import tip.cfg.CfgOps._
@@ -111,28 +111,38 @@ class IntervalAnalysisWorklistSolverWithWidening(cfg: ProgramCfg)(implicit declD
111111
}
112112
}
113113

114-
def backedge(src: CfgNode, dst: CfgNode): Boolean = cfg.rank(src) > cfg.rank(dst)
114+
def loophead(n: CfgNode): Boolean = indep(n).exists(cfg.rank(_) > cfg.rank(n))
115+
116+
type IntervalLatticeElement = lattice.sublattice.sublattice.sublattice.Element
115117

116118
private def minB(b: lattice.sublattice.sublattice.sublattice.Num) = B.filter(b <= _).min
117119

118120
private def maxB(a: lattice.sublattice.sublattice.sublattice.Num) = B.filter(_ <= a).max
119121

120-
def widen(s: lattice.sublattice.Element): lattice.sublattice.Element = {
121-
import lattice.sublattice.sublattice.sublattice._
122-
import lattice.sublattice._
123-
s match {
124-
case lattice.sublattice.Bottom => s
125-
case lattice.sublattice.Lift(m) => ??? //<--- Complete here
122+
def widenInterval(x: IntervalLatticeElement, y: IntervalLatticeElement): IntervalLatticeElement =
123+
(x, y) match {
124+
case (lattice.sublattice.sublattice.sublattice.EmptyInterval, _) => y
125+
case (_, lattice.sublattice.sublattice.sublattice.EmptyInterval) => x
126+
case ((l1, h1), (l2, h2)) => ??? //<--- Complete here
127+
}
128+
129+
def widen(x: lattice.sublattice.Element, y: lattice.sublattice.Element): lattice.sublattice.Element =
130+
(x, y) match {
131+
case (lattice.sublattice.Bottom, _) => y
132+
case (_, lattice.sublattice.Bottom) => x
133+
case (lattice.sublattice.Lift(xm), lattice.sublattice.Lift(ym)) =>
134+
lattice.sublattice.Lift(declaredVars.map { v =>
135+
v -> widenInterval(xm(v), ym(v))
136+
}.toMap)
126137
}
127-
}
128138
}
129139

130140
/**
131141
* Interval analysis, using the worklist solver with init, widening, and narrowing.
132142
*/
133143
class IntervalAnalysisWorklistSolverWithWideningAndNarrowing(cfg: ProgramCfg)(implicit declData: DeclarationData)
134144
extends IntervalAnalysisWorklistSolverWithWidening(cfg)
135-
with WorklistFixpointSolverWithInitAndSimpleWideningAndNarrowing[CfgNode] {
145+
with WorklistFixpointSolverWithReachabilityAndWideningAndNarrowing[CfgNode] {
136146

137147
val narrowingSteps = 5
138148
}

‎src/tip/analysis/SignAnalysis.scala‎

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,7 @@ abstract class SimpleSignAnalysis(cfg: ProgramCfg)(implicit val declData: Declar
244244
}
245245

246246
/**
247-
* Base class for sign analysis with lifted lattice.
247+
* Base class for sign analysis with lifted lattice, where the extra bottom element represents "unreachable".
248248
*/
249249
abstract class LiftedSignAnalysis(cfg: ProgramCfg)(implicit val declData: DeclarationData)
250250
extends FlowSensitiveAnalysis[CfgNode](cfg)
@@ -295,28 +295,29 @@ class IntraprocSignAnalysisWorklistSolver(cfg: ProgramCfg)(implicit override val
295295
with SimpleWorklistFixpointSolver[CfgNode]
296296

297297
/**
298-
* Intraprocedural sign analysis that uses [[tip.solvers.WorklistFixpointSolverWithInit]],
298+
* Intraprocedural sign analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
299299
* with all function entries as start nodes.
300300
*/
301-
class IntraprocSignAnalysisWorklistSolverWithInit(cfg: ProgramCfg)(implicit override val declData: DeclarationData)
301+
class IntraprocSignAnalysisWorklistSolverWithReachability(cfg: ProgramCfg)(implicit override val declData: DeclarationData)
302302
extends LiftedSignAnalysis(cfg)
303-
with WorklistFixpointSolverWithInit[CfgNode] {
303+
with WorklistFixpointSolverWithReachability[CfgNode] {
304304

305305
def transferUnlifted(n: CfgNode, s: lattice.sublattice.sublattice.Element): lattice.sublattice.sublattice.Element = localTransfer(n, s)
306306
}
307307

308308
/**
309309
* Intraprocedural sign analysis that uses [[tip.solvers.WorklistFixpointPropagationSolver]].
310310
*/
311-
class IntraprocSignAnalysisWorklistSolverWithInitAndPropagation(cfg: ProgramCfg)(implicit override val declData: DeclarationData)
312-
extends IntraprocSignAnalysisWorklistSolverWithInit(cfg)
311+
class IntraprocSignAnalysisWorklistSolverWithReachabilityAndPropagation(cfg: ProgramCfg)(implicit override val declData: DeclarationData)
312+
extends IntraprocSignAnalysisWorklistSolverWithReachability(cfg)
313313
with WorklistFixpointPropagationSolver[CfgNode]
314314

315315
/**
316-
* Interprocedural sign analysis that uses [[tip.solvers.WorklistFixpointSolverWithInit]].
316+
* Interprocedural sign analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]],
317+
* with the entry of the main function as the only start node.
317318
*/
318-
class InterprocSignAnalysisWorklistSolverWithInit(val cfg: InterproceduralProgramCfg)(implicit override val declData: DeclarationData)
319-
extends IntraprocSignAnalysisWorklistSolverWithInit(cfg)
319+
class InterprocSignAnalysisWorklistSolverWithReachability(val cfg: InterproceduralProgramCfg)(implicit override val declData: DeclarationData)
320+
extends IntraprocSignAnalysisWorklistSolverWithReachability(cfg)
320321
with InterprocSignAnalysisFunctions
321322
with InterproceduralForwardDependencies {
322323

@@ -328,8 +329,8 @@ class InterprocSignAnalysisWorklistSolverWithInit(val cfg: InterproceduralProgra
328329
* Note that this class uses [[tip.analysis.ForwardDependencies]] which has no interprocedural outdeps,
329330
* and it does not use indeps.
330331
*/
331-
class InterprocSignAnalysisWorklistSolverWithInitAndPropagation(val cfg: InterproceduralProgramCfg)(implicit override val declData: DeclarationData)
332-
extends IntraprocSignAnalysisWorklistSolverWithInitAndPropagation(cfg)
332+
class InterprocSignAnalysisWorklistSolverWithReachabilityAndPropagation(val cfg: InterproceduralProgramCfg)(implicit override val declData: DeclarationData)
333+
extends IntraprocSignAnalysisWorklistSolverWithReachabilityAndPropagation(cfg)
333334
with InterprocSignAnalysisFunctionsWithPropagation
334335
with ForwardDependencies {
335336

‎src/tip/cfg/FragmentCfg.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ class FragmentCfg(private[cfg] val graphEntries: Set[CfgNode], private[cfg] val
135135
* rank(x) < rank(y) iff y is visited after x in a depth-first
136136
* visit of the control-flow graph
137137
*/
138-
def rank: Map[CfgNode, Int] = {
138+
lazy val rank: Map[CfgNode, Int] = {
139139
def rankRec(elems: List[CfgNode], visited: List[List[CfgNode]], level: Int): Map[CfgNode, Int] = {
140140
val curLevel = elems.map { x =>
141141
x -> level

‎src/tip/solvers/FixpointSolvers.scala‎

Lines changed: 19 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -236,12 +236,14 @@ trait SimpleWorklistFixpointSolver[N] extends WorklistFixpointSolver[N] {
236236
}
237237

238238
/**
239-
* The worklist-based fixpoint solver with initialization.
239+
* The worklist-based fixpoint solver with reachability.
240+
*
241+
* This solver works for map lattices with lifted co-domains, where the extra bottom element typically represents "unreachable".
240242
*/
241-
trait WorklistFixpointSolverWithInit[N] extends WorklistFixpointSolver[N] with MapLiftLatticeSolver[N] {
243+
trait WorklistFixpointSolverWithReachability[N] extends WorklistFixpointSolver[N] with MapLiftLatticeSolver[N] {
242244

243245
/**
244-
* The start locations.
246+
* The start locations, used as the initial contents of the worklist.
245247
*/
246248
val first: Set[N]
247249

@@ -305,7 +307,7 @@ trait WorklistFixpointPropagationFunctions[N] extends ListSetWorklist[N] {
305307
* Note that with this approach, each abstract state represents the program point *after* the node
306308
* (for a forward analysis, and opposite for a backward analysis).
307309
*/
308-
trait WorklistFixpointPropagationSolver[N] extends WorklistFixpointSolverWithInit[N] with WorklistFixpointPropagationFunctions[N] {
310+
trait WorklistFixpointPropagationSolver[N] extends WorklistFixpointSolverWithReachability[N] with WorklistFixpointPropagationFunctions[N] {
309311

310312
val lattice: MapLattice[N, LiftLattice[Lattice]]
311313

@@ -339,38 +341,39 @@ trait WorklistFixpointPropagationSolver[N] extends WorklistFixpointSolverWithIni
339341
}
340342

341343
/**
342-
* Worklist-based fixpoint solver with initialization and simple widening.
344+
* Worklist-based fixpoint solver with reachability and widening.
343345
*/
344-
trait WorklistFixpointSolverWithInitAndSimpleWidening[N] extends WorklistFixpointSolverWithInit[N] {
346+
trait WorklistFixpointSolverWithReachabilityAndWidening[N] extends WorklistFixpointSolverWithReachability[N] {
345347

346348
/**
347-
* Set widening function.
348-
* @param s input lattice element
349+
* Widening function.
350+
* @param x lattice element from previous iteration
351+
* @param y lattice element from this iteration
349352
* @return output lattice element
350353
*/
351-
def widen(s: lattice.sublattice.Element): lattice.sublattice.Element
354+
def widen(x: lattice.sublattice.Element, y: lattice.sublattice.Element): lattice.sublattice.Element
352355

353356
/**
354-
* Tells whether (src,dst) is a back-edge.
357+
* Tells whether `n` is a loop-head.
355358
*/
356-
def backedge(src: N, dst: N): Boolean
359+
def loophead(n: N): Boolean
357360

358361
override def process(n: N) = {
359362
val xn = x(n)
360363
FixpointSolvers.log.verb(s"Processing $n in state $xn")
361364
val y = funsub(n, x)
362365
if (y != xn) {
363-
x += n -> (if (outdep(n).exists(backedge(n, _))) widen(y) else y)
366+
x += n -> (if (loophead(n)) widen(xn, y) else y)
364367
add(outdep(n))
365368
}
366369
}
367370
}
368371

369372
/**
370-
* The worklist-based fixpoint solver with initialization, simple widening, and narrowing.
373+
* The worklist-based fixpoint solver with reachability, widening, and (simple) narrowing.
371374
*/
372-
trait WorklistFixpointSolverWithInitAndSimpleWideningAndNarrowing[N]
373-
extends WorklistFixpointSolverWithInitAndSimpleWidening[N]
375+
trait WorklistFixpointSolverWithReachabilityAndWideningAndNarrowing[N]
376+
extends WorklistFixpointSolverWithReachabilityAndWidening[N]
374377
with SimpleMapLatticeFixpointSolver[N] {
375378

376379
/**
@@ -387,5 +390,5 @@ trait WorklistFixpointSolverWithInitAndSimpleWideningAndNarrowing[N]
387390
if (i <= 0) x else narrow(fun(x), i - 1) // uses the simple definition of 'fun' from SimpleMapLatticeFixpointSolver
388391

389392
override def analyze(): lattice.Element =
390-
narrow(super[WorklistFixpointSolverWithInitAndSimpleWidening].analyze(), narrowingSteps)
393+
narrow(super[WorklistFixpointSolverWithReachabilityAndWidening].analyze(), narrowingSteps)
391394
}

0 commit comments

Comments
 (0)