From a8377553075c6ed4f7a6274f24ca760ad5302501 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B8ller?= <amoeller@cs.au.dk>
Date: Sun, 14 Nov 2021 20:34:46 +0100
Subject: [PATCH] Cumulative updates

---
 src/tip/Tip.scala                             |   7 +-
 src/tip/analysis/AvailableExpAnalysis.scala   |  10 +-
 src/tip/analysis/ControlFlowAnalysis.scala    |   7 +-
 .../CopyConstantPropagationAnalysis.scala     |  51 +-
 src/tip/analysis/FlowSensitiveAnalysis.scala  |  27 +-
 src/tip/analysis/LiveVarsAnalysis.scala       |  10 +-
 .../PossiblyUninitializedVarsAnalysis.scala   | 110 ++++
 src/tip/analysis/SimpleSignAnalysis.scala     |  11 +-
 src/tip/analysis/ValueAnalysis.scala          |  38 +-
 src/tip/ast/AstOps.scala                      |   2 +-
 ...attice.scala => EdgeFunctionLattice.scala} |  25 +-
 src/tip/lattices/GenericLattices.scala        |  20 +-
 src/tip/solvers/IDEAnalysis.scala             |  51 ++
 src/tip/solvers/IDESolver.scala               | 479 ++++++++----------
 src/tip/util/Output.scala                     |  14 +-
 15 files changed, 491 insertions(+), 371 deletions(-)
 create mode 100644 src/tip/analysis/PossiblyUninitializedVarsAnalysis.scala
 rename src/tip/lattices/{EdgeLattice.scala => EdgeFunctionLattice.scala} (64%)
 create mode 100644 src/tip/solvers/IDEAnalysis.scala

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 <em>after</em> the node,
+  *                       false if represents the program point <em>before</em> 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..4f27d50
--- /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.Element)]
+
+  /**
+    * Edges for exit-to-aftercall.
+    */
+  def edgesExitToAfterCall(d: DL, exit: CfgFunExitNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.Element)]
+
+  /**
+    * Edges for call-to-aftercall.
+    */
+  def edgesCallToAfterCall(d2: DL, call: CfgCallNode, aftercall: CfgAfterCallNode): List[(DL, edgelattice.Element)]
+
+  /**
+    * Edges for other CFG nodes.
+    */
+  def edgesOther(d: DL, n: CfgNode): List[(DL, edgelattice.Element)]
+}
diff --git a/src/tip/solvers/IDESolver.scala b/src/tip/solvers/IDESolver.scala
index 8f423cd..82b513a 100644
--- a/src/tip/solvers/IDESolver.scala
+++ b/src/tip/solvers/IDESolver.scala
@@ -9,292 +9,255 @@ 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)]
-
-  /**
-    * Edges for other CFG nodes.
-    */
-  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 = _
+abstract class IDESolver[D, L <: Lattice](val cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData)
+    extends FlowSensitiveAnalysis(false)
+    with IDEAnalysis[D, L] {
 
   /**
-    * 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.
+    * 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`.
     */
-  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) 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.
-    */
-  lazy val summaries: mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, Edge]]] = phase1.summaries()
 
   /**
-    * The analysis lattice.
+    * 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.
     */
-  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)
+      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
+  }
+
+  def analyze(): Map[CfgNode, Map[D, valuelattice.Element]] = {
+    FixpointSolvers.log.verb(s"IDE phase 1")
+    val phase1 = new IDEPhase1Analysis(cfg)
+    phase1.analyze()
+    FixpointSolvers.log.verb(s"IDE phase 2")
+    val phase2 = new IDEPhase2Analysis(cfg, phase1)
+    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.