Merge pull request #4962 from diffblue/goto-symex-opX

fix exprt::opX accesses in goto-symex

Author: Daniel Kroening

src/goto-symex/expr_skeleton.cpp

@@ -21,7 +21,7 @@ expr_skeletont expr_skeletont::remove_op0(exprt e)
 {
   PRECONDITION(e.id() != ID_symbol);
   PRECONDITION(e.operands().size() >= 1);
-  e.op0().make_nil();
+  to_multi_ary_expr(e).op0().make_nil();
   return expr_skeletont{std::move(e)};
 }
 
@@ -39,7 +39,7 @@ exprt expr_skeletont::apply(exprt expr) const
     INVARIANT(
       p->operands().size() >= 1,
       "expected pointed-to expression to have at least one operand");
-    p = &p->op0();
+    p = &to_multi_ary_expr(*p).op0();
   }
 
   INVARIANT(p->is_nil(), "expected pointed-to expression to be nil");

src/goto-symex/symex_builtin_functions.cpp

@@ -58,7 +58,7 @@ void goto_symext::symex_allocate(
 
   dynamic_counter++;
 
-  exprt size=code.op0();
+  exprt size = to_binary_expr(code).op0();
   optionalt<typet> object_type;
   auto function_symbol = outer_symbol_table.lookup(state.source.function_id);
   INVARIANT(function_symbol, "function associated with allocation not found");
@@ -93,16 +93,19 @@ void goto_symext::symex_allocate(
         else if(
           !alloc_size.has_value() && tmp_size.id() == ID_mult &&
           tmp_size.operands().size() == 2 &&
-          (tmp_size.op0().is_constant() || tmp_size.op1().is_constant()))
+          (to_mult_expr(tmp_size).op0().is_constant() ||
+           to_mult_expr(tmp_size).op1().is_constant()))
         {
-          exprt s=tmp_size.op0();
+          exprt s = to_mult_expr(tmp_size).op0();
           if(s.is_constant())
           {
-            s=tmp_size.op1();
-            PRECONDITION(*c_sizeof_type_rec(tmp_size.op0()) == *tmp_type);
+            s = to_mult_expr(tmp_size).op1();
+            PRECONDITION(
+              *c_sizeof_type_rec(to_mult_expr(tmp_size).op0()) == *tmp_type);
           }
           else
-            PRECONDITION(*c_sizeof_type_rec(tmp_size.op1()) == *tmp_type);
+            PRECONDITION(
+              *c_sizeof_type_rec(to_mult_expr(tmp_size).op1()) == *tmp_type);
 
           object_type = array_typet(*tmp_type, s);
         }
@@ -167,7 +170,7 @@ void goto_symext::symex_allocate(
   state.symbol_table.add(value_symbol);
 
   // to allow constant propagation
-  exprt zero_init = state.rename(code.op1(), ns).get();
+  exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -258,7 +261,7 @@ void goto_symext::symex_va_start(
 
   // create an array holding pointers to the parameters, starting after the
   // parameter that the operand points to
-  const exprt &op = skip_typecast(code.op0());
+  const exprt &op = skip_typecast(to_unary_expr(code).op());
   // this must be the address of a symbol
   const irep_idt start_parameter =
     to_ssa_expr(to_address_of_expr(op).object()).get_object_name();

src/goto-symex/symex_goto.cpp

@@ -60,11 +60,15 @@ void goto_symext::apply_goto_condition(
   // Could use not_exprt + simplify, but let's avoid paying that cost on quite
   // a hot path:
   if(new_guard.id() == ID_not)
-    jump_not_taken_state.apply_condition(new_guard.op0(), current_state, ns);
+    jump_not_taken_state.apply_condition(
+      to_not_expr(new_guard).op(), current_state, ns);
   else if(new_guard.id() == ID_notequal)
   {
+    auto &not_equal_expr = to_notequal_expr(new_guard);
     jump_not_taken_state.apply_condition(
-      equal_exprt(new_guard.op0(), new_guard.op1()), current_state, ns);
+      equal_exprt(not_equal_expr.lhs(), not_equal_expr.rhs()),
+      current_state,
+      ns);
   }
 }
 
@@ -180,10 +184,10 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
   if(expr.id() != ID_equal && expr.id() != ID_notequal)
     return {};
 
-  if(!can_cast_type<pointer_typet>(expr.op0().type()))
+  if(!can_cast_type<pointer_typet>(to_binary_expr(expr).op0().type()))
     return {};
 
-  exprt lhs = expr.op0(), rhs = expr.op1();
+  exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1();
   if(can_cast_expr<symbol_exprt>(rhs))
     std::swap(lhs, rhs);