Verification friendly memory resizing operation support

[chinmaydd]

Hello all,

We are looking to implement a verification-friendly stubs for modules in the Rust standard library for rmc. Specifically, the first module we are targeting is Vector.

Currently, the way we envision implementing support for dynamic data structures such as the vector is to allocate memory and then resizing the allocation per requirement. For instance, below is the piece of code we are using to model the Vector in C right now:

typedef struct {
  uint32_t* mem;
  size_t len;
  size_t capacity;
} vec;
 
void grow(vec* v) {
  // Expensive operation 
  uint32_t* new_mem = (uint32_t *) realloc(v->mem, v->capacity * 2 * sizeof(uint32_t));
  v->mem = new_mem;
  v->capacity = v->capacity * 2;
}
 
void push(vec* v, uint32_t elem) {
  if (v->len == v->capacity) {
    grow(v);
  }
 
  v->mem[v->len] = elem;
  v->len += 1;
}

The grow() operation here is fairly expensive as it allocates a new chunk of memory and copies over all the elements of the previous allocation creating complex solver queries.

We could avoid this (while remaining sound) by treating memory allocations as regions of memory which can be tracked using their start and end pointers. For instance, a "verification-friendly" realloc would only change the end pointer being tracked for this specific memory region.

Ofcourse, this might not be true for an generic allocator which chooses to model memory differently but for abstractions which dont care about the underlying allocator, we believe that such an optimization would lead to significant benefits when considering dynamically resizeable data structures.

I had a talk with Michael Tautschnig about this in his office hours with the RMC dev team and he suggested that this might be a worthwhile idea to look at. I am creating this issue on recommendation of DSN, please let me know if any other information is required.

I have created a gist containing c_vec.c which implements a rudimentary Vector implementation in C which acts as a library for c_vec.rs (which treats these as extern functions). Gist here : https://gist.github.com/chinmaydd/7ccd66273c162906f037905ed1ac8e2b

I also looked at the abstraction implemented in regression/cbmc-cpp/Vector1/lib which uses the idea of an infinite array to implement a Vector (apart from the abstraction which does not use a backing-store). If that is recommended way to go about implementing dynamic data structures, please let me know. I think this would require supporting the infinite array type in rmc in codegen but I would be happy to discuss further.

Thanks !

[kroening]

Did you consider using an unbounded array? You would then never need to reallocate.

[TGWDB]

I've had a bit of a look into this (and some discussions else where), so I'm adding some notes and updates here.

One suggestion was to use an infinite size memory allocation (similar to @kroening above) to prevent the need for realloc. This could look something like the following (including some example and checking code):

#include <stddef.h>
#include <stdint.h>

typedef struct {
    size_t len;
    size_t capacity;
    uint32_t* mem;
} vec;

vec* ffi_new() {
    vec* v = (vec *) malloc(sizeof(vec));
    v->len = 0;
    v->capacity = 8;
    v->mem = (uint32_t *) malloc(__CPROVER_constant_infinity_uint);
    return v;
}

void ffi_push(vec* v, uint32_t elem) {
    v->mem[v->len] = elem;
    v->len += 1;
}

void main() {
  vec *v = ffi_new();
  uint32_t nondet1;
  uint32_t nondet2;
  ffi_push(v, nondet1);
  ffi_push(v, nondet2);
  assert(v->len == 2);
}

This appears to capture the key concepts, but unfortunately cbmc has some problems (heavily trimmed output below):

$ cbmc experiment.c --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions
CBMC version 5.36.0 (cbmc-5.36.0) 64-bit x86_64 linux
...
converting SSA
warning: ignoring infinity
  * type: unsignedbv
      * width: 32
      * #c_type: unsigned_int
  * #source_location:
    * file: experiment.c
    * line: 14
    * function: ffi_new
    * working_directory: /home/tgw/github/testing/Issue6261
Runtime Convert SSA: 0.0008649s
Running propositional reduction
...
[ffi_push.pointer_arithmetic.5] line 19 pointer arithmetic: pointer outside object bounds in v->mem + (signed long int)v->len: FAILURE
...
[ffi_push.pointer_dereference.17] line 19 dereference failure: pointer outside object bounds in v->mem[(signed long int)v->len]: FAILURE
...
** 2 of 59 failed (2 iterations)
VERIFICATION FAILED

This appears to be an issue where the __CPROVER_constant_infinity_uint is not properly translated.

One "fix" is to use a real (and large enough) value instead of infinity. For the sake of this example I ran with 4096 and the verification was successful.

So to conclude, using a "large enough" array should be fine for verification and save the need for realloc, assuming this is appropriate for the verification goals. Also there is a bug in cbmc regarding the conversion of __CPROVER_constant_infinity_uint that needs to be fixed.