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,48 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val enableUnsatCores: ScallopOption[Boolean] = opt[Boolean]("enableUnsatCores",
+    descr = "Compute UNSAT cores. Useful for evaluating the overhead of this feature in an isolated manner.",
+    default = Some(false),
+    noshort = true
+  )
+
+  /*
+   * For benchmarking and testing purposes one can also use the command `computeGraphOnly` that enables dep analysis
+   * and computes the final dependency graph but does not run any graph queries.
+   */
+  val dependencyAnalysis: ScallopOption[String] = opt[String]("dependencyAnalysis",
+    descr = "Enable dependency analysis and set the commands (separated by ;) to be executed after verification. The available commands are `interactive` " +
+      "and all commands supported by the interactive CLI tool",
+    default = None,
+    noshort = true
+  )
+
+  val disableDependencyAnalysisJoinPrecisionOpt: ScallopOption[Boolean] = opt[Boolean]("disableDependencyAnalysisJoinPrecisionOpt",
+    descr = "Use a less precise but faster algorithm for computing dependencies.",
+    default = Some(false),
+    noshort = true
+  )
+
+  val enableDependencyAnalysisDebugging: ScallopOption[Boolean] = opt[Boolean]("enableDependencyAnalysisDebugging",
+    descr = "Enable debugging for the verification dependency analysis",
+    default = Some(false),
+    noshort = true
+  )
+
+  private val disableInfeasiblePaths: ScallopOption[Boolean] = opt[Boolean]("disableInfeasiblePaths",
+    descr = "This flag makes the dependency analysis faster by skipping the analysis of dead paths, but it may produce unsound results " +
+      "where the dependencies of a proof obligation in an infeasible branch are not completely listed",
+    default = Some(false),
+    noshort = true
+  )
+
+  /**
+   * If true, verification always steps through all paths; even if provably infeasible. Might have a huge performance penalty!
+   * Note: analyzeInfeasiblePaths might be used independent of the dependency analysis but this has not been tested yet.
+   */
+  lazy val analyzeInfeasiblePaths: Boolean = dependencyAnalysis.isDefined && !disableInfeasiblePaths()
+
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {
@@ -738,6 +781,31 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   validateFileOpt(multisetAxiomatizationFile)
   validateFileOpt(sequenceAxiomatizationFile)
 
+  validateOpt(dependencyAnalysis, parallelizeBranches) {
+    case (dam, Some(true)) if dam.isDefined =>
+      Left(s"Option ${dependencyAnalysis.name} is not supported in combination with ${parallelizeBranches.name}")
+    case (_, Some(false)) => Right(())
+  }
+
+  validateOpt(rawProverArgs, dependencyAnalysis) {
+    case (_, dam) if dam.isEmpty => Right(())
+    case (Some(args), dam) if dam.isDefined && args.toLowerCase.contains("proof=true") && args.toLowerCase.contains("unsat-core=true") => Right(())
+    case (_, _) =>
+      Left(s"Option ${dependencyAnalysis.name} requires ${rawProverArgs.name} with \"proof=true unsat-core=true\"")
+  }
+
+  validateOpt(prover, dependencyAnalysis) {
+    case (p, dam) if !p.contains(Z3ProverStdIO.name) && dam.isDefined =>
+      Left(s"Dependency analysis is only supported with ${Z3ProverStdIO.name}")
+    case _ => Right(())
+  }
+
+  validateOpt(disableInfeasiblePaths, dependencyAnalysis) {
+    case (Some(true), dam) if dam.isEmpty =>
+      Left(s"The ${disableInfeasiblePaths.name} is currently only supported in combination with ${dependencyAnalysis.name}")
+    case _ => Right(())
+  }
+
   /* 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.silicon.verifier.{DefaultMainVerifier, DependencyAnalysisAwareMainVerifier}
+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
@@ -136,7 +135,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
 
     setLogLevelsFromConfig()
 
-    verifier = new DefaultMainVerifier(config, reporter, symbExLog)
+    verifier = if (config.dependencyAnalysis.isDefined) new DependencyAnalysisAwareMainVerifier(config, reporter, symbExLog) else new DefaultMainVerifier(config, reporter, symbExLog)
     verifier.start()
   }
 

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,13 +2,13 @@ package viper.silicon.debugger
 
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.decider.{Cvc5ProverStdIO, RecordedPathConditions, Z3ProverStdIO}
-import viper.silicon.interfaces.state.Chunk
+import viper.silicon.dependencyAnalysis.DependencyAnalysisInfos
 import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, Success, VerificationResult}
 import viper.silicon.resources.{FieldID, PredicateID}
 import viper.silicon.rules.evaluator
-import viper.silicon.state.Heap
+import viper.silicon.state.chunks._
 import viper.silicon.state.terms.{Term, True}
-import viper.silicon.state.{BasicChunk, IdentifierFactory, MagicWandChunk, QuantifiedFieldChunk, QuantifiedMagicWandChunk, QuantifiedPredicateChunk, State}
+import viper.silicon.state.{Heap, IdentifierFactory, State}
 import viper.silicon.utils.ast.simplifyVariableName
 import viper.silicon.verifier.{MainVerifier, Verifier, WorkerVerifier}
 import viper.silver.ast
@@ -430,7 +430,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.DefaultInfos.withEnabled(false))((_, t, newE, newV) => {
         resT = t
         resE = newE.get
         resV = newV
@@ -497,7 +497,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, v.decider.defaultAnalysisInfos)((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"