Bug: Ultimate C translation fails to annotate function contracts containing references to an array

[bahnwaerter]

The current C translation fails to annotate function contracts that contain references to a statically allocated array. The references can come from a function contract that is either manually specified for a function in the program or retrieved automatically from a witness for witness validation. This issue can be reproduced with Ultimate Automizer (0.3.0-dev-8447f03 with OpenJDK 21.0.8) using the following input:

//#include <stdio.h>
/*-----------------------------------------------------------------------------
 * START included content from stdio.h
 *---------------------------------------------------------------------------*/
struct __sbuf {
  unsigned char *_base;
  int _size;
};

typedef long _fpos_t;

struct __sFILE {
  unsigned char *_p;
  int _r;
  int _w;
  short _flags;
  short _file;
  struct __sbuf _bf;
  int _lbfsize;
  void *_cookie;
  /* ... */
};
typedef struct __sFILE __FILE;
extern __FILE __sf[3];

struct _glue {
  struct _glue *_next;
  int _niobs;
  __FILE *_iobs;
};
extern struct _glue __sglue;
/*-----------------------------------------------------------------------------
 * END included content from stdio.h
 *---------------------------------------------------------------------------*/

int x = 0;

//@ ensures ((__sf == \old(__sf)) && (__sglue == \old(__sglue)));
void func(int i)
{
  /* ... */
}

int main()
{
  int ret;
  while (ret) {
    func(x);
  }
  //@ assert (x >= 0);
  return ret;
}

The example program demonstrates a problem that occurs when validating witnesses. The function contract for function func is retrieved from a witness and uses the postcondition pattern of the form x == \old(x) to express that the function does not modify the variable or memory x. If a statically allocated array must be referenced here, Ultimate crashes with the following stack trace:

The Plugin de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator has thrown an exception:
java.lang.AssertionError: on-heap/off-heap bug: array has to be on-heap
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CHandler.moveArrayAndStructIdsOnHeap(CHandler.java:3058)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResultTransformer.switchToRValue(ExpressionResultTransformer.java:240)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResultTransformer.switchToRValueUnchecked(ExpressionResultTransformer.java:306)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.ACSLHandler.dispatchSwitch(ACSLHandler.java:414)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.ACSLHandler.visit(ACSLHandler.java:421)
	at de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.MainDispatcher.dispatch(MainDispatcher.java:305)

Following the ACSL standard, this should be possible and Ultimate should not crash.

[bahnwaerter]

This problem also raises another related question: whether the postcondition pattern of the form x == \old(x) in function contracts for witness validation really expresses what one might want to express here. Often, one might want to strictly state that a function does not change an array. However, the pattern only expresses that the pointer x to the array does not change, but says nothing about its contents (assuming I've understood the ACSL standard correctly). This would raise another issue in the generation of the postcondition and backtranslation.

[maul-esel]

Thanks for reporting the issue. There seem to indeed be multiple bugs at play here. Perhaps it would be best to open separate issues for them?

• First, the generated contract indeed intends to express that the array contents have not changed. This looks like an issue in the backtranslation from Boogie to C/ACSL. In particular, the offending equalities are probably generated by the backtranslation of contracts. On the Boogie level, the contract for func should have a modifies [] clause, stating that no variables are modified. As we do currently not support modifies-clauses for ACSL, we instead generate equalities x == \old(x) for all variables x.
  To fix this, Boogie2ACSL needs special handling for arrays (somewhere here).
  • On a related note, it would be interesting to see how we backtranslate contracts / invariants where the verification itself generated such an equality between arrays. Perhaps a similar bug exists in this case, or otherwise the solution could be adapted for the artificially-generated equalities.
• Second, the C/ACSL-2-Boogie translation should support such array equalities anyway, as they could be manually-annotated ACSL. Our translation currently performs a so-called "pre-run", which traverses the program and decides which objects must be modeled on the heap vs which can be translated to normal Boogie variables. Then, the second "main-run" performs the actual translation. I suspect the bug is due to the fact that the pre-run currently ignores ACSL completely, and thus misses the fact that __sf and __sglue occur in a pointer-equality check. Then, the main-run detects this and fails.
  To fix this, it may be necessary to let the pre-run also consider ACSL (but I am not sure if this can be easily done, or if it has other unintended consequences).