Theory of heaps translation (again)

[woosh]

This is a rebased version of PR #4 onto the current master. What follows is a restatement of that PR. In addition to that PR, a few regression tests have been added based on the results in OskarSoderberg/theory-of-heaps-translation-results. This PR closes #14.

Deviations on the test cases

The current results from the added regression tests does not match the results Oscar gives in his thesis. However, there have been quite a few changes to both TriCera and Eldarica since the time he presented his results. Some examples follows:

get-2: In his thesis Oscar mentions that the contract contains quantification expressions. But he still manages to get a contract. Now however, TriCera fails with

java.lang.Exception: Predicate generation failed
(error "Predicate generation failed")
Other Error: Predicate generation failed

Looking further in debug printouts it seems the problem is related to predicates and quantified expressions.

incdec-3: Oscar mentions problems around this case as well. Now TriCera simply stops with

(error "Out of Memory")
Out of Memory

max-1: The requires clause was

requires x == a && y == b && \separated(x, y) && \valid(x) && \valid(y);

but now what gets generated is

requires x == a && y == b;

Other tests show similar deviations.
These deviations have now been taken care of.

Question

How do we go forward with this?

Theory of Heaps Translation PR Comments

The theory of heaps translation consists in 19 changed/added files. 16 of these are in the src/tricera/postprocessor folder, and the other 3 changes are in the CCReader.scala, ACSLTranslator.scala and Main.scala.

Before merging, it would be great to do the following two fixes:

1. Fix the bug I reported in ADTExploder (my temporary fix can be seen here)

2. Make it possible to choose an arbitrary starting heap (perhaps there is already an option?).

Below follows a short summary of the changes for each file.

Main.scala:

Apply the new processors to the solution.

ACSLTranslator.scala, CCReader.scala

Add wrapperSort, getterSort, getStructMap to AnnotationContext and make changes accordingly in CCReader.scala.

This was done to be able to easily check whether an IFunction is a wrapper or a getter (see ContractProcessorUtils.scala).

Postprocessors

Note the following name correspondences between the report and the implementation:

• PostconditionSimplifier -> PostconditionSimplifier
• PrinterPropExtractor -> PointerPropProcessor
• AssignmentExtractor -> AssignmentProcessor
• TOHProcessor -> TheoryOfHeapProcessor
• ADTProcessor -> ADTSimplifier and ADTExploder
• ToVarForm -> ToVariableForm
• ACSLProcessor -> ACSLExpressionProcessor
• ClauseRemover -> ClauseRemover

Other than files directly implementing processor steps, the following files were added:

• ACSLFunctions.scala
• ContractConditionTools.scala
• ContractConditionType.scala
• ContractProcessorUtils.scala
• EqualitySwapper.scala
• HeapRepresentation.scala
• ValSet.scala

ACSLFunctions.scala

Defines heap-related ACSL functions and helper functions for creating them.

ContractConditionTools.scala

Various tools used for processing contract conditions.

ContractConditionType.scala

Definition of the contract condition types (precondition, postcondition and a union of the two).

ContractProcessorUtils.scala

Defines classes for easily accessing all information regarding a contract condition and it's terms. Also defines traits for contract processors.

EqualitySwapper.scala

Defines objects and classes for converting expressions to equivalent representations. The ToVariableForm processor is defined here.

HeapRepresentation.scala

Defines everything related to a "heap simulator" which can translate TOH expressions to a map containing relevant information.

ValSet.scala

Defines objects and classes for treating equivalences. A Val represents a Set[ITerm] where the ITerms are equivalent. A ValSet is a Set[Vals], allowing to add new equivalences. ValSet keeps the number of Vals as low as possible, merging any two Vals whenever they turn out to be equal.

[zafer-esen]

Thanks for this PR and the detailed documentation both @OskarSoderberg and @woosh !

get-2.c
The predicate generation error can happen when the theory of heaps is present, this is something we are currently working on improving.

The following version, although it contains undefined behavior, leads to a solution:

int get(int* p) {
    if (*p <= 0) {
        return 0;
    } else {
        *p = *p - 1;
        return 1 + get(p);
    }
}

void main()
{
  //Non-det assignment of variables
  int *n, n_init, r1;
  assume((n_init > 0));

  n = (int*) malloc(sizeof(int));
  // *n = n_init;
  assume(*n == n_init);
  r1 = get(n);

  assert(((r1 >= n_init) && (r1 <= (n_init * n_init))));
}

incdec-3.c
Maybe there are some opportunities to optimize the solution post-processsors, currently they seems to take a long time even for relatively simple solutions. The error might be related.

max-1: The requires clause was
requires x == a && y == b && \separated(x, y) && \valid(x) && \valid(y);
but now what gets generated is
requires x == a && y == b;

I think this one is a bug; but before coming to that, it is also good to know that TriCera now does not check for memory safety properties by default since PR #10. To check the same properties prior to this PR, the options -reachsafety -valid-deref -valid-free can be passed.

Having said that, the issue in this benchmark does not seem to be related to that. I couldn't spend enough time to fully debug this yet, but the visitor here is likely the culprit. I think it operated on some assumptions which are no longer there. In this benchmark the solution contains two existential quantifiers, and after this visitor the formula is no longer well-formed -- the quantifiers are still there and the De Brujin indexes of the arguments are shifted. I am not yet sure how to fix this, but it seems to me that without at least the valid predicates the precondition becomes too weak.

I think we can land the PR without fixing above bug after a few changes, let me know if you want to hold on until fixing the bug.

[zafer-esen]

@woosh Please let me know when you want to land this, from my side it is good to go after only disabling the translation of solutions with -log. The postcondition simplification can be optimized but this is probably not very urgent.

[woosh]

Maybe we should hold this PR just for a little. I have been looking into the "missing" \separated(...) and \valid(...) terms in the inferred contract for e.g. max-1.c. Adding the options -reachsafety -valid-deref -valid-free didn't make any difference. However, Oscar had a branch in his repository called theory-of-heaps-translation-thesis-version containing a few changes, mainly to the ADTExploder.

I have rebased those changes on the branch for this PR, (see patch). To be honest I have not fully grasped why, but these changes made the terms appear in the contracts again.

However, while working with that I ran into another issue. I get inconsistent results for e.g. get-1.c. Occasionally I get a contract for this case, but sometimes I get Out of memory and most often it just times out. Working together with @gustavung we managed to narrow down the problem to a fix-point iteration in EqualitySwapper when processing the post condition. There it ends up in a situation where it is alternating between two different expressions.

We can still land this PR and make a new one for the iterator fix. But I'm not 100% sure that the regression tests for this PR will always work at the moment because of the above mentioned inconsistent results.

Question: If we merge this PR, should I first push the fix for the \sepratated(...) and \valid(...) terms.

[zafer-esen]

I have rebased those changes on the branch for this PR, (see patch). To be honest I have not fully grasped why, but these changes made the terms appear in the contracts again.

Great! I think the fix is due to the line replacing emptyHeap with a fresh heap term at program entry. This adds a quantified heap term to the solutions, replacing the emptyHeap as the initial term, which the methods here seem to depend on to build a mapping.

I think there are two issues here, which I believe are separate:

• the building of the heap map used for inferring valid and separated predicates
• starting the program with a fresh heap term rather than the empty heap.

The former not working with an empty starting heap seems like a bug to me, it should be possible to build this map regardless of the initial value of the heap.

Starting the program with a fresh heap term makes sense when the entry point to the program is not main, but otherwise starting with an emptyHeap seems like the correct semantics to me? @pruemmer, any thoughts on this? If that makes sense, we could use a fresh heap term (as in the patch you linked) when an entry other than main is explicitly specified using the CLI, and otherwise default to the emptyHeap.

This would break the building of the heap map again in max-1.c and other examples . We could also add an option to switch the starting heap mainly so that this functionality works for now, but ideally the heap map building should work in both cases.

[zafer-esen]

However, while working with that I ran into another issue. I get inconsistent results for e.g. get-1.c. Occasionally I get a contract for this case, but sometimes I get Out of memory and most often it just times out. Working together with @gustavung we managed to narrow down the problem to a fix-point iteration in EqualitySwapper when processing the post condition. There it ends up in a situation where it is alternating between two different expressions.

I think the postcondition simplifier can be optimized, but this requires some more thought and work to get right. Since this is an issue only with -acsl (after we disable this functionality when using -log), I propose leaving that work for another PR, and disabling the unstable regression tests for now. Creating an issue for the unstable tests sounds good to me!

[woosh]

@zafer-esen I think this PR is ready for merge. The commit ed405fe is a fix for using an empty heap instead of a quantified heap term when doing contract translation.

Trying to use a quantified heap term breaks other regression test suits, like horn-hcc-heap, horn-hcc-array, acsl-contracts, uninterpreted-predicates, with errors

java.lang.Exception: Predicate generation failed
(error "Predicate generation failed")
Other Error: Predicate generation failed

(error "assertion failed")
java.lang.AssertionError: assertion failed
Other Error: assertion failed

I think being able to start with an arbitrary entry function and a fresh heap term would be a nice extension, but I consider that future work.

I have also disabled test cases in toh-contract-translation/runtests that are currently known to fail. These are

get-2      (predicate generation failure)
incdec-3   (out of memory)
multadd-2  (out of memory)
multadd-3  (timeout)
truck-1    (out of memory)

I have created separate issues describing the reasons for disabling them, please see #15, #16, #17

[woosh]

Thanks for a quick merge 😃 Would it be possible to create a new release at this point?

[zafer-esen]

Sure, I am trying to fit in a few more features and fix a few more bugs, will do a release this week!