Dependency Analysis#976
Conversation
…o keuscha/assumption_analysis # Conflicts: # src/main/scala/assumptionAnalysis/AssumptionAnalysisInterpreter.scala # src/main/scala/assumptionAnalysis/AssumptionAnalysisUserTool.scala
This reverts commit 97ec24f.
…o keuscha/assumption_analysis
# Conflicts: # src/main/scala/rules/Evaluator.scala # src/main/scala/rules/Executor.scala # src/main/scala/verifier/DefaultMainVerifier.scala
marcoeilers
left a comment
marcoeilers
left a comment
There was a problem hiding this comment.
So I had a rough look and left some nitpicky comments and some very general questions; let's discuss those at some point.
| def statistics(): Map[String, String] | ||
|
|
||
| var dependencyAnalyzer: DependencyAnalyzer | ||
| def initDependencyAnalyzer(member: Member, preambleNodes: Iterable[DependencyAnalysisNode]): Unit |
There was a problem hiding this comment.
I'm a bit surprised that this is in the Decider.
| def assume(assumptions: Iterable[(Term, Option[DebugExp])]): Unit | ||
| def assume(assumptions: InsertionOrderedSet[(Term, Option[DebugExp])], enforceAssumption: Boolean = false, isDefinition: Boolean = false): Unit | ||
| def assume(terms: Iterable[Term], debugExp: Option[DebugExp], enforceAssumption: Boolean): Unit | ||
| def registerChunk[CH <: GeneralChunk](buildChunk: Term => CH, perm: Term, analysisInfo: AnalysisInfo, isExhale: Boolean): CH |
There was a problem hiding this comment.
Should this be in the Decider? It doesn't feel very Decider-like.
| def isPathInfeasible: Boolean | ||
|
|
||
| def assume(t: Term, e: Option[ast.Exp], finalExp: Option[ast.Exp], analysisInfos: DependencyAnalysisInfos): Unit | ||
| def assume(t: Term, debugExp: Option[DebugExp], analysisInfos: DependencyAnalysisInfos): Unit |
There was a problem hiding this comment.
I'm wondering if we at some point should summarize the additional information for specific modes (debugging, dependency analysis, Joao has a branch where he is tracking query types #975) in some sort of info argument
| } | ||
|
|
||
| def registerDerivedChunk[CH <: GeneralChunk](sourceChunks: Set[Chunk], buildChunk: Term => CH, perm: Term, analysisInfo: AnalysisInfo, isExhale: Boolean, createLabel: Boolean=true): CH = { | ||
| if(!isDependencyAnalysisEnabled) |
There was a problem hiding this comment.
Wait so this does something even if the analysis is disabled?
|
|
||
| val labelNodeOpt = getOrCreateAnalysisLabelNode() | ||
|
|
||
| if(isExhale) |
There was a problem hiding this comment.
Silicon uses if ( (with a space) throughout
|
|
||
| val elseBranchVerificationTask: Verifier => VerificationResult = | ||
| if (executeElseBranch) { | ||
| if (executeElseBranch || Verifier.config.disableInfeasibilityChecks()) { |
There was a problem hiding this comment.
There is a variable skipPathFeasibilityCheck, maybe you could reuse that?
| (Q: (State, Heap, Verifier) => VerificationResult) | ||
| : VerificationResult = { | ||
|
|
||
| val analysisInfos = DependencyAnalysisInfos.DefaultDependencyAnalysisInfos.withSource(StringAnalysisSourceInfo("produce", ast.NoPosition)).withDependencyType(DependencyType.Internal) |
There was a problem hiding this comment.
That feels like it could be abbreviated :D
| : VerificationResult | ||
|
|
||
| def eval(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier) | ||
| def eval(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier, analysisInfos: DependencyAnalysisInfos) |
There was a problem hiding this comment.
Make sure this is consistent: Verifier used to be last everywhere, now AnalysisInfos are always after the Verifier (I'm not saying it's not consistent, I just didn't pay attention until now)
| } | ||
|
|
||
| def eval3(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier) | ||
| def eval3(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier, analysisInfos: DependencyAnalysisInfos) |
There was a problem hiding this comment.
So the analysisInfos couldn't possible be part of the State, could they?
| override def permMinus(perm: Term, permExp: Option[ast.Exp]): QuantifiedBasicChunk | ||
| override def permPlus(perm: Term, permExp: Option[ast.Exp]): QuantifiedBasicChunk | ||
| override def withSnapshotMap(snap: Term): QuantifiedBasicChunk | ||
| override protected def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]): QuantifiedBasicChunk |
There was a problem hiding this comment.
Aw, this was such a nice interface though :(
4 participants
Adds the dependency analysis for Silicon. It is disabled by default. When enabled, it analyzes all (direct and indirect) semantic dependencies in the program. The dependencies of a proof obligation indicate which specifications, statements, and assumptions were used to prove that obligation. The analysis builds a dependency graph, which can be exported or queried using the included CLI tool.