Introduce result class #26
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 30 commits
December 16, 2024 13:16
woosh
commented
Feb 20, 2025
| mkString(PrepareACSLPrinting(i))))) | ||
| } | ||
|
|
||
| // SSSOWO TODO: This doesn't seem to be used anywhere. Remove? |
There was a problem hiding this comment.
@zafer-esen Please advice on this.
woosh
commented
Feb 20, 2025
| (result: Either[Option[HornPreprocessor.Solution], hornconcurrency.VerificationLoop.Counterexample]) | ||
| : Result = { | ||
| import scala.collection.mutable.HashSet | ||
| // SSSOWO TODO: These constants should be defined in a single place. |
There was a problem hiding this comment.
@zafer-esen Please advice on how to go forward here.
woosh
commented
Feb 20, 2025
| subres: Seq[IExpression] | ||
| ): IExpression = { | ||
| t update subres match { | ||
| // SSSOWO TODO: Why does this need special handling? "emptyHeap" is |
There was a problem hiding this comment.
@zafer-esen Do you have any comment on this?
woosh
commented
Feb 20, 2025
| @@ -225,6 +226,9 @@ object ValSetReader { | |||
| extends CollectingVisitor[Unit, ValSet] | |||
| with ExpressionUtils { | |||
|
|
|||
| // SSSOWO: The de Bruijn version disregards disjunctions, | |||
There was a problem hiding this comment.
@zafer-esen To mee this looks really weird. The deBruijn version and the "invariant" version treat disjunctions differently. I actually think the deBruijn version is correct and that this implementation may cause some to the problems discussed in issue #15. But I think we need to have a closer look on what to do with disjunctions.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Summary
This PR introduces a
Resulttrait and related classes in order to introduce more structure into the post processing of the result from the horn solver. Therefore this PR makes substantial changes to these parts of the code, especially the post-processors related to translation of explicit heap into implicit form more suitable for ACSL contract generation.An ambition has been to introduce an interface between the translator (
CCReader) the solver and the result. A major change is a move away from the existingFunctionContextandACSLTranslator.FunctionContext. These classes kept too much information in a form tightly bound to the problem description for them to be practical to use.the
ResultConverter.hornSolverSolutionToResult()converts the solution from the horn solver and data fromCCReaderinto aSolutionresult (see below). As part of this conversion, the predicate variables representing program variables of some kind (globals, parameters, or locals in the case of loop invariants) are replaced with symbolic constants. However, in order to keep necessary meta data about them theIConstantis instantiated with a special type of constant,ProgVarProxy, derived fromConstantTerm. That way they can be separated from any other constant in the expressions.ProgVarProxydoes not rely on prefix or suffix information in the name in order to keep track of various attributes. Instead such informtion is kept in separate variables.Introduced concepts
Resulttrait. A container for a the result. There are case classes forEmpty,CounterExampleandSolution.Solutionis a set ofFunctionInvariants, one for each function we are inferring contracts for.FunctionInvariantis aPreCondition,PostCondition, andLoopInvariantsand some meta-data.PreCondition,PostCondition, andLoopInvariantsare cases extending theInvariantContexttrait.PreConditionandPostConditioneach contains anInvariant.Invariantis a container for anIFormulaand some meta-data for heap operations.HeapInfois a class that contains information regarding the heap and objects and functions related to that.ProgVarProxyis derived fromConstantTermand is used as a proxy for program variables inIFormulaandIExpressions.ProgVarProxycarries meta data about scope (global, parameter etc.) and context (pre-execution, post-execution). This is utilized in ACSL contract generation.Comments
ValSetReaderEqualitySwapperand friends. I can't see this being necessary anymore, since all free variables are replaced by symbolic constants before any processing is started. However, I noticed some differences in their implementation and have therefore kept both. This needs further consideration