elaborate typing of std_expr expression classes

Author: kroening

src/util/std_expr.h

@@ -1329,32 +1329,28 @@ inline void validate_expr(const notequal_exprt &value)
 
 /*! \brief array index operator
 */
-class index_exprt:public exprt
+class index_exprt:public binary_exprt
 {
 public:
-  index_exprt():exprt(ID_index)
+  index_exprt():binary_exprt(ID_index)
   {
-    operands().resize(2);
   }
 
-  explicit index_exprt(const typet &_type):exprt(ID_index, _type)
+  explicit index_exprt(const typet &_type):binary_exprt(ID_index, _type)
   {
-    operands().resize(2);
   }
 
   index_exprt(const exprt &_array, const exprt &_index):
-    exprt(ID_index, _array.type().subtype())
+    binary_exprt(_array, ID_index, _index, _array.type().subtype())
   {
-    copy_to_operands(_array, _index);
   }
 
   index_exprt(
     const exprt &_array,
     const exprt &_index,
     const typet &_type):
-    exprt(ID_index, _type)
+    binary_exprt(_array, ID_index, _index, _type)
   {
-    copy_to_operands(_array, _index);
   }
 
   exprt &array()
@@ -1795,12 +1791,11 @@ class namespacet;
 
 /*! \brief split an expression into a base object and a (byte) offset
 */
-class object_descriptor_exprt:public exprt
+class object_descriptor_exprt:public binary_exprt
 {
 public:
-  object_descriptor_exprt():exprt(ID_object_descriptor)
+  object_descriptor_exprt():binary_exprt(ID_object_descriptor)
   {
-    operands().resize(2);
     op0().id(ID_unknown);
     op1().id(ID_unknown);
   }
@@ -1886,20 +1881,18 @@ inline void validate_expr(const object_descriptor_exprt &value)
 
 /*! \brief TO_BE_DOCUMENTED
 */
-class dynamic_object_exprt:public exprt
+class dynamic_object_exprt:public binary_exprt
 {
 public:
-  dynamic_object_exprt():exprt(ID_dynamic_object)
+  dynamic_object_exprt():binary_exprt(ID_dynamic_object)
   {
-    operands().resize(2);
     op0().id(ID_unknown);
     op1().id(ID_unknown);
   }
 
   explicit dynamic_object_exprt(const typet &type):
-    exprt(ID_dynamic_object, type)
+    binary_exprt(ID_dynamic_object, type)
   {
-    operands().resize(2);
     op0().id(ID_unknown);
     op1().id(ID_unknown);
   }
@@ -1955,6 +1948,7 @@ template<> inline bool can_cast_expr<dynamic_object_exprt>(const exprt &base)
 {
   return base.id()==ID_dynamic_object;
 }
+
 inline void validate_expr(const dynamic_object_exprt &value)
 {
   validate_operands(value, 2, "Dynamic object must have two operands");
@@ -1963,18 +1957,16 @@ inline void validate_expr(const dynamic_object_exprt &value)
 
 /*! \brief semantic type conversion
 */
-class typecast_exprt:public exprt
+class typecast_exprt:public unary_exprt
 {
 public:
-  explicit typecast_exprt(const typet &_type):exprt(ID_typecast, _type)
+  explicit typecast_exprt(const typet &_type):unary_exprt(ID_typecast, _type)
   {
-    operands().resize(1);
   }
 
   typecast_exprt(const exprt &op, const typet &_type):
-    exprt(ID_typecast, _type)
+    unary_exprt(ID_typecast, op, _type)
   {
-    copy_to_operands(op);
   }
 
   exprt &op()
@@ -3031,17 +3023,17 @@ inline void validate_expr(const address_of_exprt &value)
 
 /*! \brief Boolean negation
 */
-class not_exprt:public exprt
+class not_exprt:public unary_exprt
 {
 public:
-  explicit not_exprt(const exprt &op):exprt(ID_not, bool_typet())
+  explicit not_exprt(const exprt &op):
+    unary_exprt(ID_not, op) // type from op.type()
   {
-    copy_to_operands(op);
+    PRECONDITION(op.type().id()==ID_bool);
   }
 
-  not_exprt():exprt(ID_not, bool_typet())
+  not_exprt():unary_exprt(ID_not, bool_typet())
   {
-    operands().resize(1);
   }
 
   exprt &op()
@@ -3086,6 +3078,7 @@ template<> inline bool can_cast_expr<not_exprt>(const exprt &base)
 {
   return base.id()==ID_not;
 }
+
 inline void validate_expr(const not_exprt &value)
 {
   validate_operands(value, 1, "Not must have one operand");
@@ -3094,30 +3087,27 @@ inline void validate_expr(const not_exprt &value)
 
 /*! \brief Operator to dereference a pointer
 */
-class dereference_exprt:public exprt
+class dereference_exprt:public unary_exprt
 {
 public:
-  explicit dereference_exprt(const typet &type):
-    exprt(ID_dereference, type)
+  dereference_exprt():unary_exprt(ID_dereference)
   {
-    operands().resize(1);
   }
 
-  explicit dereference_exprt(const exprt &op):
-    exprt(ID_dereference)
+  explicit dereference_exprt(const typet &type):
+    unary_exprt(ID_dereference, type)
   {
-    copy_to_operands(op);
   }
 
-  dereference_exprt(const exprt &op, const typet &type):
-    exprt(ID_dereference, type)
+  explicit dereference_exprt(const exprt &op):
+    unary_exprt(ID_dereference, op, op.type().subtype())
   {
-    copy_to_operands(op);
+    PRECONDITION(op.type().id()==ID_pointer);
   }
 
-  dereference_exprt():exprt(ID_dereference)
+  dereference_exprt(const exprt &op, const typet &type):
+    unary_exprt(ID_dereference, op, type)
   {
-    operands().resize(1);
   }
 
   exprt &pointer()
@@ -3684,39 +3674,33 @@ inline void validate_expr(const array_update_exprt &value)
 
 /*! \brief Extract member of struct or union
 */
-class member_exprt:public exprt
+class member_exprt:public unary_exprt
 {
 public:
-  explicit member_exprt(const exprt &op):exprt(ID_member)
+  // deprecated, and will go away -- use either of the two below
+  explicit member_exprt(const typet &_type):unary_exprt(ID_member, _type)
   {
-    copy_to_operands(op);
   }
 
-  explicit member_exprt(const typet &_type):exprt(ID_member, _type)
-  {
-    operands().resize(1);
-  }
-
-  member_exprt(const exprt &op, const irep_idt &component_name):
-    exprt(ID_member)
+  member_exprt(
+    const exprt &op,
+    const irep_idt &component_name,
+    const typet &_type):
+    unary_exprt(ID_member, op, _type)
   {
-    copy_to_operands(op);
     set_component_name(component_name);
   }
 
   member_exprt(
     const exprt &op,
-    const irep_idt &component_name,
-    const typet &_type):
-    exprt(ID_member, _type)
+    const struct_typet::componentt &c):
+    unary_exprt(ID_member, op, c.type())
   {
-    copy_to_operands(op);
-    set_component_name(component_name);
+    set_component_name(c.get_name());
   }
 
-  member_exprt():exprt(ID_member)
+  member_exprt():unary_exprt(ID_member)
   {
-    operands().resize(1);
   }
 
   irep_idt get_component_name() const
@@ -3734,11 +3718,6 @@ class member_exprt:public exprt
     return get_size_t(ID_component_number);
   }
 
-  void set_component_number(std::size_t component_number)
-  {
-    set(ID_component_number, component_number);
-  }
-
   // will go away, use compound()
   const exprt &struct_op() const
   {
@@ -3769,6 +3748,7 @@ class member_exprt:public exprt
     {
       return static_cast<const member_exprt &>(op).symbol();
     }
+
     return to_symbol_expr(op);
   }
 };
@@ -4359,18 +4339,18 @@ class null_pointer_exprt:public constant_exprt
 
 /*! \brief application of (mathematical) function
 */
-class function_application_exprt:public exprt
+class function_application_exprt:public binary_exprt
 {
 public:
-  function_application_exprt():exprt(ID_function_application)
+  function_application_exprt():binary_exprt(ID_function_application)
   {
-    operands().resize(2);
+    op0()=symbol_exprt();
   }
 
   explicit function_application_exprt(const typet &_type):
-    exprt(ID_function_application, _type)
+    binary_exprt(ID_function_application, _type)
   {
-    operands().resize(2);
+    op0()=symbol_exprt();
   }
 
   function_application_exprt(
@@ -4380,14 +4360,14 @@ class function_application_exprt:public exprt
     function()=_function;
   }
 
-  exprt &function()
+  symbol_exprt &function()
   {
-    return op0();
+    return static_cast<symbol_exprt &>(op0());
   }
 
-  const exprt &function() const
+  const symbol_exprt &function() const
   {
-    return op0();
+    return static_cast<const symbol_exprt &>(op0());
   }
 
   typedef exprt::operandst argumentst;
@@ -4612,12 +4592,11 @@ inline void validate_expr(const let_exprt &value)
 
 /*! \brief A forall expression
 */
-class forall_exprt:public exprt
+class forall_exprt:public binary_exprt
 {
 public:
-  forall_exprt():exprt(ID_forall)
+  forall_exprt():binary_exprt(ID_forall)
   {
-    operands().resize(2);
     op0()=symbol_exprt();
   }
 
@@ -4644,12 +4623,11 @@ class forall_exprt:public exprt
 
 /*! \brief An exists expression
 */
-class exists_exprt:public exprt
+class exists_exprt:public binary_exprt
 {
 public:
-  exists_exprt():exprt(ID_exists)
+  exists_exprt():binary_exprt(ID_exists)
   {
-    operands().resize(2);
     op0()=symbol_exprt();
   }