From dc4157ec5c5b5a6438854c9c0d64ff0dc6d95eaf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Sep 2024 12:39:29 +0000 Subject: [PATCH] Re-enable array theory as default for array size above threshold Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way. We previously attempted to do this in in #6194 (inspired by #2108, but not picking up all its changes), but then reverted the gist of the change in #6232 as `array-bug-6230/main.c` demonstrated lingering issues. This PR now addresses the flaw in the array theory back-end. We may still run into performance regressions as the threshold of 1000 bits of total size of the array object is possibly lower than where the cost of bit-blasting exceeds the cost of constraints produced by our current array theory implementation. Two of our existing regression tests already demonstrate this problem, hence those now use `--arrays-uf-never`. --- regression/cbmc/array-bug-6230/main.c | 4 ++- regression/cbmc/bounds_check1/test.desc | 2 +- regression/cbmc/union/union_large_array.desc | 2 +- src/solvers/flattening/arrays.cpp | 27 +++++++++++++------- src/solvers/flattening/boolbv.h | 2 +- 5 files changed, 24 insertions(+), 13 deletions(-) diff --git a/regression/cbmc/array-bug-6230/main.c b/regression/cbmc/array-bug-6230/main.c index 5dc539954b7..f25a4e0a0ad 100644 --- a/regression/cbmc/array-bug-6230/main.c +++ b/regression/cbmc/array-bug-6230/main.c @@ -3,7 +3,9 @@ struct inner { - uint32_t exts[32]; // 32 is the minimum to crash + // 32 is the minimum to crash as it will produce an array wider than 1000 bits + // (the default value of MAX_FLATTENED_ARRAY_SIZE) + uint32_t exts[32]; }; struct outer diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc index ce90426706c..7eb6f1a51ea 100644 --- a/regression/cbmc/bounds_check1/test.desc +++ b/regression/cbmc/bounds_check1/test.desc @@ -1,6 +1,6 @@ CORE thorough-smt-backend no-new-smt main.c ---no-malloc-may-fail +--no-malloc-may-fail --arrays-uf-never ^EXIT=10$ ^SIGNAL=0$ \[\(.*\)i2\]: FAILURE diff --git a/regression/cbmc/union/union_large_array.desc b/regression/cbmc/union/union_large_array.desc index 7dd292448b7..ab27b6363b5 100644 --- a/regression/cbmc/union/union_large_array.desc +++ b/regression/cbmc/union/union_large_array.desc @@ -1,6 +1,6 @@ CORE thorough-smt-backend no-new-smt union_large_array.c - +--arrays-uf-never ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.1\] line \d+ should fail: FAILURE$ diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index ad3562ed4d4..629cadeb409 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -196,12 +196,24 @@ void arrayst::collect_arrays(const exprt &a) } else if(a.id()==ID_member) { - const auto &struct_op = to_member_expr(a).struct_op(); + const exprt *struct_op_ptr = &to_member_expr(a).struct_op(); + while(struct_op_ptr->id() == ID_member) + struct_op_ptr = &to_member_expr(*struct_op_ptr).struct_op(); - DATA_INVARIANT( - struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol, - "unexpected array expression: member with '" + struct_op.id_string() + - "'"); + if(struct_op_ptr->id() == ID_index) + { + const auto &array_op = to_index_expr(*struct_op_ptr).array(); + arrays.make_union(a, array_op); + collect_arrays(array_op); + } + else + { + DATA_INVARIANT( + struct_op_ptr->id() == ID_struct || struct_op_ptr->id() == ID_symbol || + struct_op_ptr->id() == ID_nondet_symbol, + "unexpected array expression: member with '" + + struct_op_ptr->id_string() + "'"); + } } else if(a.is_constant() || a.id() == ID_array || a.id() == ID_string_constant) { @@ -497,10 +509,7 @@ void arrayst::add_array_constraints( expr.id() == ID_string_constant) { } - else if( - expr.id() == ID_member && - (to_member_expr(expr).struct_op().id() == ID_symbol || - to_member_expr(expr).struct_op().id() == ID_nondet_symbol)) + else if(expr.id() == ID_member) { } else if(expr.id()==ID_byte_update_little_endian || diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 78987b734ec..e57fa97963f 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -51,7 +51,7 @@ class boolbvt:public arrayst message_handlert &message_handler, bool get_array_constraints = false) : arrayst(_ns, _prop, message_handler, get_array_constraints), - unbounded_array(unbounded_arrayt::U_NONE), + unbounded_array(unbounded_arrayt::U_AUTO), bv_width(_ns), bv_utils(_prop), functions(*this),