diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 4478dd7d856..8cd410c97a8 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "goto_convert_functions.h" #include "read_goto_binary.h" @@ -36,8 +37,10 @@ goto_modelt initialize_goto_model( const std::vector &files=cmdline.args; if(files.empty()) { - msg.error() << "Please provide a program" << messaget::eom; - throw 0; + throw invalid_command_line_argument_exceptiont( + "missing program argument", + "filename", + "one or more paths to program files"); } std::vector binaries, sources; @@ -69,9 +72,8 @@ goto_modelt initialize_goto_model( if(!infile) { - msg.error() << "failed to open input file `" << filename - << '\'' << messaget::eom; - throw 0; + throw system_exceptiont( + "Failed to open input file `" + filename + '\''); } language_filet &lf=language_files.add_file(filename); @@ -79,11 +81,8 @@ goto_modelt initialize_goto_model( if(lf.language==nullptr) { - source_locationt location; - location.set_file(filename); - msg.error().source_location=location; - msg.error() << "failed to figure out type of file" << messaget::eom; - throw 0; + throw invalid_source_file_exceptiont( + "Failed to figure out type of file `" + filename + '\''); } languaget &language=*lf.language; @@ -94,8 +93,7 @@ goto_modelt initialize_goto_model( if(language.parse(infile, filename)) { - msg.error() << "PARSING ERROR" << messaget::eom; - throw 0; + throw invalid_source_file_exceptiont("PARSING ERROR"); } lf.get_modules(); @@ -105,8 +103,7 @@ goto_modelt initialize_goto_model( if(language_files.typecheck(goto_model.symbol_table)) { - msg.error() << "CONVERSION ERROR" << messaget::eom; - throw 0; + throw invalid_source_file_exceptiont("CONVERSION ERROR"); } } @@ -115,7 +112,10 @@ goto_modelt initialize_goto_model( msg.status() << "Reading GOTO program from file" << messaget::eom; if(read_object_and_link(file, goto_model, message_handler)) - throw 0; + { + throw invalid_source_file_exceptiont( + "failed to read object or link in file `" + file + '\''); + } } bool binaries_provided_start= @@ -150,14 +150,12 @@ goto_modelt initialize_goto_model( if(entry_point_generation_failed) { - msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom; - throw 0; + throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR"); } if(language_files.final(goto_model.symbol_table)) { - msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom; - throw 0; + throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR"); } msg.status() << "Generating GOTO Program" << messaget::eom; diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index fe25fbf334b..ef9a42dfcce 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -69,12 +69,12 @@ void interpretert::initialize(bool init) main_it=goto_functions.function_map.find(goto_functionst::entry_point()); if(main_it==goto_functions.function_map.end()) - throw "main not found"; + throw analysis_exceptiont("main not found"); const goto_functionst::goto_functiont &goto_function=main_it->second; if(!goto_function.body_available()) - throw "main has no body"; + throw analysis_exceptiont("main has no body"); pc=goto_function.body.instructions.begin(); function=main_it; @@ -292,7 +292,10 @@ void interpretert::step() case RETURN: trace_step.type=goto_trace_stept::typet::FUNCTION_RETURN; if(call_stack.empty()) - throw "RETURN without call"; // NOLINT(readability/throw) + { + throw analysis_exceptiont( + "RETURN without call"); // NOLINT(readability/throw) + } if(pc->code.operands().size()==1 && call_stack.top().return_value_address!=0) @@ -317,19 +320,23 @@ void interpretert::step() case START_THREAD: trace_step.type=goto_trace_stept::typet::SPAWN; - throw "START_THREAD not yet implemented"; // NOLINT(readability/throw) + throw analysis_exceptiont( + "START_THREAD not yet implemented"); // NOLINT(readability/throw) case END_THREAD: - throw "END_THREAD not yet implemented"; // NOLINT(readability/throw) + throw analysis_exceptiont( + "END_THREAD not yet implemented"); // NOLINT(readability/throw) break; case ATOMIC_BEGIN: trace_step.type=goto_trace_stept::typet::ATOMIC_BEGIN; - throw "ATOMIC_BEGIN not yet implemented"; // NOLINT(readability/throw) + throw analysis_exceptiont( + "ATOMIC_BEGIN not yet implemented"); // NOLINT(readability/throw) case ATOMIC_END: trace_step.type=goto_trace_stept::typet::ATOMIC_END; - throw "ATOMIC_END not yet implemented"; // NOLINT(readability/throw) + throw analysis_exceptiont( + "ATOMIC_END not yet implemented"); // NOLINT(readability/throw) case DEAD: trace_step.type=goto_trace_stept::typet::DEAD; @@ -359,7 +366,7 @@ void interpretert::step() case CATCH: break; default: - throw "encountered instruction with undefined instruction type"; + UNREACHABLE; // I'm assuming we'd catch such a thing before this point } pc=next_pc; } @@ -369,11 +376,9 @@ void interpretert::execute_goto() { if(evaluate_boolean(pc->guard)) { - if(pc->targets.empty()) - throw "taken goto without target"; - - if(pc->targets.size()>=2) - throw "non-deterministic goto encountered"; + DATA_INVARIANT( + pc->targets.size() == 1, + "a goto should have exactly one target location"); next_pc=pc->targets.front(); } @@ -383,6 +388,10 @@ void interpretert::execute_goto() void interpretert::execute_other() { const irep_idt &statement=pc->code.get_statement(); + PRECONDITION( + statement == ID_expression || statement == ID_array_set || + statement == ID_output); + if(statement==ID_expression) { DATA_INVARIANT( @@ -410,8 +419,6 @@ void interpretert::execute_other() { return; } - else - throw "unexpected OTHER statement: "+id2string(statement); } void interpretert::execute_decl() @@ -427,8 +434,7 @@ struct_typet::componentt interpretert::get_component( { const symbolt &symbol=ns.lookup(object); const typet real_type=ns.follow(symbol.type); - if(real_type.id()!=ID_struct) - throw "request for member of non-struct"; + PRECONDITION(real_type.id() == ID_struct); const struct_typet &struct_type=to_struct_type(real_type); const struct_typet::componentst &components=struct_type.components(); @@ -443,7 +449,7 @@ struct_typet::componentt interpretert::get_component( tmp_offset-=get_size(c.type()); } - throw "access out of struct bounds"; + throw analysis_exceptiont("access out of struct bounds"); } /// returns the type object corresponding to id @@ -634,7 +640,7 @@ exprt interpretert::get_value( error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)] << " > object count " << memory.size() << eom; - throw "interpreter: reading from invalid pointer"; + throw analysis_exceptiont("interpreter: reading from invalid pointer"); } else if(real_type.id()==ID_string) { @@ -724,7 +730,7 @@ void interpretert::assign( void interpretert::execute_assume() { if(!evaluate_boolean(pc->guard)) - throw "assumption failed"; + throw analysis_exceptiont("assumption failed"); } void interpretert::execute_assert() @@ -732,7 +738,7 @@ void interpretert::execute_assert() if(!evaluate_boolean(pc->guard)) { if((target_assert==pc) || stop_on_assertion) - throw "program assertion reached"; + throw analysis_exceptiont("program assertion reached"); else if(show) error() << "assertion failed at " << pc->location_number << "\n" << eom; @@ -748,9 +754,9 @@ void interpretert::execute_function_call() mp_integer address=evaluate_address(function_call.function()); if(address==0) - throw "function call to NULL"; + throw analysis_exceptiont("function call to NULL"); else if(address>=memory.size()) - throw "out-of-range function call"; + throw analysis_exceptiont("out-of-range function call"); // Retrieve the empty last trace step struct we pushed for this step // of the interpreter run to fill it with the corresponding data @@ -764,8 +770,9 @@ void interpretert::execute_function_call() const goto_functionst::function_mapt::const_iterator f_it= goto_functions.function_map.find(identifier); - if(f_it==goto_functions.function_map.end()) - throw "failed to find function "+id2string(identifier); + INVARIANT( + f_it != goto_functions.function_map.end(), + "calls to missing functions should be caught during typechecking"); // return value mp_integer return_value_address; @@ -810,8 +817,10 @@ void interpretert::execute_function_call() const code_typet::parameterst ¶meters= to_code_type(f_it->second.type).parameters(); - if(argument_values.size() #include #include "goto_model.h" diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index e0fefe283f9..9dca877dab4 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -15,10 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include -#include #include +#include +#include #include "goto_functions.h" #include "goto_trace.h" @@ -279,8 +280,9 @@ class interpretert:public messaget { mp_vectort v; evaluate(expr, v); + // FIXME not sure if this can happen if(v.size()!=1) - throw "invalid boolean value"; + throw analysis_exceptiont("invalid boolean value"); return v.front()!=0; } diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 46c0a1b0cca..21ac91562aa 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include /// Reads a memory address and loads it into the `dest` variable. /// Marks cell as `READ_BEFORE_WRITTEN` if cell has never been written. @@ -474,11 +475,9 @@ void interpretert::evaluate( } else if(expr.id()==ID_bitor) { - if(expr.operands().size()<2) - throw id2string(expr.id())+" expects at least two operands"; - + auto const &bitor_expr = to_bitor_expr(expr); mp_integer final=0; - forall_operands(it, expr) + forall_operands(it, bitor_expr) { mp_vectort tmp; evaluate(*it, tmp); @@ -490,11 +489,10 @@ void interpretert::evaluate( } else if(expr.id()==ID_bitand) { - if(expr.operands().size()<2) - throw id2string(expr.id())+" expects at least two operands"; + auto const &bitand_expr = to_bitand_expr(expr); mp_integer final=-1; - forall_operands(it, expr) + forall_operands(it, bitand_expr) { mp_vectort tmp; evaluate(*it, tmp); @@ -506,11 +504,10 @@ void interpretert::evaluate( } else if(expr.id()==ID_bitxor) { - if(expr.operands().size()<2) - throw id2string(expr.id())+" expects at least two operands"; + auto const &bitxor_expr = to_bitxor_expr(expr); mp_integer final=0; - forall_operands(it, expr) + forall_operands(it, bitxor_expr) { mp_vectort tmp; evaluate(*it, tmp); @@ -522,10 +519,9 @@ void interpretert::evaluate( } else if(expr.id()==ID_bitnot) { - if(expr.operands().size()!=1) - throw id2string(expr.id())+" expects one operand"; + auto const &bitnot_expr = to_bitnot_expr(expr); mp_vectort tmp; - evaluate(expr.op0(), tmp); + evaluate(bitnot_expr.op(), tmp); if(tmp.size()==1) { const auto width = to_bitvector_type(expr.op0().type()).get_width(); @@ -536,88 +532,83 @@ void interpretert::evaluate( } else if(expr.id()==ID_shl) { - if(expr.operands().size()!=2) - throw id2string(expr.id())+" expects two operands"; + auto const &shl_expr = to_shift_expr(expr); - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - if(tmp0.size()==1 && tmp1.size()==1) + mp_vectort op, distance; + evaluate(shl_expr.op(), op); + evaluate(shl_expr.distance(), distance); + if(op.size() == 1 && distance.size() == 1) { - mp_integer final=arith_left_shift( - tmp0.front(), - tmp1.front(), - to_bitvector_type(expr.op0().type()).get_width()); + mp_integer final = arith_left_shift( + op.front(), + distance.front(), + to_bitvector_type(shl_expr.op().type()).get_width()); dest.push_back(final); return; } } else if((expr.id()==ID_shr) || (expr.id()==ID_lshr)) { - if(expr.operands().size()!=2) - throw id2string(expr.id())+" expects two operands"; + auto const &shr_or_lshr_expr = to_shift_expr(expr); - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - if(tmp0.size()==1 && tmp1.size()==1) + mp_vectort op, distance; + evaluate(shr_or_lshr_expr.op(), op); + evaluate(shr_or_lshr_expr.distance(), distance); + if(op.size() == 1 && distance.size() == 1) { - mp_integer final=logic_right_shift( - tmp0.front(), - tmp1.front(), - to_bitvector_type(expr.op0().type()).get_width()); + mp_integer final = logic_right_shift( + op.front(), + distance.front(), + to_bitvector_type(shr_or_lshr_expr.op().type()).get_width()); dest.push_back(final); return; } } else if(expr.id()==ID_ashr) { - if(expr.operands().size()!=2) - throw id2string(expr.id())+" expects two operands"; - - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - if(tmp0.size()==1 && tmp1.size()==1) + auto const &ashr_expr = to_shift_expr(expr); + mp_vectort op, distance; + evaluate(ashr_expr.op(), op); + evaluate(ashr_expr.distance(), distance); + if(op.size() == 1 && distance.size() == 1) { - mp_integer final=arith_right_shift( - tmp0.front(), - tmp1.front(), - to_bitvector_type(expr.op0().type()).get_width()); + mp_integer final = arith_right_shift( + op.front(), + distance.front(), + to_bitvector_type(ashr_expr.op().type()).get_width()); dest.push_back(final); return; } } else if(expr.id()==ID_ror) { - if(expr.operands().size()!=2) - throw id2string(expr.id())+" expects two operands"; - - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - if(tmp0.size()==1 && tmp1.size()==1) + auto const &ror_expr = to_shift_expr(expr); + mp_vectort op, distance; + evaluate(ror_expr.op(), op); + evaluate(ror_expr.distance(), distance); + if(op.size() == 1 && distance.size() == 1) { - mp_integer final=rotate_right(tmp0.front(), - tmp1.front(), - to_bitvector_type(expr.op0().type()).get_width()); + mp_integer final = rotate_right( + op.front(), + distance.front(), + to_bitvector_type(ror_expr.op().type()).get_width()); dest.push_back(final); return; } } else if(expr.id()==ID_rol) { - if(expr.operands().size()!=2) - throw id2string(expr.id())+" expects two operands"; + auto const &rol_expr = to_shift_expr(expr); - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); - if(tmp0.size()==1 && tmp1.size()==1) + mp_vectort op, distance; + evaluate(rol_expr.op(), op); + evaluate(rol_expr.distance(), distance); + if(op.size() == 1 && distance.size() == 1) { - mp_integer final=rotate_left(tmp0.front(), - tmp1.front(), - to_bitvector_type(expr.op0().type()).get_width()); + mp_integer final = rotate_left( + op.front(), + distance.front(), + to_bitvector_type(rol_expr.op().type()).get_width()); dest.push_back(final); return; } @@ -629,42 +620,40 @@ void interpretert::evaluate( expr.id()==ID_lt || expr.id()==ID_gt) { - if(expr.operands().size()!=2) - throw id2string(expr.id())+" expects two operands"; + auto const &relation_expr = to_binary_relation_expr(expr); - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); + mp_vectort lhs, rhs; + evaluate(relation_expr.lhs(), lhs); + evaluate(relation_expr.rhs(), rhs); - if(tmp0.size()==1 && tmp1.size()==1) + if(lhs.size() == 1 && rhs.size() == 1) { - const mp_integer &op0=tmp0.front(); - const mp_integer &op1=tmp1.front(); + const mp_integer &lhs_as_integer = lhs.front(); + const mp_integer &rhs_as_integer = rhs.front(); if(expr.id()==ID_equal) - dest.push_back(op0==op1); + dest.push_back(lhs_as_integer == rhs_as_integer); else if(expr.id()==ID_notequal) - dest.push_back(op0!=op1); + dest.push_back(lhs_as_integer != rhs_as_integer); else if(expr.id()==ID_le) - dest.push_back(op0<=op1); + dest.push_back(lhs_as_integer <= rhs_as_integer); else if(expr.id()==ID_ge) - dest.push_back(op0>=op1); + dest.push_back(lhs_as_integer >= rhs_as_integer); else if(expr.id()==ID_lt) - dest.push_back(op0op1); + dest.push_back(lhs_as_integer > rhs_as_integer); } return; } else if(expr.id()==ID_or) { - if(expr.operands().empty()) - throw id2string(expr.id())+" expects at least one operand"; + auto const &or_expr = to_or_expr(expr); bool result=false; - forall_operands(it, expr) + forall_operands(it, or_expr) { mp_vectort tmp; evaluate(*it, tmp); @@ -682,33 +671,31 @@ void interpretert::evaluate( } else if(expr.id()==ID_if) { - if(expr.operands().size()!=3) - throw "if expects three operands"; + auto const &if_expr = to_if_expr(expr); - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); + mp_vectort condition, if_result; + evaluate(if_expr.cond(), condition); - if(tmp0.size()==1) + if(condition.size() == 1) { - if(tmp0.front()!=0) - evaluate(expr.op1(), tmp1); + if(condition.front() != 0) + evaluate(if_expr.true_case(), if_result); else - evaluate(expr.op2(), tmp1); + evaluate(if_expr.false_case(), if_result); } - if(tmp1.size()==1) - dest.push_back(tmp1.front()); + if(if_result.size() == 1) + dest.push_back(if_result.front()); return; } else if(expr.id()==ID_and) { - if(expr.operands().empty()) - throw id2string(expr.id())+" expects at least one operand"; + auto const &and_expr = to_and_expr(expr); bool result=true; - forall_operands(it, expr) + forall_operands(it, and_expr) { mp_vectort tmp; evaluate(*it, tmp); @@ -726,27 +713,26 @@ void interpretert::evaluate( } else if(expr.id()==ID_not) { - if(expr.operands().size()!=1) - throw id2string(expr.id())+" expects one operand"; + auto const ¬_expr = to_not_expr(expr); - mp_vectort tmp; - evaluate(expr.op0(), tmp); + mp_vectort result_before_not; + evaluate(not_expr.op(), result_before_not); - if(tmp.size()==1) - dest.push_back(tmp.front()==0); + if(result_before_not.size() == 1) + dest.push_back(result_before_not.front() == 0); return; } else if(expr.id()==ID_plus) { + auto const &plus_expr = to_plus_expr(expr); mp_integer result=0; - - forall_operands(it, expr) + forall_operands(it, plus_expr) { - mp_vectort tmp; - evaluate(*it, tmp); - if(tmp.size()==1) - result+=tmp.front(); + mp_vectort operand; + evaluate(*it, operand); + if(operand.size() == 1) + result += operand.front(); } dest.push_back(result); @@ -754,52 +740,53 @@ void interpretert::evaluate( } else if(expr.id()==ID_mult) { + auto const &mult_expr = to_mult_expr(expr); // type-dependent! mp_integer result; if(expr.type().id()==ID_fixedbv) { fixedbvt f; - f.spec=fixedbv_spect(to_fixedbv_type(expr.type())); + f.spec = fixedbv_spect(to_fixedbv_type(mult_expr.type())); f.from_integer(1); result=f.get_value(); } else if(expr.type().id()==ID_floatbv) { - ieee_floatt f(to_floatbv_type(expr.type())); + ieee_floatt f(to_floatbv_type(mult_expr.type())); f.from_integer(1); result=f.pack(); } else result=1; - forall_operands(it, expr) + forall_operands(it, mult_expr) { - mp_vectort tmp; - evaluate(*it, tmp); - if(tmp.size()==1) + mp_vectort operand; + evaluate(*it, operand); + if(operand.size() == 1) { - if(expr.type().id()==ID_fixedbv) + if(mult_expr.type().id() == ID_fixedbv) { fixedbvt f1, f2; - f1.spec=fixedbv_spect(to_fixedbv_type(expr.type())); + f1.spec = fixedbv_spect(to_fixedbv_type(mult_expr.type())); f2.spec=fixedbv_spect(to_fixedbv_type(it->type())); f1.set_value(result); - f2.set_value(tmp.front()); + f2.set_value(operand.front()); f1*=f2; result=f1.get_value(); } - else if(expr.type().id()==ID_floatbv) + else if(mult_expr.type().id() == ID_floatbv) { - ieee_floatt f1(to_floatbv_type(expr.type())); + ieee_floatt f1(to_floatbv_type(mult_expr.type())); ieee_floatt f2(to_floatbv_type(it->type())); f1.unpack(result); - f2.unpack(tmp.front()); + f2.unpack(operand.front()); f1*=f2; result=f2.pack(); } else - result*=tmp.front(); + result *= operand.front(); } } @@ -808,58 +795,50 @@ void interpretert::evaluate( } else if(expr.id()==ID_minus) { - if(expr.operands().size()!=2) - throw "- expects two operands"; + auto const &minus_expr = to_minus_expr(expr); - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); + mp_vectort minuend, subtrahend; + evaluate(minus_expr.op0(), minuend); + evaluate(minus_expr.op1(), subtrahend); - if(tmp0.size()==1 && tmp1.size()==1) - dest.push_back(tmp0.front()-tmp1.front()); + if(minuend.size() == 1 && subtrahend.size() == 1) + dest.push_back(minuend.front() - subtrahend.front()); return; } else if(expr.id()==ID_div) { - if(expr.operands().size()!=2) - throw "/ expects two operands"; + auto const &div_expr = to_div_expr(expr); - mp_vectort tmp0, tmp1; - evaluate(expr.op0(), tmp0); - evaluate(expr.op1(), tmp1); + mp_vectort dividend, divisor; + evaluate(div_expr.dividend(), dividend); + evaluate(div_expr.divisor(), divisor); - if(tmp0.size()==1 && tmp1.size()==1) - dest.push_back(tmp0.front()/tmp1.front()); + if(dividend.size() == 1 && divisor.size() == 1) + dest.push_back(dividend.front() / divisor.front()); return; } else if(expr.id()==ID_unary_minus) { - if(expr.operands().size()!=1) - throw "unary- expects one operand"; + auto const &unary_minus_expr = to_unary_minus_expr(expr); - mp_vectort tmp0; - evaluate(expr.op0(), tmp0); + mp_vectort negated; + evaluate(unary_minus_expr.op(), negated); - if(tmp0.size()==1) - dest.push_back(-tmp0.front()); + if(negated.size() == 1) + dest.push_back(-negated.front()); return; } else if(expr.id()==ID_address_of) { - if(expr.operands().size()!=1) - throw "address_of expects one operand"; - - dest.push_back(evaluate_address(expr.op0())); + auto const &address_of_expr = to_address_of_expr(expr); + dest.push_back(evaluate_address(address_of_expr.op())); return; } else if(expr.id()==ID_pointer_offset) { - if(expr.operands().size()!=1) - throw "pointer_offset expects one operand"; - if(expr.op0().type().id()!=ID_pointer) - throw "pointer_offset expects a pointer operand"; + auto const &pointer_offset_expr = to_pointer_offset_expr(expr); mp_vectort result; - evaluate(expr.op0(), result); + evaluate(pointer_offset_expr.op(), result); if(result.size()==1) { // Return the distance, in bytes, between the address returned @@ -880,12 +859,11 @@ void interpretert::evaluate( else if(expr.id()==ID_byte_extract_little_endian || expr.id()==ID_byte_extract_big_endian) { - if(expr.operands().size()!=2) - throw "byte_extract should have two operands"; + auto const &byte_extract_expr = to_byte_extract_expr(expr); mp_vectort extract_offset; - evaluate(expr.op1(), extract_offset); + evaluate(byte_extract_expr.offset(), extract_offset); mp_vectort extract_from; - evaluate(expr.op0(), extract_from); + evaluate(byte_extract_expr.op(), extract_from); if(extract_offset.size()==1 && extract_from.size()!=0) { const typet &target_type=expr.type(); @@ -893,9 +871,7 @@ void interpretert::evaluate( // If memory offset is found (which should normally be the case) // extract the corresponding data from the appropriate memory location if(!byte_offset_to_memory_offset( - expr.op0().type(), - extract_offset[0], - memory_offset)) + byte_extract_expr.op().type(), extract_offset[0], memory_offset)) { mp_integer target_type_leaves; if(!count_type_leaves(target_type, target_type_leaves) && @@ -924,13 +900,14 @@ void interpretert::evaluate( // simplify. if(expr.id() == ID_index) { - exprt evaluated_index = expr; - mp_vectort idx; - evaluate(expr.op1(), idx); - if(idx.size() == 1) + auto const &index_expr = to_index_expr(expr); + index_exprt evaluated_index = index_expr; + mp_vectort index; + evaluate(index_expr.index(), index); + if(index.size() == 1) { - evaluated_index.op1() = - constant_exprt(integer2string(idx[0]), expr.op1().type()); + evaluated_index.index() = + constant_exprt(integer2string(index[0]), index_expr.index().type()); } simplified = simplify_expr(evaluated_index, ns); } @@ -966,36 +943,37 @@ void interpretert::evaluate( } else if(expr.id()==ID_typecast) { - if(expr.operands().size()!=1) - throw "typecast expects one operand"; + auto const &typecast_expr = to_typecast_expr(expr); - mp_vectort tmp; - evaluate(expr.op0(), tmp); + mp_vectort casted; + evaluate(typecast_expr.op(), casted); - if(tmp.size()==1) + if(casted.size() == 1) { - const mp_integer &value=tmp.front(); + const mp_integer &value = casted.front(); - if(expr.type().id()==ID_pointer) + if(typecast_expr.type().id() == ID_pointer) { dest.push_back(value); return; } - else if(expr.type().id()==ID_signedbv) + else if(typecast_expr.type().id() == ID_signedbv) { const std::string s = - integer2bv(value, to_signedbv_type(expr.type()).get_width()); + integer2bv(value, to_signedbv_type(typecast_expr.type()).get_width()); dest.push_back(bv2integer(s, true)); return; } - else if(expr.type().id()==ID_unsignedbv) + else if(typecast_expr.type().id() == ID_unsignedbv) { - const std::string s = - integer2bv(value, to_unsignedbv_type(expr.type()).get_width()); + const std::string s = integer2bv( + value, to_unsignedbv_type(typecast_expr.type()).get_width()); dest.push_back(bv2integer(s, false)); return; } - else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool)) + else if( + (typecast_expr.type().id() == ID_bool) || + (typecast_expr.type().id() == ID_c_bool)) { dest.push_back(value!=0); return; @@ -1004,7 +982,8 @@ void interpretert::evaluate( } else if(expr.id()==ID_array) { - forall_operands(it, expr) + auto const &array_expr = to_array_expr(expr); + forall_operands(it, array_expr) { evaluate(*it, dest); } @@ -1012,18 +991,19 @@ void interpretert::evaluate( } else if(expr.id()==ID_array_of) { - const auto &ty=to_array_type(expr.type()); + auto const &array_of_expr = to_array_of_expr(expr); + const auto &array_of_type = to_array_type(array_of_expr.type()); std::vector size; - if(ty.size().id()==ID_infinity) + if(array_of_type.size().id() == ID_infinity) size.push_back(0); else - evaluate(ty.size(), size); + evaluate(array_of_type.size(), size); if(size.size()==1) { std::size_t size_int=integer2size_t(size[0]); for(std::size_t i=0; i(expr); +} + +inline const pointer_offset_exprt &to_pointer_offset_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_pointer_offset); + PRECONDITION(expr.operands().size() == 1); + PRECONDITION(expr.op0().id() == ID_pointer); + return static_cast(expr); +} + #endif // CPROVER_UTIL_STD_EXPR_H