diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 65a6bb2f38b..658c589a66c 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -92,12 +92,9 @@ exprt build_full_lhs_rec( else if(id==ID_byte_extract_little_endian || id==ID_byte_extract_big_endian) { - exprt tmp=src_original; - tmp.op0() = build_full_lhs_rec( - prop_conv, - ns, - to_byte_extract_expr(tmp).op(), - to_byte_extract_expr(src_ssa).op()); + byte_extract_exprt tmp = to_byte_extract_expr(src_original); + tmp.op() = build_full_lhs_rec( + prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op()); // re-write into big case-split } diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index b6ea8d6274a..d4ceea5cc77 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -132,13 +132,20 @@ static bool check_renaming(const exprt &expr) if(check_renaming(expr.type())) return true; - if(expr.id()==ID_address_of && - expr.op0().id()==ID_symbol) - return check_renaming_l1(expr.op0()); - else if(expr.id()==ID_address_of && - expr.op0().id()==ID_index) - return check_renaming_l1(expr.op0().op0()) || - check_renaming(expr.op0().op1()); + if( + expr.id() == ID_address_of && + to_address_of_expr(expr).object().id() == ID_symbol) + { + return check_renaming_l1(to_address_of_expr(expr).object()); + } + else if( + expr.id() == ID_address_of && + to_address_of_expr(expr).object().id() == ID_index) + { + const auto index_expr = to_index_expr(to_address_of_expr(expr).object()); + return check_renaming_l1(index_expr.array()) || + check_renaming(index_expr.index()); + } else if(expr.id()==ID_symbol) { if(!expr.get_bool(ID_C_SSA_symbol)) diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index 8e951d6eeb8..f4d4a792469 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -30,7 +30,7 @@ void goto_symext::symex_dead(statet &state) state.rename(ssa, ns, goto_symex_statet::L1); // in case of pointers, put something into the value set - if(ns.follow(code.op0().type()).id()==ID_pointer) + if(ns.follow(code.symbol().type()).id() == ID_pointer) { exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns); diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index fbbbf5f7abe..3942382be1a 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -28,9 +28,8 @@ void goto_symext::symex_decl(statet &state) // two-operand decl not supported here // we handle the decl with only one operand PRECONDITION(code.operands().size() == 1); - PRECONDITION(code.op0().id() == ID_symbol); - symex_decl(state, to_symbol_expr(code.op0())); + symex_decl(state, to_symbol_expr(to_code_decl(code).symbol())); } void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 7c229557a7b..b4be01f113e 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -270,7 +270,7 @@ void goto_symext::dereference_rec( } exprt tmp1; - tmp1.swap(expr.op0()); + tmp1.swap(to_dereference_expr(expr).pointer()); // first make sure there are no dereferences in there dereference_rec(tmp1, state, guard, false); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index a6994b0ebb3..508d48aa52f 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -435,7 +435,7 @@ void goto_symext::return_assignment(statet &state) PRECONDITION(code.operands().size() == 1 || frame.return_value.is_nil()); - exprt value = code.op0(); + exprt value = code.return_value(); if(frame.return_value.is_not_nil()) { diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index be8dbb2b099..95b91a14360 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -233,11 +233,13 @@ void goto_symext::symex_goto(statet &state) // produce new guard symbol exprt guard_expr; - if(new_guard.id()==ID_symbol || - (new_guard.id()==ID_not && - new_guard.operands().size()==1 && - new_guard.op0().id()==ID_symbol)) + if( + new_guard.id() == ID_symbol || + (new_guard.id() == ID_not && + to_not_expr(new_guard).op().id() == ID_symbol)) + { guard_expr=new_guard; + } else { symbol_exprt guard_symbol_expr= diff --git a/src/util/config.cpp b/src/util/config.cpp index b7ad362da9e..05ff16d3ec7 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1101,13 +1101,14 @@ static irep_idt string_from_ns( const exprt &tmp=symbol->value; INVARIANT( - tmp.id() == ID_address_of && tmp.operands().size() == 1 && - tmp.op0().id() == ID_index && tmp.op0().operands().size() == 2 && - tmp.op0().op0().id() == ID_string_constant, + tmp.id() == ID_address_of && + to_address_of_expr(tmp).object().id() == ID_index && + to_index_expr(to_address_of_expr(tmp).object()).array().id() == + ID_string_constant, "symbol table configuration entry `" + id2string(id) + "' must be a string constant"); - return tmp.op0().op0().get(ID_value); + return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value); } static unsigned unsigned_from_ns( diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 75248019d77..e20d823a84e 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -56,8 +56,8 @@ exprt make_binary(const exprt &expr) exprt tmp=expr; tmp.operands().clear(); tmp.operands().resize(2); - tmp.op0().swap(previous); - tmp.op1()=*it; + to_binary_expr(tmp).op0().swap(previous); + to_binary_expr(tmp).op1() = *it; previous.swap(tmp); } @@ -126,8 +126,8 @@ exprt is_not_zero( exprt boolean_negate(const exprt &src) { - if(src.id()==ID_not && src.operands().size()==1) - return src.op0(); + if(src.id() == ID_not) + return to_not_expr(src).op(); else if(src.is_true()) return false_exprt(); else if(src.is_false()) diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 1bb4e8bd77d..dbdeb5f22f2 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -39,42 +39,47 @@ static exprt simplify_json_expr( { const irep_idt &value=to_constant_expr(src).get_value(); - if(value!=ID_NULL && - (value!=std::string(value.size(), '0') || - !config.ansi_c.NULL_is_zero) && - src.operands().size()==1 && - src.op0().id()!=ID_constant) - // try to simplify the constant pointer - return simplify_json_expr(src.op0(), ns); + if( + value != ID_NULL && + (value != std::string(value.size(), '0') || + !config.ansi_c.NULL_is_zero) && + src.operands().size() == 1 && + to_unary_expr(src).op().id() != ID_constant) + // try to simplify the constant pointer + { + return simplify_json_expr(to_unary_expr(src).op(), ns); + } } } - else if(src.id()==ID_address_of && - src.operands().size()==1 && - src.op0().id()==ID_member && - id2string(to_member_expr( - src.op0()).get_component_name()).find("@")!=std::string::npos) + else if( + src.id() == ID_address_of && + to_address_of_expr(src).object().id() == ID_member && + id2string( + to_member_expr(to_address_of_expr(src).object()).get_component_name()) + .find("@") != std::string::npos) { // simplify expressions of the form &member_expr(object, @class_identifier) - return simplify_json_expr(src.op0(), ns); + return simplify_json_expr(to_address_of_expr(src).object(), ns); } - else if(src.id()==ID_address_of && - src.operands().size()==1 && - src.op0().id()==ID_index && - to_index_expr(src.op0()).index().id()==ID_constant && - to_constant_expr( - to_index_expr(src.op0()).index()).value_is_zero_string()) + else if( + src.id() == ID_address_of && + to_address_of_expr(src).object().id() == ID_index && + to_index_expr(to_address_of_expr(src).object()).index().id() == + ID_constant && + to_constant_expr(to_index_expr(to_address_of_expr(src).object()).index()) + .value_is_zero_string()) { // simplify expressions of the form &array[0] - return simplify_json_expr(to_index_expr(src.op0()).array(), ns); + return simplify_json_expr( + to_index_expr(to_address_of_expr(src).object()).array(), ns); } else if(src.id()==ID_member && - src.operands().size()==1 && id2string( to_member_expr(src).get_component_name()) .find("@")!=std::string::npos) { // simplify expressions of the form member_expr(object, @class_identifier) - return simplify_json_expr(src.op0(), ns); + return simplify_json_expr(to_member_expr(src).struct_op(), ns); } return src; @@ -317,11 +322,15 @@ json_objectt json( result["name"]=json_stringt("pointer"); result["type"]=json_stringt(type_string); exprt simpl_expr=simplify_json_expr(expr, ns); - if(simpl_expr.get(ID_value)==ID_NULL || - // remove typecast on NULL - (simpl_expr.id()==ID_constant && simpl_expr.type().id()==ID_pointer && - simpl_expr.op0().get(ID_value)==ID_NULL)) + if( + simpl_expr.get(ID_value) == ID_NULL || + // remove typecast on NULL + (simpl_expr.id() == ID_constant && + simpl_expr.type().id() == ID_pointer && + to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL)) + { result["data"]=json_stringt(value_string); + } else if(simpl_expr.id()==ID_symbol) { const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier(); diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 3e687b2bb55..4409934e8bc 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -77,9 +77,10 @@ bool ssa_exprt::can_build_identifier(const exprt &expr) { if(expr.id()==ID_symbol) return true; - else if(expr.id()==ID_member || - expr.id()==ID_index) - return can_build_identifier(expr.op0()); + else if(expr.id() == ID_member) + return can_build_identifier(to_member_expr(expr).compound()); + else if(expr.id() == ID_index) + return can_build_identifier(to_index_expr(expr).array()); else return false; } diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index 8ff7cdbdae3..50b8e2d1f4a 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -134,9 +134,7 @@ codet &code_blockt::find_last_statement() } else if(statement==ID_label) { - DATA_INVARIANT( - last->operands().size() == 1, "label must have one operand"); - last=&(to_code(last->op0())); + last = &(to_code_label(*last).code()); } else break;