Soundness bug with array havocing in loop contracts

[SaswatPadhi]

CBMC version: 99f1a2e

Operating system: 10.15.7

Test case:

#include <assert.h>
#include <stdlib.h>

#define SIZE 8

void main()
{
  char *data = malloc(SIZE);
  data[5] = 0;

  for (unsigned i = 0; i < SIZE; i++)
    __CPROVER_loop_invariant(i <= SIZE)
  {
    data[i] = 1;
  }

  assert(data[5] == 0);
}

Exact command line resulting in the issue:

$ goto-cc test.c -o test.1.gb
$ goto-instrument --enforce-all-contracts test.1.gb test.2.gb
$ cbmc test.2.gb

What behaviour did you expect:

Clearly the verification should fail because we are initializing all elements of data to 1.

What happened instead:

CBMC reports that verification was successful!

Running cbmc test.c unwinds the loop and ignored the loop invariant contract. This results in a verification failure, as expected.

Additional Information:

I think, the bug is in the build_havoc_code routine:

cbmc/src/goto-instrument/loop_utils.cpp

Lines 38 to 56 in 99f1a2e

	void build_havoc_code(
	const goto_programt::targett loop_head,
	const modifiest &modifies,
	goto_programt &dest)
	{
	for(modifiest::const_iterator
	m_it=modifies.begin();
	m_it!=modifies.end();
	m_it++)
	{
	exprt lhs=*m_it;
	side_effect_expr_nondett rhs(lhs.type(), loop_head->source_location);
	goto_programt::targett t = dest.add(goto_programt::make_assignment(
	code_assignt(std::move(lhs), std::move(rhs)),
	loop_head->source_location));
	t->code_nonconst().add_source_location() = loop_head->source_location;
	}
	}

It simply havocs a pointer without considering its size. So for arrays, it only havocs the first element.

[SaswatPadhi]

cc: @feliperodri

The same issue might appear with __CPROVER_assigns contracts on functions as well.