diff --git a/src/tip/Tip.scala b/src/tip/Tip.scala
index 9a5529e..9988e9a 100644
--- a/src/tip/Tip.scala
+++ b/src/tip/Tip.scala
@@ -117,6 +117,7 @@ object Tip extends App {
| -constprop enable constant propagation analysis
| -interval enable interval analysis
| -copyconstprop enable copy constant propagation analysis
+ | -uninitvars enable possibly-uninitialized variables analysis
|
| For the dataflow analyses, the choice of fixpoint solver can be chosen by these modifiers
| immediately after the analysis name (default: use the simple fixpoint solver):
@@ -212,7 +213,7 @@ object Tip extends App {
// run the analysis
log.verb(s"Performing ${an.getClass.getSimpleName}")
val res = an.analyze().asInstanceOf[Map[CfgNode, _]]
- Output.output(file, DataFlowOutput(s), wcfg.toDot(Output.labeler(res), Output.dotIder), options.out)
+ Output.output(file, DataFlowOutput(s), wcfg.toDot(Output.labeler(res, an.stateAfterNode), Output.dotIder), options.out)
}
}
}
@@ -248,7 +249,7 @@ object Tip extends App {
Output.transform(res.asInstanceOf[Map[(CallContext, CfgNode), _]])
else
res.asInstanceOf[Map[CfgNode, _]]
- Output.output(file, DataFlowOutput(s), wcfg.toDot(Output.labeler(res2), Output.dotIder), options.out)
+ Output.output(file, DataFlowOutput(s), wcfg.toDot(Output.labeler(res2, an.stateAfterNode), Output.dotIder), options.out)
}
}
}
@@ -333,7 +334,7 @@ object Tip extends App {
options.andersen = true
case "-steensgaard" =>
options.steensgaard = true
- case "-sign" | "-livevars" | "-available" | "-vbusy" | "-reaching" | "-constprop" | "-interval" | "-copyconstprop" =>
+ case "-sign" | "-livevars" | "-available" | "-vbusy" | "-reaching" | "-constprop" | "-interval" | "-copyconstprop" | "-uninitvars" =>
options.dfAnalysis += dfa.withName(args(i).drop(1)) -> {
if (i + 1 < args.length && dfo.values.map(_.toString()).contains(args(i + 1))) {
i = i + 1
diff --git a/src/tip/analysis/AvailableExpAnalysis.scala b/src/tip/analysis/AvailableExpAnalysis.scala
index 33a18ec..3a8fbb3 100644
--- a/src/tip/analysis/AvailableExpAnalysis.scala
+++ b/src/tip/analysis/AvailableExpAnalysis.scala
@@ -6,21 +6,25 @@ import tip.lattices.{MapLattice, ReversePowersetLattice}
import tip.solvers.{SimpleMapLatticeFixpointSolver, SimpleWorklistFixpointSolver}
import tip.ast.AstNodeData.DeclarationData
+import scala.collection.immutable.Set
+
/**
* Base class for available expressions analysis.
*/
-abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis[CfgNode](cfg) {
+abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis(true) {
import tip.cfg.CfgOps._
import tip.ast.AstOps._
val allExps: Set[UnlabelledNode[AExpr]] = cfg.nodes.flatMap(_.appearingNonInputExpressions.map(UnlabelledNode[AExpr]))
+ val lattice: MapLattice[CfgNode, ReversePowersetLattice[UnlabelledNode[AExpr]]] = new MapLattice(new ReversePowersetLattice(allExps))
+
+ val domain: Set[CfgNode] = cfg.nodes
+
NoPointers.assertContainsProgram(cfg.prog)
NoRecords.assertContainsProgram(cfg.prog)
- val lattice = new MapLattice(cfg.nodes, new ReversePowersetLattice(allExps))
-
def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element =
n match {
case _: CfgFunEntryNode => Set()
diff --git a/src/tip/analysis/ControlFlowAnalysis.scala b/src/tip/analysis/ControlFlowAnalysis.scala
index dcc202c..6a30bf9 100644
--- a/src/tip/analysis/ControlFlowAnalysis.scala
+++ b/src/tip/analysis/ControlFlowAnalysis.scala
@@ -7,6 +7,9 @@ import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData}
import scala.language.implicitConversions
+/**
+ * Control flow analysis.
+ */
class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
extends DepthFirstAstVisitor[Unit]
with Analysis[Map[AstNode, Set[AFunDeclaration]]] {
@@ -18,7 +21,7 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
}
case class AstVariable(n: AstNode) {
- override def toString = n match {
+ override def toString: String = n match {
case fun: AFunDeclaration => s"${fun.name}:${fun.loc}"
case _ => n.toString
}
@@ -46,7 +49,7 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
* @param node the node for which it generates the constraints
* @param arg unused for this visitor
*/
- def visit(node: AstNode, arg: Unit) = {
+ def visit(node: AstNode, arg: Unit): Unit = {
/**
* Get the declaration if the supplied AstNode is an identifier,
diff --git a/src/tip/analysis/CopyConstantPropagationAnalysis.scala b/src/tip/analysis/CopyConstantPropagationAnalysis.scala
index 1b3ad90..661343a 100644
--- a/src/tip/analysis/CopyConstantPropagationAnalysis.scala
+++ b/src/tip/analysis/CopyConstantPropagationAnalysis.scala
@@ -4,41 +4,44 @@ import tip.ast._
import tip.cfg._
import tip.lattices._
import tip.solvers._
+import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData}
import scala.collection.mutable
-import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData}
/**
* Micro-transfer-functions for copy-constant-propagation analysis.
*/
trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration, FlatLattice[Int]] {
+ NoPointers.assertContainsProgram(cfg.prog)
+ NoRecords.assertContainsProgram(cfg.prog)
+
implicit val declData: DeclarationData
- lazy val valuelattice = new FlatLattice[Int]()
+ val valuelattice = new FlatLattice[Int]()
- lazy val edgelattice: EdgeLattice[valuelattice.type] = new EdgeLattice(valuelattice)
+ val edgelattice: EdgeFunctionLattice[valuelattice.type] = new EdgeFunctionLattice(valuelattice)
import cfg._
- import edgelattice.{ConstEdge, Edge, IdEdge}
- import edgelattice.valuelattice.{FlatEl, Top}
+ import edgelattice._
+ import edgelattice.valuelattice._
- def edgesCallToEntry(d: DL, call: CfgCallNode, entry: CfgFunEntryNode): List[(DL, edgelattice.Edge)] =
- entry.data.params.zip(call.invocation.args).foldLeft(List[(DL, edgelattice.Edge)]()) {
+ def edgesCallToEntry(d: DL, call: CfgCallNode, entry: CfgFunEntryNode): List[(DL, edgelattice.EdgeFunction)] =
+ entry.data.params.zip(call.invocation.args).foldLeft(List[(DL, edgelattice.EdgeFunction)]()) {
case (acc, (id, exp)) =>
acc ++ assign(d, id, exp)
}
- def edgesExitToAfterCall(d: DL, exit: CfgFunExitNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.Edge)] =
+ def edgesExitToAfterCall(d: DL, exit: CfgFunExitNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.EdgeFunction)] =
assign(d, aftercall.targetIdentifier.declaration, AstOps.returnId)
- def edgesCallToAfterCall(d2: DL, call: CfgCallNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.Edge)] =
+ def edgesCallToAfterCall(d2: DL, call: CfgCallNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.EdgeFunction)] =
d2 match {
case Right(_) => List((d2, IdEdge()))
case Left(a) => if (a == aftercall.targetIdentifier.declaration) List() else List((d2, IdEdge()))
}
- def edgesOther(d: DL, n: CfgNode): List[(DL, edgelattice.Edge)] =
+ def edgesOther(d: DL, n: CfgNode): List[(DL, edgelattice.EdgeFunction)] =
n match {
case r: CfgStmtNode =>
r.data match {
@@ -47,7 +50,7 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration,
case varr: AVarStmt =>
d match {
case Right(_) =>
- varr.declIds.foldLeft(List((d, IdEdge())): List[(DL, Edge)]) { (ps, id) => // identity edge from lambda to lambda
+ varr.declIds.foldLeft(List((d, IdEdge())): List[(DL, EdgeFunction)]) { (ps, id) => // identity edge from lambda to lambda
ps :+ (Left(id), ConstEdge(Top)) // top edge from lambda to each variable being declared
}
case Left(a) =>
@@ -84,8 +87,8 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration,
/**
* Micro-transfer-functions for assigning an expression to an identifier.
*/
- private def assign(d: DL, id: ADeclaration, exp: AExprOrIdentifierDeclaration): List[(DL, edgelattice.Edge)] = {
- val edges = mutable.ListBuffer[(DL, Edge)]()
+ private def assign(d: DL, id: ADeclaration, exp: AExprOrIdentifierDeclaration): List[(DL, edgelattice.EdgeFunction)] = {
+ val edges = mutable.ListBuffer[(DL, EdgeFunction)]()
d match {
case Right(_) =>
edges += ((d, IdEdge())) // identity edge from lambda to lambda
@@ -116,22 +119,6 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration,
/**
* Copy-constant-propagation analysis using IDE solver.
*/
-class CopyConstantPropagationIDEAnalysis(val cfg: InterproceduralProgramCfg)(implicit val declData: DeclarationData)
- extends FlowSensitiveAnalysis[CfgNode](cfg) {
-
- import tip.cfg.CfgOps._
-
- val phase1 = new IDEPhase1Analysis[ADeclaration, FlatLattice[Int]](cfg) with CopyConstantPropagationAnalysisFunctions
- val phase2 = new IDEPhase2Analysis[ADeclaration, FlatLattice[Int]](cfg, phase1) with CopyConstantPropagationAnalysisFunctions
-
- val declaredVars: Set[ADeclaration] = domain.flatMap(_.declaredVarsAndParams)
-
- val lattice: MapLattice[CfgNode, MapLattice[ADeclaration, FlatLattice[Int]]] = phase2.restructedlattice
-
- def analyze(): lattice.Element = {
- FixpointSolvers.log.verb(s"IDE phase 1")
- phase1.analyze()
- FixpointSolvers.log.verb(s"IDE phase 2")
- phase2.restructure(phase2.analyze()).asInstanceOf[lattice.Element] // FIXME: avoid this asInstanceOf
- }
-}
+class CopyConstantPropagationIDEAnalysis(cfg: InterproceduralProgramCfg)(implicit val declData: DeclarationData)
+ extends IDESolver[ADeclaration, FlatLattice[Int]](cfg)
+ with CopyConstantPropagationAnalysisFunctions
diff --git a/src/tip/analysis/FlowSensitiveAnalysis.scala b/src/tip/analysis/FlowSensitiveAnalysis.scala
index 65c6da2..703592f 100644
--- a/src/tip/analysis/FlowSensitiveAnalysis.scala
+++ b/src/tip/analysis/FlowSensitiveAnalysis.scala
@@ -1,36 +1,22 @@
package tip.analysis
import tip.cfg._
-import tip.lattices.{Lattice, MapLattice}
import tip.ast.AstNodeData.DeclarationData
/**
* A flow-sensitive analysis.
+ * @param stateAfterNode true if the abstract state of a CFG node represents the program point after the node,
+ * false if represents the program point before the node
+ * (used when outputting analysis results)
*/
-abstract class FlowSensitiveAnalysis[N](cfg: FragmentCfg) extends Analysis[Any] {
-
- /**
- * The lattice used by the analysis.
- */
- val lattice: MapLattice[N, Lattice]
-
- /**
- * The domain of the map lattice.
- */
- val domain: Set[CfgNode] = cfg.nodes
-
- /**
- * @inheritdoc
- */
- def analyze(): lattice.Element
-}
+abstract class FlowSensitiveAnalysis(val stateAfterNode: Boolean) extends Analysis[Any]
/**
* A factory to create a specific flow-sensitive analysis that matches the options.
*/
object FlowSensitiveAnalysis {
- def select(kind: Analysis.Value, options: AnalysisOption.Value, cfg: FragmentCfg)(implicit declData: DeclarationData): Option[FlowSensitiveAnalysis[_]] = {
+ def select(kind: Analysis.Value, options: AnalysisOption.Value, cfg: FragmentCfg)(implicit declData: DeclarationData): Option[FlowSensitiveAnalysis] = {
val typedCfg = options match {
case AnalysisOption.`iwlr` | AnalysisOption.`iwlrp` | AnalysisOption.`csiwlrp` | AnalysisOption.`cfiwlrp` | AnalysisOption.`ide` =>
@@ -116,6 +102,7 @@ object FlowSensitiveAnalysis {
case AnalysisOption.`ide` =>
Some(kind match {
case Analysis.copyconstprop => new CopyConstantPropagationIDEAnalysis(typedCfg.right.get)
+ case Analysis.uninitvars => new PossiblyUninitializedVarsIDEAnalysis(typedCfg.right.get)
case _ => throw new RuntimeException(s"Unsupported solver option `$options` for the analysis $kind")
})
}
@@ -168,6 +155,6 @@ object FlowSensitiveAnalysis {
* A flow sensitive analysis kind
*/
object Analysis extends Enumeration {
- val sign, livevars, available, vbusy, reaching, constprop, interval, copyconstprop = Value
+ val sign, livevars, available, vbusy, reaching, constprop, interval, copyconstprop, uninitvars = Value
}
}
diff --git a/src/tip/analysis/LiveVarsAnalysis.scala b/src/tip/analysis/LiveVarsAnalysis.scala
index acdfad4..37fad88 100644
--- a/src/tip/analysis/LiveVarsAnalysis.scala
+++ b/src/tip/analysis/LiveVarsAnalysis.scala
@@ -1,21 +1,21 @@
package tip.analysis
import tip.ast._
-import tip.cfg.CfgOps._
import tip.lattices._
import tip.ast.AstNodeData.DeclarationData
-
import tip.solvers._
import tip.cfg._
+import scala.collection.immutable.Set
+
/**
* Base class for live variables analysis.
*/
-abstract class LiveVarsAnalysis(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis[CfgNode](cfg) {
+abstract class LiveVarsAnalysis(cfg: IntraproceduralProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis(false) {
- val allVars: Set[ADeclaration] = cfg.nodes.flatMap(_.appearingIds)
+ val lattice: MapLattice[CfgNode, PowersetLattice[ADeclaration]] = new MapLattice(new PowersetLattice())
- val lattice = new MapLattice(cfg.nodes, new PowersetLattice(allVars))
+ val domain: Set[CfgNode] = cfg.nodes
NoPointers.assertContainsProgram(cfg.prog)
NoRecords.assertContainsProgram(cfg.prog)
diff --git a/src/tip/analysis/PossiblyUninitializedVarsAnalysis.scala b/src/tip/analysis/PossiblyUninitializedVarsAnalysis.scala
new file mode 100644
index 0000000..5a8a394
--- /dev/null
+++ b/src/tip/analysis/PossiblyUninitializedVarsAnalysis.scala
@@ -0,0 +1,110 @@
+package tip.analysis
+
+import tip.ast._
+import tip.cfg._
+import tip.lattices._
+import tip.solvers._
+import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData}
+import tip.ast.AstOps.AstOp
+
+import scala.collection.mutable
+
+/**
+ * Micro-transfer-functions for possibly-uninitialized variables analysis.
+ */
+trait PossiblyUninitializedVarsAnalysisFunctions extends IDEAnalysis[ADeclaration, TwoElementLattice] {
+
+ NoPointers.assertContainsProgram(cfg.prog)
+ NoRecords.assertContainsProgram(cfg.prog)
+
+ implicit val declData: DeclarationData
+
+ val valuelattice = new TwoElementLattice()
+
+ val edgelattice: EdgeFunctionLattice[valuelattice.type] = new EdgeFunctionLattice(valuelattice)
+
+ import cfg._
+ import edgelattice._
+ import edgelattice.valuelattice._
+
+ def edgesCallToEntry(d: DL, call: CfgCallNode, entry: CfgFunEntryNode): List[(DL, edgelattice.EdgeFunction)] =
+ entry.data.params.zip(call.invocation.args).foldLeft(List[(DL, edgelattice.EdgeFunction)]()) {
+ case (acc, (id, exp)) =>
+ acc ++ assign(d, id, exp)
+ }
+
+ def edgesExitToAfterCall(d: DL, exit: CfgFunExitNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.EdgeFunction)] =
+ assign(d, aftercall.targetIdentifier.declaration, AstOps.returnId)
+
+ def edgesCallToAfterCall(d2: DL, call: CfgCallNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.EdgeFunction)] =
+ d2 match {
+ case Right(_) => List((d2, IdEdge()))
+ case Left(a) => if (a == aftercall.targetIdentifier.declaration) List() else List((d2, IdEdge()))
+ }
+
+ def edgesOther(d: DL, n: CfgNode): List[(DL, edgelattice.EdgeFunction)] =
+ n match {
+ case r: CfgStmtNode =>
+ r.data match {
+
+ // var declarations
+ case varr: AVarStmt =>
+ d match {
+ case Right(_) =>
+ varr.declIds.foldLeft(List((d, IdEdge())): List[(DL, EdgeFunction)]) { (ps, id) => // identity edge from lambda to lambda
+ ps :+ (Left(id), ConstEdge(Top)) // top edge from lambda to each variable being declared
+ }
+ case Left(a) =>
+ if (varr.declIds.contains(a))
+ List() // no edges from the variables being declared
+ else
+ List((d, IdEdge())) // identity edge from all other variables to themselves
+ }
+
+ // assignments
+ case as: AAssignStmt =>
+ as match {
+ case AAssignStmt(id: AIdentifier, right, _) =>
+ val edges = assign(d, id.declaration, right)
+ d match {
+ case Left(a) if id.declaration != a =>
+ edges :+ ((d, IdEdge())) // not at the variable being written to, so add identity edge
+ case _ =>
+ edges
+ }
+ case AAssignStmt(_, _, _) => NoPointers.LanguageRestrictionViolation(s"$as not allowed", as.loc)
+ }
+
+ // return statement
+ case ret: AReturnStmt => assign(d, AstOps.returnId, ret.exp)
+
+ // all other kinds of statements: like no-ops
+ case _ => List((d, IdEdge()))
+ }
+ // all other kinds of nodes: like no-ops
+ case _ => List((d, IdEdge()))
+ }
+
+ /**
+ * Micro-transfer-functions for assigning an expression to an identifier.
+ */
+ private def assign(d: DL, id: ADeclaration, exp: AExprOrIdentifierDeclaration): List[(DL, edgelattice.EdgeFunction)] = {
+ val edges = mutable.ListBuffer[(DL, EdgeFunction)]()
+ d match {
+ case Right(_) =>
+ edges += ((d, IdEdge())) // identity edge from lambda to lambda
+ case Left(a) =>
+ // identity edge from d to the variable being assigned to if d appears in exp
+ if (exp.appearingIds.contains(a))
+ edges += ((Left(id), IdEdge()))
+ }
+ edges.toList
+ }
+}
+
+/**
+ * Possibly-uninitialized variables analysis using IDE solver.
+ */
+class PossiblyUninitializedVarsIDEAnalysis(cfg: InterproceduralProgramCfg)(implicit val declData: DeclarationData)
+ extends IDESolver[ADeclaration, TwoElementLattice](cfg)
+ with PossiblyUninitializedVarsAnalysisFunctions
diff --git a/src/tip/analysis/SimpleSignAnalysis.scala b/src/tip/analysis/SimpleSignAnalysis.scala
index f2bff50..27ff7c7 100644
--- a/src/tip/analysis/SimpleSignAnalysis.scala
+++ b/src/tip/analysis/SimpleSignAnalysis.scala
@@ -15,7 +15,7 @@ import scala.collection.immutable.Set
* This is a specialized version of `SignAnalysis.Intraprocedural.SimpleSolver`
* where most of the involved traits, classes, methods, and fields have been inlined.
*/
-class SimpleSignAnalysis(cfg: ProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis[CfgNode](cfg) {
+class SimpleSignAnalysis(cfg: ProgramCfg)(implicit declData: DeclarationData) extends FlowSensitiveAnalysis(true) {
/**
* The lattice of abstract values.
@@ -30,12 +30,17 @@ class SimpleSignAnalysis(cfg: ProgramCfg)(implicit declData: DeclarationData) ex
/**
* The lattice of abstract states.
*/
- val statelattice: MapLattice[ADeclaration, SignLattice.type] = new MapLattice(declaredVars, valuelattice)
+ val statelattice: MapLattice[ADeclaration, SignLattice.type] = new MapLattice(valuelattice)
/**
* The program lattice.
*/
- val lattice: MapLattice[CfgNode, statelattice.type] = new MapLattice(domain, statelattice)
+ val lattice: MapLattice[CfgNode, statelattice.type] = new MapLattice(statelattice)
+
+ /**
+ * The domain of the program lattice.
+ */
+ val domain: Set[CfgNode] = cfg.nodes
/**
* Abstract evaluation of expressions.
diff --git a/src/tip/analysis/ValueAnalysis.scala b/src/tip/analysis/ValueAnalysis.scala
index f48c76a..db1dc0d 100644
--- a/src/tip/analysis/ValueAnalysis.scala
+++ b/src/tip/analysis/ValueAnalysis.scala
@@ -7,6 +7,8 @@ import tip.lattices._
import tip.solvers._
import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData}
+import scala.collection.immutable.Set
+
/**
* General definitions for value analysis.
*/
@@ -29,7 +31,7 @@ trait ValueAnalysisMisc {
/**
* The lattice of abstract states.
*/
- val statelattice: MapLattice[ADeclaration, valuelattice.type] = new MapLattice(declaredVars, valuelattice)
+ val statelattice: MapLattice[ADeclaration, valuelattice.type] = new MapLattice(valuelattice)
/**
* Default implementation of eval.
@@ -113,7 +115,7 @@ trait InterprocValueAnalysisMisc[N] extends ValueAnalysisMisc {
* Constraint functions for value analysis (including interprocedural).
* This version is for the basic worklist algorithm.
*/
-trait InterprocValueAnalysisFunctions[L <: LatticeWithOps] extends MapLiftLatticeSolver[CfgNode] with InterprocValueAnalysisMisc[CfgNode] {
+trait InterprocValueAnalysisFunctions extends MapLiftLatticeSolver[CfgNode] with InterprocValueAnalysisMisc[CfgNode] {
/**
* Overrides `funsub` from [[tip.solvers.MapLatticeSolver]] adding support for function calls and returns.
@@ -209,14 +211,14 @@ trait InterprocValueAnalysisFunctionsWithPropagation
/**
* Base class for value analysis with simple (non-lifted) lattice.
*/
-abstract class SimpleValueAnalysis[L <: LatticeWithOps](val cfg: ProgramCfg)(implicit val decl: DeclarationData)
- extends FlowSensitiveAnalysis[CfgNode](cfg)
- with ValueAnalysisMisc {
+abstract class SimpleValueAnalysis(val cfg: ProgramCfg)(implicit val decl: DeclarationData) extends FlowSensitiveAnalysis(true) with ValueAnalysisMisc {
/**
* The analysis lattice.
*/
- val lattice: MapLattice[CfgNode, statelattice.type] = new MapLattice(cfg.nodes, statelattice)
+ val lattice: MapLattice[CfgNode, statelattice.type] = new MapLattice(statelattice)
+
+ val domain: Set[CfgNode] = cfg.nodes
/**
* Transfer function for state lattice elements.
@@ -229,7 +231,7 @@ abstract class SimpleValueAnalysis[L <: LatticeWithOps](val cfg: ProgramCfg)(imp
* Base class for value analysis with lifted lattice, where the extra bottom element represents "unreachable".
*/
abstract class LiftedValueAnalysis[P <: ProgramCfg](val cfg: P)(implicit val declData: DeclarationData)
- extends FlowSensitiveAnalysis[CfgNode](cfg)
+ extends FlowSensitiveAnalysis(true)
with MapLatticeSolver[CfgNode]
with ValueAnalysisMisc {
@@ -241,7 +243,9 @@ abstract class LiftedValueAnalysis[P <: ProgramCfg](val cfg: P)(implicit val dec
/**
* The analysis lattice.
*/
- val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(cfg.nodes, liftedstatelattice)
+ val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(liftedstatelattice)
+
+ val domain: Set[CfgNode] = cfg.nodes
/**
* The worklist is initialized with all function entry nodes.
@@ -277,8 +281,8 @@ trait LiftedValueAnalysisMisc extends ValueAnalysisMisc {
/**
* Base class for value analysis with context sensitivity and lifted lattice.
*/
-abstract class ContextSensitiveValueAnalysis[C <: CallContext, L <: LatticeWithOps](val cfg: InterproceduralProgramCfg)(implicit val declData: DeclarationData)
- extends FlowSensitiveAnalysis[(C, CfgNode)](cfg)
+abstract class ContextSensitiveValueAnalysis[C <: CallContext](val cfg: InterproceduralProgramCfg)(implicit val declData: DeclarationData)
+ extends FlowSensitiveAnalysis(false)
with ContextSensitiveForwardDependencies[C]
with MapLiftLatticeSolver[(C, CfgNode)]
with WorklistFixpointPropagationSolver[(C, CfgNode)]
@@ -303,9 +307,7 @@ abstract class ContextSensitiveValueAnalysis[C <: CallContext, L <: LatticeWithO
/**
* The analysis lattice.
*/
- val lattice = new MapLattice({ _: (C, CfgNode) =>
- true // in principle, we should check that the node is in the CFG, but this function is not called anyway...
- }, liftedstatelattice)
+ val lattice: MapLattice[(C, CfgNode), liftedstatelattice.type] = new MapLattice(liftedstatelattice)
/**
* Collect (reverse) call edges, such that we don't have to search through the global lattice element to find the relevant call contexts.
@@ -415,9 +417,9 @@ abstract class IntraprocValueAnalysisWorklistSolverWithReachabilityAndPropagatio
*/
abstract class InterprocValueAnalysisWorklistSolverWithReachability[L <: LatticeWithOps](cfg: InterproceduralProgramCfg, val valuelattice: L)(
implicit override val declData: DeclarationData
-) extends LiftedValueAnalysis[InterproceduralProgramCfg](cfg)
+) extends LiftedValueAnalysis(cfg)
with LiftedValueAnalysisMisc
- with InterprocValueAnalysisFunctions[L]
+ with InterprocValueAnalysisFunctions
with WorklistFixpointSolverWithReachability[CfgNode]
with InterproceduralForwardDependencies {
@@ -434,7 +436,7 @@ abstract class InterprocValueAnalysisWorklistSolverWithReachability[L <: Lattice
*/
abstract class InterprocValueAnalysisWorklistSolverWithReachabilityAndPropagation[L <: LatticeWithOps](cfg: InterproceduralProgramCfg, val valuelattice: L)(
implicit override val declData: DeclarationData
-) extends LiftedValueAnalysis[InterproceduralProgramCfg](cfg)
+) extends LiftedValueAnalysis(cfg)
with InterprocValueAnalysisFunctionsWithPropagation
with WorklistFixpointPropagationSolver[CfgNode]
with InterproceduralForwardDependencies {
@@ -450,7 +452,7 @@ abstract class InterprocValueAnalysisWorklistSolverWithReachabilityAndPropagatio
*/
abstract class CallStringValueAnalysis[L <: LatticeWithOps](cfg: InterproceduralProgramCfg, val valuelattice: L)(
implicit override val declData: DeclarationData
-) extends ContextSensitiveValueAnalysis[CallStringContext, L](cfg)
+) extends ContextSensitiveValueAnalysis[CallStringContext](cfg)
with CallStringFunctions {
override val maxCallStringLength = 2; // overriding default from CallStringFunctions
@@ -461,5 +463,5 @@ abstract class CallStringValueAnalysis[L <: LatticeWithOps](cfg: Interprocedural
*/
abstract class FunctionalValueAnalysis[L <: LatticeWithOps](cfg: InterproceduralProgramCfg, val valuelattice: L)(
implicit override val declData: DeclarationData
-) extends ContextSensitiveValueAnalysis[FunctionalContext, L](cfg)
+) extends ContextSensitiveValueAnalysis[FunctionalContext](cfg)
with FunctionalFunctions
diff --git a/src/tip/ast/AstOps.scala b/src/tip/ast/AstOps.scala
index b9208fd..a17ad3a 100644
--- a/src/tip/ast/AstOps.scala
+++ b/src/tip/ast/AstOps.scala
@@ -48,7 +48,7 @@ object AstOps {
}
/**
- * Returns the set of identifier declarations appearing in the subtree of the node.
+ * Returns the set of identifiers (represented by their declarations) appearing in the subtree of the node.
*/
def appearingIds(implicit declData: DeclarationData): Set[ADeclaration] = {
val ids = mutable.Set[ADeclaration]()
diff --git a/src/tip/lattices/EdgeLattice.scala b/src/tip/lattices/EdgeFunctionLattice.scala
similarity index 64%
rename from src/tip/lattices/EdgeLattice.scala
rename to src/tip/lattices/EdgeFunctionLattice.scala
index 4e99d18..7367350 100644
--- a/src/tip/lattices/EdgeLattice.scala
+++ b/src/tip/lattices/EdgeFunctionLattice.scala
@@ -2,11 +2,12 @@ package tip.lattices
/**
* The lattice of edge functions, used by [[tip.solvers.IDEAnalysis]].
- * Technically a map lattice, but we don't bother implementing it as extension of MapLattice.
+ * A map lattice, but maps are represent differently than in `MapLattice`.
+ * Currently only supports the identity function and constant functions.
*/
-class EdgeLattice[L <: Lattice](val valuelattice: L) extends Lattice {
+class EdgeFunctionLattice[L <: Lattice](val valuelattice: L) extends Lattice {
- type Element = Edge
+ type Element = EdgeFunction
val bottom = ConstEdge(valuelattice.bottom)
@@ -15,7 +16,7 @@ class EdgeLattice[L <: Lattice](val valuelattice: L) extends Lattice {
/**
* An "edge" represents a function L -> L where L is the value lattice.
*/
- trait Edge extends (valuelattice.Element => valuelattice.Element) {
+ trait EdgeFunction extends (valuelattice.Element => valuelattice.Element) {
/**
* Applies the function to the given lattice element.
@@ -26,24 +27,24 @@ class EdgeLattice[L <: Lattice](val valuelattice: L) extends Lattice {
* Composes this function with the given one.
* The resulting function first applies `e` then this function.
*/
- def composeWith(e: Edge): Edge
+ def composeWith(e: EdgeFunction): EdgeFunction
/**
* Finds the least upper bound of this function and the given one.
*/
- def joinWith(e: Edge): Edge
+ def joinWith(e: EdgeFunction): EdgeFunction
}
/**
* Edge labeled with identity function.
*/
- case class IdEdge() extends Edge {
+ case class IdEdge() extends EdgeFunction {
def apply(x: valuelattice.Element): valuelattice.Element = x
- def composeWith(e: Edge): Edge = e
+ def composeWith(e: EdgeFunction): EdgeFunction = e
- def joinWith(e: Edge): Edge =
+ def joinWith(e: EdgeFunction): EdgeFunction =
if (e == this) this
else e.joinWith(this)
@@ -53,13 +54,13 @@ class EdgeLattice[L <: Lattice](val valuelattice: L) extends Lattice {
/**
* Edge labeled with constant function.
*/
- case class ConstEdge(c: valuelattice.Element) extends Edge {
+ case class ConstEdge(c: valuelattice.Element) extends EdgeFunction {
def apply(x: valuelattice.Element): valuelattice.Element = c
- def composeWith(e: Edge): Edge = this
+ def composeWith(e: EdgeFunction): EdgeFunction = this
- def joinWith(e: Edge): Edge =
+ def joinWith(e: EdgeFunction): EdgeFunction =
if (e == this || c == valuelattice.top) this
else if (c == valuelattice.bottom) e
else
diff --git a/src/tip/lattices/GenericLattices.scala b/src/tip/lattices/GenericLattices.scala
index 0cf662f..b2d3c35 100644
--- a/src/tip/lattices/GenericLattices.scala
+++ b/src/tip/lattices/GenericLattices.scala
@@ -114,6 +114,11 @@ class FlatLattice[X] extends Lattice {
Top
}
+/**
+ * The two-element lattice containing only Top and Bot.
+ */
+class TwoElementLattice extends FlatLattice[Nothing]
+
/**
* The product lattice made by `l1` and `l2`.
*/
@@ -127,14 +132,12 @@ class PairLattice[L1 <: Lattice, L2 <: Lattice](val sublattice1: L1, val sublatt
}
/**
- * A lattice of maps from the set `X` to the lattice `sublattice`.
- * The set `X` is a subset of `A` and it is defined by the characteristic function `ch`, i.e. `a` is in `X` if and only if `ch(a)` returns true.
+ * A lattice of maps from a set of elements of type `A` to the lattice `sublattice`.
* Bottom is the default value.
*/
-class MapLattice[A, +L <: Lattice](ch: A => Boolean, val sublattice: L) extends Lattice {
- // note: 'ch' isn't used in the class, but having it as a class parameter avoids a lot of type annotations
+class MapLattice[A, +L <: Lattice](val sublattice: L) extends Lattice {
- type Element = Map[A, sublattice.Element] // TODO: replace this with a more type safe solution?
+ type Element = Map[A, sublattice.Element]
val bottom: Element = Map().withDefaultValue(sublattice.bottom)
@@ -143,10 +146,9 @@ class MapLattice[A, +L <: Lattice](ch: A => Boolean, val sublattice: L) extends
}
/**
- * The powerset lattice of `X`, where `X` is the subset of `A` defined by the characteristic function `ch`, with subset ordering.
+ * The powerset lattice of a set of elements of type `A` with subset ordering.
*/
-class PowersetLattice[A](ch: A => Boolean) extends Lattice {
- // note: 'ch' isn't used in the class, but having it as a class parameter avoids a lot of type annotations
+class PowersetLattice[A] extends Lattice {
type Element = Set[A]
@@ -156,7 +158,7 @@ class PowersetLattice[A](ch: A => Boolean) extends Lattice {
}
/**
- * The powerset lattice of `X`, where `X` is the subset of `A` defined by the characteristic function `ch`, with superset ordering.
+ * The powerset lattice of the given set of elements of type `A` with superset ordering.
*/
class ReversePowersetLattice[A](s: Set[A]) extends Lattice {
diff --git a/src/tip/solvers/IDEAnalysis.scala b/src/tip/solvers/IDEAnalysis.scala
new file mode 100644
index 0000000..2240ee8
--- /dev/null
+++ b/src/tip/solvers/IDEAnalysis.scala
@@ -0,0 +1,51 @@
+package tip.solvers
+
+import tip.cfg.{CfgAfterCallNode, CfgCallNode, CfgFunEntryNode, CfgFunExitNode, CfgNode, InterproceduralProgramCfg}
+import tip.lattices.{EdgeFunctionLattice, Lattice}
+
+/**
+ * The special item representing the empty element in IDE.
+ */
+final case class Lambda()
+
+/**
+ * Base trait for IDE analyses.
+ * @tparam D the type of items
+ * @tparam L the type of the value lattice
+ */
+trait IDEAnalysis[D, L <: Lattice] {
+
+ val cfg: InterproceduralProgramCfg
+
+ type DL = Either[D, Lambda]
+
+ /**
+ * The value lattice.
+ */
+ val valuelattice: L
+
+ /**
+ * The edge lattice.
+ */
+ val edgelattice: EdgeFunctionLattice[valuelattice.type]
+
+ /**
+ * Edges for call-to-entry.
+ */
+ def edgesCallToEntry(d: DL, call: CfgCallNode, entry: CfgFunEntryNode): List[(DL, edgelattice.EdgeFunction)]
+
+ /**
+ * Edges for exit-to-aftercall.
+ */
+ def edgesExitToAfterCall(d: DL, exit: CfgFunExitNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.EdgeFunction)]
+
+ /**
+ * Edges for call-to-aftercall.
+ */
+ def edgesCallToAfterCall(d2: DL, call: CfgCallNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.EdgeFunction)]
+
+ /**
+ * Edges for other CFG nodes.
+ */
+ def edgesOther(d: DL, n: CfgNode): List[(DL, edgelattice.EdgeFunction)]
+}
diff --git a/src/tip/solvers/IDESolver.scala b/src/tip/solvers/IDESolver.scala
index 8f423cd..5466c73 100644
--- a/src/tip/solvers/IDESolver.scala
+++ b/src/tip/solvers/IDESolver.scala
@@ -9,292 +9,259 @@ import scala.collection.mutable
import tip.ast.AstNodeData.DeclarationData
/**
- * The special item representing the empty set in IDE.
+ * (A variant of) the IDE analysis algorithm.
*/
-final case class Lambda()
-
-/**
- * Base trait for IDE analyses.
- * @tparam D the type of items
- * @tparam L the type of the value lattice
- */
-trait IDEAnalysis[D, L <: Lattice] {
-
- val cfg: InterproceduralProgramCfg
-
- type DL = Either[D, Lambda]
-
- /**
- * The value lattice.
- */
- val valuelattice: L
-
- /**
- * The edge lattice.
- */
- val edgelattice: EdgeLattice[valuelattice.type]
-
- /**
- * Edges for call-to-entry.
- */
- def edgesCallToEntry(d: DL, call: CfgCallNode, entry: CfgFunEntryNode): List[(DL, edgelattice.Edge)]
-
- /**
- * Edges for exit-to-aftercall.
- */
- def edgesExitToAfterCall(d: DL, exit: CfgFunExitNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.Edge)]
-
- /**
- * Edges for call-to-aftercall.
- */
- def edgesCallToAfterCall(d2: DL, call: CfgCallNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.Edge)]
+abstract class IDESolver[D, L <: Lattice](val cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData)
+ extends FlowSensitiveAnalysis(false)
+ with IDEAnalysis[D, L] {
/**
- * Edges for other CFG nodes.
+ * Phase 1 of the IDE algorithm.
+ * The original version of the algorithm uses summary edges from call nodes to after-call nodes
+ * instead of `callJumpCache` and `exitJumpCache`.
*/
- def edgesOther(d: DL, n: CfgNode): List[(DL, edgelattice.Edge)]
-}
-
-/**
- * Phase 1 of the IDE algorithm.
- */
-abstract class IDEPhase1Analysis[D, L <: Lattice](val cfg: InterproceduralProgramCfg)(implicit val declData: DeclarationData)
- extends FlowSensitiveAnalysis[(CfgNode, Either[D, Lambda], Either[D, Lambda])](cfg)
- with IDEAnalysis[D, L]
- with WorklistFixpointPropagationFunctions[(CfgNode, Either[D, Lambda], Either[D, Lambda])] {
-
- /**
- * The analysis lattice.
- */
- val lattice: MapLattice[(CfgNode, DL, DL), edgelattice.type] = new MapLattice({ _: (CfgNode, DL, DL) =>
- true
- }, edgelattice)
-
- /**
- * The current lattice element.
- */
- var x: lattice.Element = _
-
- /**
- * callJumpCache(funentry, d1, call)(d3) returns the composition of the edges (call.funentry, d3) -> (call, *) -> (funentry, d1).
- * Allows faster lookup than scanning through the current lattice element.
- */
- private val callJumpCache = mutable.Map[(CfgFunEntryNode, DL, CfgCallNode), mutable.Map[DL, edgelattice.Edge]]()
-
- /**
- * exitJumpCache(funentry, d1) contains d2 if there is a non-bottom edge (funentry, d1) -> (funentry.exit, d2).
- * Allows faster lookup than scanning through the current lattice element.
- */
- private val exitJumpCache = mutable.Map[(CfgFunEntryNode, DL), mutable.Set[DL]]()
-
- import edgelattice.{Edge, IdEdge}
-
- val first: Set[(CfgNode, DL, DL)] = Set((cfg.funEntries(cfg.program.mainFunction), Right(Lambda()), Right(Lambda())))
-
- val init = IdEdge()
+ class IDEPhase1Analysis(val cfg: InterproceduralProgramCfg)(implicit val declData: DeclarationData)
+ extends WorklistFixpointPropagationFunctions[(CfgNode, Either[D, Lambda], Either[D, Lambda])] {
+
+ /**
+ * The analysis lattice.
+ */
+ val lattice: MapLattice[(CfgNode, DL, DL), edgelattice.type] = new MapLattice(edgelattice)
+
+ /**
+ * The current lattice element.
+ */
+ var x: lattice.Element = _
+
+ /**
+ * callJumpCache(funentry, d1, call)(d3) returns the composition of the edges (call.funentry, d3) -> (call, *) -> (funentry, d1).
+ * Allows faster lookup than scanning through the current lattice element.
+ */
+ private val callJumpCache = mutable.Map[(CfgFunEntryNode, DL, CfgCallNode), mutable.Map[DL, edgelattice.EdgeFunction]]()
+
+ /**
+ * exitJumpCache(funentry, d1) contains d2 if there is a non-bottom edge (funentry, d1) -> (funentry.exit, d2).
+ * Allows faster lookup than scanning through the current lattice element.
+ */
+ private val exitJumpCache = mutable.Map[(CfgFunEntryNode, DL), mutable.Set[DL]]()
+
+ import edgelattice.{EdgeFunction, IdEdge}
+
+ val first: Set[(CfgNode, DL, DL)] = Set((cfg.funEntries(cfg.program.mainFunction), Right(Lambda()), Right(Lambda())))
+
+ val init = IdEdge()
+
+ /**
+ * Joins the given edge into the call jump cache.
+ */
+ private def storeCallJump(funentry: CfgFunEntryNode, d1: DL, call: CfgCallNode, e: EdgeFunction, d3: DL): Unit = {
+ val m = callJumpCache.getOrElseUpdate((funentry, d1, call), mutable.Map[DL, edgelattice.EdgeFunction]())
+ m += d3 -> m.getOrElse(d3, edgelattice.bottom).joinWith(e)
+ }
- /**
- * Joins the given edge into the call jump cache.
- */
- private def storeCallJump(funentry: CfgFunEntryNode, d1: DL, call: CfgCallNode, e: Edge, d3: DL) = {
- val m = callJumpCache.getOrElseUpdate((funentry, d1, call), mutable.Map[DL, edgelattice.Edge]())
- m += d3 -> m.getOrElse(d3, edgelattice.bottom).joinWith(e)
- }
+ /**
+ * Adds the given item to the exit jump cache.
+ */
+ private def storeExitJump(funentry: CfgFunEntryNode, d1: DL, d2: DL): Unit =
+ exitJumpCache.getOrElseUpdate((funentry, d1), mutable.Set[DL]()) += d2
+
+ /**
+ * Models flow from function exit to aftercall node.
+ *
+ * @param d1 item at the entry of the function containing the function exit
+ * @param d2 item at the function exit
+ * @param funexit the function exit node
+ * @param aftercall the aftercall node
+ */
+ private def returnflow(d1: DL, d2: DL, funexit: CfgFunExitNode, aftercall: CfgAfterCallNode): Unit = {
+ import cfg._
+ callJumpCache.getOrElseUpdate((funexit.entry, d1, aftercall.callNode), mutable.Map[DL, edgelattice.EdgeFunction]()).foreach {
+ case (d3, e12) => // d3 is now an item at the caller function entry, and e12 is the composed edge to d1 at the callee entry
+ val e3 = x(funexit, d1, d2) // summary edge from d1 to d2 at the callee function
+ val e123 = e3.composeWith(e12)
+ edgesExitToAfterCall(d2, funexit, aftercall).foreach {
+ case (d4, e4) => // d4 is now an item at the aftercall node, and e4 is the edge from the function exit to the aftercall node
+ val e = e4.composeWith(e123) // e is now the composed edge from e3 at the caller entry to d4 at the aftercall node
+ propagate(e, (aftercall, d3, d4))
+ }
+ }
+ }
- /**
- * Adds the given item to the exit jump cache.
- */
- private def storeExitJump(funentry: CfgFunEntryNode, d1: DL, d2: DL) =
- exitJumpCache.getOrElseUpdate((funentry, d1), mutable.Set[DL]()) += d2
+ def process(nab: (CfgNode, DL, DL)) = {
+ import cfg._
+ nab match {
+ case (n, d1, d2) =>
+ NoPointers.assertContainsNode(n.data)
+ val e1 = x(nab) // e1 is the composed edge from item d1 at the entry of the function containing node n to item d2 at n
+ n match {
+
+ // function call nodes
+ case call: CfgCallNode =>
+ call.callees.foreach { entry =>
+ edgesCallToEntry(d2, call, entry).foreach {
+ case (d3, e2) =>
+ // propagate to function entry
+ propagate(IdEdge(), (entry, d3, d3))
+ // cache the composed edge from the entry of the caller to the entry of the callee
+ storeCallJump(entry, d3, call, e2.composeWith(e1), d1)
+ // propagate existing return flow to the after-call node
+ exitJumpCache.getOrElseUpdate((entry, d3), mutable.Set[DL]()).foreach { d4 =>
+ returnflow(d3, d4, entry.exit, call.afterCallNode)
+ }
+ }
+ }
+ // propagate bypassing local variables to after-call
+ edgesCallToAfterCall(d2, call, call.afterCallNode).foreach {
+ case (d3, e2) =>
+ propagate(e2.composeWith(e1), (call.afterCallNode, d1, d3))
+ }
- /**
- * Models flow from function exit to aftercall node.
- * @param d1 item at the entry of the function containing the function exit
- * @param d2 item at the function exit
- * @param funexit the function exit node
- * @param aftercall the aftercall node
- */
- private def returnflow(d1: DL, d2: DL, funexit: CfgFunExitNode, aftercall: CfgAfterCallNode): Unit = {
- import cfg._
- callJumpCache.getOrElseUpdate((funexit.entry, d1, aftercall.callNode), mutable.Map[DL, edgelattice.Edge]()).foreach {
- case (d3, e12) => // d3 is now an item at the caller function entry, and e12 is the composed edge to d1 at the callee entry
- val e3 = x(funexit, d1, d2) // summary edge from d1 to d2 at the callee function
- val e123 = e3.composeWith(e12)
- edgesExitToAfterCall(d2, funexit, aftercall).foreach {
- case (d4, e4) => // d4 is now an item at the aftercall node, and e4 is the edge from the function exit to the aftercall node
- val e = e4.composeWith(e123) // e is now the composed edge from e3 at the caller entry to d4 at the aftercall node
- propagate(e, (aftercall, d3, d4))
- }
- }
- }
+ // function exit nodes
+ case funexit: CfgFunExitNode =>
+ funexit.callersAfterCall.foreach { aftercall =>
+ returnflow(d1, d2, funexit, aftercall)
+ }
+ storeExitJump(funexit.entry, d1, d2)
- def process(nab: (CfgNode, DL, DL)) = {
- import cfg._
- nab match {
- case (n, d1, d2) =>
- NoPointers.assertContainsNode(n.data)
- val e1 = x(nab) // e1 is the composed edge from item d1 at the entry of the function containing node n to item d2 at n
- n match {
-
- // function call nodes
- case call: CfgCallNode =>
- call.callees.foreach { entry =>
- edgesCallToEntry(d2, call, entry).foreach {
+ // other nodes
+ case _ =>
+ edgesOther(d2, n).foreach {
case (d3, e2) =>
- // propagate to function entry
- propagate(IdEdge(), (entry, d3, d3))
- // cache the composed edge from the entry of the caller to the entry of the callee
- storeCallJump(cfg.enclosingFunctionEntry(call), d3, call, e2.composeWith(e1), d1)
- // propagate existing return flow to the after-call node
- exitJumpCache.getOrElseUpdate((entry, d3), mutable.Set[DL]()).foreach { d4 =>
- returnflow(d3, d4, entry.exit, call.afterCallNode)
+ val e3 = e2.composeWith(e1)
+ n.succ.foreach { m =>
+ propagate(e3, (m, d1, d3))
}
}
- }
- // propagate bypassing local variables to after-call
- edgesCallToAfterCall(d2, call, call.afterCallNode).foreach {
- case (d3, e2) =>
- propagate(e2.composeWith(e1), (call.afterCallNode, d1, d3))
- }
-
- // function exit nodes
- case funexit: CfgFunExitNode =>
- funexit.callersAfterCall.foreach { aftercall =>
- returnflow(d1, d2, funexit, aftercall)
- }
- storeExitJump(funexit.entry, d1, d2)
-
- // other nodes
- case _ =>
- edgesOther(d2, n).foreach {
- case (d3, e2) =>
- val e3 = e2.composeWith(e1)
- n.succ.foreach { m =>
- propagate(e3, (m, d1, d3))
- }
- }
- }
+ }
+ }
}
- }
- /**
- * Extracts the function summaries from the analysis result.
- * @return a map s such that s(f)(d1)(d2) is the transfer function for function f from d1 at function entry to d2 at function exit
- */
- def summaries(): mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, Edge]]] = {
- import edgelattice.Edge
- val res = mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, Edge]]]()
- x.foreach {
- case ((n, d1, d2), e) =>
- n match {
- case funexit: CfgFunExitNode =>
- val m1 = res.getOrElseUpdate(funexit.data, mutable.Map[DL, mutable.Map[DL, Edge]]().withDefaultValue(mutable.Map[DL, Edge]()))
- val m2 = m1.getOrElseUpdate(d1, mutable.Map[DL, Edge]())
- m2 += d2 -> e
- case _ => // ignore other node kinds
- }
+ /**
+ * Extracts the function summaries from the analysis result.
+ *
+ * @return a map s such that s(f)(d1)(d2) is the transfer function for function f from d1 at function entry to d2 at function exit
+ */
+ def summaries(): mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, EdgeFunction]]] = {
+ import edgelattice.EdgeFunction
+ val res = mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, EdgeFunction]]]()
+ x.foreach {
+ case ((n, d1, d2), e) =>
+ n match {
+ case funexit: CfgFunExitNode =>
+ val m1 = res.getOrElseUpdate(funexit.data, mutable.Map[DL, mutable.Map[DL, EdgeFunction]]().withDefaultValue(mutable.Map[DL, EdgeFunction]()))
+ val m2 = m1.getOrElseUpdate(d1, mutable.Map[DL, EdgeFunction]())
+ m2 += d2 -> e
+ case _ => // ignore other node kinds
+ }
+ }
+ FixpointSolvers.log.verb(s"Function summaries:\n${res.map {
+ case (f, s) => s" function $f:\n${s.map { case (d1, m) => s"${m.map { case (d2, e) => s" ($d1,$d2): $e" }.mkString("\n")}" }.mkString("\n")}"
+ }.mkString("\n")} ")
+ res
}
- FixpointSolvers.log.verb(s"Function summaries:\n${res.map {
- case (f, s) => s" function $f:\n${s.map { case (d1, m) => s"${m.map { case (d2, e) => s" ($d1,$d2): $e" }.mkString("\n")}" }.mkString("\n")}"
- }.mkString("\n")} ")
- res
}
-}
-
-/**
- * Phase 2 of the IDE algorithm.
- * Performs a forward dataflow analysis using the decomposed lattice and the micro-transformers.
- * The original RHS version of IDE uses jump functions for all nodes, not only at exits, but the analysis result and complexity is the same.
- */
-class IDEPhase2Analysis[D, L <: Lattice](val cfg: InterproceduralProgramCfg, val phase1: IDEPhase1Analysis[D, L])(implicit val declData: DeclarationData)
- extends FlowSensitiveAnalysis[(CfgNode, Either[D, Lambda])](cfg)
- with WorklistFixpointPropagationFunctions[(CfgNode, Either[D, Lambda])] {
-
- import phase1._
- import edgelattice.Edge
/**
- * Function summaries from phase 1.
- * Built when first invoked.
+ * Phase 2 of the IDE algorithm.
+ * Performs a forward dataflow analysis using the decomposed lattice and the micro-transformers.
+ * The original RHS version of IDE uses jump functions for all nodes, not only at exits, but the analysis result and complexity is the same.
*/
- lazy val summaries: mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, Edge]]] = phase1.summaries()
-
- /**
- * The analysis lattice.
- */
- val lattice: MapLattice[(CfgNode, DL), valuelattice.type] = new MapLattice({ _: (CfgNode, DL) =>
- true
- }, valuelattice)
-
- /**
- * The current lattice element.
- */
- var x: lattice.Element = _
-
- val first: Set[(CfgNode, DL)] = Set((cfg.funEntries(cfg.program.mainFunction), Right(Lambda())))
-
- val init: lattice.sublattice.Element = lattice.sublattice.top
+ class IDEPhase2Analysis(val cfg: InterproceduralProgramCfg, val phase1: IDEPhase1Analysis)(implicit val declData: DeclarationData)
+ extends FlowSensitiveAnalysis(false)
+ with WorklistFixpointPropagationFunctions[(CfgNode, Either[D, Lambda])] {
+
+ import edgelattice.EdgeFunction
+
+ /**
+ * Function summaries from phase 1.
+ * Built when first invoked.
+ */
+ lazy val summaries: mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, EdgeFunction]]] = phase1.summaries()
+
+ /**
+ * The analysis lattice.
+ */
+ val lattice: MapLattice[(CfgNode, DL), valuelattice.type] = new MapLattice(valuelattice)
+
+ /**
+ * The current lattice element.
+ */
+ var x: lattice.Element = _
+
+ val first: Set[(CfgNode, DL)] = Set((cfg.funEntries(cfg.program.mainFunction), Right(Lambda())))
+
+ val init: lattice.sublattice.Element = lattice.sublattice.top
+
+ def process(nd: (CfgNode, DL)): Unit = {
+ import cfg._
+ val xnd = x(nd)
+ nd match {
+ case (n, d) =>
+ NoPointers.assertContainsNode(n.data)
+ n match {
+
+ // function call nodes
+ case call: CfgCallNode =>
+ call.callees.foreach { entry =>
+ edgesCallToEntry(d, call, entry).foreach {
+ case (d2, e) =>
+ // propagate to function entry
+ propagate(e(xnd), (entry, d2))
+ // propagate to after-call, via the function summary and exit edges
+ summaries(entry.data)(d2).foreach {
+ case (d3, e2) =>
+ edgesExitToAfterCall(d3, entry.exit, call.afterCallNode).foreach {
+ case (d4, e3) =>
+ propagate(e3(e2(e(xnd))), (call.afterCallNode, d4))
+ }
+ }
+ }
+ }
+ // propagate bypassing local variables to after-call
+ edgesCallToAfterCall(d, call, call.afterCallNode).foreach {
+ case (d2, e) =>
+ propagate(e(xnd), (call.afterCallNode, d2))
+ }
- def process(nd: (CfgNode, DL)) = {
- import cfg._
- val xnd = x(nd)
- nd match {
- case (n, d) =>
- NoPointers.assertContainsNode(n.data)
- n match {
+ // function exit nodes
+ case _: CfgFunExitNode => // ignore, return flow is handled at the call nodes
- // function call nodes
- case call: CfgCallNode =>
- call.callees.foreach { entry =>
- edgesCallToEntry(d, call, entry).foreach {
+ // all other nodes, just use the micro-transformer edges
+ case _ =>
+ edgesOther(d, n).foreach {
case (d2, e) =>
- // propagate to function entry
- propagate(e(xnd), (entry, d2))
- // propagate to after-call, via the function summary and exit edges
- summaries(entry.data)(d2).foreach {
- case (d3, e2) =>
- edgesExitToAfterCall(d3, entry.exit, call.afterCallNode).foreach {
- case (d4, e3) =>
- propagate(e3(e2(e(xnd))), (call.afterCallNode, d4))
- }
+ n.succ.foreach { m =>
+ propagate(e(xnd), (m, d2))
}
}
- }
- // propagate bypassing local variables to after-call
- edgesCallToAfterCall(d, call, call.afterCallNode).foreach {
- case (d2, e) =>
- propagate(e(xnd), (call.afterCallNode, d2))
- }
-
- // function exit nodes
- case funexit: CfgFunExitNode => // ignore, return flow is handled at the call nodes
-
- // all other nodes, just use the micro-transformer edges
- case _ =>
- edgesOther(d, n).foreach {
- case (d2, e) =>
- n.succ.foreach { m =>
- propagate(e(xnd), (m, d2))
- }
- }
- }
+ }
+ }
}
- }
- val restructedlattice = new MapLattice(cfg.nodes, new MapLattice({ _: D =>
- true
- }, lattice.sublattice))
+ val restructuredlattice: MapLattice[CfgNode, MapLattice[D, valuelattice.type]] = new MapLattice(new MapLattice(valuelattice))
- /**
- * Restructures the analysis output to match `restructedlattice`.
- */
- def restructure(y: lattice.Element): restructedlattice.Element =
- y.foldLeft(Map[CfgNode, Map[D, lattice.sublattice.Element]]()) {
+ /**
+ * Restructures the analysis output to match `restructuredlattice`.
+ */
+ def restructure(y: lattice.Element): restructuredlattice.Element =
+ y.foldLeft(Map[CfgNode, Map[D, valuelattice.Element]]()) {
case (acc, ((n, dl), e)) =>
dl match {
- case Left(d) => acc + (n -> (acc.getOrElse(n, Map[D, lattice.sublattice.Element]()) + (d -> e)))
- case _ => acc // FIXME: use lifted lattice and map this to unreachable?
+ case Left(d) => acc + (n -> (acc.getOrElse(n, Map[D, valuelattice.Element]()) + (d -> e)))
+ case _ => acc // TODO: could use lifted lattice and map this to unreachable
}
}
- .asInstanceOf[restructedlattice.Element] // FIXME: avoid this asInstanceOf
+ }
+
+ lazy val phase1 = new IDEPhase1Analysis(cfg)
+ lazy val phase2 = new IDEPhase2Analysis(cfg, phase1)
+
+ lazy val lattice: MapLattice[CfgNode, MapLattice[D, valuelattice.type]] = phase2.restructuredlattice
+
+ def analyze(): lattice.Element = {
+ FixpointSolvers.log.verb(s"IDE phase 1")
+ phase1.analyze()
+ FixpointSolvers.log.verb(s"IDE phase 2")
+ phase2.restructure(phase2.analyze())
+ }
}
diff --git a/src/tip/util/Output.scala b/src/tip/util/Output.scala
index 4899fda..c7ffab2 100644
--- a/src/tip/util/Output.scala
+++ b/src/tip/util/Output.scala
@@ -83,12 +83,16 @@ object Output {
* Helper function for producing string output for a control-flow graph node after an analysis.
* @param res map from control-flow graph nodes to strings, as produced by the analysis
*/
- def labeler(res: Map[CfgNode, _])(n: CfgNode): String =
- n match {
- case entry: CfgFunEntryNode => s"Function ${entry.data.name} entry\n${res.getOrElse(n, "-")}"
- case exit: CfgFunExitNode => s"Function ${exit.data.name} exit\n${res.getOrElse(n, "-")}"
- case _ => s"$n\n${res.getOrElse(n, "-")}"
+ def labeler(res: Map[CfgNode, _], stateAfterNode: Boolean)(n: CfgNode): String = {
+ val r = res.getOrElse(n, "-")
+ val desc = n match {
+ case entry: CfgFunEntryNode => s"Function ${entry.data.name} entry"
+ case exit: CfgFunExitNode => s"Function ${exit.data.name} exit"
+ case _ => n.toString
}
+ if (stateAfterNode) s"$desc\n$r"
+ else s"$r\n$desc"
+ }
/**
* Transforms a map from pairs of call contexts and CFG nodes to values into a map from CFG nodes to strings.