Fix typing of array expressions within an C ternary ? : operator

regression/cbmc/issue_9008_smt_array_ite_typing/main.c

@@ -0,0 +1,36 @@
+// Regression test for https://github.com/diffblue/cbmc/issues/9008
+//
+// CBMC used to emit ill-typed SMT-LIB 2 of the form
+//   (select (ite cond <bit-vector> <bit-vector>) <index>)
+// when convert_index was applied to an array-typed if_exprt whose two
+// branches were both encoded as bit-vectors (the common case being a
+// member access of a struct that is read out of memory as a flat
+// bit-vector).  Conforming SMT-LIB 2 solvers reject this with messages
+// such as "select expects array operand" / "array select operating on
+// non-array".
+//
+// The conditional pointer dereference below keeps the if_exprt from
+// being lifted into the surrounding indexing expression by the
+// simplifier, so that convert_index is invoked on an array-typed
+// if_exprt whose branches are bit-vector encodings of mat_t.
+
+typedef struct
+{
+  int row[4];
+} row_t;
+
+typedef row_t mat_t[4];
+
+int main(void)
+{
+  mat_t A, B;
+  int cond;
+  unsigned x, i;
+  __CPROVER_assume(x < 4 && i < 4);
+
+  mat_t *p = cond ? &A : &B;
+  int v = (*p)[x].row[i];
+
+  __CPROVER_assert(v == 0, "may fail");
+  return 0;
+}

regression/cbmc/issue_9008_smt_array_ite_typing/test.desc

@@ -0,0 +1,29 @@
+CORE smt-backend no-new-smt
+main.c
+--smt2 --no-array-field-sensitivity --no-bounds-check --no-pointer-check
+^\[main\.assertion\.1\] line \d+ may fail: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+select expects array operand
+^VERIFICATION ERROR$
+--
+This test exercises the SMT2 back-end's handling of an if_exprt that has
+array type and whose two branches are encoded as bit-vectors.  Without
+the fix associated with issue #9008, CBMC emits an ill-typed (select
+<bit-vector> <index>) form, which the bundled smt2_solver (cprover-smt2)
+flags with "select expects array operand", causing CBMC to report
+VERIFICATION ERROR.  With the fix, the if_exprt is correctly recognised
+as a bit-vector ITE and the index access is encoded as bvlshr/extract,
+so the assertion is checked normally and reported as FAILURE.
+
+The bug only manifests for SMT2 solvers that strictly enforce SMT-LIB 2
+type checking (the bundled smt2_solver, Bitwuzla, cvc5).  Z3 silently
+accepts the malformed formula, so this regression is detected by CI in
+the test-cprover-smt2 makefile target.
+
+--no-array-field-sensitivity is required because field sensitivity
+splits array-of-struct accesses into per-field SMT arrays, which avoids
+the buggy code path; --no-bounds-check and --no-pointer-check trim the
+property set down to the assertion of interest.

src/solvers/smt2/smt2_conv.cpp

@@ -5957,6 +5957,36 @@ bool smt2_convt::use_array_theory(const exprt &expr)
   // arrays inside structs get flattened, unless we have datatypes
   if(expr.id() == ID_with)
     return use_array_theory(to_with_expr(expr).old());
+  else if(expr.id() == ID_if)
+  {
+    // For an array-typed if-then-else, the SMT sort produced by
+    // convert_expr (see the ID_if branch above) is determined by the
+    // sorts chosen for its two operands:
+    // - if both branches are bit-vector-encoded, i.e. neither uses array
+    //   theory (typically because both are array-typed members of a
+    //   struct that has been flattened to a bit-vector), the resulting
+    //   ite is a bit-vector;
+    // - if both branches use array theory, the ite is an SMT array;
+    // - if exactly one branch uses array theory, the ID_if handler in
+    //   convert_expr unflattens the bit-vector branch back to an SMT
+    //   array (see the wheret::BEGIN/wheret::END unflatten calls), so
+    //   the ite is again an SMT array.
+    // The ite therefore "uses array theory" iff at least one branch
+    // does. Without this clause, the fall-through below would
+    // unconditionally return true for ID_if (since ID_if != ID_member),
+    // which is wrong in the symmetric bit-vector case: callers like
+    // convert_index, convert_with, flatten2bv, and the array-typed
+    // define-fun path would then emit array-theory operators -- e.g.
+    // (select <ite> ...) or (store <ite> ...) -- on a bit-vector
+    // operand, producing ill-typed SMT-LIB 2 that is rejected by
+    // conforming solvers (cf. issue #9008). The asymmetric case was
+    // already handled, for ID_with branches, in the ID_if conversion
+    // logic of convert_expr; the present clause makes use_array_theory
+    // consistent with that conversion in all four combinations.
+    const if_exprt &if_expr = to_if_expr(expr);
+    return use_array_theory(if_expr.true_case()) ||
+           use_array_theory(if_expr.false_case());
+  }
   else
     return use_datatypes || expr.id() != ID_member;
 }