Unstable ACSL contract translation

[woosh]

This issue was discovered during the work with PR #13.

The translation into ACSL contracts is unstable. A number of (currently disabled) test cases for the theory-of-heaps contract translation either fails consistently or intermittently, either with "out of memory" or "timeout". (That they fail intermittently seems to be related to the fact that sets are involved, and that they don't guarantee a given order of iteration.) The problem seems to be rooted in the rewriting of the expression in order to figure out valid and separate pointers. Currently disabled tests are

incdec-3   (out of memory)
multadd-2  (out of memory)
multadd-3  (timeout)
truck-1    (out of memory) 

More specifically the problem seems to be in the so named swapMap used by EqualitySwapper (postprocessor/EqualitySwapper.scala). The EqualitySwapper tries to rewrite a given expression until a fix point is reached. However, the given swapMap does not guarentee that such a point is reached. The observed behavior is that sometimes the map contains substitutions like

A -> f(A)
...

which esults in "A => f(A) => f(f(A)) => ..." causing the "out of memory" condition. Sometimes the map contains substitutions on the form

f(A) -> f(B)
B -> A

causing the rewriting to alternate between two expressions, f(A) => f(B) => f(A) => f(B) => ... which ends in "timeout" (given that a timeout value has been set).

The swapMap is created from a so called valueSet by calling valueSet.ToExplicitFormMap. However, the valueSet looks strange at times. The following set has been collected when running the get-1.c test case, and using a quantified heap term. The valueSet is of type Set[Set[ITerm]], and :: is used as a separator between elements in the inner set.

{O_Int(1) :: read(_0, counterAddr(_0))}, 
{_6 :: _1}, 
{read(_0, _3) :: O_Int(_7)}, 
{getInt(read(_0, _3)) :: 0 :: _7 :: (-1 + getInt(read(_0, counterAddr(_0)))) :: _9 :: _2 :: getInt(read(_0, counterAddr(_0)))}, 
{_3 :: _8 :: counterAddr(_0) :: _4})

The strange thing is the fourth set {getInt(read(_0, _3)) :: 0 :: _7 :: (-1 + getInt(read(_0, counterAddr(_0)))) :: _9 :: _2 :: getInt(read(_0, counterAddr(_0)))}. Apparently it corresponds to the constant value 0 (the second element in the set). Therefore getInt(read(_0, counterAddr(_0)) (the last element) should also correspond to 0. However, since (-1 + getInt(read(_0, counterAddr(_0)))) is also part of the set, this means that -1 + 0 should also correspond to 0. Which seems plain wrong.