Cumulative updates

vorpal-research · Nov 9, 2020 · cfdd9dd · cfdd9dd
1 parent a8e9428
commit cfdd9dd
Show file tree

Hide file tree

Showing 39 changed files with 669 additions and 448 deletions.
diff --git a/README.md b/README.md
@@ -143,8 +143,8 @@ To automatically format when the file is saved, go to File -> Settings..., under
 
 ## Authors
 
-- [Gianluca Mezzetti](http://gmezzetti.name/)
 - [Anders M&oslash;ller](http://cs.au.dk/~amoeller/)
+- [Gianluca Mezzetti](http://gmezzetti.name/)
 
 with contributions from
 

diff --git a/examples/cfa.tip b/examples/cfa.tip
@@ -5,13 +5,13 @@ ide(k) { return k; }
 foo(n,f) {
     var r;
     if (n==0) { f=ide; }
-    r = (f)(n);
+    r = f(n);
     return r;
 }
 
 main() {
     var x,y;
-    x = 1;//input;
+    x = input;
     if (x>0) { y = foo(x,inc); } else { y = foo(x,dec); }
     return y;
 }
diff --git a/src/tip/Tip.scala b/src/tip/Tip.scala
@@ -6,7 +6,7 @@ import org.parboiled2.ParseError
 import tip.analysis.FlowSensitiveAnalysis.{Analysis => dfa, AnalysisOption => dfo}
 import tip.analysis._
 import tip.ast.AstNodeData._
-import tip.ast.AProgram
+import tip.ast.{AProgram, NoNormalizer}
 import tip.concolic.ConcolicEngine
 import tip.cfg._
 import tip.interpreter.ConcreteInterpreter
@@ -20,7 +20,6 @@ import scala.util.{Failure, Success}
   * Options for running the TIP system.
   */
 class RunOption {
-  val log = Log.logger[this.type]()
 
   /**
     * If set, construct the (intraprocedural) control-flow graph after parsing.
@@ -82,7 +81,7 @@ class RunOption {
     */
   def check(): Boolean =
     if (source == null) {
-      log.error(s"Source file/directory missing")
+      Tip.log.error(s"Source file/directory missing")
       false
     } else
       true
@@ -158,9 +157,17 @@ object Tip extends App {
     */
   def processFile(file: File, options: RunOption) = {
     try {
-      val program = Source.fromFile(file).mkString
+      val program = {
+        val bs = Source.fromFile(file)
+        try {
+          bs.mkString
+        } finally {
+          bs.close()
+        }
+      }
 
       // parse the program
+      log.verb("Parsing")
       val tipParser = new TipParser(program)
       val res = tipParser.InputLine.run()
 
@@ -173,17 +180,21 @@ object Tip extends App {
           sys.exit(1)
         case Success(parsedNode: AProgram) =>
           // run normalizer
+          log.verb("Normalizing")
           val programNode = options.normalizer.normalizeProgram(parsedNode)
-          Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out)
+          if (options.normalizer != NoNormalizer)
+            Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out)
 
           // run declaration analysis
           // (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]])
+          log.verb("Declaration analysis")
           implicit val declData: DeclarationData = new DeclarationAnalysis(programNode).analyze()
 
           // run selected intraprocedural flow-sensitive analyses
           if (options.cfg | options.dfAnalysis.exists(p => p._2 != dfo.Disabled && !dfo.interprocedural(p._2))) {
 
             // generate control-flow graph
+            log.verb("Building intraprocedural control flow graphs")
             val wcfg = IntraproceduralProgramCfg.generateFromProgram(programNode)
             if (options.cfg)
               Output.output(file, OtherOutput(OutputKindE.cfg), wcfg.toDot({ x =>
@@ -195,6 +206,7 @@ object Tip extends App {
                 if (!dfo.interprocedural(v)) {
                   FlowSensitiveAnalysis.select(s, v, wcfg).foreach { an =>
                     // 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)
                   }
@@ -207,8 +219,10 @@ object Tip extends App {
 
             // generate control-flow graph
             val wcfg = if (options.cfa) {
+              log.verb("Building interprocedural control flow graph using control flow analysis")
               InterproceduralProgramCfg.generateFromProgramWithCfa(programNode)
             } else {
+              log.verb("Building interprocedural control flow graph")
               InterproceduralProgramCfg.generateFromProgram(programNode)
             }
 
@@ -223,6 +237,7 @@ object Tip extends App {
                 if (dfo.interprocedural(v)) {
                   FlowSensitiveAnalysis.select(s, v, wcfg).foreach { an =>
                     // run the analysis
+                    log.verb(s"Starting ${an.getClass.getSimpleName}")
                     val res = an.analyze()
                     val res2 =
                       if (dfo.contextsensitive(v))
@@ -238,19 +253,22 @@ object Tip extends App {
           // run type analysis, if selected
           if (options.types) {
             // (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]])
+            log.verb("Starting TypeAnalysis")
             implicit val typeData: TypeData = new TypeAnalysis(programNode).analyze()
             Output.output(file, OtherOutput(OutputKindE.types), programNode.toTypedString, options.out)
           }
 
           // run Andersen analysis, if selected
           if (options.andersen) {
+            log.verb("Starting AndersenAnalysis")
             val s = new AndersenAnalysis(programNode)
             s.analyze()
             s.pointsTo()
           }
 
           // run Steensgaard analysis, if selected
           if (options.steensgaard) {
+            log.verb("Starting SteensgaardAnalysis")
             val s = new SteensgaardAnalysis(programNode)
             s.analyze()
             s.pointsTo()
@@ -259,31 +277,34 @@ object Tip extends App {
           // run control-flow analysis, if selected
           if (options.cfa) { // TODO: skip if InterproceduralProgramCfg.generateFromProgramWithCfa has been executed above
             val s = new ControlFlowAnalysis(programNode)
+            log.verb("Starting ControlFlowAnalysis")
             s.analyze()
           }
 
           // execute the program, if selected
           if (options.run) {
+            log.verb("Starting ConcreteInterpreter")
             val intp = new ConcreteInterpreter(programNode)
             intp.semp()
           }
 
           // concolically execute the program, if selected
           if (options.concolic) {
+            log.verb("Starting ConcolicEngine")
             new ConcolicEngine(programNode).test()
           }
-
-          log.info("Success")
       }
     } catch {
+      case e: TipProgramException =>
+        log.error(e.getMessage)
+        sys.exit(1)
       case e: Exception =>
-        log.error(s"Error: ${e.getMessage}", e)
+        log.error(s"Internal error: ${e.getMessage}", e)
         sys.exit(1)
     }
   }
 
   // parse options
-  Log.defaultLevel = Log.Level.Info
   val options = new RunOption()
   var i = 0
   while (i < args.length) {
@@ -322,6 +343,7 @@ object Tip extends App {
           options.concolic = true
         case "-verbose" =>
           Log.defaultLevel = Log.Level.Verbose
+          log.level = Log.Level.Verbose
         case _ =>
           log.error(s"Unrecognized option $s")
           printUsage()

diff --git a/src/tip/analysis/AndersenAnalysis.scala b/src/tip/analysis/AndersenAnalysis.scala
@@ -6,7 +6,7 @@ import tip.util.Log
 import tip.ast.AstNodeData.DeclarationData
 import scala.language.implicitConversions
 
-class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Null] with PointsToAnalysis {
+class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) extends DepthFirstAstVisitor[Unit] with PointsToAnalysis {
 
   val log = Log.logger[this.type]()
 
@@ -21,7 +21,7 @@ class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) ex
   val solver = new CubicSolver[Cell, Cell]
 
   import AstOps._
-  val allTargets: Set[Cell] = (program.appearingIds.map(Var): Set[Cell]) union program.appearingAllocs.map(Alloc)
+  val cells: Set[Cell] = (program.appearingIds.map(Var): Set[Cell]) union program.appearingAllocs.map(Alloc)
 
   NormalizedForPointsToAnalysis.assertContainsProgram(program)
   NoRecords.assertContainsProgram(program)
@@ -30,30 +30,27 @@ class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) ex
     * @inheritdoc
     */
   def analyze(): Unit =
-    visit(program, null)
+    visit(program, ())
 
   /**
     * Generates the constraints for the given sub-AST.
     * @param node the node for which it generates the constraints
     * @param arg unused for this visitor
     */
-  def visit(node: AstNode, arg: Null): Unit = {
+  def visit(node: AstNode, arg: Unit): Unit = {
 
     implicit def identifierToTarget(id: AIdentifier): Var = Var(id)
     implicit def allocToTarget(alloc: AAlloc): Alloc = Alloc(alloc)
 
     node match {
       case AAssignStmt(id: AIdentifier, alloc: AAlloc, _) => ??? //<--- Complete here
-      case AAssignStmt(id1: AIdentifier, AUnaryOp(RefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here
+      case AAssignStmt(id1: AIdentifier, AVarRef(id2: AIdentifier, _), _) => ??? //<--- Complete here
       case AAssignStmt(id1: AIdentifier, id2: AIdentifier, _) => ??? //<--- Complete here
       case AAssignStmt(id1: AIdentifier, AUnaryOp(DerefOp, id2: AIdentifier, _), _) => ??? //<--- Complete here
-      case AAssignStmt(AUnaryOp(_, id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here
-      case AAssignStmt(_: AIdentifier, ANull(_), _) =>
-      case AAssignStmt(_: AIdentifier, _: AAtomicExpr, _) =>
-      case ass: AAssignStmt => NormalizedForPointsToAnalysis.LanguageRestrictionViolation(s"Assignment $ass not expected")
+      case AAssignStmt(ADerefWrite(id1: AIdentifier, _), id2: AIdentifier, _) => ??? //<--- Complete here
       case _ =>
     }
-    visitChildren(node, null)
+    visitChildren(node, ())
   }
 
   /**

diff --git a/src/tip/analysis/AvailableExpAnalysis.scala b/src/tip/analysis/AvailableExpAnalysis.scala
@@ -14,7 +14,7 @@ abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit dec
   import tip.cfg.CfgOps._
   import tip.ast.AstOps._
 
-  val allExps: Set[UnlabelledNode[AExpr]] = cfg.nodes.flatMap(_.appearingExpressions.map(UnlabelledNode[AExpr]))
+  val allExps: Set[UnlabelledNode[AExpr]] = cfg.nodes.flatMap(_.appearingNonInputExpressions.map(UnlabelledNode[AExpr]))
 
   NoPointers.assertContainsProgram(cfg.prog)
   NoRecords.assertContainsProgram(cfg.prog)
@@ -26,20 +26,20 @@ abstract class AvailableExpAnalysis(cfg: IntraproceduralProgramCfg)(implicit dec
       case _: CfgFunEntryNode => Set()
       case r: CfgStmtNode =>
         r.data match {
-          case ass: AAssignStmt =>
-            ass.left match {
+          case as: AAssignStmt =>
+            as.left match {
               case id: AIdentifier =>
-                (s union ass.right.appearingExpressions.map(UnlabelledNode[AExpr])).filter { e =>
+                (s union as.right.appearingNonInputExpressions.map(UnlabelledNode[AExpr])).filter { e =>
                   !(id.appearingIds subsetOf e.n.appearingIds)
                 }
               case _ => ???
             }
           case exp: AExpr =>
-            s union exp.appearingExpressions.map(UnlabelledNode[AExpr])
+            s union exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr])
           case out: AOutputStmt =>
-            s union out.value.appearingExpressions.map(UnlabelledNode[AExpr])
+            s union out.exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr])
           case ret: AReturnStmt =>
-            s union ret.value.appearingExpressions.map(UnlabelledNode[AExpr])
+            s union ret.exp.appearingNonInputExpressions.map(UnlabelledNode[AExpr])
           case _ => s
         }
       case _ => s

diff --git a/src/tip/analysis/ConstantPropagationAnalysis.scala b/src/tip/analysis/ConstantPropagationAnalysis.scala
@@ -49,13 +49,13 @@ object ConstantPropagationAnalysis {
 
     /**
       * Interprocedural analysis that uses the worklist solver with reachability and propagation-style.
-      * with call-string context sensivity.
+      * with call-string context sensitivity.
       */
     class CallString(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends CallStringValueAnalysis(cfg, ConstantPropagationLattice)
 
     /**
       * Interprocedural analysis that uses the worklist solver with reachability and propagation-style.
-      * with functional-approach context sensivity.
+      * with functional-approach context sensitivity.
       */
     class Functional(cfg: InterproceduralProgramCfg)(implicit declData: DeclarationData) extends FunctionalValueAnalysis(cfg, ConstantPropagationLattice)
   }

diff --git a/src/tip/analysis/ControlFlowAnalysis.scala b/src/tip/analysis/ControlFlowAnalysis.scala
@@ -8,7 +8,7 @@ import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData}
 import scala.language.implicitConversions
 
 class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
-    extends DepthFirstAstVisitor[Null]
+    extends DepthFirstAstVisitor[Unit]
     with Analysis[Map[AstNode, Set[AFunDeclaration]]] {
 
   val log = Log.logger[this.type]()
@@ -35,9 +35,9 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
     * @inheritdoc
     */
   def analyze(): Map[AstNode, Set[AFunDeclaration]] = {
-    visit(program, null)
+    visit(program, ())
     val sol = solver.getSolution
-    log.info(s"Solution is:\n${sol.map { case (k, v) => s"  [[$k]] = {${v.mkString(",")}}" }.mkString("\n")}")
+    log.info(s"Solution is:\n${sol.map { case (k, v) => s"  \u27E6$k\u27E7 = {${v.mkString(",")}}" }.mkString("\n")}")
     sol.map(vardecl => vardecl._1.n -> vardecl._2.map(_.fun))
   }
 
@@ -46,7 +46,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: Null) = {
+  def visit(node: AstNode, arg: Unit) = {
 
     /**
       * Get the declaration if the supplied AstNode is an identifier,
@@ -63,9 +63,10 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData)
     node match {
       case fun: AFunDeclaration => ??? //<--- Complete here
       case AAssignStmt(id: AIdentifier, e, _) => ??? //<--- Complete here
+      case ACallFuncExpr(targetFun: AIdentifier, args, _) if decl(targetFun).isInstanceOf[AFunDeclaration] => ??? //<--- Complete here (or remove this case)
       case ACallFuncExpr(targetFun, args, _) => ??? //<--- Complete here
       case _ =>
     }
-    visitChildren(node, null)
+    visitChildren(node, ())
   }
 }
diff --git a/src/tip/analysis/CopyConstantPropagationAnalysis.scala b/src/tip/analysis/CopyConstantPropagationAnalysis.scala
@@ -58,8 +58,8 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration,
             }
 
           // assignments
-          case ass: AAssignStmt =>
-            ass match {
+          case as: AAssignStmt =>
+            as match {
               case AAssignStmt(id: AIdentifier, right, _) =>
                 val edges = assign(d, id.declaration, right)
                 d match {
@@ -68,11 +68,11 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration,
                   case _ =>
                     edges
                 }
-              case AAssignStmt(_, _, _) => NoPointers.LanguageRestrictionViolation(s"$ass not allowed")
+              case AAssignStmt(_, _, _) => NoPointers.LanguageRestrictionViolation(s"$as not allowed", as.loc)
             }
 
           // return statement
-          case ret: AReturnStmt => assign(d, AstOps.returnId, ret.value)
+          case ret: AReturnStmt => assign(d, AstOps.returnId, ret.exp)
 
           // all other kinds of statements: like no-ops
           case _ => List((d, IdEdge()))