Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unexpected failure with array_copy/array_equals #8176

Open
remi-delmas-3000 opened this issue Feb 1, 2024 · 1 comment · May be fixed by #8208
Open

Unexpected failure with array_copy/array_equals #8176

remi-delmas-3000 opened this issue Feb 1, 2024 · 1 comment · May be fixed by #8208
Labels
aws Bugs or features of importance to AWS CBMC users aws-high pending merge

Comments

@remi-delmas-3000
Copy link
Collaborator

The assertion in this program fails unexpectedly, but passes with size = N for many different concrete N

#include <stdlib.h>
#include <assert.h>
size_t nondet_size_t();
int main() {
  size_t size = nondet_size_t();
  if (0 < size && size <= __CPROVER_max_malloc_size) {
    char *a = malloc(size);
    char *b = malloc(size);
    __CPROVER_array_copy(a, b);
    assert(__CPROVER_array_equal(a, b));
  }
}

CBMC version: 5.95.1
Operating system: Ubuntu 20.04, macOS 14.3
Exact command line resulting in the issue: cbmc array_copy.c
What behaviour did you expect: SUCCESS for assert(__CPROVER_array_equal(a, b));
What happened instead: FAILURE for assert(__CPROVER_array_equal(a, b));
@remi-delmas-3000 remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high labels Feb 1, 2024
@tautschnig
Copy link
Collaborator

The problem is caused by use creating a fresh object-size symbol for each allocation of dynamic size. So these are two arrays of size symex_dynamic::dynamic_object_size!0#1 and symex_dynamic::dynamic_object_size$0!0#1, respectively. Looks like we need to fix how we build those object sizes.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 16, 2024
@tautschnig
Support comparing arrays of non-constant size with array_equal
fe543af 
Using simple type equality is too strict for arrays of non-constant
size: we introduce a fresh symbol for the size of each dynamically
allocated object of non-constant size. Consequently, two dynamically
allocated arrays of non-constant size will never pass type equality
checking, even when their underlying sizes are the same.

We now explicitly compare the sizes of the two arrays passed to
array_equal when types are not trivially equal.

Fixes: diffblue#8176
@tautschnig tautschnig linked a pull request Feb 16, 2024 that will close this issue
Open
3 tasks
@tautschnig tautschnig removed their assignment Feb 16, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
aws Bugs or features of importance to AWS CBMC users aws-high pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Support comparing arrays of non-constant size with array_equal tautschnig/cbmc
2 participants
@tautschnig @remi-delmas-3000