goto-instrument --apply-loop-contracts aborts on instrument_spec_assigns.h:286 invariant when the loop write set is inferred (regression 6.3.1 → 6.6.0)

[rcalvom]

goto-instrument --apply-loop-contracts aborts on instrument_spec_assigns.h:286 invariant when the loop write set is inferred (regression 6.3.1 → 6.6.0)

Summary

goto-instrument --apply-loop-contracts aborts with an internal invariant violation when instrumenting loops annotated only with __CPROVER_loop_invariant and __CPROVER_decreases. No __CPROVER_assigns is supplied anywhere, so the loop write set is inferred.

The same GOTO binary, with the same flags, is instrumented successfully by 6.3.1 and aborts under 6.6.0. The failure happens at instrumentation time, so affected programs produce no verification result at all, and the message carries no source location or loop identifier, so nothing in the output points at which annotation to change.

A GOTO binary that reproduces the abort is attached, along with the annotated and unannotated sources it was built from.

Environment

Failing	6.6.0 (cbmc-6.6.0), official ubuntu-22.04-cbmc-6.6.0-Linux.deb
Working	6.3.1 (cbmc-6.3.1)
OS	Ubuntu 22.04, x86-64; sources built with the matching goto-cc, -m32

Observed behavior

$ goto-instrument --apply-loop-contracts --loop-contracts-no-unwind \
      --slice-global-inits cfs_open3.goto out.goto

...
line 220 function read_header: no body for function 'xmem_pread'
line 214 function write_header: no body for function 'xmem_pwrite'
line 397 function collect_garbage: no body for function 'xmem_erase'
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-instrument/contracts/instrument_spec_assigns.h:286 function: update
Condition: source_location.is_not_nil()
Reason: Precondition
--- end invariant violation report ---
Aborted (core dumped)

Exit status 134 (SIGABRT). The full run, including the backtrace, is in the attached goto-instrument-6.6.0-abort.txt.

Expected behavior

Instrumentation completes and emits the transformed GOTO binary, as it does under 6.3.1 for the identical input and flags. If some construct genuinely cannot be instrumented, a diagnostic naming the offending loop and its source location would be far more actionable than an internal invariant violation.

Regression evidence

The same cfs_open3.goto, produced once by goto-cc 6.6.0, was passed through both instrumenters. Under 6.3.1 it completes with Writing GOTO program to '/tmp/out.goto' and exit 0; under 6.6.0 the same command aborts as above. The input is byte-identical in both runs, so the difference lies entirely in goto-instrument, and the attached binary can be fed directly to a bisection over the commits between the two releases without rebuilding anything.

What the annotations look like

Ordinary counter loops carrying only an invariant and a decreases clause:

for(i = 0; i < MAX_OPEN_FILES; i++)
  __CPROVER_loop_invariant(0 <= i)
  __CPROVER_loop_invariant(i <= MAX_OPEN_FILES)
  __CPROVER_decreases(MAX_OPEN_FILES - i)
{
  if(is_free(&files[i])) {
    continue;
  }
  read_header(&hdr, files[i].page);
  ...
}

Which annotations are needed to trigger it

The file has ten annotatable loops, and the trigger is a combination rather than any one of them.

No single annotated loop reproduces the abort: each of the ten, annotated on its own, instruments cleanly. Leave-one-out over the full set shows four loops are individually necessary, in that removing the contract from any one of them makes the abort go away. Those four alone are not sufficient either. A fifth annotated loop tips it over, and that fifth is interchangeable: any of four other loops works in its place. Two further loops do not work as the fifth, and both turn out to be unreachable from the entry function, so their annotations are dropped before instrumentation sees them.

The smallest reproducing configuration is therefore five contracted loops reachable from the entry point: four fixed, plus one drawn from four alternatives. This is not a count threshold, since nine annotated loops instrument fine as long as one of the four necessary loops is left out. That the trigger is a combination suggests state accumulated across loops during assigns instrumentation rather than a malformed clause.

I also tried to reduce this to a self-contained synthetic example and did not succeed: a program mirroring the structure — five reachable contracted loops across mutually calling functions, bodyless extern callees, struct locals written through them, continue and break paths, and a memcpy model built on __CPROVER_array_copy — instruments cleanly under 6.6.0. The attached binary is the reduced artifact, not a first attempt.

Workarounds tried

Attempt	Result
Downgrade goto-instrument to 6.3.1 for the instrumentation step	Works — same GOTO binary instruments cleanly
Supply an explicit __CPROVER_assigns on each annotated loop	Works — no abort
Remove --loop-contracts-no-unwind	No effect — still aborts
Add --unwind 2 to the instrumentation step	No effect — still aborts
Drop the contract from any one of the four necessary loops	Abort disappears

The second row is the diagnostically interesting one. With the identical set of loops and identical clauses, adding an explicit assigns clause makes the abort disappear. That places the fault in the inference of the loop write set rather than in the instrumentation of a user-supplied one, consistent with the assertion living in instrument_spec_assigns.h.

Attachments

File	What it is
cfs_open3.goto	The GOTO binary that reproduces. Feed it directly to goto-instrument.
source.original.c	The C source, unannotated.
source.annotated.c	The same file with the five loop contracts that trigger the abort; diff shows what was added.
goto-instrument-6.6.0-abort.txt	Full output of the failing run, including the backtrace.

Happy to run further reduction experiments against the attached binary on request.

cbmc-repro-instrument-assigns.zip