protect opX in codet subclasses

This will prevent accesses that are not type safe.

Author: Daniel Kroening

src/cpp/cpp_typecheck_initializer.cpp

@@ -326,7 +326,7 @@ void cpp_typecheckt::zero_initializer(
     code_assignt assign(object, *value);
     assign.add_source_location()=source_location;
 
-    typecheck_expr(assign.op0());
+    typecheck_expr(assign.lhs());
     assign.lhs().type().set(ID_C_constant, false);
     already_typechecked(assign.lhs());
 

src/goto-programs/goto_convert.cpp

@@ -317,18 +317,19 @@ void goto_convertt::convert_label(
     // the body of the thread is expected to be
     // in the operand.
     DATA_INVARIANT(
-      code.op0().is_not_nil(), "op0 in magic thread creation label is null");
+      to_code_label(code).code().is_not_nil(),
+      "code() in magic thread creation label is null");
 
     // replace the magic thread creation label with a
     // thread block (START_THREAD...END_THREAD).
     code_blockt thread_body;
-    thread_body.add(to_code(code.op0()));
+    thread_body.add(to_code_label(code).code());
     thread_body.add_source_location()=code.source_location();
     generate_thread_block(thread_body, dest, mode);
   }
   else
   {
-    convert(to_code(code.op0()), tmp, mode);
+    convert(to_code_label(code).code(), tmp, mode);
 
     goto_programt::targett target=tmp.instructions.begin();
     dest.destructive_append(tmp);

src/jsil/jsil_typecheck.cpp

@@ -840,10 +840,10 @@ void jsil_typecheckt::typecheck_ifthenelse(code_ifthenelset &code)
 
 void jsil_typecheckt::typecheck_assign(code_assignt &code)
 {
-  typecheck_expr(code.op0());
-  typecheck_expr(code.op1());
+  typecheck_expr(code.lhs());
+  typecheck_expr(code.rhs());
 
-  make_type_compatible(code.op0(), code.op1().type(), false);
+  make_type_compatible(code.lhs(), code.rhs().type(), false);
 }
 
 /// typechecking procedure declaration; any other symbols should have been

src/pointer-analysis/goto_program_dereference.cpp

@@ -326,8 +326,9 @@ void goto_program_dereferencet::dereference_instruction(
       function_call.function(),
       checks_only,
       value_set_dereferencet::modet::READ);
-    dereference_expr(
-      function_call.op2(), checks_only, value_set_dereferencet::modet::READ);
+
+    for(auto &arg : function_call.arguments())
+      dereference_expr(arg, checks_only, value_set_dereferencet::modet::READ);
   }
   else if(i.is_return())
   {

src/pointer-analysis/value_set.cpp

@@ -1525,7 +1525,7 @@ void value_sett::apply_code_rec(
   }
   else if(statement==ID_assume)
   {
-    guard(to_code_assume(code).op0(), ns);
+    guard(to_code_assume(code).assumption(), ns);
   }
   else if(statement==ID_user_specified_predicate ||
           statement==ID_user_specified_parameter_predicates ||

src/util/std_code.h

@@ -264,6 +264,12 @@ class code_skipt:public codet
   code_skipt():codet(ID_skip)
   {
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
@@ -343,6 +349,12 @@ class code_assignt:public codet
 
     validate(code, ns, vm);
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
@@ -481,6 +493,12 @@ class code_deadt:public codet
       "removing a non-symbol: " +
         id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope");
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
@@ -538,6 +556,12 @@ class code_assumet:public codet
   {
     return op0();
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
@@ -589,6 +613,12 @@ class code_assertt:public codet
   {
     return op0();
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
@@ -692,6 +722,12 @@ class code_ifthenelset:public codet
   {
     return static_cast<codet &>(op2());
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
@@ -754,6 +790,12 @@ class code_switcht:public codet
   {
     return static_cast<codet &>(op1());
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
@@ -814,6 +856,12 @@ class code_whilet:public codet
   {
     return static_cast<codet &>(op1());
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
@@ -874,6 +922,12 @@ class code_dowhilet:public codet
   {
     return static_cast<codet &>(op1());
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
@@ -963,6 +1017,12 @@ class code_fort:public codet
   {
     return static_cast<codet &>(op3());
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_fort>(const exprt &base)
@@ -1012,6 +1072,12 @@ class code_gotot:public codet
   {
     return get(ID_destination);
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
@@ -1165,6 +1231,12 @@ class code_function_callt:public codet
 
     validate(code, ns, vm);
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
@@ -1229,6 +1301,12 @@ class code_returnt:public codet
   {
     DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
@@ -1298,6 +1376,12 @@ class code_labelt:public codet
   {
     return static_cast<const codet &>(op0());
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
@@ -1369,6 +1453,12 @@ class code_switch_caset:public codet
   {
     return static_cast<const codet &>(op1());
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
@@ -1405,6 +1495,12 @@ class code_breakt:public codet
   code_breakt():codet(ID_break)
   {
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
@@ -1435,6 +1531,12 @@ class code_continuet:public codet
   code_continuet():codet(ID_continue)
   {
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
@@ -1524,6 +1626,12 @@ class code_expressiont:public codet
   {
     return op0();
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
@@ -2001,6 +2109,12 @@ class code_push_catcht:public codet
   const exception_listt &exception_list() const {
     return (const exception_listt &)find(ID_exception_list).get_sub();
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
@@ -2032,6 +2146,12 @@ class code_pop_catcht:public codet
   code_pop_catcht():codet(ID_pop_catch)
   {
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
@@ -2077,6 +2197,12 @@ class code_landingpadt:public codet
   {
     return op0();
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
@@ -2153,6 +2279,12 @@ class code_try_catcht:public codet
   {
     add_to_operands(to_catch, code_catch);
   }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
 };
 
 template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)