Add dependency analysis features

src/main/scala/viper/silver/ast/Ast.scala

@@ -6,16 +6,17 @@
 
 package viper.silver.ast
 
-import scala.collection.mutable
-import scala.reflect.ClassTag
-import pretty.FastPrettyPrinter
-import utility._
+import viper.silver.ast.pretty.FastPrettyPrinter
+import viper.silver.ast.utility._
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
 import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
 import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason}
 
+import scala.collection.mutable
+import scala.reflect.ClassTag
+
 /*
 
 This is the Viper abstract syntax description.

src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala

@@ -227,7 +227,7 @@ object ImpureAssumeRewriter {
     }).execute(p)
 
     val pAssume: Program = ViperStrategy.Slim({
-      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos))
+      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos, a.info, a.errT))
     }).execute(pInvs)
 
     if (funcs.isEmpty && domains.isEmpty) {

src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala

@@ -9,6 +9,7 @@ package viper.silver.ast.utility
 import scala.collection.mutable
 import scala.language.postfixOps
 import viper.silver.ast._
+import viper.silver.dependencyAnalysis.AnalysisSourceInfo
 
 /** Utility methods for quantified predicate permissions. */
 object QuantifiedPermissions {
@@ -164,7 +165,7 @@ object QuantifiedPermissions {
   def desugarSourceQuantifiedPermissionSyntax(source: Forall): Seq[Forall] = {
 
 
-    source match {
+    val res = source match {
       case SourceQuantifiedPermissionAssertion(_, Implies(cond, rhs)) if (!rhs.isPure) =>
         /* Source forall denotes a quantified permission assertion that potentially
          * needs to be desugared
@@ -272,5 +273,7 @@ object QuantifiedPermissions {
          */
         Seq(source)
     }
+
+    res.map(e => e.withMeta(e.pos, MakeInfoPair(AnalysisSourceInfo.createAnalysisSourceInfo(e), e.info), e.errT))
   }
 }

src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala

@@ -6,8 +6,9 @@
 
 package viper.silver.ast.utility.rewriter
 
+import viper.silver.ast._
 import viper.silver.parser.PNode
-import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position}
+import viper.silver.plugin.standard.adt.{AdtConstructor, AdtConstructorApp, AdtDestructorApp, AdtDiscriminatorApp}
 
 import scala.reflect.runtime.{universe => reflection}
 
@@ -45,7 +46,7 @@ trait Rewritable extends Product {
         // Add additional arguments to constructor call, besides children
         val firstArgList = children
         var secondArgList = Seq.empty[Any]
-        import viper.silver.ast.{DomainType, DomainAxiom, FuncApp, DomainFunc, DomainFuncApp}
+        import viper.silver.ast.{DomainAxiom, DomainFunc, DomainFuncApp, DomainType, FuncApp}
         this match {
           // TODO: remove the following cases by implementing `HasExtraValList` on the respective classes
           case dt: DomainType => secondArgList = Seq(dt.typeParameters)
@@ -112,6 +113,12 @@ trait Rewritable extends Product {
       val arguments = this match {
         case fa: FuncApp => this.children ++ Seq(pos, info, fa.typ, trafo)
         case df: DomainFuncApp => this.children ++ Seq(pos, info, df.typ, df.domainName, trafo)
+				case bfa: BackendFuncApp => this.children ++ Seq(pos, info, bfa.typ, bfa.interpretation, trafo)
+        case dm: DomainMember => this.children ++ Seq(pos, info, dm.domainName, trafo)
+				case d: AdtDiscriminatorApp => this.children ++ Seq(pos, info, d.adtName, trafo)
+				case d: AdtConstructor => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo)
+				case d: AdtConstructorApp => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo)
+				case d: AdtDestructorApp => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo)
         case _ => this.children ++ Seq(pos, info, trafo)
       }
 

src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala

@@ -10,8 +10,8 @@ import viper.silver.ast._
 import viper.silver.cfg._
 import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge}
 import viper.silver.cfg.utility.{CfgSimplifier, IdInfo, LoopDetector}
-import java.util.concurrent.atomic.AtomicInteger
 
+import java.util.concurrent.atomic.AtomicInteger
 import scala.collection.mutable
 
 /**

src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala

@@ -0,0 +1,80 @@
+package viper.silver.dependencyAnalysis
+
+import viper.silver.ast
+import viper.silver.ast._
+
+object AnalysisSourceInfo {
+  def extractPositionString(p: Position): String = {
+    p match {
+      case NoPosition => "???"
+      case filePos: AbstractSourcePosition => filePos.file.getFileName.toString + " @ line " + filePos.line
+      case filePos: FilePosition => filePos.file.getFileName.toString + " @ line " + filePos.line
+      case lineColumn: HasLineColumn => "line " + lineColumn.line.toString
+      case VirtualPosition(identifier) => "label " + identifier
+    }
+  }
+
+	def createAnalysisSourceInfo(node: ast.Node): AnalysisSourceInfo = {
+		node match {
+			case stmt: ast.Stmt => StmtAnalysisSourceInfo(stmt, stmt.pos)
+			case exp: ast.Exp => ExpAnalysisSourceInfo(exp, exp.pos)
+			case _ => createAnalysisSourceInfo("Unknown", NoPosition)
+		}
+	}
+
+  def createAnalysisSourceInfo(description: String, pos: Position): AnalysisSourceInfo = StringAnalysisSourceInfo(description, pos)
+
+}
+
+trait AnalysisSourceInfo extends ast.Info {
+  override def toString: String = getPositionString
+
+  def getDescription: String
+
+  def getLineNumber: Option[Int] = getPosition match {
+    case column: HasLineColumn => Some(column.line)
+    case _ => None
+  }
+
+  def getPositionString: String = {
+    AnalysisSourceInfo.extractPositionString(getPosition)
+  }
+
+  def getPosition: Position
+
+  override def comment: Seq[String] = Nil
+  override def isCached: Boolean = false
+}
+
+case class NoAnalysisSourceInfo() extends AnalysisSourceInfo {
+  override def getPosition: Position = NoPosition
+
+  override def getDescription: String = ""
+
+  override def equals(obj: Any): Boolean = false
+}
+
+case class ExpAnalysisSourceInfo(source: ast.Exp, pos: Position) extends AnalysisSourceInfo {
+
+  override def toString: String = getDescription + " (" + super.toString + ")"
+
+  override def getPosition: Position = pos
+
+  override def getDescription: String = source.toString.replaceAll("\n", "\t")
+}
+
+case class StmtAnalysisSourceInfo(source: ast.Stmt, pos: Position) extends AnalysisSourceInfo {
+
+  override def toString: String = getDescription + " (" + super.toString + ")"
+  override def getPosition: Position = pos
+
+  override def getDescription: String = source.toString().replaceAll("\n", "\t")
+}
+
+case class StringAnalysisSourceInfo(description: String, position: Position) extends AnalysisSourceInfo {
+  override def toString: String = getDescription + " (" + getPositionString + ")"
+  override def getPosition: Position = position
+
+  override def getDescription: String = description.replaceAll("\n", "\t")
+}
+

src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala

@@ -0,0 +1,114 @@
+package viper.silver.dependencyAnalysis
+
+import viper.silver.ast
+import viper.silver.dependencyAnalysis.DependencyType._
+import viper.silver.dependencyAnalysis.EdgeType.EdgeType
+import viper.silver.dependencyAnalysis.JoinType.JoinType
+
+object DependencyTypeInfo {
+	def getDependencyTypeInfo(stmt: ast.Stmt): DependencyTypeInfo = {
+		val depType = stmt match {
+			case _: ast.MethodCall => MethodCall
+			case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
+			case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
+			case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
+			case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
+			case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.SourceCode
+			case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */
+		}
+		DependencyTypeInfo(depType)
+	}
+}
+
+case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info {
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+object JoinType extends Enumeration {
+	type JoinType = Value
+	val Source, Sink = Value
+}
+
+object EdgeType extends Enumeration {
+	type EdgeType = Value
+	val Up, Down = Value
+}
+
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to join dependency graphs of
+ * individual verification components. Nodes with matching join information are connected by an interprocedural edge.
+ */
+trait DependencyAnalysisJoinInfo extends ast.Info {
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+
+	def matches(dependencyAnalysisJoinInfo: DependencyAnalysisJoinInfo) = {
+		(this, dependencyAnalysisJoinInfo) match {
+			case (SimpleDependencyAnalysisJoin(sourceInfo, joinType, edgeType), SimpleDependencyAnalysisJoin(sourceInfo1, joinType1, edgeType1)) =>
+				sourceInfo.equals(sourceInfo1) && edgeType.equals(edgeType1)
+		}
+	}
+}
+
+case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to finalize the intraprocedural
+ * dependency graph. Nodes with matching merge information are connected by an intraprocedural edge.
+ */
+trait DependencyAnalysisMergeInfo extends ast.Info {
+
+	def isMerge: Boolean
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+case class NoDependencyAnalysisMerge() extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = false
+}
+
+case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = true
+}
+
+case class CompositeDependencyAnalysisMergeInfo(sourceInfo1: AnalysisSourceInfo, sourceInfo2: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = true
+}
+
+object DependencyAnalysisMergeInfo {
+	def attachExpMergeInfo(exps: Seq[ast.Exp], sourceInfo2: Option[AnalysisSourceInfo]): Seq[ast.Exp] = {
+		exps.map(attachExpMergeInfo(_, sourceInfo2))
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val expSourceInfo = AnalysisSourceInfo.createAnalysisSourceInfo(exp)
+		attachExpMergeInfo(exp, expSourceInfo, sourceInfo2)
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp, mergeInfo: DependencyAnalysisMergeInfo): ast.Exp = {
+		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val mergeInfo = if(sourceInfo2.isDefined)
+			CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get)
+		else
+			SimpleDependencyAnalysisMerge(sourceInfo1)
+		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	}
+}
+
+trait AdditionalDependencyNodeInfo extends ast.Info {
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+case class AdditionalAssertionNode() extends AdditionalDependencyNodeInfo
+
+case class AdditionalAssumptionNode() extends AdditionalDependencyNodeInfo

src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala

@@ -0,0 +1,54 @@
+package viper.silver.dependencyAnalysis
+
+object AssumptionType extends Enumeration {
+  type AssumptionType = Value
+  val Explicit, LoopInvariant, PathCondition, Rewrite, SourceCode, DomainAxiom, Implicit, Internal, Trigger, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, MethodCall, FunctionBody, Precondition, Ghost, Annotation, Unknown = Value
+
+  def fromString(s: String): Option[Value] = values.find(_.toString == s)
+
+  def explicitAssumptionTypes: Set[AssumptionType] = Set(Explicit, ExplicitPostcondition)
+  def postconditionTypes: Set[AssumptionType] = Set(ImplicitPostcondition, ExplicitPostcondition, ImportedPostcondition)
+  def preconditionTypes: Set[AssumptionType] = Set(Precondition)
+  def explicitAssertionTypes: Set[AssumptionType] = Set(Explicit, ImplicitPostcondition, ExplicitPostcondition)
+  def internalTypes: Set[AssumptionType] = Set(Internal, Trigger) // will always be hidden from user
+  def importedTypes: Set[AssumptionType] = Set(ImportedPostcondition)
+  def verificationAnnotationTypes: Set[AssumptionType] = Set(FunctionBody /* TODO ake: review */, LoopInvariant, Rewrite, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, Precondition, Explicit, DomainAxiom, Annotation)
+
+
+  def getPostcondType(isAbstractFunction: Boolean, dependencyType: Option[DependencyType]=None, isImported: Boolean=false): AssumptionType = {
+    if(isImported) return ImportedPostcondition
+
+    dependencyType.flatMap(_.assertionType match {
+      case AssumptionType.Explicit | AssumptionType.ExplicitPostcondition => Some(AssumptionType.ExplicitPostcondition)
+      case AssumptionType.ImportedPostcondition => Some(AssumptionType.ImportedPostcondition)
+      case AssumptionType.ImplicitPostcondition  => Some(AssumptionType.ImplicitPostcondition)
+      case AssumptionType.Internal => Some(AssumptionType.Internal)
+      case AssumptionType.Annotation | AssumptionType.Ghost => None
+      case _ => None
+    }).getOrElse(
+      if(isAbstractFunction) AssumptionType.ExplicitPostcondition else AssumptionType.ImplicitPostcondition
+    )
+  }
+}
+
+import viper.silver.dependencyAnalysis.AssumptionType.AssumptionType
+
+object DependencyType {
+  val SourceCode: DependencyType = make(AssumptionType.SourceCode)
+  val Explicit: DependencyType = make(AssumptionType.Explicit)
+  val ExplicitAssertion: DependencyType = DependencyType(AssumptionType.Internal, AssumptionType.Explicit)
+  val ExplicitAssumption: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Implicit)
+  val PathCondition: DependencyType = make(AssumptionType.PathCondition)
+  val Invariant: DependencyType = make(AssumptionType.LoopInvariant)
+  val Rewrite: DependencyType = make(AssumptionType.Rewrite)
+  val Internal: DependencyType = make(AssumptionType.Internal)
+  val Trigger: DependencyType = make(AssumptionType.Trigger)
+  val MethodCall: DependencyType = make(AssumptionType.MethodCall)
+  val Ghost: DependencyType = make(AssumptionType.Ghost)
+  val Annotation: DependencyType = make(AssumptionType.Annotation)
+  val Axiom: DependencyType = make(AssumptionType.DomainAxiom)
+
+  def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
+}
+
+case class DependencyType(assumptionType: AssumptionType, assertionType: AssumptionType)