Spurious pointer check violation with smt2 backend and z3 4.12.1

[remi-delmas-3000]

This program is proved correct with the SAT backend but fails with with SMT2 backend with --pointer-check --bounds-check:

[stk_push.pointer_dereference.17] line 57 dereference failure: pointer outside object bounds in stk->elems[(signed long int)stk->top]: FAILURE

The analysis using the SMT2 backend succeeds if we change the assumption at line 46:

__CPROVER_assume(UINT8_MAX <= stk_size && stk_size <= UINT8_MAX);

into

  __CPROVER_assume(UINT8_MAX == stk_size);

or into an assignment

stk_size = UINT8_MAX;

#include <stdlib.h>
#include <stdint.h>

extern size_t __CPROVER_max_malloc_size;
int __builtin_clzll(unsigned long long);

#define __nof_symex_objects                                                    \
  ((size_t)(1ULL << __builtin_clzll(__CPROVER_max_malloc_size)))

typedef struct {
  size_t k;
  void **ptrs;
} smap_t;

void smap_init(smap_t *smap, size_t k) {
  *smap = (smap_t){
      .k = k, .ptrs = __CPROVER_allocate(__nof_symex_objects * sizeof(void *), 1)};
}

void *smap_get(smap_t *smap, void *ptr) {
  size_t id = __CPROVER_POINTER_OBJECT(ptr);
  void *sptr = smap->ptrs[id];
  if (!sptr) {
    sptr = __CPROVER_allocate(smap->k * __CPROVER_OBJECT_SIZE(ptr), 1);
    smap->ptrs[id] = sptr;
  }
  return sptr + smap->k * __CPROVER_POINTER_OFFSET(ptr);
}

typedef struct {
  uint8_t key;
  uint8_t value;
} stk_elem_t;

typedef struct {
  int8_t top;
  stk_elem_t *elems;
} stk_t;

size_t nondet_size_t();

// Creates a fresh borrow stack
stk_t *stk_new() {
  stk_t *stk = __CPROVER_allocate(sizeof(stk_t), 1);
  size_t stk_size = nondet_size_t();
  __CPROVER_assume(UINT8_MAX <= stk_size && stk_size <= UINT8_MAX);
  // works with
  // __CPROVER_assume(stk_size == UINT8_MAX);
  *stk = (stk_t){
      .top = 0,
      .elems = __CPROVER_allocate(sizeof(stk_elem_t) * stk_size, 1)};
  return stk;
}

void stk_push(stk_t *stk, uint8_t key, uint8_t value) {
  assert(stk->top < UINT8_MAX);
  stk->elems[stk->top] = (stk_elem_t){.key = key, .value = value};
  stk->top++;
}

stk_t *get_stk(smap_t *smap, void *ptr) {
  stk_t **stk_ptr = (stk_t **) smap_get(smap, ptr);
  if (!(*stk_ptr)) {
    *stk_ptr = stk_new();
  }
  return *stk_ptr;
}

typedef struct {
  int a;
  int b;
} my_struct_t;

int main() {
  smap_t smap;
  smap_init(&smap, sizeof(stk_t*));
  my_struct_t my_struct;
  stk_t *stk_a = get_stk(&smap, &(my_struct.a));
  stk_push(stk_a, 1, 1);
  stk_t *stk_b = get_stk(&smap, &(my_struct.b));
  assert(stk_b);
  stk_push(stk_b, 1, 1);
}

CBMC version: 5.79.0 (cbmc-5.79.0-49-gb34e991f30), Z3 version 4.12.1 - 64 bit
Operating system: macOS
Exact command line resulting in the issue:cbmc --pointer-check --smt2 stack_push.c
What behaviour did you expect: analysis suceeds
What happened instead: analysis fails

[NlightNFotis]

Hello,

I have been working on this over the last few days, and it just struck me that I haven't provided any sort of update on this one, so let me rectify the situation by providing you with an update of my investigation so far.

I had a lengthy play with the file provided in the bug report, toggling between the two different assumptions (by two assumptions, I mean one with the __CPROVER_assume(UINT8_MAX <= stk_size && stk_size <= UINT8_MAX); and the other with __CPROVER_assume(stk_size == UINT8_MAX);).

Superficially, there was no difference between the VCCs (produced with --show-vcc) or the expressions produced by the instrumentation (which I investigated manually through a combination of .pretty() printing the exprts produced in src/ansi-c/goto_check_c.cpp between the two versions of the file.

There were observable differences however in the SMT2 output produced (using the flag --outfile). Of all these differences, the difference in the verification outcome comes from the following assertion that is missing from the version that doesn't work:

(assert (=> (= ((_ extract 63 56) (ite (= |stk_push::stk!0@2#1| (concat (_ bv10 8) (_ bv0 56))) (concat (_ bv3 8) (_ bv0 56)) |stk_push::stk$object#0..elems|)) (_ bv3 8))(= object_size.2 (_ bv510 64))))

I also observed differences in the size expression associated with object_size.2 (which is associated with a symex_dynamic_object_size object): In the version with just = 255 (the value of UINT_MAX8 on my machine), constant propagation seems to work and we can observe a size of FF for the size associated with the object_size.2. In the version that doesn't work, we are seeing a new symex_dynamic_object_size being produced, with no discernible value produced for that (I believe it's left nondet for the solver).

My current working hypothesis is that the version of the assumption __CPROVER_assume(UINT8_MAX <= stk_size && stk_size <= UINT8_MAX); contains a compound expression which doesn't simplify correctly, which ends up propagating in a way that hinders deduction of the value of the object later on.

While this is what I'm speculate for now, I also had a couple of other suggestions of avenues to investigate, so I will be keeping an open mind for possible issues/resolutions to this.

---

As an aside, we have exercised the new SMT2 backend with this code (the one that gets exercised with the --incremental-smt2-solver) and it seems the new SMT backend is for now free of this particular issue (its behaviour is consistent to the one that the SAT backend produces).

[NlightNFotis]

Hi @remi-delmas-3000 would it be possible to run the code in #7761 against your internal benchmarks and let me know if there's the performance degradation we talked about previously?

[NlightNFotis]

@remi-delmas-3000 By the way, in reference to our discussion yesterday, the maximum array size that gets flattened is 1000, set in src/util/magic.h:11:

const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000;

[NlightNFotis]

Hi @remi-delmas-3000, we still intend to merge the singleton interval simplification and I wanted to touch base to ask if there are any concerns about this from your end.

I seem to recall that you mentioned last time that this could potentially raise some performance issues but that was speculative and you wanted to play around with this a bit. Is this still the case?

[remi-delmas-3000]

@NlightNFotis , I'll do a regression run on my end today and post an update on #7761