From 550251bf6b972730fec28abcb31c0c8e35ed756a Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 6 Jan 2024 09:16:08 -0800
Subject: [PATCH] add nullary_exprt::check(expr)

This adds nullary_exprt::check(expr), which checks that the expression is
indeed nullary.  This follows the same pattern as binary_exprt::check and
ternary_exprt::check.
---
 src/util/std_expr.cpp | 17 +++++++------
 src/util/std_expr.h   | 55 ++++++++++++++++++++++++++-----------------
 2 files changed, 42 insertions(+), 30 deletions(-)

diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 9eda7364a8f..3b95e3e96b9 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -23,28 +23,27 @@ bool constant_exprt::value_is_zero_string() const
 
 void constant_exprt::check(const exprt &expr, const validation_modet vm)
 {
-  DATA_CHECK(
-    vm, !expr.has_operands(), "constant expression must not have operands");
+  nullary_exprt::check(expr, vm);
+
+  const auto value = expr.get(ID_value);
 
   DATA_CHECK(
     vm,
-    !can_cast_type<bitvector_typet>(expr.type()) ||
-      !id2string(to_constant_expr(expr).get_value()).empty(),
+    !can_cast_type<bitvector_typet>(expr.type()) || !value.empty(),
     "bitvector constant must have a non-empty value");
 
   DATA_CHECK(
     vm,
     !can_cast_type<bitvector_typet>(expr.type()) ||
       can_cast_type<pointer_typet>(expr.type()) ||
-      id2string(to_constant_expr(expr).get_value())
-          .find_first_not_of("0123456789ABCDEF") == std::string::npos,
+      id2string(value).find_first_not_of("0123456789ABCDEF") ==
+        std::string::npos,
     "negative bitvector constant must use two's complement");
 
   DATA_CHECK(
     vm,
-    !can_cast_type<bitvector_typet>(expr.type()) ||
-      to_constant_expr(expr).get_value() == ID_0 ||
-      id2string(to_constant_expr(expr).get_value())[0] != '0',
+    !can_cast_type<bitvector_typet>(expr.type()) || value == ID_0 ||
+      id2string(value)[0] != '0',
     "bitvector constant must not have leading zeros");
 }
 
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index d21596befa1..3445073c17c 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -26,6 +26,24 @@ class nullary_exprt : public expr_protectedt
   {
   }
 
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm,
+      expr.operands().size() == 0,
+      "nullary expression must not have operands");
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
+
   /// remove all operand methods
   operandst &operands() = delete;
   const operandst &operands() const = delete;
@@ -293,19 +311,16 @@ inline void validate_expr(const nondet_symbol_exprt &value)
 inline const nondet_symbol_exprt &to_nondet_symbol_expr(const exprt &expr)
 {
   PRECONDITION(expr.id()==ID_nondet_symbol);
-  const nondet_symbol_exprt &ret =
-    static_cast<const nondet_symbol_exprt &>(expr);
-  validate_expr(ret);
-  return ret;
+  nondet_symbol_exprt::check(expr);
+  return static_cast<const nondet_symbol_exprt &>(expr);
 }
 
 /// \copydoc to_nondet_symbol_expr(const exprt &)
 inline nondet_symbol_exprt &to_nondet_symbol_expr(exprt &expr)
 {
   PRECONDITION(expr.id()==ID_symbol);
-  nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
-  validate_expr(ret);
-  return ret;
+  nondet_symbol_exprt::check(expr);
+  return static_cast<nondet_symbol_exprt &>(expr);
 }
 
 
@@ -1804,18 +1819,16 @@ inline void validate_expr(const empty_union_exprt &value)
 inline const empty_union_exprt &to_empty_union_expr(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_empty_union);
-  const empty_union_exprt &ret = static_cast<const empty_union_exprt &>(expr);
-  validate_expr(ret);
-  return ret;
+  empty_union_exprt::check(expr);
+  return static_cast<const empty_union_exprt &>(expr);
 }
 
 /// \copydoc to_empty_union_expr(const exprt &)
 inline empty_union_exprt &to_empty_union_expr(exprt &expr)
 {
   PRECONDITION(expr.id() == ID_empty_union);
-  empty_union_exprt &ret = static_cast<empty_union_exprt &>(expr);
-  validate_expr(ret);
-  return ret;
+  empty_union_exprt::check(expr);
+  return static_cast<empty_union_exprt &>(expr);
 }
 
 /// \brief Struct constructor from list of elements
@@ -2921,16 +2934,16 @@ inline bool can_cast_expr<type_exprt>(const exprt &base)
 inline const type_exprt &to_type_expr(const exprt &expr)
 {
   PRECONDITION(can_cast_expr<type_exprt>(expr));
-  const type_exprt &ret = static_cast<const type_exprt &>(expr);
-  return ret;
+  type_exprt::check(expr);
+  return static_cast<const type_exprt &>(expr);
 }
 
 /// \copydoc to_type_expr(const exprt &)
 inline type_exprt &to_type_expr(exprt &expr)
 {
   PRECONDITION(can_cast_expr<type_exprt>(expr));
-  type_exprt &ret = static_cast<type_exprt &>(expr);
-  return ret;
+  type_exprt::check(expr);
+  return static_cast<type_exprt &>(expr);
 }
 
 /// \brief A constant literal expression
@@ -2988,6 +3001,7 @@ inline void validate_expr(const constant_exprt &value)
 inline const constant_exprt &to_constant_expr(const exprt &expr)
 {
   PRECONDITION(expr.is_constant());
+  constant_exprt::check(expr);
   return static_cast<const constant_exprt &>(expr);
 }
 
@@ -2995,6 +3009,7 @@ inline const constant_exprt &to_constant_expr(const exprt &expr)
 inline constant_exprt &to_constant_expr(exprt &expr)
 {
   PRECONDITION(expr.is_constant());
+  constant_exprt::check(expr);
   return static_cast<constant_exprt &>(expr);
 }
 
@@ -3534,10 +3549,8 @@ inline const class_method_descriptor_exprt &
 to_class_method_descriptor_expr(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_virtual_function);
-  const class_method_descriptor_exprt &ret =
-    static_cast<const class_method_descriptor_exprt &>(expr);
-  validate_expr(ret);
-  return ret;
+  class_method_descriptor_exprt::check(expr);
+  return static_cast<const class_method_descriptor_exprt &>(expr);
 }
 
 template <>