[Question / Clarification] Overapproximation attribute does more than expected?

[martin-neuhaeusser]

We were assuming that Boogie functions labeled with the {:overapproximation "foo"} attribute could be used to recognize counter-examples that involve overapproximations of otherwise unsupported or expensive operations. In our current encoding, we use those attributes to define UFs that over-approximate cryptographic hash functions, bitwise operators, and the like.

But there seems to be a semantic issue with that attribute. Consider the following Boogie example:

function BitwiseAnd (_$_bitwise__1: int, _$_bitwise__2: int) returns (int);

procedure TestBitwiseAnd (x : int, y : int) returns (res:bool)
ensures res;
{
  var res1 : int;
  var res2 : int;
  res1 := BitwiseAnd(x, y);
  res2 := BitwiseAnd(x, y);
  res := res1 == res2;
  return;
}

procedure  ULTIMATE.start  ()
returns ()
{
  var b : bool;
  call b := TestBitwiseAnd(1, 1);
}

• If we run this through Automizer, it proves the postcondition on TestBitwiseAnd as expected: With an underlying UF, the result of BitwiseAnd(x,y) is non-deterministic, but fixed for given x and y. So equality must hold.
• If we now attach an attribute to BitwiseAnd and label it as being an over-approximation (we add {:overapproximation "BitwiseAnd"}), Automizer suddenly reports the post-condition to be violated. It now replaces the calls to the underlying UF with two independent fresh variables. So res1 and res2 are no longer constrained to hold the same value.

I suspect the relevant code is here where the application of the UF is replaced by a fresh variable.

Especially for cryptographic hash functions, the property of hash(param) = hash(param) is pretty important - probably more important than the actual value. And we'd like to make use of the nice feature of Ultimate reporting "unknown" instead of a violation in case an overapproximation attribute occurs in a counterexample.

Is that difference in the semantics between labeled and unlabeled Boogie functions really intentional, or is that a bug?

The examples are included here: test.zip

[Heizmann]

When I implemented this I intentionally choose to use to overapproximate as much a possible and to have not even congruence. We typically utilize the :overapproximation attribute for bitprecise functions or for operations on floating point numbers. My guesses were that in our applications,

• congruence will give us hardly more precision, and
• that the uninterpreted functions make the formulas in the resulting control-flow graph significantly more complicated.
  Definitely true is that we typically do not have uninterpreted functions and these are hence not tested very well.

[Heizmann]

I have to discuss with the other developers what we can do.

At a first glance, I would guess:

• We want to keep the maximal overapproximation for our applications.
• We could add a different attribute which overapproximates the result but makes sure that congruence still holds. (What would be good names to distinguish both?)
• There will be unexpected problems because we seldomly had uninterpreted functions (some of our algorithms may crash).
• Having congruence will cost some performance.

[martin-neuhaeusser]

@Heizmann Thanks for the clarification. We simply didn't expect that behavior, as the descriptions we found seemed to imply that the {:overapproximation} attribute is only used when analyzing a counter-example. So we didn't expect that annotation to influence the semantics of the Boogie function.

Before causing discussions and potentially introducing a different attribute, I'd propose that we experiment a bit with the existing two options:

1. Omit the {:overapproximation} attribute from our models and see how Ultimate performs with "real" uninterpreted functions. The good news is: We have been using them a little already (we didn't know those were uncharted territories) and they didn't cause any issues that we are aware of. But we'll watch this closely.
2. Add {:overapproximation} and see the ramifications of loosing the congruence property. Further, we should first assess if labeling counterexamples as "unknown" is actually helpful in our case: Given a counter-example that contains a call to an overapproximating Boogie function, can the analysis distinguish between it being caused by that overapproximation or by something completely independent?

[Heizmann]

Our current analysis cannot detect if a counterexample is only feasible because of the overapproximation. We are planning to implement such an analysis. Currently, my plan is to issue this as a project for students, so it will be ready only in a few month. (And it may turn out that my current idea for such an analysis will be too costly in practise.)

[Heizmann]

We discussed your issue today. The conclusion of our discussion was that the semantics that you expect is more natural. (In fact the current documentation also says that your expectation is justified.)
I will change the implementation such that congruence still holds for {:overapproximation}. I will introduce another keyword for our application where we overapproximate a function by nondeterministic values. I guess I will find time for that within in the next days.