Create new __CPROVER_havoc_slice & __CPROVER_havoc_from primitives

[jimgrundy]

We need the following new havoc primitives in CBMC:

void __CPROVER_havoc_slice(void *p, size_t s);
void __CPROVER_havoc_from (void *p);

(Reference implementation for havoc_object: symex_other.cpp)

The semantics of these primitives are described below.

__CPROVER_havoc_slice(void *p, size_t s)

Precondition:

s == 0 || __CPROVER_w_ok(p, s)

• If s is zero then no action is performed.
• If s is non-zero and p is a valid pointer to an object with at least s writable bytes starting at address p, that is if __CPROVER_w_ok(p, s), then the effect is to replace the s bytes starting at address p with fresh symbolic values.

__CPROVER_havoc_from(void *p)

Precondition:

p == NULL ||
     __CPROVER_OBJECT_SIZE(p) == __CPROVER_POINTER_OFFSET(p) ||
     __CPROVER_w_ok(p, __CPROVER_OBJECT_SIZE(p) - __CPROVER_POINTER_OFFSET(p))

• If p is NULL then no action is performed.
• Otherwise, equivalent to:
  __CPROVER_havoc_slice(p, __CPROVER_OBJECT_SIZE(p) - __CPROVER_POINTER_OFFSET(p))

[SaswatPadhi]

Only __CPROVER_havoc_slice should suffice. It might be desirable to minimize the number of new primitives we introduce.

Some reference material

• Implementation for havoc_object:

  cbmc/src/goto-symex/symex_other.cpp

  Line 244 in 56adbb2

  else if(statement==ID_havoc_object)

• Implementation for malloc:

  cbmc/src/ansi-c/library/stdlib.c

  Line 139 in 56adbb2

  inline void *malloc(__CPROVER_size_t malloc_size)

• List of builtin functions: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/cprover_builtin_headers.h

[kroening]

Use an assignment, with the appropriate byte_extract expression on the left hand side.

[kroening]

In the long term, I'd like to shrink symex_other until it's gone.

[kroening]

Another option is to assign a byte array of the appropriate size to a dereferencing expression that has the same type. This avoids the low-level expression.

[NlightNFotis]

Hello, is #6430 related to this issue? It appears to be fulfilling the requirements of at least the first of the primitives requested, or am I mistaken?

[jimgrundy]

It is related, and, actually we can build havoc_from using havoc_slice, so we will only need the the one primitive, which Remi's PR implements.