Dependency Analysis#976
Conversation
This reverts commit c769b79.
marcoeilers
left a comment
marcoeilers
left a comment
There was a problem hiding this comment.
Some comments here and there, otherwise LGTM
| trait Decider { | ||
| def functionDecls: Set[FunctionDecl] | ||
|
|
There was a problem hiding this comment.
So, we are making extensive changes to the decider so that we always propagate the analysisInfos data. Is it ever the case that this object is propagated through every call without changing it? If so, do we really need to make such extensive changes to the decider? Instead, couldn't we just either
(1) extend the decider with a single function analysisInfos and call it only where this info is relevant, or
(2) implement a subtrait of the decider for "dependency aware decider" that adds the necessary instrumentation to every decider by performing super calls?
There was a problem hiding this comment.
I don't see how I could get rid of the analysisInfo argument. While it might happen that several consecutive calls to assume/assert have the same analysisInfo, this does not hold in general. Usually, the info is specific to a single call to assume and assert, so passing it as an argument makes most sense to me. Let me know when you have an idea on how to improve it.
As a side note, I used to store the analysisInfos as a field in the decider and thus didn't have this extra argument (neither in the decider, nor in the evaluator, executor, producer, ...). However, I had to implement several hacks to keep the info consistent and as a result assumptions were associated with a wrong source/dependency type. That's why I switched to the current design at some point.
There was a problem hiding this comment.
why does this become an InsertionOrderedSet?
There was a problem hiding this comment.
Not sure, this was already there...
| if (enforceAssumption) assumptions | ||
| else assumptions filterNot isKnownToBeTrue | ||
|
|
||
| if (filteredTerms.isEmpty) return |
There was a problem hiding this comment.
return expressions have a somewhat funky semantics in scala due to non-local semantics. In general, I think it would be better to restrcutre the code such that the early return is not used
| val analyzeInfeasiblePaths: ScallopOption[Boolean] = opt[Boolean]("analyzeInfeasiblePaths", | ||
| descr = "Enable analysis of infeasible paths by making the verification step through all paths (even if provably infeasible)", | ||
| default = Some(false), | ||
| noshort = true | ||
| ) |
There was a problem hiding this comment.
hmm, I would probably set this as the default behaviour (it seems that we always use the two together, and disabling it leads to potentially unsound results for the dependency analysis). This means that we should probably rename this to "disableInfeasiblePaths". We should also explain why people might want to use it with a sentence of the kind "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."
| val enableDependencyAnalysis: ScallopOption[Boolean] = opt[Boolean]("enableDependencyAnalysis", | ||
| descr = "Enable the verification dependency analysis", | ||
| default = Some(false), | ||
| noshort = true | ||
| ) |
There was a problem hiding this comment.
are we always expected to provide a mode togehter with this flag? That makes this flag redundant. In that case, we could drop it and just rename the dependencyAnalysisMode to depAnalysis
There was a problem hiding this comment.
(I guess the point I am making in this comment and others is that the typical use of the dependency analysis should involve only one extra flag, not three like we currently have, which makes it hard to remember which combination of flags we need to pass)
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
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.