Dependency Analysis

src/main/scala/Config.scala

@@ -6,16 +6,17 @@
 
 package viper.silicon
 
-import java.nio.file.{Files, Path, Paths}
-import scala.collection.immutable.ArraySeq
-import scala.util.matching.Regex
-import scala.util.Properties._
 import org.rogach.scallop._
 import viper.silicon.Config.JoinMode.JoinMode
 import viper.silicon.Config.StateConsolidationMode.StateConsolidationMode
 import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverAPI, Z3ProverStdIO}
 import viper.silver.frontend.SilFrontendConfig
 
+import java.nio.file.{Files, Path, Paths}
+import scala.collection.immutable.ArraySeq
+import scala.util.Properties._
+import scala.util.matching.Regex
+
 class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   import Config._
 
@@ -691,6 +692,78 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val startDebuggerAutomatically: ScallopOption[Boolean] = opt[Boolean]("startDebuggerAutomatically",
+    descr = "Starts the debugging mode automatically after verification completes",
+    default = Some(false),
+    noshort = true
+  )
+
+  val enableDependencyAnalysis: ScallopOption[Boolean] = opt[Boolean]("enableDependencyAnalysis",
+    descr = "Enable dependency analysis mode",
+    default = Some(false),
+    noshort = true
+  )
+
+  val enableDependencyAnalysisDebugging: ScallopOption[Boolean] = opt[Boolean]("enableDependencyAnalysisDebugging",
+    descr = "Enable debugging for dependency analysis mode",
+    default = Some(false),
+    noshort = true
+  )
+
+  val disableInfeasibilityChecks: ScallopOption[Boolean] = opt[Boolean]("disableInfeasibilityChecks",
+    descr = "Disable infeasibility checks. As a consequence all paths will be explored to the end. (Potentially) huge performance overhead!",
+    default = Some(false),
+    noshort = true
+  )
+
+  val dependencyAnalysisExportPath: ScallopOption[String] = opt[String]("dependencyAnalysisExportPath",
+    descr = "Path to the directory where the dependency analysis graphs should be exported to",
+    default = None,
+    noshort = true
+  )
+
+  val startDependencyAnalysisTool: ScallopOption[Boolean] = opt[Boolean]("startDependencyAnalysisTool",
+    descr = "Starts the dependency analysis command line tool after verification",
+    default = Some(false),
+    noshort = true
+  )
+
+	val executeDependencyAnalysisTests: ScallopOption[Boolean] = opt[Boolean]("executeDependencyAnalysisTests",
+		descr = "Automatically executes dependency analysis tests",
+		default = Some(false),
+		noshort = true
+	)
+
+  val enableUnsatCores: ScallopOption[Boolean] = opt[Boolean]("enableUnsatCores",
+    descr = "Enables UNSAT cores",
+    default = Some(false),
+    noshort = true
+  )
+
+  val pruneLines: ScallopOption[List[Int]] = opt[List[Int]]("pruneLines",
+    descr = "Line numbers to prune the program with respect to. Part of the dependency analysis tool.",
+    default = None,
+    noshort = true
+  )
+
+  val pruneExportFileName: ScallopOption[String] = opt[String]("pruneExportFileName",
+    descr = "Export file name for the pruned program (used with --pruneLines)",
+    default = Some("prunedExport.vpr"),
+    noshort = true
+  )
+
+  val computeVerificationProgress: ScallopOption[Boolean] = opt[Boolean]("computeVerificationProgress",
+    descr = "Computes verification progress of the program",
+    default = Some(false),
+    noshort = true
+  )
+
+  val computeVerificationProgressFileName: ScallopOption[String] = opt[String]("computeVerificationProgressFileName",
+    descr = "Export file name for the verification progress output (used with --computeVerificationProgress)",
+    default = Some("progressExport.vpr"),
+    noshort = true
+  )
+
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {
@@ -738,6 +811,66 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   validateFileOpt(multisetAxiomatizationFile)
   validateFileOpt(sequenceAxiomatizationFile)
 
+  validateOpt(enableDependencyAnalysis, parallelizeBranches) {
+    case (Some(false), _) => Right(())
+    case (_, Some(false)) => Right(())
+    case (Some(true), Some(true)) =>
+      Left(s"Option ${enableDependencyAnalysis.name} is not supported in combination with ${parallelizeBranches.name}")
+    case other =>
+      sys.error(s"Unexpected combination: $other")
+  }
+
+  validateOpt(rawProverArgs, enableDependencyAnalysis) {
+    case (_, Some(false)) => Right(())
+    case (Some(args), Some(true)) if args.contains("proof=true") && args.contains("unsat-core=true") => Right(())
+    case (_, _) =>
+      Left(s"Option ${enableDependencyAnalysis.name} requires ${rawProverArgs.name} with \"proof=true unsat-core=true\"")
+  }
+
+  validateOpt(dependencyAnalysisExportPath, enableDependencyAnalysis) {
+    case (None, _) => Right(())
+    case (Some(_), Some(true)) => Right(())
+    case (Some(_), Some(false)) =>
+      Left(s"Option ${dependencyAnalysisExportPath.name} requires option ${enableDependencyAnalysis.name}")
+  }
+
+	validateOpt(executeDependencyAnalysisTests, enableDependencyAnalysis) {
+		case (Some(false), _) => Right(())
+		case (_, Some(true)) => Right(())
+		case (_, _) =>
+			Left(s"Option ${executeDependencyAnalysisTests.name} requires option ${enableDependencyAnalysis.name}")
+	}
+
+  validateOpt(startDependencyAnalysisTool, enableDependencyAnalysis) {
+    case (Some(false), _) => Right(())
+    case (_, Some(true)) => Right(())
+    case (_, _) =>
+      Left(s"Option ${startDependencyAnalysisTool.name} requires option ${enableDependencyAnalysis.name}")
+  }
+
+  validateOpt(pruneLines, enableDependencyAnalysis) {
+    case (None, _) => Right(())
+    case (Some(_), Some(true)) => Right(())
+    case (Some(_), _) =>
+      Left(s"Option ${pruneLines.name} requires option ${enableDependencyAnalysis.name}")
+  }
+
+  validateOpt(computeVerificationProgress, enableDependencyAnalysis) {
+    case (Some(false), _) => Right(())
+    case (_, Some(true)) => Right(())
+    case (_, _) =>
+      Left(s"Option ${computeVerificationProgress.name} requires option ${enableDependencyAnalysis.name}")
+  }
+
+  validateOpt(startDebuggerAutomatically, enableDebugging) {
+    case (Some(false), _) => Right(())
+    case (Some(true), Some(true)) => Right(())
+    case (Some(true), Some(false)) =>
+      Left(s"Option ${startDebuggerAutomatically.name} requires option ${enableDebugging.name}")
+    case other =>
+      sys.error(s"Unexpected combination: $other")
+  }
+
   /* Finalise configuration */
 
   verify()

src/main/scala/Silicon.scala

@@ -6,27 +6,26 @@
 
 package viper.silicon
 
-import java.text.SimpleDateFormat
-import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException}
-import scala.collection.immutable.ArraySeq
-import scala.util.{Left, Right}
 import ch.qos.logback.classic.{Level, Logger}
 import com.typesafe.scalalogging.LazyLogging
 import org.slf4j.LoggerFactory
-import viper.silver.ast
-import viper.silver.frontend.{DefaultStates, MinimalViperFrontendAPI, SilFrontend, ViperFrontendAPI}
-import viper.silver.reporter._
-import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
+import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO}
 import viper.silicon.interfaces.Failure
 import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger}
 import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
 import viper.silicon.verifier.DefaultMainVerifier
-import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO}
+import viper.silver.ast
 import viper.silver.cfg.silver.SilverCfg
+import viper.silver.frontend.{DefaultStates, MinimalViperFrontendAPI, SilFrontend, ViperFrontendAPI}
 import viper.silver.logger.ViperStdOutLogger
-import viper.silver.utility.{FileProgramSubmitter}
+import viper.silver.reporter._
+import viper.silver.utility.FileProgramSubmitter
+import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 
-import scala.util.chaining._
+import java.text.SimpleDateFormat
+import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException}
+import scala.collection.immutable.ArraySeq
+import scala.util.{Left, Right}
 
 object Silicon {
   val name = BuildInfo.projectName

src/main/scala/debugger/DebugParser.scala

@@ -2,6 +2,7 @@ package viper.silicon.debugger
 
 import fastparse._
 import viper.silver.ast._
+import viper.silver.dependencyAnalysis.DependencyType
 import viper.silver.parser._
 
 import scala.collection.mutable
@@ -36,7 +37,7 @@ class DebugParser extends FastParser {
 
 class DebugTranslator(p: PProgram, override val members: mutable.Map[String, Node]) extends Translator(p) {
 
-  override protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = {
+  override protected def expInternal(pexp: PExp, pos: PExp, info: Info, dependencyType: Option[DependencyType]): Exp = {
     pexp match {
       case pviu@PVersionedIdnUseExp(_, _, _) =>
         pexp.typ match {
@@ -45,7 +46,7 @@ class DebugTranslator(p: PProgram, override val members: mutable.Map[String, Nod
         }
       case PDebugLabelledOldExp(_, lbl, e) =>
         DebugLabelledOld(exp(e), lbl.versionedName)(pos, info)
-      case _ => super.expInternal(pexp, pos, info)
+      case _ => super.expInternal(pexp, pos, info, dependencyType)
     }
   }
 

src/main/scala/debugger/SiliconDebugger.scala

@@ -2,6 +2,7 @@ package viper.silicon.debugger
 
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.decider.{Cvc5ProverStdIO, RecordedPathConditions, Z3ProverStdIO}
+import viper.silicon.dependencyAnalysis.DependencyAnalysisInfos
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, Success, VerificationResult}
 import viper.silicon.resources.{FieldID, PredicateID}
@@ -270,7 +271,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
   }
 
   private def initVerifier(obl: ProofObligation, proverName: String, userArgsString: Option[String]): ProofObligation = {
-    val v = new WorkerVerifier(this.mainVerifier, obl.v.uniqueId, NoopReporter, false)
+    val v = new WorkerVerifier(this.mainVerifier, "debugger_01", NoopReporter, false)
     counter += 1
     v.start()
     v.decider.createProver(proverName, userArgsString)
@@ -430,7 +431,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
       var resE: ast.Exp = null
       var resV: Verifier = null
       val pve: PartialVerificationError = PartialVerificationError(r => ContractNotWellformed(assertionE, r))
-      val verificationResult = evaluator.eval3(obl.s, assertionE, pve, obl.v)((_, t, newE, newV) => {
+      val verificationResult = evaluator.eval3(obl.s, assertionE, pve, obl.v, DependencyAnalysisInfos.DefaultDependencyAnalysisInfos)((_, t, newE, newV) => {
         resT = t
         resE = newE.get
         resV = newV
@@ -497,7 +498,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     var evalPcs: RecordedPathConditions = null
     val pve: PartialVerificationError = PartialVerificationError(r => ContractNotWellformed(e, r))
     val beforeEval = v.decider.setPathConditionMark()
-    val verificationResult = evaluator.eval3(obl.s, e, pve, v)((newS, t, newE, newV) => {
+    val verificationResult = evaluator.eval3(obl.s, e, pve, v, DependencyAnalysisInfos.DefaultDependencyAnalysisInfos)((newS, t, newE, newV) => {
       resS = newS
       resT = t
       resE = newE.get

src/main/scala/decider/CVC5ProverStdIO.scala

@@ -6,12 +6,13 @@
 
 package viper.silicon.decider
 
-import java.nio.file.{Path, Paths}
+import viper.silicon.common.config.Version
 import viper.silicon.state.IdentifierFactory
 import viper.silicon.verifier.Verifier
-import viper.silver.verifier.{DefaultDependency => SilDefaultDependency}
 import viper.silver.reporter.Reporter
-import viper.silicon.common.config.Version
+import viper.silver.verifier.{DefaultDependency => SilDefaultDependency}
+
+import java.nio.file.{Path, Paths}
 
 object Cvc5ProverStdIO {
   val name = "cvc5"