CBMC getting stuck when post-processing functions with memmove and non-deterministic sizes

[AmPaschal]

When verifying functions containing memmove and non-deterministic sizes, the cbmc tool does not proceed beyond the post-processing stage.

For example, given the program below

#include <stdio.h>
#include <stdint.h>
#include <string.h>

struct net_buf {
    uint16_t len;
    uint8_t *data;
    struct net_buf *frags;
};

struct net_pkt {
    struct net_buf *buffer;
};

#define NET_6LO_FRAG1_HDR_LEN		4
#define NET_6LO_FRAGN_HDR_LEN		5
#define NET_6LO_DISPATCH_FRAG1		0xC0 /* 11000xxx */
#define NET_FRAG_DISPATCH_MASK 0xF8

static inline uint8_t get_datagram_type(uint8_t *ptr)
{
	return ptr[0] & NET_FRAG_DISPATCH_MASK;
}

void fragment_remove_headers(struct net_pkt *pkt)
{
	struct net_buf *frag;

	frag = pkt->buffer;

	uint16_t frag_hdr_len = NET_6LO_FRAGN_HDR_LEN;

	if (get_datagram_type(frag->data) == NET_6LO_DISPATCH_FRAG1) {
		frag_hdr_len = NET_6LO_FRAG1_HDR_LEN;
	}

	memmove(frag->data, frag->data + frag_hdr_len, frag->len - frag_hdr_len);  <-- This line causes verification to stall
	frag->len -= frag_hdr_len;

}

void harness(){
    struct net_pkt *pkt = malloc(sizeof(struct net_pkt));
	__CPROVER_assume(pkt != NULL);
	
	struct net_buf* buf = malloc(sizeof(struct net_buf));
	__CPROVER_assume(buf != NULL);
	uint8_t size;
    __CPROVER_assume(size > NET_6LO_FRAGN_HDR_LEN);
	uint8_t* data = (uint8_t*) malloc(size);
	__CPROVER_assume(data != NULL);
	buf -> data = data;
	buf -> len = size;
	buf->frags = NULL;

    pkt->buffer = buf;

    fragment_remove_headers(pkt);
	
	free(data);
	free(buf);
	free(pkt);
}

If we run it with the cbmc command
cbmc --verbosity 9 --function harness cbmc4_harness.c

We get the output

CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 linux
Parsing cbmc4_harness.c
Converting
Type-checking cbmc4_harness
file cbmc4_harness.c line 44 function harness: function 'malloc' is not declared
file cbmc4_harness.c line 61 function harness: function 'free' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-malloc> line 11: implicit function declaration 'malloc'
old definition in module cbmc4_harness file cbmc4_harness.c line 44 function harness
void * (void)
new definition in module <built-in-library> file <builtin-library-malloc> line 11
void * (__CPROVER_size_t malloc_size)
file <builtin-library-free> line 14: implicit function declaration 'free'
old definition in module cbmc4_harness file cbmc4_harness.c line 61 function harness
signed int (void)
new definition in module <built-in-library> file <builtin-library-free> line 14
void (void *ptr)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.0141128s
size of program expression: 368 steps
simple slicing removed 29 assignments
Generated 82 VCC(s), 75 remaining after simplification
Runtime Postprocess Equation: 3.6186e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00283073s
Running propositional reduction
Post-processing

As seen, the verification gets stuck in Post-processing and does not proceed to the SAT solving stage.

If we remove the line with memmove, the verification completes in one second.

We have observed this with multiple functions containing memmove across different embedded software.

Please, is this a problem with CBMC or is there something we are not doing?