From 0289d31dba9c5ce82eacc4a375b35397e4198cc0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 1 Mar 2023 12:37:09 +0000
Subject: [PATCH] ITE and binary relations are constant when all operands are
 constants

This expands the definition of is_constantt to cover if-then-else as
well as binary relations and logic or bit operations. In many, but not,
cases the simplifier will have turned these into simpler constants. The
included regression test is derived from Rust code, where the
intermediate representation (together with constant propagation) will
yield such comparisons.
---
 regression/cbmc/constant_folding3/main.c    | 8 ++++++++
 regression/cbmc/constant_folding3/test.desc | 9 +++++++++
 src/util/expr_util.cpp                      | 8 ++++++--
 3 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/constant_folding3/main.c
 create mode 100644 regression/cbmc/constant_folding3/test.desc

diff --git a/regression/cbmc/constant_folding3/main.c b/regression/cbmc/constant_folding3/main.c
new file mode 100644
index 00000000000..4d53aa377b4
--- /dev/null
+++ b/regression/cbmc/constant_folding3/main.c
@@ -0,0 +1,8 @@
+int main(void)
+{
+  int x;
+  int plus_one_is_null = &x + 1 == (int *)0 ? 1 : 0;
+  __CPROVER_assert(plus_one_is_null != 2, "cannot be 2");
+
+  return 0;
+}
diff --git a/regression/cbmc/constant_folding3/test.desc b/regression/cbmc/constant_folding3/test.desc
new file mode 100644
index 00000000000..30d812ee484
--- /dev/null
+++ b/regression/cbmc/constant_folding3/test.desc
@@ -0,0 +1,9 @@
+CORE new-smt-backend
+main.c
+
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index 96ac38827dd..089dc217aa2 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -239,8 +239,12 @@ bool is_constantt::is_constant(const exprt &expr) const
     expr.id() == ID_typecast || expr.id() == ID_array_of ||
     expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
     expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
-    expr.id() == ID_empty_union ||
-    expr.id() == ID_byte_update_big_endian ||
+    expr.id() == ID_empty_union || expr.id() == ID_equal ||
+    expr.id() == ID_notequal || expr.id() == ID_lt || expr.id() == ID_le ||
+    expr.id() == ID_gt || expr.id() == ID_ge || expr.id() == ID_if ||
+    expr.id() == ID_not || expr.id() == ID_and || expr.id() == ID_or ||
+    expr.id() == ID_bitnot || expr.id() == ID_bitand || expr.id() == ID_bitor ||
+    expr.id() == ID_bitxor || expr.id() == ID_byte_update_big_endian ||
     expr.id() == ID_byte_update_little_endian)
   {
     return std::all_of(