From f7693975875c151cebb6939ea1aefe2df31fbfde Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Mar 2022 23:51:29 +0000 Subject: [PATCH] Array theory: gracefully handle negative out-of-bounds access Attempts to convert an access at a constant negative (!) index of an array constant should just lead to the access being ignored. This situation was already handled for a positive out-of-bounds case, but should really be considered in both directions. --- regression/cbmc/Array_UF21/main.c | 6 ++++++ regression/cbmc/Array_UF21/test.desc | 9 +++++++++ src/solvers/flattening/arrays.cpp | 8 ++++---- 3 files changed, 19 insertions(+), 4 deletions(-) create mode 100644 regression/cbmc/Array_UF21/main.c create mode 100644 regression/cbmc/Array_UF21/test.desc diff --git a/regression/cbmc/Array_UF21/main.c b/regression/cbmc/Array_UF21/main.c new file mode 100644 index 00000000000..e2a99771004 --- /dev/null +++ b/regression/cbmc/Array_UF21/main.c @@ -0,0 +1,6 @@ +int main() +{ + int x[0] = {}; + int a = x[-1]; + x[a] = 42; +} diff --git a/regression/cbmc/Array_UF21/test.desc b/regression/cbmc/Array_UF21/test.desc new file mode 100644 index 00000000000..e9d3c4ebe15 --- /dev/null +++ b/regression/cbmc/Array_UF21/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--arrays-uf-always --bounds-check +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +^Invariant check failed diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 111a627e919..0fdd83ec127 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -715,13 +715,13 @@ void arrayst::add_array_constraints_array_constant( // We have a constant index - just pick the element at that index from the // array constant. - const std::size_t i = - numeric_cast_v(to_constant_expr(index)); + const optionalt i = + numeric_cast(to_constant_expr(index)); // if the access is out of bounds, we leave it unconstrained - if(i >= operands.size()) + if(!i.has_value() || *i >= operands.size()) continue; - const exprt v = operands[i]; + const exprt v = operands[*i]; DATA_INVARIANT( index_expr.type() == v.type(), "array operand type should match array element type");