fix exprt::opX() accesses in cpp/

This improves type safety.

Author: Daniel Kroening

src/cpp/cpp_constructor.cpp

@@ -235,8 +235,8 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
     assert(initializer.id()==ID_code &&
            initializer.get(ID_statement)==ID_expression);
 
-    side_effect_expr_function_callt &func_ini=
-      to_side_effect_expr_function_call(initializer.op0());
+    side_effect_expr_function_callt &func_ini =
+      to_side_effect_expr_function_call(to_unary_expr(initializer).op());
 
     exprt &tmp_this=func_ini.arguments().front();
     DATA_INVARIANT(

src/cpp/cpp_static_assert.h

@@ -12,14 +12,13 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_CPP_CPP_STATIC_ASSERT_H
 #define CPROVER_CPP_CPP_STATIC_ASSERT_H
 
-#include <util/expr.h>
+#include <util/std_expr.h>
 
-class cpp_static_assertt:public exprt
+class cpp_static_assertt : public binary_exprt
 {
 public:
-  cpp_static_assertt():exprt(ID_cpp_static_assert)
+  cpp_static_assertt() : binary_exprt(ID_cpp_static_assert)
   {
-    operands().resize(2);
   }
 
   exprt &cond()

src/cpp/cpp_typecheck.cpp

@@ -243,7 +243,7 @@ void cpp_typecheckt::do_not_typechecked()
         }
         else if(symbol.value.operands().size()==1)
         {
-          value = symbol.value.op0();
+          value = to_unary_expr(symbol.value).op();
           cont=true;
         }
         else

src/cpp/cpp_typecheck_code.cpp

@@ -55,22 +55,29 @@ void cpp_typecheckt::typecheck_code(codet &code)
     // as an extension, we support indexed access into signed/unsigned
     // bitvectors, typically used with __CPROVER::(un)signedbv<N>
     exprt &expr = code.op0();
-    if(
-      expr.operands().size() == 2 && expr.op0().id() == ID_index &&
-      expr.op0().operands().size() == 2)
+
+    if(expr.operands().size() == 2)
     {
-      exprt array = expr.op0().op0();
-      typecheck_expr(array);
+      auto &binary_expr = to_binary_expr(expr);
 
-      if(array.type().id() == ID_signedbv || array.type().id() == ID_unsignedbv)
+      if(binary_expr.op0().id() == ID_index)
       {
-        shl_exprt shl{from_integer(1, array.type()), expr.op0().op1()};
-        exprt rhs =
-          if_exprt{equal_exprt{expr.op1(), from_integer(0, array.type())},
-                   bitand_exprt{array, bitnot_exprt{shl}},
-                   bitor_exprt{array, shl}};
-        expr.op0() = expr.op0().op0();
-        expr.op1() = rhs;
+        exprt array = to_index_expr(binary_expr.op0()).array();
+        typecheck_expr(array);
+
+        if(
+          array.type().id() == ID_signedbv ||
+          array.type().id() == ID_unsignedbv)
+        {
+          shl_exprt shl{from_integer(1, array.type()),
+                        to_index_expr(binary_expr.op0()).index()};
+          exprt rhs = if_exprt{
+            equal_exprt{binary_expr.op1(), from_integer(0, array.type())},
+            bitand_exprt{array, bitnot_exprt{shl}},
+            bitor_exprt{array, shl}};
+          binary_expr.op0() = to_index_expr(binary_expr.op0()).array();
+          binary_expr.op1() = rhs;
+        }
       }
     }
 
@@ -191,8 +198,10 @@ void cpp_typecheckt::typecheck_switch(codet &code)
     assert(decl.operands().size()==1);
 
     // replace declaration by its symbol
-    assert(decl.op0().op0().id()==ID_symbol);
-    value = decl.op0().op0();
+    DATA_INVARIANT(
+      to_unary_expr(decl).op().op0().id() == ID_symbol,
+      "declaration must have symbol as operand");
+    value = to_unary_expr(decl).op().op0();
 
     c_typecheck_baset::typecheck_switch(code);
 
@@ -287,11 +296,11 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
     // a reference member
     if(
       symbol_expr.id() == ID_dereference &&
-      symbol_expr.op0().id() == ID_member &&
+      to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
       symbol_expr.get_bool(ID_C_implicit))
     {
       // treat references as normal pointers
-      exprt tmp = symbol_expr.op0();
+      exprt tmp = to_dereference_expr(symbol_expr).pointer();
       symbol_expr.swap(tmp);
     }
 
@@ -316,18 +325,20 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
 
       if(
         symbol_expr.id() == ID_dereference &&
-        symbol_expr.op0().id() == ID_member &&
+        to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
         symbol_expr.get_bool(ID_C_implicit))
       {
         // treat references as normal pointers
-        exprt tmp = symbol_expr.op0();
+        exprt tmp = to_dereference_expr(symbol_expr).pointer();
         symbol_expr.swap(tmp);
       }
     }
 
-    if(symbol_expr.id() == ID_member &&
-       symbol_expr.op0().id() == ID_dereference &&
-       symbol_expr.op0().op0() == cpp_scopes.current_scope().this_expr)
+    if(
+      symbol_expr.id() == ID_member &&
+      to_member_expr(symbol_expr).op().id() == ID_dereference &&
+      to_dereference_expr(to_member_expr(symbol_expr).op()).pointer() ==
+        cpp_scopes.current_scope().this_expr)
     {
       if(is_reference(symbol_expr.type()))
       {

src/cpp/cpp_typecheck_compound_type.cpp

@@ -1278,7 +1278,10 @@ void cpp_typecheckt::typecheck_member_function(
   }
 
   if(value.id() == ID_cpp_not_typechecked && value.has_operands())
-    move_member_initializers(initializers, type, value.op0());
+  {
+    move_member_initializers(
+      initializers, type, to_multi_ary_expr(value).op0());
+  }
   else
     move_member_initializers(initializers, type, value);
 

src/cpp/cpp_typecheck_constructor.cpp

@@ -69,9 +69,8 @@ static void copy_member(
   op1.add_source_location()=source_location;
 
   side_effect_exprt assign(ID_assign, typet(), source_location);
-  assign.copy_to_operands(op0.as_expr());
-  assign.op0().add_source_location() = source_location;
-  assign.copy_to_operands(op1);
+  assign.copy_to_operands(op0.as_expr(), op1);
+  to_binary_expr(assign).op0().add_source_location() = source_location;
 
   code_expressiont code(assign);
   code.add_source_location() = source_location;
@@ -105,10 +104,10 @@ static void copy_array(
   side_effect_exprt assign(ID_assign, typet(), source_location);
 
   assign.copy_to_operands(index_exprt(array.as_expr(), constant));
-  assign.op0().add_source_location() = source_location;
-
   assign.copy_to_operands(index_exprt(member, constant));
-  assign.op1().add_source_location() = source_location;
+
+  to_binary_expr(assign).op0().add_source_location() = source_location;
+  to_binary_expr(assign).op1().add_source_location() = source_location;
 
   code_expressiont code(assign);
   code.add_source_location() = source_location;
@@ -295,7 +294,7 @@ void cpp_typecheckt::default_assignop(
   cpctor.operands().push_back(exprt(ID_cpp_declarator));
   cpctor.add_source_location()=source_location;
 
-  cpp_declaratort &declarator=(cpp_declaratort&) cpctor.op0();
+  cpp_declaratort &declarator = static_cast<cpp_declaratort &>(cpctor.op0());
   declarator.add_source_location()=source_location;
 
   cpp_namet &declarator_name=declarator.name();

src/cpp/cpp_typecheck_conversions.cpp

@@ -894,7 +894,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
 
           // simplify address
           if(expr.id()==ID_dereference)
-            address=expr.op0();
+            address = to_dereference_expr(expr).pointer();
 
           pointer_typet ptr_sub=pointer_type(type);
           c_qualifierst qual_from;
@@ -1333,8 +1333,9 @@ bool cpp_typecheckt::reference_binding(
            reference_compatible(returned_value, type, rank))
         {
           // returned values are lvalues in case of references only
-          assert(returned_value.id()==ID_dereference &&
-                 is_reference(returned_value.op0().type()));
+          DATA_INVARIANT(
+            is_reference(to_dereference_expr(returned_value).op().type()),
+            "the returned value must be pointer to reference");
 
           new_expr=returned_value.op0();
 
@@ -1484,7 +1485,7 @@ void cpp_typecheckt::implicit_typecast(exprt &expr, const typet &type)
     e.id() == ID_initializer_list && cpp_is_pod(type) &&
     e.operands().size() == 1)
   {
-    e = expr.op0();
+    e = to_unary_expr(expr).op();
   }
 
   if(!implicit_conversion_sequence(e, type, expr))
@@ -1696,7 +1697,7 @@ bool cpp_typecheckt::dynamic_typecast(
   if(type.id()==ID_pointer)
   {
     if(e.id()==ID_dereference && e.get_bool(ID_C_implicit))
-      e=expr.op0();
+      e = to_dereference_expr(expr).pointer();
 
     if(e.type().id()==ID_pointer &&
        cast_away_constness(e.type(), type))
@@ -1749,7 +1750,7 @@ bool cpp_typecheckt::reinterpret_typecast(
   if(check_constantness && type.id()==ID_pointer)
   {
     if(e.id()==ID_dereference && e.get_bool(ID_C_implicit))
-      e=expr.op0();
+      e = to_dereference_expr(expr).pointer();
 
     if(e.type().id()==ID_pointer &&
        cast_away_constness(e.type(), type))
@@ -1845,7 +1846,7 @@ bool cpp_typecheckt::static_typecast(
   if(check_constantness && type.id()==ID_pointer)
   {
     if(e.id()==ID_dereference && e.get_bool(ID_C_implicit))
-      e=expr.op0();
+      e = to_dereference_expr(expr).pointer();
 
     if(e.type().id()==ID_pointer &&
        cast_away_constness(e.type(), type))
@@ -1884,8 +1885,8 @@ bool cpp_typecheckt::static_typecast(
       {
         if(e.id()==ID_dereference)
         {
-          make_ptr_typecast(e.op0(), type);
-          new_expr.swap(e.op0());
+          make_ptr_typecast(to_dereference_expr(e).pointer(), type);
+          new_expr.swap(to_dereference_expr(e).pointer());
           return true;
         }
 

src/cpp/cpp_typecheck_function.cpp

@@ -123,8 +123,10 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
     PRECONDITION(symbol.value.get(ID_statement) == ID_block);
 
     if(
-      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
-      symbol.value.op0().op0().id() != ID_already_typechecked)
+      !symbol.value.has_operands() ||
+      !to_multi_ary_expr(symbol.value).op0().has_operands() ||
+      to_multi_ary_expr(symbol.value).op0().op0().id() !=
+        ID_already_typechecked)
     {
       symbol.value.copy_to_operands(
         dtor(msymb, to_symbol_expr(function_scope.this_expr)));

src/cpp/expr2cpp.cpp

@@ -404,7 +404,7 @@ std::string expr2cppt::convert_code_cpp_delete(
     return convert_norep(src, precedence);
   }
 
-  std::string tmp=convert(src.op0());
+  std::string tmp = convert(to_unary_expr(src).op());
 
   dest+=tmp+";\n";
 
@@ -476,16 +476,17 @@ std::string expr2cppt::convert_code(
 
 std::string expr2cppt::convert_extractbit(const exprt &src)
 {
-  assert(src.operands().size()==2);
-  return convert(src.op0())+"["+convert(src.op1())+"]";
+  const auto &extractbit_expr = to_extractbit_expr(src);
+  return convert(extractbit_expr.op0()) + "[" + convert(extractbit_expr.op1()) +
+         "]";
 }
 
 std::string expr2cppt::convert_extractbits(const exprt &src)
 {
-  assert(src.operands().size()==3);
-  return
-    convert(src.op0())+".range("+convert(src.op1())+ ","+
-    convert(src.op2())+")";
+  const auto &extractbits_expr = to_extractbits_expr(src);
+  return convert(extractbits_expr.src()) + ".range(" +
+         convert(extractbits_expr.upper()) + "," +
+         convert(extractbits_expr.lower()) + ")";
 }
 
 std::string expr2cpp(const exprt &expr, const namespacet &ns)