Introduce result class #26

woosh · 2025-02-20T13:52:19Z

Summary

This PR introduces a Result trait 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 existing FunctionContext and ACSLTranslator.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 from CCReader into a Solution result (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 the IConstant is instantiated with a special type of constant, ProgVarProxy, derived from ConstantTerm. That way they can be separated from any other constant in the expressions. ProgVarProxy does 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

Result trait. A container for a the result. There are case classes for Empty, CounterExample and Solution.
A Solution is a set of FunctionInvariants, one for each function we are inferring contracts for.
A FunctionInvariant is a PreCondition, PostCondition, and LoopInvariants and some meta-data.
PreCondition, PostCondition, and LoopInvariants are cases extending the InvariantContext trait.
PreCondition and PostCondition each contains an Invariant.
Invariant is a container for an IFormula and some meta-data for heap operations.
HeapInfo is a class that contains information regarding the heap and objects and functions related to that.
ProgVarProxy is derived from ConstantTerm and is used as a proxy for program variables in IFormula and IExpressions. ProgVarProxy carries meta data about scope (global, parameter etc.) and context (pre-execution, post-execution). This is utilized in ACSL contract generation.

Comments

There are still "DeBruijn" and "invariant" versions of ValSetReader EqualitySwapper and 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
I have moved a lot of the presentation and printing stuff into separate functions in an effort to emphasize the flow of the data. Presentation and calculations are still entangled in the counter-example part of the result processing. This needs further consideration.

woosh · 2025-02-20T13:56:52Z

src/tricera/postprocessor/ACSLLineariser.scala

+            mkString(PrepareACSLPrinting(i)))))
+  }
+
+  // SSSOWO TODO: This doesn't seem to be used anywhere. Remove?


@zafer-esen Please advice on this.

Sounds good, I think these are just remnants of the Princess' lineariser code that we started with.

woosh · 2025-02-20T13:58:27Z

src/tricera/postprocessor/ResultConverter.scala

+    (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.


@zafer-esen Please advice on how to go forward here.

Maybe collect internal parameters/constants like these in a new class under src/tricera/params/? We could also be able to eliminate these altogether, but that's probably work for another PR.

woosh · 2025-02-20T13:58:52Z

src/tricera/postprocessor/SafePointerExtractor.scala

+      subres: Seq[IExpression]
+  ): IExpression = {
+    t update subres match {
+      // SSSOWO TODO: Why does this need special handling? "emptyHeap" is


@zafer-esen Do you have any comment on this?

I don't think it needs special handling. We probably just missed this, relying on function names and string comparisons is not a good idea. I think we also do not need to use TheoryOfHeapFunApp in general here. That is useful when, given some IFunction, we do not have the heap theory (an object of the Heap class) and we want to get the heap theory if the function matches one of the theory functions.

Here we already have the heap theory in heapInfo, so why not simply do:
case IFunApp(f, _) if heapInfo.isEmptyHeapFun(f) and similarly for the other cases.

woosh · 2025-02-20T14:05:57Z

src/tricera/postprocessor/ValSet.scala

@@ -225,6 +226,9 @@ object ValSetReader {
      extends CollectingVisitor[Unit, ValSet]
      with ExpressionUtils {

+    // SSSOWO: The de Bruijn version disregards disjunctions,


@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.

Hmm, I think we should just add this as a note to #15 and do the closer look when resolving that.

zafer-esen

The PR looks like a great step in the right direction, thanks for contributing it!
I left a few minor comments and tried to address the questions. I think we can merge it after addressing those and you give the green light.

zafer-esen · 2025-03-02T21:35:27Z

src/tricera/postprocessor/SafePointerExtractor.scala

+      subres: Seq[IExpression]
+  ): IExpression = {
+    t update subres match {
+      // SSSOWO TODO: Why does this need special handling? "emptyHeap" is


I don't think it needs special handling. We probably just missed this, relying on function names and string comparisons is not a good idea. I think we also do not need to use TheoryOfHeapFunApp in general here. That is useful when, given some IFunction, we do not have the heap theory (an object of the Heap class) and we want to get the heap theory if the function matches one of the theory functions.

Here we already have the heap theory in heapInfo, so why not simply do:
case IFunApp(f, _) if heapInfo.isEmptyHeapFun(f) and similarly for the other cases.

zafer-esen · 2025-03-02T21:52:37Z

src/tricera/Main.scala

+    val result = verificationLoop.result
+      .tapIf(displaySolutionProlog)(printSolutionProlog(reader.PredPrintContext.predArgNames))
+      .tapIf(lazabs.GlobalParameters.get.displaySolutionSMT)(printSolutionSMT)
+      .through(hornSolverSolutionToResult(reader))


I really like the simplification here!
One question is, does the result conversion always run now? I think it would be good to have an option to toggle it.

zafer-esen · 2025-03-02T22:02:26Z

src/tricera/postprocessor/ACSLLineariser.scala

+            mkString(PrepareACSLPrinting(i)))))
+  }
+
+  // SSSOWO TODO: This doesn't seem to be used anywhere. Remove?


Sounds good, I think these are just remnants of the Princess' lineariser code that we started with.

zafer-esen · 2025-03-02T22:09:11Z

src/tricera/postprocessor/PostconditionSimplifier.scala

+import scala.collection.mutable.{Set, HashSet}
+import tricera.Util.printlnDebug
+
+object PostconditionSimplifier extends ResultProcessor {


I think this class can be made much more efficient (not related to this PR), but that's for another PR...

zafer-esen · 2025-03-02T22:12:48Z

src/tricera/postprocessor/ResultConverter.scala

+    (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.


Maybe collect internal parameters/constants like these in a new class under src/tricera/params/? We could also be able to eliminate these altogether, but that's probably work for another PR.

zafer-esen · 2025-03-02T22:21:53Z

src/tricera/postprocessor/ValSet.scala

@@ -225,6 +226,9 @@ object ValSetReader {
      extends CollectingVisitor[Unit, ValSet]
      with ExpressionUtils {

+    // SSSOWO: The de Bruijn version disregards disjunctions,


Hmm, I think we should just add this as a note to #15 and do the closer look when resolving that.

zafer-esen · 2025-03-02T22:22:47Z

tmp/example.c

Was the tmp directory added intentionally?

zafer-esen · 2025-03-02T22:36:45Z

src/tricera/Main.scala

+            .through(ADTExploder.apply)
+            .through(FunctionInvariantsFilter(i => !i.isSrcAnnotated)(_))
+            .through(r =>
+              if (solution.isHeapUsed) { r


Similar to the previous comment, I think there should be an option to use log, but not run the processors (at least until we fix the performance of PostconditionSimplifier). With displayACSL it makes sense to do the simplification by default though.

Ola Wingbrant added 30 commits December 16, 2024 13:16

Create Result classes

da2ce41

Rearrange post processing

9f39406

Backup commit for Christmas

d325496

PointerPropPProcessor uses HeapInfo instead of FunctionContext

72f1f93

EqualitySwapper uses HeapInfo

67adc69

Backup commit. Test crashes.

1aeff9e

Some temporary files

b5a2b7a

Add external constants in PostconditionSiplifier

e6ea648

Pointer and assignment processors almost working

6d1e0d3

Pointer and assignment processors working.

5f9a624

Begin TheoryOfHeapProcessor adaptation

385d323

TheoryOfHeapsProcessor working

a78ba94

Rewrite of ADTSimplifier

5daaf66

Test ADTSimplifier

fa75e64

ADTSimplifier works

8a5a4ff

ToVariableForm working

3ca76fa

Change to ProgVarProxy

564ba47

Refactor ACSLExpressionProcessor

814dced

ClauseRemover refactored

a6974a5

Refactor ACSLLineariser

3f32834

Correct loop invariant syntax

60bb4d4

Fix unit tests

5df98af

Fix whitespace diff in contracts

caf9da1

Fix ValSet bug in EqualitySwapper

39a5dff

Complete result processing.

152d43d

Cleanup of post processors

c9d69d0

Major cleanup

331477b

Backup commit when extracting safe pointers

30770d9

Factor out safe pointer extraction

ebf741b

Merge master branch

571847f

Ola Wingbrant added 2 commits February 20, 2025 12:47

Rename variables representing heapInfo

30aab80

Remove TODO

e747e25

woosh commented Feb 20, 2025

View reviewed changes

Ola Wingbrant added 2 commits February 20, 2025 15:11

Perform some cleanup

dd3e931

Restore project/build.properties

904d0e5

zafer-esen reviewed Mar 2, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Introduce result class #26

Introduce result class #26

woosh commented Feb 20, 2025 •

edited

Loading

woosh Feb 20, 2025

zafer-esen Mar 2, 2025

woosh Feb 20, 2025

zafer-esen Mar 2, 2025

woosh Feb 20, 2025

zafer-esen Mar 2, 2025

woosh Feb 20, 2025

zafer-esen Mar 2, 2025

zafer-esen left a comment

zafer-esen Mar 2, 2025

zafer-esen Mar 2, 2025

zafer-esen Mar 2, 2025

zafer-esen Mar 2, 2025

zafer-esen Mar 2, 2025

zafer-esen Mar 2, 2025

zafer-esen Mar 2, 2025

zafer-esen Mar 2, 2025

Introduce result class #26

Are you sure you want to change the base?

Introduce result class #26

Conversation

woosh commented Feb 20, 2025 • edited Loading

Summary

Introduced concepts

Comments

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zafer-esen left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

woosh commented Feb 20, 2025 •

edited

Loading