avoid access to exprt::op0 and op1

Author: Daniel Kroening

src/analyses/flow_insensitive_analysis.cpp

@@ -317,24 +317,15 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
   }
   else if(function.id()==ID_if)
   {
-    if(function.operands().size()!=3)
-      throw "if takes three arguments";
+    const auto &if_expr = to_if_expr(function);
 
-    new_data =
-      do_function_call_rec(
-        l_call,
-        function.op1(),
-        arguments,
-        state,
-        goto_functions);
+    new_data = do_function_call_rec(
+      l_call, if_expr.true_case(), arguments, state, goto_functions);
 
     new_data =
       do_function_call_rec(
-        l_call,
-        function.op2(),
-        arguments,
-        state,
-        goto_functions) || new_data;
+        l_call, if_expr.false_case(), arguments, state, goto_functions) ||
+      new_data;
   }
   else if(function.id()==ID_dereference)
   {

src/analyses/interval_domain.cpp

@@ -339,25 +339,25 @@ void interval_domaint::assume_rec(
      cond.id()==ID_gt || cond.id()==ID_ge ||
      cond.id()==ID_equal || cond.id()==ID_notequal)
   {
-    assert(cond.operands().size()==2);
+    const auto &rel = to_binary_relation_expr(cond);
 
     if(negation) // !x<y  ---> x>=y
     {
-      if(cond.id()==ID_lt)
-        assume_rec(cond.op0(), ID_ge, cond.op1());
-      else if(cond.id()==ID_le)
-        assume_rec(cond.op0(), ID_gt, cond.op1());
-      else if(cond.id()==ID_gt)
-        assume_rec(cond.op0(), ID_le, cond.op1());
-      else if(cond.id()==ID_ge)
-        assume_rec(cond.op0(), ID_lt, cond.op1());
-      else if(cond.id()==ID_equal)
-        assume_rec(cond.op0(), ID_notequal, cond.op1());
-      else if(cond.id()==ID_notequal)
-        assume_rec(cond.op0(), ID_equal, cond.op1());
+      if(rel.id() == ID_lt)
+        assume_rec(rel.op0(), ID_ge, rel.op1());
+      else if(rel.id() == ID_le)
+        assume_rec(rel.op0(), ID_gt, rel.op1());
+      else if(rel.id() == ID_gt)
+        assume_rec(rel.op0(), ID_le, rel.op1());
+      else if(rel.id() == ID_ge)
+        assume_rec(rel.op0(), ID_lt, rel.op1());
+      else if(rel.id() == ID_equal)
+        assume_rec(rel.op0(), ID_notequal, rel.op1());
+      else if(rel.id() == ID_notequal)
+        assume_rec(rel.op0(), ID_equal, rel.op1());
     }
     else
-      assume_rec(cond.op0(), cond.id(), cond.op1());
+      assume_rec(rel.op0(), rel.id(), rel.op1());
   }
   else if(cond.id()==ID_not)
   {

src/analyses/invariant_set.cpp

@@ -95,21 +95,24 @@ std::string inv_object_storet::build_string(const exprt &expr) const
   // we ignore some casts
   if(expr.id()==ID_typecast)
   {
-    assert(expr.operands().size()==1);
+    const auto &typecast_expr = to_typecast_expr(expr);
 
-    if(expr.type().id()==ID_signedbv ||
-       expr.type().id()==ID_unsignedbv)
+    if(
+      typecast_expr.type().id() == ID_signedbv ||
+      typecast_expr.type().id() == ID_unsignedbv)
     {
-      if(expr.op0().type().id()==ID_signedbv ||
-         expr.op0().type().id()==ID_unsignedbv)
+      if(
+        typecast_expr.op().type().id() == ID_signedbv ||
+        typecast_expr.op().type().id() == ID_unsignedbv)
       {
-        if(to_bitvector_type(expr.type()).get_width()>=
-           to_bitvector_type(expr.op0().type()).get_width())
-          return build_string(expr.op0());
+        if(
+          to_bitvector_type(typecast_expr.type()).get_width() >=
+          to_bitvector_type(typecast_expr.op().type()).get_width())
+          return build_string(typecast_expr.op());
       }
-      else if(expr.op0().type().id()==ID_bool)
+      else if(typecast_expr.op().type().id() == ID_bool)
       {
-        return build_string(expr.op0());
+        return build_string(typecast_expr.op());
       }
     }
   }
@@ -137,8 +140,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const
 
   if(expr.id()==ID_member)
   {
-    assert(expr.operands().size()==1);
-    return build_string(expr.op0())+"."+expr.get_string(ID_component_name);
+    return build_string(to_member_expr(expr).struct_op()) + "." +
+           expr.get_string(ID_component_name);
   }
 
   if(expr.id()==ID_symbol)
@@ -158,8 +161,7 @@ bool invariant_sett::get_object(
 bool inv_object_storet::is_constant_address(const exprt &expr)
 {
   if(expr.id()==ID_address_of)
-    if(expr.operands().size()==1)
-      return is_constant_address_rec(expr.op0());
+    return is_constant_address_rec(to_address_of_expr(expr).object());
 
   return false;
 }
@@ -169,15 +171,12 @@ bool inv_object_storet::is_constant_address_rec(const exprt &expr)
   if(expr.id()==ID_symbol)
     return true;
   else if(expr.id()==ID_member)
-  {
-    assert(expr.operands().size()==1);
-    return is_constant_address_rec(expr.op0());
-  }
+    return is_constant_address_rec(to_member_expr(expr).struct_op());
   else if(expr.id()==ID_index)
   {
-    assert(expr.operands().size()==2);
-    if(expr.op1().is_constant())
-      return is_constant_address_rec(expr.op0());
+    const auto &index_expr = to_index_expr(expr);
+    if(index_expr.index().is_constant())
+      return is_constant_address_rec(index_expr.array());
   }
 
   return false;
@@ -429,14 +428,14 @@ void invariant_sett::strengthen_rec(const exprt &expr)
   else if(expr.id()==ID_le ||
           expr.id()==ID_lt)
   {
-    assert(expr.operands().size()==2);
+    const auto &rel = to_binary_relation_expr(expr);
 
     // special rule: x <= (a & b)
     // implies:      x<=a && x<=b
 
-    if(expr.op1().id()==ID_bitand)
+    if(rel.op1().id() == ID_bitand)
     {
-      const exprt &bitand_op=expr.op1();
+      const exprt &bitand_op = rel.op1();
 
       forall_operands(it, bitand_op)
       {
@@ -450,12 +449,11 @@ void invariant_sett::strengthen_rec(const exprt &expr)
 
     std::pair<unsigned, unsigned> p;
 
-    if(get_object(expr.op0(), p.first) ||
-       get_object(expr.op1(), p.second))
+    if(get_object(rel.op0(), p.first) || get_object(rel.op1(), p.second))
       return;
 
-    const auto i0 = numeric_cast<mp_integer>(expr.op0());
-    const auto i1 = numeric_cast<mp_integer>(expr.op1());
+    const auto i0 = numeric_cast<mp_integer>(rel.op0());
+    const auto i1 = numeric_cast<mp_integer>(rel.op1());
 
     if(expr.id()==ID_le)
     {
@@ -483,9 +481,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
   }
   else if(expr.id()==ID_equal)
   {
-    assert(expr.operands().size()==2);
+    const auto &equal_expr = to_equal_expr(expr);
 
-    const typet &op_type=ns->follow(expr.op0().type());
+    const typet &op_type = ns->follow(equal_expr.op0().type());
 
     if(op_type.id()==ID_struct)
     {
@@ -495,9 +493,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
       for(const auto &comp : struct_type.components())
       {
         const member_exprt lhs_member_expr(
-          expr.op0(), comp.get_name(), comp.type());
+          equal_expr.op0(), comp.get_name(), comp.type());
         const member_exprt rhs_member_expr(
-          expr.op1(), comp.get_name(), comp.type());
+          equal_expr.op1(), comp.get_name(), comp.type());
 
         const equal_exprt equality(lhs_member_expr, rhs_member_expr);
 
@@ -511,48 +509,49 @@ void invariant_sett::strengthen_rec(const exprt &expr)
     // special rule: x = (a & b)
     // implies:      x<=a && x<=b
 
-    if(expr.op1().id()==ID_bitand)
+    if(equal_expr.op1().id() == ID_bitand)
     {
-      const exprt &bitand_op=expr.op1();
+      const exprt &bitand_op = equal_expr.op1();
 
       forall_operands(it, bitand_op)
       {
-        exprt tmp(expr);
+        exprt tmp(equal_expr);
         tmp.op1()=*it;
         tmp.id(ID_le);
         strengthen_rec(tmp);
       }
 
       return;
     }
-    else if(expr.op0().id()==ID_bitand)
+    else if(equal_expr.op0().id() == ID_bitand)
     {
-      exprt tmp(expr);
+      exprt tmp(equal_expr);
       std::swap(tmp.op0(), tmp.op1());
       strengthen_rec(tmp);
       return;
     }
 
     // special rule: x = (type) y
-    if(expr.op1().id()==ID_typecast)
+    if(equal_expr.op1().id() == ID_typecast)
     {
-      assert(expr.op1().operands().size()==1);
-      add_type_bounds(expr.op0(), expr.op1().op0().type());
+      assert(equal_expr.op1().operands().size() == 1);
+      add_type_bounds(equal_expr.op0(), equal_expr.op1().op0().type());
     }
-    else if(expr.op0().id()==ID_typecast)
+    else if(equal_expr.op0().id() == ID_typecast)
     {
-      assert(expr.op0().operands().size()==1);
-      add_type_bounds(expr.op1(), expr.op0().op0().type());
+      assert(equal_expr.op0().operands().size() == 1);
+      add_type_bounds(equal_expr.op1(), equal_expr.op0().op0().type());
     }
 
     std::pair<unsigned, unsigned> p, s;
 
-    if(get_object(expr.op0(), p.first) ||
-       get_object(expr.op1(), p.second))
+    if(
+      get_object(equal_expr.op0(), p.first) ||
+      get_object(equal_expr.op1(), p.second))
       return;
 
-    const auto i0 = numeric_cast<mp_integer>(expr.op0());
-    const auto i1 = numeric_cast<mp_integer>(expr.op1());
+    const auto i0 = numeric_cast<mp_integer>(equal_expr.op0());
+    const auto i1 = numeric_cast<mp_integer>(equal_expr.op1());
     if(i0.has_value())
       add_bounds(p.second, boundst(*i0));
     else if(i1.has_value())
@@ -569,12 +568,13 @@ void invariant_sett::strengthen_rec(const exprt &expr)
   }
   else if(expr.id()==ID_notequal)
   {
-    assert(expr.operands().size()==2);
+    const auto &notequal_expr = to_notequal_expr(expr);
 
     std::pair<unsigned, unsigned> p;
 
-    if(get_object(expr.op0(), p.first) ||
-       get_object(expr.op1(), p.second))
+    if(
+      get_object(notequal_expr.op0(), p.first) ||
+      get_object(notequal_expr.op1(), p.second))
       return;
 
     // check if this is a contradiction
@@ -629,19 +629,19 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
           expr.id()==ID_equal ||
           expr.id()==ID_notequal)
   {
-    assert(expr.operands().size()==2);
+    const auto &rel = to_binary_relation_expr(expr);
 
     std::pair<unsigned, unsigned> p;
 
-    bool ob0=get_object(expr.op0(), p.first);
-    bool ob1=get_object(expr.op1(), p.second);
+    bool ob0 = get_object(rel.op0(), p.first);
+    bool ob1 = get_object(rel.op1(), p.second);
 
     if(ob0 || ob1)
       return tvt::unknown();
 
     tvt r;
 
-    if(expr.id()==ID_le)
+    if(rel.id() == ID_le)
     {
       r=is_le(p);
       if(!r.is_unknown())
@@ -653,7 +653,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
 
       return b0<=b1;
     }
-    else if(expr.id()==ID_lt)
+    else if(rel.id() == ID_lt)
     {
       r=is_lt(p);
       if(!r.is_unknown())
@@ -665,9 +665,9 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
 
       return b0<b1;
     }
-    else if(expr.id()==ID_equal)
+    else if(rel.id() == ID_equal)
       return is_eq(p);
-    else if(expr.id()==ID_notequal)
+    else if(rel.id() == ID_notequal)
       return is_ne(p);
     else
       UNREACHABLE;
@@ -717,10 +717,9 @@ void invariant_sett::nnf(exprt &expr, bool negate)
   }
   else if(expr.id()==ID_not)
   {
-    assert(expr.operands().size()==1);
-    nnf(expr.op0(), !negate);
+    nnf(to_not_expr(expr).op(), !negate);
     exprt tmp;
-    tmp.swap(expr.op0());
+    tmp.swap(to_not_expr(expr).op());
     expr.swap(tmp);
   }
   else if(expr.id()==ID_and)
@@ -741,14 +740,15 @@ void invariant_sett::nnf(exprt &expr, bool negate)
   }
   else if(expr.id()==ID_typecast)
   {
-    assert(expr.operands().size()==1);
+    const auto &typecast_expr = to_typecast_expr(expr);
 
-    if(expr.op0().type().id()==ID_unsignedbv ||
-       expr.op0().type().id()==ID_signedbv)
+    if(
+      typecast_expr.op().type().id() == ID_unsignedbv ||
+      typecast_expr.op().type().id() == ID_signedbv)
     {
       equal_exprt tmp;
-      tmp.lhs()=expr.op0();
-      tmp.rhs()=from_integer(0, expr.op0().type());
+      tmp.lhs() = typecast_expr.op();
+      tmp.rhs() = from_integer(0, typecast_expr.op().type());
       nnf(tmp, !negate);
       expr.swap(tmp);
     }

src/goto-symex/symex_builtin_functions.cpp

@@ -281,12 +281,13 @@ irep_idt get_string_argument_rec(const exprt &src)
     PRECONDITION(src.operands().size() == 1);
     if(src.op0().id()==ID_index)
     {
-      PRECONDITION(src.op0().operands().size() == 2);
+      const auto &index_expr = to_index_expr(src.op0());
 
-      if(src.op0().op0().id()==ID_string_constant &&
-         src.op0().op1().is_zero())
+      if(
+        index_expr.array().id() == ID_string_constant &&
+        index_expr.index().is_zero())
       {
-        const exprt &fmt_str=src.op0().op0();
+        const exprt &fmt_str = index_expr.array();
         return fmt_str.get_string(ID_value);
       }
     }