From fe543afad457c94a948528d1c9366c30eac21894 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 16 Feb 2024 20:53:57 +0000 Subject: [PATCH] Support comparing arrays of non-constant size with array_equal 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: #8176 --- regression/cbmc/Array_operations4/main.c | 16 +++++++++++ regression/cbmc/Array_operations4/test.desc | 13 +++++++++ src/goto-symex/symex_other.cpp | 30 ++++++++++++++------- 3 files changed, 49 insertions(+), 10 deletions(-) create mode 100644 regression/cbmc/Array_operations4/main.c create mode 100644 regression/cbmc/Array_operations4/test.desc diff --git a/regression/cbmc/Array_operations4/main.c b/regression/cbmc/Array_operations4/main.c new file mode 100644 index 00000000000..54e98f60ef4 --- /dev/null +++ b/regression/cbmc/Array_operations4/main.c @@ -0,0 +1,16 @@ +#include + +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); + __CPROVER_assert(__CPROVER_array_equal(a, b), "should pass"); + a[0] = 0; + __CPROVER_assert(__CPROVER_array_equal(a, b), "may fail"); + } +} diff --git a/regression/cbmc/Array_operations4/test.desc b/regression/cbmc/Array_operations4/test.desc new file mode 100644 index 00000000000..2c9cab21eaa --- /dev/null +++ b/regression/cbmc/Array_operations4/test.desc @@ -0,0 +1,13 @@ +CORE +main.c + +^\[main.assertion.1\] line 12 should pass: SUCCESS +^\[main.assertion.2\] line 14 may fail: FAILURE +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Verify that array_equal works for arrays of non-constant size. diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 188cb44b21f..c46c2b69450 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -9,14 +9,15 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Symbolic Execution -#include "goto_symex.h" - #include #include #include #include +#include #include +#include "goto_symex.h" + void goto_symext::havoc_rec( statet &state, const guardt &guard, @@ -219,27 +220,36 @@ void goto_symext::symex_other( // 2. find the actual array objects/candidates for objects (via // process_array_expr) // 3. build an assignment where the lhs is the previous third argument, and - // the right-hand side is an equality over the arrays, if their types match; - // if the types don't match the result trivially is false + // the right-hand side is an equality over the size of their arrays and + // their contents DATA_INVARIANT( code.operands().size() == 3, "expected array_equal statement to have three operands"); // we need to add dereferencing for the first two - exprt array1 = clean_expr(code.op0(), state, false); - exprt array2 = clean_expr(code.op1(), state, false); + exprt array_ptr1 = clean_expr(code.op0(), state, false); + exprt array_ptr2 = clean_expr(code.op1(), state, false); // obtain the actual arrays + exprt array1 = array_ptr1; process_array_expr(state, array1); + exprt array2 = array_ptr2; process_array_expr(state, array2); exprt rhs; - // Types don't match? Make it 'false'. - if(array1.type() != array2.type()) - rhs = false_exprt(); - else + // Types match: just compare contents + if(array1.type() == array2.type()) rhs = equal_exprt(array1, array2); + else + { + rhs = and_exprt{ + equal_exprt{object_size(array_ptr1), object_size(array_ptr2)}, + equal_exprt{ + array1, + make_byte_extract( + array2, from_integer(0, c_index_type()), array1.type())}}; + } symex_assign(state, code.op2(), rhs); }