Cumulative updates

Author: amoeller

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

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()

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,

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

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
   }
 }

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)

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