From 1b4ef10d135cb3ec0f6f7e402338188f941f8512 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 30 Nov 2025 19:57:17 +0000
Subject: [PATCH] Fix C++ ternary operator type checking for bitfield operands

`implicit_conversion_sequence` does not guarantee to produce the exact type
requested as bitfields promote to the underlying type. Therefore, add typecasts
as needed to ensure type consistency.

Fixes: #933
---
 .../cbmc-cpp/Bitfields_Ternary1/main.cpp      | 69 +++++++++++++++++++
 .../cbmc-cpp/Bitfields_Ternary1/test.desc     |  8 +++
 src/cpp/cpp_typecheck_expr.cpp                | 10 +++
 3 files changed, 87 insertions(+)
 create mode 100644 regression/cbmc-cpp/Bitfields_Ternary1/main.cpp
 create mode 100644 regression/cbmc-cpp/Bitfields_Ternary1/test.desc

diff --git a/regression/cbmc-cpp/Bitfields_Ternary1/main.cpp b/regression/cbmc-cpp/Bitfields_Ternary1/main.cpp
new file mode 100644
index 00000000000..1ebf8c1e364
--- /dev/null
+++ b/regression/cbmc-cpp/Bitfields_Ternary1/main.cpp
@@ -0,0 +1,69 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdint.h>
+
+// Regression test for issue where CBMC incorrectly failed with an
+// "equality without matching types" error when using ternary expressions
+// with bitfield types. The issue occurred when the third argument of a
+// ternary operator was a bitfield type (uint8_t : 1) that needed to be
+// implicitly converted to bool. GCC and Clang accept this code without
+// warnings, and CBMC should handle the implicit conversion as well.
+
+typedef struct
+{
+  uint32_t value_31_0 : 32;
+} signal32_t;
+
+typedef struct
+{
+  uint8_t value_0_0 : 1;
+} signal1_t;
+
+static inline bool yosys_simplec_get_bit_25_of_32(const signal32_t *sig)
+{
+  return (sig->value_31_0 >> 25) & 1;
+}
+
+typedef struct rvfi_insn_srai_state_t
+{
+  signal32_t rvfi_insn;
+  signal32_t rvfi_rs1_rdata;
+  signal1_t _abc_1398_n364;
+  signal1_t _abc_1398_n363;
+} rvfi_insn_srai_state_t;
+
+int main()
+{
+  rvfi_insn_srai_state_t state;
+
+  // Test case 1: Both operands are function calls returning bool
+  state.rvfi_insn.value_31_0 = 0;
+  state.rvfi_rs1_rdata.value_31_0 = 0;
+  state._abc_1398_n363.value_0_0 = 1;
+
+  // This ternary should work: condition ? bool : uint8_t:1
+  // The third operand is a bitfield that should be implicitly converted to bool
+  state._abc_1398_n364.value_0_0 =
+    yosys_simplec_get_bit_25_of_32(&state.rvfi_insn)
+      ? yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata)
+      : state._abc_1398_n363.value_0_0;
+
+  // Since bit 25 of rvfi_insn is 0, the condition is false,
+  // so the result should be _abc_1398_n363.value_0_0, which is 1
+  assert(state._abc_1398_n364.value_0_0 == 1);
+
+  // Test case 2: Condition is true
+  state.rvfi_insn.value_31_0 = (1u << 25); // Set bit 25
+  state.rvfi_rs1_rdata.value_31_0 = 0;
+
+  state._abc_1398_n364.value_0_0 =
+    yosys_simplec_get_bit_25_of_32(&state.rvfi_insn)
+      ? yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata)
+      : state._abc_1398_n363.value_0_0;
+
+  // Since bit 25 of rvfi_insn is 1, the condition is true,
+  // so the result should be the bit 25 of rvfi_rs1_rdata, which is 0
+  assert(state._abc_1398_n364.value_0_0 == 0);
+
+  return 0;
+}
diff --git a/regression/cbmc-cpp/Bitfields_Ternary1/test.desc b/regression/cbmc-cpp/Bitfields_Ternary1/test.desc
new file mode 100644
index 00000000000..91d9cf8b52e
--- /dev/null
+++ b/regression/cbmc-cpp/Bitfields_Ternary1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 2685771889c..d104bc0bfcc 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -243,11 +243,21 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr)
     {
       expr.type()=e1.type();
       expr.op1().swap(e1);
+      if(expr.type() != expr.op2().type())
+      {
+        implicit_conversion_sequence(expr.op2(), expr.type(), e2);
+        expr.op2().swap(e2);
+      }
     }
     else if(implicit_conversion_sequence(expr.op2(), expr.op1().type(), e2))
     {
       expr.type()=e2.type();
       expr.op2().swap(e2);
+      if(expr.type() != expr.op1().type())
+      {
+        implicit_conversion_sequence(expr.op1(), expr.type(), e1);
+        expr.op1().swap(e1);
+      }
     }
     else if(
       expr.op1().type().id() == ID_array &&