diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index f2632fcf3b0..6d8a6fe0702 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -8,6 +8,7 @@ macro(add_test_pl_profile name cmdline flag profile) ) set_tests_properties("${name}-${profile}" PROPERTIES LABELS "${profile};CBMC" + TIMEOUT 1200 ) endmacro(add_test_pl_profile) diff --git a/regression/cbmc/Array_UF23/main.c b/regression/cbmc/Array_UF23/main.c new file mode 100644 index 00000000000..77b15f695f7 --- /dev/null +++ b/regression/cbmc/Array_UF23/main.c @@ -0,0 +1,21 @@ +/// \file +/// Test that Ackermann constraints are reduced by the weak equivalence +/// optimisation: derived arrays (with, if, etc.) do not need Ackermann +/// constraints because they are implied by the with/if constraints plus +/// Ackermann on base arrays. +#include +int main() +{ + size_t array_size; + int a[array_size]; + int i0, i1, i2, i3, i4; + + a[i0] = 0; + a[i1] = 1; + a[i2] = 2; + a[i3] = 3; + a[i4] = 4; + + __CPROVER_assert(a[i0] >= 0, "a[i0] >= 0"); + return 0; +} diff --git a/regression/cbmc/Array_UF23/test.desc b/regression/cbmc/Array_UF23/test.desc new file mode 100644 index 00000000000..0af9f08b602 --- /dev/null +++ b/regression/cbmc/Array_UF23/test.desc @@ -0,0 +1,13 @@ +CORE broken-refine-arrays broken-smt-backend no-new-smt +main.c +--arrays-uf-always --unwind 1 --show-array-constraints --json-ui +"arrayAckermann": 60 +^EXIT=10$ +^SIGNAL=0$ +-- +"arrayAckermann": 110 +-- +Checks that the weak equivalence optimisation reduces Ackermann constraints. +With 5 stores to the same unbounded array, the old code produced 110 Ackermann +constraints (one per pair of indices per array term). The optimised code skips +derived arrays (with, if, etc.) and produces only 60. diff --git a/regression/cbmc/Array_operations2/test-arrays-uf-always.desc b/regression/cbmc/Array_operations2/test-arrays-uf-always.desc new file mode 100644 index 00000000000..71ebea4f13c --- /dev/null +++ b/regression/cbmc/Array_operations2/test-arrays-uf-always.desc @@ -0,0 +1,36 @@ +KNOWNBUG broken-cprover-smt-backend no-new-smt +main.c +--arrays-uf-always +^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$ +^\[main.assertion.13\] line 35 assertion arr\[1\].c\[3\] == 0: FAILURE$ +^\[main.assertion.14\] line 36 assertion arr\[1\].c\[4\] == 0: FAILURE$ +^\*\* 3 of 21 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +With --arrays-uf-always the array theory's union-find incorrectly conflates +structurally different arrays that happen to have equal initial values. + +The SSA equations for the zero-initialised struct array produce: + arr#2[0].c = {0,0,0,0,0} + arr#2[1].c = {0,0,0,0,0} + arr#2[2].c = {0,0,0,0,0} + +Because all three equalities share the same RHS literal {0,0,0,0,0}, +record_array_equality transitively unifies arr#2[0].c, arr#2[1].c, and +arr#2[2].c into a single equivalence class. After __CPROVER_array_replace +modifies arr (producing arr#3 via byte_update), the array theory cannot +distinguish the three .c sub-arrays: constraints meant for arr#3[1].c +(the replaced region) bleed into arr#3[0].c and arr#3[2].c, causing +spurious failures on assertions 1-11 and 15-21. + +Without --arrays-uf-always the char[5] sub-arrays are small enough to be +flattened to bitvectors, bypassing the array decision procedure entirely, +so the test passes. + +Fixing this requires the union-find to distinguish "structurally same +array" from "arrays with equal values", which is a fundamental change to +the Nelson-Oppen style array decision procedure as used in CBMC. diff --git a/regression/cbmc/Array_operations2/test.desc b/regression/cbmc/Array_operations2/test.desc index 559e087cce9..652d05a691c 100644 --- a/regression/cbmc/Array_operations2/test.desc +++ b/regression/cbmc/Array_operations2/test.desc @@ -1,4 +1,4 @@ -CORE broken-cprover-smt-backend no-new-smt +CORE broken-cprover-smt-backend no-new-smt broken-arrays-uf-always main.c ^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$ diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt index 82bb6a06236..cdcb9a42f99 100644 --- a/regression/cbmc/CMakeLists.txt +++ b/regression/cbmc/CMakeLists.txt @@ -32,6 +32,20 @@ add_test_pl_profile( "CORE" ) +add_test_pl_profile( + "cbmc-arrays-uf-always" + "$ --arrays-uf-always" + "-C;-X;broken-arrays-uf-always;-X;thorough-arrays-uf-always;-X;smt-backend;${gcc_only_string}-s;arrays-uf-always" + "CORE" +) + +add_test_pl_profile( + "cbmc-arrays-uf-always-refine-arrays" + "$ --arrays-uf-always --refine-arrays" + "-C;-X;broken-arrays-uf-always;-X;thorough-arrays-uf-always;-X;broken-refine-arrays;-X;smt-backend;${gcc_only_string}-s;arrays-uf-always-refine-arrays" + "CORE" +) + # solver appears on the PATH in Windows already if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows") set_property( diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc index d757d3e38af..67ab82dbe4d 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc +++ b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend no-new-smt +CORE broken-smt-backend no-new-smt broken-refine-arrays main.c --no-malloc-may-fail --smt2 --outfile - \(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\) diff --git a/regression/cbmc/arrays-uf-always-large-struct-soundness/main.c b/regression/cbmc/arrays-uf-always-large-struct-soundness/main.c new file mode 100644 index 00000000000..0ba8d547bbf --- /dev/null +++ b/regression/cbmc/arrays-uf-always-large-struct-soundness/main.c @@ -0,0 +1,16 @@ +struct S +{ + int d[65]; +}; + +unsigned nondet_unsigned(void); + +int main() +{ + struct S a[2]; + a[0].d[0] = 1; + a[1].d[0] = 1; + unsigned i = nondet_unsigned(); + __CPROVER_assume(i < 2); + __CPROVER_assert(a[i].d[0] == 1, ""); +} diff --git a/regression/cbmc/arrays-uf-always-large-struct-soundness/test.desc b/regression/cbmc/arrays-uf-always-large-struct-soundness/test.desc new file mode 100644 index 00000000000..6fa36be2289 --- /dev/null +++ b/regression/cbmc/arrays-uf-always-large-struct-soundness/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--arrays-uf-always --no-standard-checks +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +With --arrays-uf-always, indexing an array of structs containing array members +with 65+ elements through a nondeterministic index must produce correct results. +The bitvector solver connects the array symbol's map literals to the array +theory's element-wise constraints so that struct-level equalities properly +constrain the array elements. diff --git a/regression/cbmc/arrays-uf-always-member-crash/main.c b/regression/cbmc/arrays-uf-always-member-crash/main.c new file mode 100644 index 00000000000..533c2858f52 --- /dev/null +++ b/regression/cbmc/arrays-uf-always-member-crash/main.c @@ -0,0 +1,12 @@ +struct S +{ + int a[1]; +}; + +int main() +{ + struct S x[2]; + int i; + __CPROVER_assume(i >= 0 && i < 2); + __CPROVER_assert(x[i].a[0] == 0, ""); +} diff --git a/regression/cbmc/arrays-uf-always-member-crash/test.desc b/regression/cbmc/arrays-uf-always-member-crash/test.desc new file mode 100644 index 00000000000..c941d5374d1 --- /dev/null +++ b/regression/cbmc/arrays-uf-always-member-crash/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--arrays-uf-always --no-standard-checks +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Verify that --arrays-uf-always handles array-of-structs containing array +members accessed through a nondet index. The arrays theory must accept member +expressions where the struct operand is an index expression. diff --git a/regression/cbmc/arrays-uf-always-member-soundness/main.c b/regression/cbmc/arrays-uf-always-member-soundness/main.c new file mode 100644 index 00000000000..3e1913441d3 --- /dev/null +++ b/regression/cbmc/arrays-uf-always-member-soundness/main.c @@ -0,0 +1,16 @@ +struct S +{ + int d[1]; +}; + +int nondet_int(void); + +int main() +{ + struct S a[2]; + a[0].d[0] = 1; + a[1].d[0] = 1; + int i = nondet_int(); + __CPROVER_assume(i == 0 || i == 1); + __CPROVER_assert(a[i].d[0] == 1, ""); +} diff --git a/regression/cbmc/arrays-uf-always-member-soundness/test.desc b/regression/cbmc/arrays-uf-always-member-soundness/test.desc new file mode 100644 index 00000000000..6d7452abfd6 --- /dev/null +++ b/regression/cbmc/arrays-uf-always-member-soundness/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--arrays-uf-always --no-standard-checks +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +With --arrays-uf-always, indexing an array of structs that contain array members +through a nondeterministic index must produce correct results. The bitvector +solver handles member expressions with non-symbol struct operands (e.g., +member(index(outer_array, i), field)) directly, bypassing the array theory. diff --git a/regression/cbmc/bounds_check1/refine-arrays.desc b/regression/cbmc/bounds_check1/refine-arrays.desc new file mode 100644 index 00000000000..8e8f1c5175d --- /dev/null +++ b/regression/cbmc/bounds_check1/refine-arrays.desc @@ -0,0 +1,18 @@ +CORE thorough-smt-backend no-new-smt +main.c +--no-malloc-may-fail --arrays-uf-always --refine-arrays +^EXIT=10$ +^SIGNAL=0$ +\[\(.*\)i2\]: FAILURE +dest\[\(.*\)j2\]: FAILURE +payload\[\(.*\)[kl]2\]: FAILURE +\*\* 7 of [0-9]+ failed +-- +^warning: ignoring +\[\(.*\)i\]: FAILURE +dest\[\(.*\)j\]: FAILURE +payload\[\(.*\)[kl]\]: FAILURE +-- +Tests that --refine-arrays with --arrays-uf-always produces correct results +and completes quickly. Without --refine-arrays this test takes ~85 seconds; +with --refine-arrays the lazy with/if/Ackermann constraints reduce it to ~2s. diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc index ce90426706c..79ccfbd95cb 100644 --- a/regression/cbmc/bounds_check1/test.desc +++ b/regression/cbmc/bounds_check1/test.desc @@ -1,4 +1,4 @@ -CORE thorough-smt-backend no-new-smt +CORE thorough-smt-backend no-new-smt thorough-arrays-uf-always main.c --no-malloc-may-fail ^EXIT=10$ diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc index 98d0d6e9ce4..5b1d316e798 100644 --- a/regression/cbmc/trace-values/trace-values.desc +++ b/regression/cbmc/trace-values/trace-values.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE no-new-smt broken-arrays-uf-always trace-values.c --no-malloc-may-fail --trace ^EXIT=10$ diff --git a/regression/libcprover-cpp/CMakeLists.txt b/regression/libcprover-cpp/CMakeLists.txt index 0c57cb71d46..8efb91967b8 100644 --- a/regression/libcprover-cpp/CMakeLists.txt +++ b/regression/libcprover-cpp/CMakeLists.txt @@ -20,6 +20,7 @@ macro(add_test_pl_profile name cmdline flag profile) ) set_tests_properties("${name}-${profile}" PROPERTIES LABELS "${profile};CBMC" + TIMEOUT 1200 ) endmacro(add_test_pl_profile) diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index ac67cb87600..b7c89ca8cc0 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -204,7 +204,8 @@ get_sat_solver(message_handlert &message_handler, const optionst &options) { const bool no_simplifier = options.get_bool_option("beautify") || !options.get_bool_option("sat-preprocessor") || - options.get_bool_option("refine-strings"); + options.get_bool_option("refine-strings") || + options.get_bool_option("refine-arrays"); if(options.is_set("sat-solver")) { diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 96cb3c8045f..7ce0896ecce 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -193,12 +193,6 @@ void arrayst::collect_arrays(const exprt &a) } else if(a.id()==ID_member) { - const auto &struct_op = to_member_expr(a).struct_op(); - - DATA_INVARIANT( - struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol, - "unexpected array expression: member with '" + struct_op.id_string() + - "'"); } else if(a.is_constant() || a.id() == ID_array || a.id() == ID_string_constant) { @@ -222,7 +216,15 @@ void arrayst::collect_arrays(const exprt &a) typecast_op.type().id() == ID_array, "unexpected array type cast from " + typecast_op.type().id_string()); - arrays.make_union(a, typecast_op); + // Only unify when element types match; casts between different + // element sizes (e.g., SIMD reinterpretation) are handled at the + // bitvector level. + if( + to_array_type(a.type()).element_type() == + to_array_type(typecast_op.type()).element_type()) + { + arrays.make_union(a, typecast_op); + } collect_arrays(typecast_op); } else if(a.id()==ID_index) @@ -335,6 +337,25 @@ void arrayst::add_array_Ackermann_constraints() // iterate over arrays for(std::size_t i=0; i(arr)) + continue; + const index_sett &index_set=index_map[arrays.find_number(i)]; #ifdef DEBUG @@ -494,10 +515,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 || @@ -510,22 +528,32 @@ void arrayst::add_array_constraints( // we got a=(type[])b const auto &expr_typecast_op = to_typecast_expr(expr).op(); - // add a[i]=b[i] - for(const auto &index : index_set) + const typet &dest_element_type = to_array_type(expr.type()).element_type(); + const typet &src_element_type = + to_array_type(expr_typecast_op.type()).element_type(); + + // When element types differ in size (e.g., SIMD vector reinterpretation + // casts like int32[4] <-> int64[2]), the element-wise constraint + // a[i]=b[i] is incorrect. The bitvector-level conversion handles + // these as bitwise copies, so skip the array-level constraint. + if(dest_element_type == src_element_type) { - const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, index, element_type); - index_exprt index_expr2(expr_typecast_op, index, element_type); + // add a[i]=b[i] + for(const auto &index : index_set) + { + index_exprt index_expr1(expr, index, dest_element_type); + index_exprt index_expr2(expr_typecast_op, index, dest_element_type); - DATA_INVARIANT( - index_expr1.type()==index_expr2.type(), - "array elements should all have same type"); + DATA_INVARIANT( + index_expr1.type() == index_expr2.type(), + "array elements should all have same type"); - // add constraint - lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST, - equal_exprt(index_expr1, index_expr2)); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_TYPECAST]++; + // add constraint + lazy_constraintt lazy( + lazy_typet::ARRAY_TYPECAST, equal_exprt(index_expr1, index_expr2)); + add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_TYPECAST]++; + } } } else if(expr.id()==ID_index) @@ -585,7 +613,7 @@ void arrayst::add_array_constraints_with( lazy_constraintt lazy( lazy_typet::ARRAY_WITH, equal_exprt(index_expr, expr.new_value())); - add_array_constraint(lazy, false); // added immediately + add_array_constraint(lazy, false); // always eager array_constraint_count[constraint_typet::ARRAY_WITH]++; updated_indices.insert(expr.where()); @@ -620,7 +648,7 @@ void arrayst::add_array_constraints_with( lazy_constraintt lazy(lazy_typet::ARRAY_WITH, or_exprt(equality_expr, literal_exprt(guard_lit))); - add_array_constraint(lazy, false); // added immediately + add_array_constraint(lazy, false); // always eager array_constraint_count[constraint_typet::ARRAY_WITH]++; #if 0 // old code for adding, not significantly faster @@ -849,7 +877,7 @@ void arrayst::add_array_constraints_if( lazy_constraintt lazy(lazy_typet::ARRAY_IF, or_exprt(literal_exprt(!cond_lit), equal_exprt(index_expr1, index_expr2))); - add_array_constraint(lazy, false); // added immediately + add_array_constraint(lazy, false); // always eager array_constraint_count[constraint_typet::ARRAY_IF]++; #if 0 // old code for adding, not significantly faster @@ -869,7 +897,7 @@ void arrayst::add_array_constraints_if( lazy_typet::ARRAY_IF, or_exprt(literal_exprt(cond_lit), equal_exprt(index_expr1, index_expr2))); - add_array_constraint(lazy, false); // added immediately + add_array_constraint(lazy, false); // always eager array_constraint_count[constraint_typet::ARRAY_IF]++; #if 0 // old code for adding, not significantly faster diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 94813350942..1abbea85a88 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -508,7 +508,47 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) { // see if it is an unbounded array if(is_unbounded_array(type)) + { + // For arrays with a known finite size that fit within the + // flattening limit, connect the symbol's map literals to the + // element-wise bitvectors. This is needed when the array appears + // inside a struct that is an element of another array: the + // struct's bitvector uses the map literals, but the array theory + // constrains element-wise free variables. Without this + // connection, the map literals remain unconstrained. + const auto &array_type = to_array_type(type); + const auto size = numeric_cast(array_type.size()); + const auto elem_width_opt = + bv_width.get_width_opt(array_type.element_type()); + if( + size.has_value() && *size > 0 && *size <= MAX_FLATTENED_ARRAY_SIZE && + elem_width_opt.has_value() && *elem_width_opt > 0) + { + const irep_idt &identifier = + to_symbol_expr(expr.lhs()).get_identifier(); + const std::size_t elem_width = *elem_width_opt; + + bvt bv; + bv.reserve( + numeric_cast_v(*size) * elem_width); + + for(mp_integer i = 0; i < *size; ++i) + { + index_exprt idx( + expr.lhs(), from_integer(i, array_type.index_type())); + const bvt &elem_bv = convert_bv(idx, elem_width); + bv.insert(bv.end(), elem_bv.begin(), elem_bv.end()); + } + + map.set_literals(identifier, type, bv); + + if(freeze_all) + set_frozen(bv); + } + + // still let the array theory handle the equality return true; + } const bvt &bv1=convert_bv(expr.rhs()); diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 8e604fe9ac1..61a0d58cf56 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "boolbv.h" @@ -28,8 +29,10 @@ literalt boolbvt::convert_equality(const equal_exprt &expr) if(has_byte_operator(expr)) { - return record_array_equality( - to_equal_expr(lower_byte_operators(expr, ns))); + exprt simplified = simplify_expr(lower_byte_operators(expr, ns), ns); + if(simplified.id() != ID_equal) + return convert_bool(simplified); + return record_array_equality(to_equal_expr(simplified)); } return record_array_equality(expr); diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index 2e400a57345..0ea1594fcae 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -6,18 +6,19 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "boolbv.h" - -#include - #include #include +#include #include #include #include #include #include +#include "boolbv.h" + +#include + bvt boolbvt::convert_index(const index_exprt &expr) { const exprt &array=expr.array(); @@ -33,32 +34,78 @@ bvt boolbvt::convert_index(const index_exprt &expr) to_array_type(array_op_type); // see if the array size is constant - - if(is_unbounded_array(array_type)) + // Member expressions with non-symbol struct operands (e.g., + // member(index(outer_array, i), field)) cannot be properly + // constrained by the array theory, which treats them as opaque + // base arrays. Fall through to the bounded-array encoding when + // the array has a known finite size so that the bitvector solver + // directly connects the element to the struct field bits. + const bool member_with_non_symbol_struct = + array.id() == ID_member && + to_member_expr(array).compound().id() != ID_symbol && + to_member_expr(array).compound().id() != ID_nondet_symbol && + array_type.size().is_constant(); + + if(is_unbounded_array(array_type) && !member_with_non_symbol_struct) { // use array decision procedure + // Typecast between array types with different element sizes + // (e.g., SIMD reinterpretation int32[4] <-> int64[2]) cannot be + // handled by the array theory's element-wise constraints. + // Lower to byte_extract which the bitvector solver handles. + if( + array.id() == ID_typecast && + to_typecast_expr(array).op().type().id() == ID_array && + to_array_type(array.type()).element_type() != + to_array_type(to_typecast_expr(array).op().type()).element_type()) + { + const auto &src = to_typecast_expr(array).op(); + const auto elem_size = boolbv_width(array_type.element_type()) / 8; + return convert_bv(lower_byte_operators( + byte_extract_exprt( + ID_byte_extract_little_endian, + src, + mult_exprt( + typecast_exprt::conditional_cast( + index, signedbv_typet(config.ansi_c.pointer_width)), + from_integer( + elem_size, signedbv_typet(config.ansi_c.pointer_width))), + config.ansi_c.char_width, + array_type.element_type()), + ns)); + } + if(has_byte_operator(expr)) { - const index_exprt final_expr = - to_index_expr(lower_byte_operators(expr, ns)); - CHECK_RETURN(final_expr != expr); - bv = convert_bv(final_expr); + exprt lowered = simplify_expr(lower_byte_operators(expr, ns), ns); + CHECK_RETURN(lowered != expr); - // record type if array is a symbol - const exprt &final_array = final_expr.array(); - if( - final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol) + if(lowered.id() == ID_index) { - const auto &array_width_opt = bv_width.get_width_opt(array_type); - (void)map.get_literals( - final_array.get(ID_identifier), - array_type, - array_width_opt.value_or(0)); + const index_exprt &final_expr = to_index_expr(lowered); + bv = convert_bv(final_expr); + + // record type if array is a symbol + const exprt &final_array = final_expr.array(); + if( + final_array.id() == ID_symbol || + final_array.id() == ID_nondet_symbol) + { + const auto &array_width_opt = bv_width.get_width_opt(array_type); + (void)map.get_literals( + final_array.get(ID_identifier), + array_type, + array_width_opt.value_or(0)); + } + + // make sure we have the index in the cache + convert_bv(final_expr.index()); + } + else + { + bv = convert_bv(lowered); } - - // make sure we have the index in the cache - convert_bv(final_expr.index()); } else { diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index 2ba9ecdb6b2..3c7b4af9fd6 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_types.h" #include "endianness_map.h" #include "expr_util.h" +#include "magic.h" #include "namespace.h" #include "narrow.h" #include "pointer_offset_size.h" @@ -1112,7 +1113,13 @@ static exprt lower_byte_extract_array_vector( else num_elements = numeric_cast(to_vector_type(src.type()).size()); - if(num_elements.has_value()) + // For large arrays, element-by-element expansion creates N expressions + // that are each recursively lowered and simplified, resulting in O(N^2) + // behaviour. Use array_comprehension_exprt (below) instead, which + // represents the same semantics with a single symbolic expression. + if( + num_elements.has_value() && + !(src.type().id() == ID_array && *num_elements > MAX_FLATTENED_ARRAY_SIZE)) { exprt::operandst operands; operands.reserve(*num_elements);